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:1; :: 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:1; :: thesis: verum