let R be Relation; :: thesis: ( R is reflexive implies ( dom R = dom (R ~ ) & rng R = rng (R ~ ) ) )
assume A1: R is reflexive ; :: thesis: ( dom R = dom (R ~ ) & rng R = rng (R ~ ) )
then A2: R is_reflexive_in field R by Def9;
R ~ is reflexive by A1, Th27;
then A3: R ~ is_reflexive_in field (R ~ ) by Def9;

now

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

A4: now

assume x in dom (R ~ ) ; :: thesis: x in dom R
then x in (dom (R ~ )) \/ (rng (R ~ )) by XBOOLE_0:def 3;
then x in field (R ~ ) by RELAT_1:def 6;
then [x,x] in R ~ by A3, Def1;
then [x,x] in R by RELAT_1:def 7;
hence x in dom R by RELAT_1:def 4; :: thesis: verum

end;

now

assume x in dom R ; :: thesis: x in dom (R ~ )
then x in (dom R) \/ (rng R) by XBOOLE_0:def 3;
then x in field R by RELAT_1:def 6;
then [x,x] in R by A2, Def1;
then [x,x] in R ~ by RELAT_1:def 7;
hence x in dom (R ~ ) by RELAT_1:def 4; :: thesis: verum

end;

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

end;

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

now

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

A5: now

assume x in rng (R ~ ) ; :: thesis: x in rng R
then x in (dom (R ~ )) \/ (rng (R ~ )) by XBOOLE_0:def 3;
then x in field (R ~ ) by RELAT_1:def 6;
then [x,x] in R ~ by A3, Def1;
then [x,x] in R by RELAT_1:def 7;
hence x in rng R by RELAT_1:def 5; :: thesis: verum

end;

now

assume x in rng R ; :: thesis: x in rng (R ~ )
then x in (dom R) \/ (rng R) by XBOOLE_0:def 3;
then x in field R by RELAT_1:def 6;
then [x,x] in R by A2, Def1;
then [x,x] in R ~ by RELAT_1:def 7;
hence x in rng (R ~ ) by RELAT_1:def 5; :: thesis: verum

end;

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

end;

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