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

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