let R be Relation; :: thesis: R .: (dom R) = rng R
A1: rng R c= R .: (dom R)

proof

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
A2: [x,y] in R by Def5;
x in dom R by A2, Def4;
hence y in R .: (dom R) by A2, Def13; :: thesis: verum

end;

R .: (dom R) c= rng R by Th144;
hence R .: (dom R) = rng R by A1, XBOOLE_0:def 10; :: thesis: verum