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 ) )
byFINSET_1:12, A0, A2, A19; A4:
X c= Z
consider x being Element of X such that A6:
( Z = the Element of H1(x) & x in X )
byA1;
not H1(x) is emptybyA6, A18; then
Z in H1(x)
byA6; 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 )
byA4, A0, U1; :: thesis: verum