let x be set ; :: thesis: for R being Relation st x in field R holds
ex y being set st
( [x,y] in R or [y,x] in R )
let R be Relation; :: thesis: ( x in field R implies ex y being set st
( [x,y] in R or [y,x] in R ) )
assume x in field R ; :: thesis: ex y being set st
( [x,y] in R or [y,x] in R )
then ( x in dom R or x in rng R ) by XBOOLE_0:def 3;
hence ex y being set st
( [x,y] in R or [y,x] in R ) by RELAT_1:def 4, RELAT_1:def 5; :: thesis: verum