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 )

thus x in dom R by A2, XTUPLE_0:def 12; :: thesis: verum

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

given y being Element of E such that A2:
[x,y] in R
; :: thesis: x in dom R
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;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

thus x in dom R by A2, XTUPLE_0:def 12; :: thesis: verum