theorem Th51: :: ORDERS_1:51

for R being Relation
for X being set holds
( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ )