let R be Relation; :: thesis: for x being set st x in R holds
( x `1 in dom R & x `2 in rng R )
let x be set ; :: 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 Th23;
hence ( x `1 in dom R & x `2 in rng R ) by A1, RELAT_1:def 4, RELAT_1:def 5; :: thesis: verum