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
Y c= X1 ) ) ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) ) )
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
Y c= X1 ) ) ; :: thesis: ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) )
reconsider D = X as non empty set by A1;
set R = (RelIncl D) ~ ;
A3: for x being set st x in D holds
[x,x] in (RelIncl D) ~
proof
let x be set ; :: thesis: ( x in D implies [x,x] in (RelIncl D) ~ )
( x in D implies [x,x] in RelIncl D ) by WELLORD2:def 1;
hence ( x in D implies [x,x] in (RelIncl D) ~ ) by RELAT_1:def 7; :: thesis: verum
end;
A4: 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
A5: Z c= D and
A6: ((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;
A7: 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 A8: x in Z ; :: thesis: x in field (((RelIncl D) ~) |_2 Z)
then A9: [x,x] in [:Z,Z:] by ZFMISC_1:87;
[x,x] in (RelIncl D) ~ by A3, A5, A8;
then [x,x] in ((RelIncl D) ~) |_2 Z by A9, 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 A6;
then A10: ((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
A11: X1 in Z and
A12: 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 A10, A7, A11, A12;
then ( not X1 <> X2 or [X1,X2] in (RelIncl D) ~ or [X2,X1] in (RelIncl D) ~ ) by XBOOLE_0:def 4;
then ( not X1 <> X2 or [X1,X2] in RelIncl D or [X2,X1] in RelIncl D ) by RELAT_1:def 7;
hence ( X1 c= X2 or X2 c= X1 ) by A5, A11, A12, WELLORD2:def 1; :: according to XBOOLE_0:def 9 :: thesis: verum
end;
then consider Y being set such that
A13: Y in X and
A14: for X1 being set st X1 in Z holds
Y c= X1 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 A13; :: 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 A15: y in Z ; :: thesis: [y,x] in (RelIncl D) ~
then Y c= y by A14;
then [Y,y] in RelIncl D by A5, A13, A15, WELLORD2:def 1;
hence [y,x] in (RelIncl D) ~ by RELAT_1:def 7; :: thesis: verum
end;
A16: field ((RelIncl D) ~) = field (RelIncl D) by RELAT_1:21
.= D by WELLORD2:def 1 ;
A17: field (RelIncl D) = D by WELLORD2:def 1;
RelIncl D is_antisymmetric_in D by A17, RELAT_2:def 12;
then A18: (RelIncl D) ~ is_antisymmetric_in D by Lm14;
RelIncl D is_transitive_in D by A17, RELAT_2:def 16;
then A19: (RelIncl D) ~ is_transitive_in D by Lm13;
RelIncl D is_reflexive_in D by A17, RELAT_2:def 9;
then (RelIncl D) ~ is_reflexive_in D by Lm12;
then (RelIncl D) ~ partially_orders D by A19, A18;
then consider x being set such that
A20: x is_maximal_in (RelIncl D) ~ by A16, A4, Th63;
take Y = x; :: thesis: ( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) )
A21: Y in field ((RelIncl D) ~) by A20;
thus Y in X by A16, A20; :: thesis: for Z being set st Z in X & Z <> Y holds
not Z c= Y
let Z be set ; :: thesis: ( Z in X & Z <> Y implies not Z c= Y )
assume that
A22: Z in X and
A23: Z <> Y ; :: thesis: not Z c= Y
not [Y,Z] in (RelIncl D) ~ by A16, A20, A22, A23;
then not [Z,Y] in RelIncl D by RELAT_1:def 7;
hence not Z c= Y by A16, A21, A22, WELLORD2:def 1; :: thesis: verum