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 10 :: thesis: X has_lower_Zorn_property_wrt R ~
let Y be set ; :: according to ORDERS_1:def 11 :: 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 ;
assume that
A3: Y c= X and
A4: (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 ~ ) )
(R ~) |_2 Y = (R |_2 Y) ~ by Lm16;
then consider x being set such that
A5: x in X and
A6: for y being set st y in Y holds
[y,x] in R by A1, A2, A3, A4, Th18;
take x ; :: thesis: ( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) )
thus x in X by A5; :: 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 A6;
hence [x,y] in R ~ by RELAT_1:def 7; :: thesis: verum
end;
assume A7: 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 11 :: thesis: X has_upper_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
[y,x] in R ) ) )
assume that
A8: Y c= X and
A9: 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 ) )
(R ~) |_2 Y = (R |_2 Y) ~ by Lm16;
then consider x being set such that
A10: x in X and
A11: for y being set st y in Y holds
[x,y] in R ~ by A7, A8, A9, Th18;
take x ; :: thesis: ( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
thus x in X by A10; :: 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 A11;
hence [y,x] in R by RELAT_1:def 7; :: thesis: verum