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: D has_upper_Zorn_property_wrt RelIncl D
proof
let Z be set ; :: according to ORDERS_1:def 10 :: 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 that
A4: Z c= D and
A5: (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 ) )
set Q = (RelIncl D) |_2 Z;
A6: Z c= field ((RelIncl D) |_2 Z)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in field ((RelIncl D) |_2 Z) )
assume A7: x in Z ; :: thesis: x in field ((RelIncl D) |_2 Z)
then A8: [x,x] in [:Z,Z:] by ZFMISC_1:87;
[x,x] in RelIncl D by A4, A7, WELLORD2:def 1;
then [x,x] in (RelIncl D) |_2 Z by A8, XBOOLE_0:def 4;
hence x in field ((RelIncl D) |_2 Z) by RELAT_1:15; :: thesis: verum
end;
(RelIncl D) |_2 Z is connected by A5;
then A9: (RelIncl D) |_2 Z is_connected_in field ((RelIncl D) |_2 Z) ;
Z is c=-linear
proof
let X1 be set ; :: according to ORDINAL1:def 8 :: thesis: for b1 being set holds
( not X1 in Z or not b1 in Z or X1,b1 are_c=-comparable )
let X2 be set ; :: thesis: ( not X1 in Z or not X2 in Z or X1,X2 are_c=-comparable )
assume that
A10: X1 in Z and
A11: X2 in Z ; :: thesis: X1,X2 are_c=-comparable
( not X1 <> X2 or [X1,X2] in (RelIncl D) |_2 Z or [X2,X1] in (RelIncl D) |_2 Z ) by A9, A6, A10, A11;
then ( not X1 <> X2 or [X1,X2] in RelIncl D or [X2,X1] in RelIncl D ) by XBOOLE_0:def 4;
hence ( X1 c= X2 or X2 c= X1 ) by A4, A10, A11, WELLORD2:def 1; :: according to XBOOLE_0:def 9 :: thesis: verum
end;
then consider Y being set such that
A12: Y in X and
A13: for X1 being set st X1 in Z holds
X1 c= Y by A2, A4;
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 A12; :: 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 A14: y in Z ; :: thesis: [y,x] in RelIncl D
then y c= Y by A13;
hence [y,x] in RelIncl D by A4, A12, A14, WELLORD2:def 1; :: thesis: verum
end;
A15: field (RelIncl D) = D by WELLORD2:def 1;
A16: RelIncl D is_antisymmetric_in D by A15, RELAT_2:def 12;
A17: RelIncl D is_transitive_in D by A15, RELAT_2:def 16;
RelIncl D is_reflexive_in D by A15, RELAT_2:def 9;
then RelIncl D partially_orders D by A17, A16;
then consider x being set such that
A18: x is_maximal_in RelIncl D by A15, A3, Th63;
take Y = x; :: thesis: ( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
A19: Y in field (RelIncl D) by A18;
thus Y in X by A15, A18; :: 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 that
A20: Z in X and
A21: Z <> Y ; :: thesis: not Y c= Z
not [Y,Z] in RelIncl D by A15, A18, A20, A21;
hence not Y c= Z by A15, A19, A20, WELLORD2:def 1; :: thesis: verum