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