let X be set ; :: thesis: for x, y being object

for R being Relation of X st [x,y] in R holds

( x in X & y in X )

let x, y be object ; :: thesis: for R being Relation of X st [x,y] in R holds

( x in X & y in X )

let R be Relation of X; :: thesis: ( [x,y] in R implies ( x in X & y in X ) )

assume [x,y] in R ; :: thesis: ( x in X & y in X )

then ( x in dom R & y in rng R ) by XTUPLE_0:def 12, XTUPLE_0:def 13;

hence ( x in X & y in X ) ; :: thesis: verum

for R being Relation of X st [x,y] in R holds

( x in X & y in X )

let x, y be object ; :: thesis: for R being Relation of X st [x,y] in R holds

( x in X & y in X )

let R be Relation of X; :: thesis: ( [x,y] in R implies ( x in X & y in X ) )

assume [x,y] in R ; :: thesis: ( x in X & y in X )

then ( x in dom R & y in rng R ) by XTUPLE_0:def 12, XTUPLE_0:def 13;

hence ( x in X & y in X ) ; :: thesis: verum