let a, b be object ; :: thesis: for R being Relation st [a,b] in R holds
( a in field R & b in field R )
let R be Relation; :: thesis: ( [a,b] in R implies ( a in field R & b in field R ) )
assume A1: [a,b] in R ; :: thesis: ( a in field R & b in field R )
then a in dom R by XTUPLE_0:def 12;
hence a in field R by XBOOLE_0:def 3; :: thesis: b in field R
b in rng R by A1, XTUPLE_0:def 13;
hence b in field R by XBOOLE_0:def 3; :: thesis: verum