let x be object ; :: thesis: for R being Relation st x in field R holds
ex y being object st
( [x,y] in R or [y,x] in R )
let R be Relation; :: thesis: ( x in field R implies ex y being object st
( [x,y] in R or [y,x] in R ) )
assume x in field R ; :: thesis: ex y being object 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 object st
( [x,y] in R or [y,x] in R ) by XTUPLE_0:def 12, XTUPLE_0:def 13; :: thesis: verum