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