theorem Th64: :: ORDERS_1:64

for R being Relation
for X being set st R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R holds
ex x being set st x is_minimal_in R