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