let R be Relation; :: thesis: ( rng R = dom (R ~ ) & dom R = rng (R ~ ) )
thus rng R c= dom (R ~ ) :: according to XBOOLE_0:def 10 :: thesis: ( dom (R ~ ) c= rng R & dom R = rng (R ~ ) )

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng R or u in dom (R ~ ) )
assume u in rng R ; :: thesis: u in dom (R ~ )
then consider x being set such that
A1: [x,u] in R by Def5;
[u,x] in R ~ by A1, Def7;
hence u in dom (R ~ ) by Def4; :: thesis: verum

end;

thus dom (R ~ ) c= rng R :: thesis: dom R = rng (R ~ )

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in dom (R ~ ) or u in rng R )
assume u in dom (R ~ ) ; :: thesis: u in rng R
then consider x being set such that
A2: [u,x] in R ~ by Def4;
[x,u] in R by A2, Def7;
hence u in rng R by Def5; :: thesis: verum

end;

thus dom R c= rng (R ~ ) :: according to XBOOLE_0:def 10 :: thesis: rng (R ~ ) c= dom R

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in dom R or u in rng (R ~ ) )
assume u in dom R ; :: thesis: u in rng (R ~ )
then consider x being set such that
A3: [u,x] in R by Def4;
[x,u] in R ~ by A3, Def7;
hence u in rng (R ~ ) by Def5; :: thesis: verum

end;

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng (R ~ ) or u in dom R )
assume u in rng (R ~ ) ; :: thesis: u in dom R
then consider x being set such that
A4: [x,u] in R ~ by Def5;
[u,x] in R by A4, Def7;
hence u in dom R by Def4; :: thesis: verum