let X be set ; :: thesis: ( X <> {} & ( for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) )
assume that
A1: X <> {} and
A2: for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ; :: thesis: ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
reconsider D = X as non empty set by A1;
set R = RelIncl D;
A3: field (RelIncl D) = D by WELLORD2:def 1;
A4: RelIncl D partially_orders D

proof

( RelIncl D is reflexive & RelIncl D is transitive & RelIncl D is antisymmetric ) by WELLORD2:2, WELLORD2:3, WELLORD2:5;
hence ( RelIncl D is_reflexive_in D & RelIncl D is_transitive_in D & RelIncl D is_antisymmetric_in D ) by A3, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: according to ORDERS_1:def 7 :: thesis: verum

end;

D has_upper_Zorn_property_wrt RelIncl D

proof

let Z be set ; :: according to ORDERS_1:def 9 :: thesis: ( Z c= D & (RelIncl D) |_2 Z is being_linear-order implies ex x being set st
( x in D & ( for y being set st y in Z holds
[y,x] in RelIncl D ) ) )
assume A5: ( Z c= D & (RelIncl D) |_2 Z is being_linear-order ) ; :: thesis: ex x being set st
( x in D & ( for y being set st y in Z holds
[y,x] in RelIncl D ) )
then (RelIncl D) |_2 Z is connected by Def5;
then A6: (RelIncl D) |_2 Z is_connected_in field ((RelIncl D) |_2 Z) by RELAT_2:def 14;
A7: Z c= field ((RelIncl D) |_2 Z)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in field ((RelIncl D) |_2 Z) )
assume x in Z ; :: thesis: x in field ((RelIncl D) |_2 Z)
then ( [x,x] in [:Z,Z:] & [x,x] in RelIncl D ) by A5, WELLORD2:def 1, ZFMISC_1:106;
then [x,x] in (RelIncl D) |_2 Z by XBOOLE_0:def 4;
hence x in field ((RelIncl D) |_2 Z) by RELAT_1:30; :: thesis: verum

end;

set Q = (RelIncl D) |_2 Z;
Z is c=-linear

proof

let X1 be set ; :: according to ORDINAL1:def 9 :: thesis: for b₁ being set holds
( not X1 in Z or not b₁ in Z or X1,b₁ are_c=-comparable )
let X2 be set ; :: thesis: ( not X1 in Z or not X2 in Z or X1,X2 are_c=-comparable )
assume A8: ( X1 in Z & X2 in Z ) ; :: thesis: X1,X2 are_c=-comparable
then ( not X1 <> X2 or [X1,X2] in (RelIncl D) |_2 Z or [X2,X1] in (RelIncl D) |_2 Z ) by A6, A7, RELAT_2:def 6;
then ( ( not X1 <> X2 or [X1,X2] in RelIncl D or [X2,X1] in RelIncl D ) & X1 in D & X2 in D & X1 c= X1 ) by A5, A8, XBOOLE_0:def 4;
hence ( X1 c= X2 or X2 c= X1 ) by WELLORD2:def 1; :: according to XBOOLE_0:def 9 :: thesis: verum

end;

then consider Y being set such that
A9: ( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A2, A5;
take x = Y; :: thesis: ( x in D & ( for y being set st y in Z holds
[y,x] in RelIncl D ) )
thus x in D by A9; :: thesis: for y being set st y in Z holds
[y,x] in RelIncl D
let y be set ; :: thesis: ( y in Z implies [y,x] in RelIncl D )
assume y in Z ; :: thesis: [y,x] in RelIncl D
then ( y c= Y & y in D ) by A5, A9;
hence [y,x] in RelIncl D by A9, WELLORD2:def 1; :: thesis: verum

end;

then consider x being set such that
A10: x is_maximal_in RelIncl D by A3, A4, Th173;
take Y = x; :: thesis: ( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
A11: ( Y in field (RelIncl D) & ( for y being set holds
( not y in field (RelIncl D) or not y <> Y or not [Y,y] in RelIncl D ) ) ) by A10, Def11;
thus Y in X by A3, A10, Def11; :: thesis: for Z being set st Z in X & Z <> Y holds
not Y c= Z
let Z be set ; :: thesis: ( Z in X & Z <> Y implies not Y c= Z )
assume A12: ( Z in X & Z <> Y ) ; :: thesis: not Y c= Z
then not [Y,Z] in RelIncl D by A3, A10, Def11;
hence not Y c= Z by A3, A11, A12, WELLORD2:def 1; :: thesis: verum