let x be set ; :: thesis: for R being Relation holds
( x in field R iff ex y being set st
( [x,y] in R or [y,x] in R ) )
let R be Relation; :: thesis: ( x in field R iff ex y being set 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 set st
( [x,y] in R or [y,x] in R ) ) by RELAT_1:def 4, RELAT_1:def 5, RELAT_1:def 6; :: thesis: verum