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 ~ )
thus ( X has_upper_Zorn_property_wrt R implies X has_lower_Zorn_property_wrt R ~ ) :: thesis: ( X has_lower_Zorn_property_wrt R ~ implies X has_upper_Zorn_property_wrt R )

proof

assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) ; :: according to ORDERS_1:def 9 :: thesis: X has_lower_Zorn_property_wrt R ~
let Y be set ; :: according to ORDERS_1:def 10 :: thesis: ( Y c= X & (R ~ ) |_2 Y is being_linear-order implies ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) ) )
A2: ( (R ~ ) |_2 Y = (R |_2 Y) ~ & ((R |_2 Y) ~ ) ~ = R |_2 Y ) by Lm15;
assume A3: ( Y c= X & (R ~ ) |_2 Y is being_linear-order ) ; :: thesis: ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) )
then R |_2 Y is being_linear-order by A2, Th106;
then consider x being set such that
A4: ( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) by A1, A3;
take x ; :: thesis: ( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) )
thus x in X by A4; :: thesis: for y being set st y in Y holds
[x,y] in R ~
let y be set ; :: thesis: ( y in Y implies [x,y] in R ~ )
assume y in Y ; :: thesis: [x,y] in R ~
then [y,x] in R by A4;
hence [x,y] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

assume A5: for Y being set st Y c= X & (R ~ ) |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) ) ; :: according to ORDERS_1:def 10 :: thesis: X has_upper_Zorn_property_wrt R
let Y be set ; :: according to ORDERS_1:def 9 :: thesis: ( Y c= X & R |_2 Y is being_linear-order implies ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) )
A6: ( (R ~ ) |_2 Y = (R |_2 Y) ~ & ((R |_2 Y) ~ ) ~ = R |_2 Y ) by Lm15;
assume A7: ( Y c= X & R |_2 Y is being_linear-order ) ; :: thesis: ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
then (R ~ ) |_2 Y is being_linear-order by A6, Th106;
then consider x being set such that
A8: ( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) ) by A5, A7;
take x ; :: thesis: ( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
thus x in X by A8; :: thesis: for y being set st y in Y holds
[y,x] in R
let y be set ; :: thesis: ( y in Y implies [y,x] in R )
assume y in Y ; :: thesis: [y,x] in R
then [x,y] in R ~ by A8;
hence [y,x] in R by RELAT_1:def 7; :: thesis: verum