let z be object ; 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 ; ( 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 )
; 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; verum