for R being Relation
for X being set st R partially_orders X & field R = X & X has_upper_Zorn_property_wrt R holds
ex x being set st x is_maximal_in R