let X, Y be set ; :: thesis: for R being Relation of X,Y holds
( dom (R ~ ) = rng R & rng (R ~ ) = dom R )
let R be Relation of X,Y; :: thesis: ( dom (R ~ ) = rng R & rng (R ~ ) = dom R )

now

let x be set ; :: thesis: ( x in dom (R ~ ) iff x in rng R )

A1: now

assume x in rng R ; :: thesis: x in dom (R ~ )
then consider y being set such that
A2: [y,x] in R by RELAT_1:def 5;
[x,y] in R ~ by A2, RELAT_1:def 7;
hence x in dom (R ~ ) by RELAT_1:20; :: thesis: verum

end;

now

assume x in dom (R ~ ) ; :: thesis: x in rng R
then consider y being set such that
A3: [x,y] in R ~ by RELAT_1:def 4;
[y,x] in R by A3, RELAT_1:def 7;
hence x in rng R by RELAT_1:20; :: thesis: verum

end;

hence ( x in dom (R ~ ) iff x in rng R ) by A1; :: thesis: verum

end;

hence dom (R ~ ) = rng R by TARSKI:2; :: thesis: rng (R ~ ) = dom R

now

let x be set ; :: thesis: ( x in rng (R ~ ) iff x in dom R )

A4: now

assume x in dom R ; :: thesis: x in rng (R ~ )
then consider y being set such that
A5: [x,y] in R by RELAT_1:def 4;
[y,x] in R ~ by A5, RELAT_1:def 7;
hence x in rng (R ~ ) by RELAT_1:20; :: thesis: verum

end;

now

assume x in rng (R ~ ) ; :: thesis: x in dom R
then consider y being set such that
A6: [y,x] in R ~ by RELAT_1:def 5;
[x,y] in R by A6, RELAT_1:def 7;
hence x in dom R by RELAT_1:20; :: thesis: verum

end;

hence ( x in rng (R ~ ) iff x in dom R ) by A4; :: thesis: verum

end;

hence rng (R ~ ) = dom R by TARSKI:2; :: thesis: verum