let R be Relation; :: thesis: for x being object holds
( x in field R iff ex y being object st
( [x,y] in R or [y,x] in R ) )
let x be object ; :: thesis: ( x in field R iff ex y being object st
( [x,y] in R or [y,x] in R ) )
( x in (dom R) \/ (rng R) iff ( x in dom R or x in rng R ) ) by XBOOLE_0:def 3;
hence ( x in field R iff ex y being object st
( [x,y] in R or [y,x] in R ) ) by RELAT_1:def 6, XTUPLE_0:def 12, XTUPLE_0:def 13; :: thesis: verum