let X be finite set ; :: thesis: for Y being set st Y is c=-linear & X c= union Y & Y <> {} holds
ex Z being set st
( X c= Z & Z in Y )
let Y be set ; :: thesis: ( Y is c=-linear & X c= union Y & Y <> {} implies ex Z being set st
( X c= Z & Z in Y ) )
assume A0: ( Y is c=-linear & X c= union Y & Y <> {} ) ; :: thesis: ex Z being set st
( X c= Z & Z in Y )
deffunc H1( object ) -> set = { y where y is Element of Y : $1 in y } ;
deffunc H2( object ) -> Element of H1($1) = the Element of H1($1);
A18: for x being object st x in X holds
not H1(x) is empty
proof
let x be object ; :: thesis: ( x in X implies not H1(x) is empty )
assume x in X ; :: thesis: not H1(x) is empty
then consider y being set such that
A11: ( x in y & y in Y ) by TARSKI:def 4, A0;
reconsider y = y as Element of Y by A11;
y in H1(x) by A11;
hence not H1(x) is empty ; :: thesis: verum
end;
per cases ( X is empty or not X is empty ) ;
suppose S1: X is empty ; :: thesis: ex Z being set st
( X c= Z & Z in Y )
consider Z being object such that
A15: Z in Y by A0, XBOOLE_0:def 1;
consider Z1 being set such that
A16: ( Z1 in Y & ( for x being object holds
( not x in Y or not x in Z1 ) ) ) by TARSKI:3, A15;
X c= Z1 by S1;
hence ex Z being set st
( X c= Z & Z in Y ) by A16; :: thesis: verum
end;
suppose S2: not X is empty ; :: thesis: ex Z being set st
( X c= Z & Z in Y )
set Y1 = { H2(x) where x is Element of X : x in X } ;
A20: X is finite ;
A2: { H2(x) where x is Element of X : x in X } is finite from FRAENKEL:sch 21(A20);
A19: { H2(x) where x is Element of X : x in X } c= Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H2(x) where x is Element of X : x in X } or x in Y )
assume x in { H2(x) where x is Element of X : x in X } ; :: thesis: x in Y
then consider x1 being Element of X such that
A13: ( x = the Element of H1(x1) & x1 in X ) ;
not H1(x1) is empty by A18, A13;
then x in H1(x1) by A13;
then consider x2 being Element of Y such that
A14: ( x2 = x & x1 in x2 ) ;
thus x in Y by A0, A14; :: thesis: verum
end;
{ H2(x) where x is Element of X : x in X } <> {}
proof
consider x being object such that
A15: x in X by XBOOLE_0:def 1, S2;
consider x1 being set such that
A16: ( x1 in X & ( for x being object holds
( not x in X or not x in x1 ) ) ) by TARSKI:3, A15;
reconsider x1 = x1 as Element of X by A16;
the Element of H1(x1) in { H2(x) where x is Element of X : x in X } by A16;
hence { H2(x) where x is Element of X : x in X } <> {} ; :: thesis: verum
end;
then consider Z being set such that
A1: ( Z in { H2(x) where x is Element of X : x in X } & ( for y being set st y in { H2(x) where x is Element of X : x in X } holds
y c= Z ) ) by FINSET_1:12, A0, A2, A19;
A4: X c= Z
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume A8: x in X ; :: thesis: x in Z
then the Element of H1(x) in { H2(x) where x is Element of X : x in X } ;
then A9: the Element of H1(x) c= Z by A1;
not H1(x) is empty by A8, A18;
then the Element of H1(x) in H1(x) ;
then consider y3 being Element of Y such that
A10: ( y3 = the Element of H1(x) & x in y3 ) ;
thus x in Z by A10, A9; :: thesis: verum
end;
consider x being Element of X such that
A6: ( Z = the Element of H1(x) & x in X ) by A1;
not H1(x) is empty by A6, A18;
then Z in H1(x) by A6;
then consider y being Element of Y such that
U1: ( y = Z & x in y ) ;
thus ex Z being set st
( X c= Z & Z in Y ) by A4, A0, U1; :: thesis: verum
end;
end;