let R be Relation; :: thesis: for x being object st x in R holds
( x `1 in dom R & x `2 in rng R )
let x be object ; :: thesis: ( x in R implies ( x `1 in dom R & x `2 in rng R ) )
assume A1: x in R ; :: thesis: ( x `1 in dom R & x `2 in rng R )
then x = [(x `1),(x `2)] by Th15;
hence ( x `1 in dom R & x `2 in rng R ) by A1, XTUPLE_0:def 12, XTUPLE_0:def 13; :: thesis: verum