let R be Relation; :: thesis: R .: (dom R) = rng R
thus R .: (dom R) c= rng R by Th144; :: according to XBOOLE_0:def 10 :: thesis: rng R c= R .: (dom R)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng R or y in R .: (dom R) )
assume y in rng R ; :: thesis: y in R .: (dom R)
then consider x being set such that
A1: [x,y] in R by Def5;
x in dom R by A1, Def4;
hence y in R .: (dom R) by A1, Def13; :: thesis: verum