let D, E be non empty set ; :: thesis: for R being Relation of D,E
for x being Element of D holds
( x in dom R iff ex y being Element of E st [x,y] in R )
let R be Relation of D,E; :: thesis: for x being Element of D holds
( x in dom R iff ex y being Element of E st [x,y] in R )
let x be Element of D; :: thesis: ( x in dom R iff ex y being Element of E st [x,y] in R )
thus ( x in dom R implies ex y being Element of E st [x,y] in R ) :: thesis: ( ex y being Element of E st [x,y] in R implies x in dom R )

proof

assume x in dom R ; :: thesis: ex y being Element of E st [x,y] in R
then consider y being object such that
A1: [x,y] in R by XTUPLE_0:def 12;
reconsider b = y as Element of E by A1, ZFMISC_1:87;
take b ; :: thesis: [x,b] in R
thus [x,b] in R by A1; :: thesis: verum

end;

given y being Element of E such that A2: [x,y] in R ; :: thesis: x in dom R
thus x in dom R by A2, XTUPLE_0:def 12; :: thesis: verum