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 ;

A3: R ~ is_reflexive_in field (R ~) by A1, Def9;

assume A1: R is reflexive ; :: thesis: ( dom R = dom (R ~) & rng R = rng (R ~) )

then A2: R is_reflexive_in field R ;

A3: R ~ is_reflexive_in field (R ~) by A1, Def9;

now :: thesis: for x being object holds

( x in dom R iff x in dom (R ~) )

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

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

end;A4: now :: thesis: ( x in dom (R ~) implies x in dom R )

assume
x in dom (R ~)
; :: thesis: x in dom R

then x in field (R ~) by XBOOLE_0:def 3;

then [x,x] in R ~ by A1, Def1, Def9;

then [x,x] in R by RELAT_1:def 7;

hence x in dom R by XTUPLE_0:def 12; :: thesis: verum

end;then x in field (R ~) by XBOOLE_0:def 3;

then [x,x] in R ~ by A1, Def1, Def9;

then [x,x] in R by RELAT_1:def 7;

hence x in dom R by XTUPLE_0:def 12; :: thesis: verum

now :: thesis: ( x in dom R implies x in dom (R ~) )

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

then x in field R by XBOOLE_0:def 3;

then [x,x] in R by A1, Def1;

then [x,x] in R ~ by RELAT_1:def 7;

hence x in dom (R ~) by XTUPLE_0:def 12; :: thesis: verum

end;then x in field R by XBOOLE_0:def 3;

then [x,x] in R by A1, Def1;

then [x,x] in R ~ by RELAT_1:def 7;

hence x in dom (R ~) by XTUPLE_0:def 12; :: thesis: verum

now :: thesis: for x being object holds

( x in rng R iff x in rng (R ~) )

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

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

end;A5: now :: thesis: ( x in rng (R ~) implies x in rng R )

assume
x in rng (R ~)
; :: thesis: x in rng R

then x in field (R ~) by XBOOLE_0:def 3;

then [x,x] in R ~ by A3;

then [x,x] in R by RELAT_1:def 7;

hence x in rng R by XTUPLE_0:def 13; :: thesis: verum

end;then x in field (R ~) by XBOOLE_0:def 3;

then [x,x] in R ~ by A3;

then [x,x] in R by RELAT_1:def 7;

hence x in rng R by XTUPLE_0:def 13; :: thesis: verum

now :: thesis: ( x in rng R implies x in rng (R ~) )

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

then x in field R by XBOOLE_0:def 3;

then [x,x] in R by A2;

then [x,x] in R ~ by RELAT_1:def 7;

hence x in rng (R ~) by XTUPLE_0:def 13; :: thesis: verum

end;then x in field R by XBOOLE_0:def 3;

then [x,x] in R by A2;

then [x,x] in R ~ by RELAT_1:def 7;

hence x in rng (R ~) by XTUPLE_0:def 13; :: thesis: verum