let X, Y, Z be set ; :: thesis: ( X is finite & X c= [:Y,Z:] implies ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] ) )
assume that
A1: X is finite and
A2: 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
A3: dom f = X and
A4: for a being object 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, A3, Th8; :: thesis: ( A c= Y & X c= [:A,Z:] )
thus A c= Y :: thesis: X c= [:A,Z:]

proof

let a be object ; :: 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 object such that
A5: x in dom f and
A6: f . x = a by FUNCT_1:def 3;
consider y, z being object such that
A7: y in Y and
z in Z and
A8: x = [y,z] by A2, A3, A5, ZFMISC_1:def 2;
f . x = x `1 by A3, A4, A5
.= y by A8 ;
hence a in Y by A6, A7; :: thesis: verum

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in [:A,Z:] )
assume A9: a in X ; :: thesis: a in [:A,Z:]
then consider x, y being object such that
x in Y and
A10: y in Z and
A11: a = [x,y] by A2, ZFMISC_1:def 2;
f . a = a `1 by A4, A9
.= x by A11 ;
then x in A by A3, A9, FUNCT_1:def 3;
hence a in [:A,Z:] by A10, A11, ZFMISC_1:87; :: thesis: verum

end;