let X, Z, Y be set ; :: thesis: ( X is finite & Z is finite & X c= [:Y,Z:] implies ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] ) )
assume A1: ( X is finite & Z is finite & X c= [:Y,Z:] ) ; :: thesis: ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] )
consider f being Function such that
A2: dom f = X and
A3: for a being set st a in X holds
f . a = H₁(a) from FUNCT_1:sch 3();
take A = rng f; :: thesis: ( A is finite & A c= Y & X c= [:A,Z:] )
thus A is finite by A1, A2, Th26; :: thesis: ( A c= Y & X c= [:A,Z:] )
thus A c= Y :: thesis: X c= [:A,Z:]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in Y )
assume a in A ; :: thesis: a in Y
then consider x being set such that
A4: ( x in dom f & f . x = a ) by FUNCT_1:def 5;
consider y, z being set such that
A5: ( y in Y & z in Z & x = [y,z] ) by A1, A2, A4, ZFMISC_1:def 2;
f . x = x `1 by A2, A3, A4
.= y by A5, MCART_1:7 ;
hence a in Y by A4, A5; :: thesis: verum

end;

thus X c= [:A,Z:] :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in [:A,Z:] )
assume A6: a in X ; :: thesis: a in [:A,Z:]
then consider x, y being set such that
A7: ( x in Y & y in Z & a = [x,y] ) by A1, ZFMISC_1:def 2;
f . a = a `1 by A3, A6
.= x by A7, MCART_1:7 ;
then x in A by A2, A6, FUNCT_1:def 5;
hence a in [:A,Z:] by A7, ZFMISC_1:106; :: thesis: verum

end;