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