theorem :: ORDERS_1:57

for R being Relation
for X, x being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds
X has_upper_Zorn_property_wrt R