let R be Relation; for X being set holds
( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ )
let X be set ; ( 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 ~ )
( 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 ) )
;
ORDERS_1:def 10 X has_lower_Zorn_property_wrt R ~
let Y be
set ;
ORDERS_1:def 11 ( 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
;
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
;
( x in X & ( for y being set st y in Y holds
[x,y] in R ~ ) )
thus
x in X
by A5;
for y being set st y in Y holds
[x,y] in R ~
let y be
set ;
( y in Y implies [x,y] in R ~ )
assume
y in Y
;
[x,y] in R ~
then
[y,x] in R
by A6;
hence
[x,y] in R ~
by RELAT_1:def 7;
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 ~ ) )
; ORDERS_1:def 11 X has_upper_Zorn_property_wrt R
let Y be set ; ORDERS_1:def 10 ( 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
; 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
; ( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
thus
x in X
by A10; for y being set st y in Y holds
[y,x] in R
let y be set ; ( y in Y implies [y,x] in R )
assume
y in Y
; [y,x] in R
then
[x,y] in R ~
by A11;
hence
[y,x] in R
by RELAT_1:def 7; verum