let R be Relation; :: thesis: for X being set holds
( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R )
let X be set ; :: thesis: ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R )
(R ~) ~ = R ;
hence ( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R ) by Th51; :: thesis: verum