let R be Relation; for X, x being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds
X has_upper_Zorn_property_wrt R
let X, x be set ; ( x in X & x is_superior_of R & X c= field R & R is reflexive implies X has_upper_Zorn_property_wrt R )
assume that
A1:
x in X
and
A2:
x is_superior_of R
and
A3:
X c= field R
and
A4:
R is_reflexive_in field R
; RELAT_2:def 9 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
A5:
Y c= X
and
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 ) )
take
x
; ( x in X & ( for y being set st y in Y holds
[y,x] in R ) )
thus
x in X
by A1; 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 A6:
y in X
by A5;
( y = x or y <> x )
;
hence
[y,x] in R
by A2, A3, A4, A6; verum