let R be Relation; :: thesis: R " (rng R) = dom R
thus R " (rng R) c= dom R by Th167; :: according to XBOOLE_0:def 10 :: thesis: dom R c= R " (rng R)
let x be set ; :: 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 set such that
A1: [x,y] in R by Def4;
y in rng R by A1, Def5;
hence x in R " (rng R) by A1, Def14; :: thesis: verum