theorem :: ORDERS_1:50

for R being Relation
for X being set st X has_lower_Zorn_property_wrt R holds
X <> {}