let R be Relation; :: thesis: 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
let X be set ; :: thesis: ( R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R implies ex x being set st x is_minimal_in R )
assume that
A1: R partially_orders X and
A2: field R = X and
A3: X has_lower_Zorn_property_wrt R ; :: thesis: ex x being set st x is_minimal_in R
R = (R ~) ~ ;
then A4: X has_upper_Zorn_property_wrt R ~ by A3, Th51;
field (R ~) = X by A2, RELAT_1:21;
then consider x being set such that
A5: x is_maximal_in R ~ by A1, A4, Th41, Th63;
take x ; :: thesis: x is_minimal_in R
thus x is_minimal_in R by A5, Th59; :: thesis: verum