let X, Y be set ; :: thesis: for a being object
for R being Relation of X,Y st a in R holds
ex x, y being object st
( a = [x,y] & x in X & y in Y )
let a be object ; :: thesis: for R being Relation of X,Y st a in R holds
ex x, y being object st
( a = [x,y] & x in X & y in Y )
let R be Relation of X,Y; :: thesis: ( a in R implies ex x, y being object st
( a = [x,y] & x in X & y in Y ) )
assume A1: a in R ; :: thesis: ex x, y being object st
( a = [x,y] & x in X & y in Y )
then consider x, y being object such that
A2: a = [x,y] by RELAT_1:def 1;
( x in X & y in Y ) by A1, A2, ZFMISC_1:87;
hence ex x, y being object st
( a = [x,y] & x in X & y in Y ) by A2; :: thesis: verum