let D, E be non empty set ; 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; 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; ( 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 )
( ex y being Element of E st [x,y] in R implies x in dom R )
given y being Element of E such that A2:
[x,y] in R
; x in dom R
thus
x in dom R
by A2, XTUPLE_0:def 12; verum