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