let A, X, Y, z be set ; :: thesis: ( A c= [:X,Y:] & z in A implies ex x, y being set st
( x in X & y in Y & z = [x,y] ) )
assume ( A c= [:X,Y:] & z in A ) ; :: thesis: ex x, y being set st
( x in X & y in Y & z = [x,y] )
then z in [:X,Y:] by TARSKI:def 3;
hence ex x, y being set st
( x in X & y in Y & z = [x,y] ) by Def2; :: thesis: verum