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 A1: ( R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R ) ; :: thesis: ex x being set st x is_minimal_in R
R = (R ~ ) ~ ;
then ( X has_upper_Zorn_property_wrt R ~ & R ~ partially_orders X & field (R ~ ) = X ) by A1, Th137, Th151, RELAT_1:38;
then consider x being set such that
A2: x is_maximal_in R ~ by Th173;
take x ; :: thesis: x is_minimal_in R
thus x is_minimal_in R by A2, Th163; :: thesis: verum