let R be Relation; :: thesis: R " (rng R) = dom R
thus R " (rng R) c= dom R by Th124; :: according to XBOOLE_0:def 10 :: thesis: dom R c= R " (rng R)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom R or x in R " (rng R) )
assume x in dom R ; :: thesis: x in R " (rng R)
then consider y being object such that
A1: [x,y] in R by XTUPLE_0:def 12;
y in rng R by A1, XTUPLE_0:def 13;
hence x in R " (rng R) by A1, Def12; :: thesis: verum