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;
now :: thesis: for x being object holds
( x in dom R iff x in dom (R ~) )
let x be object ; :: thesis: ( x in dom R iff x in dom (R ~) )
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;
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;
then [x,x] in R ~ by RELAT_1:def 7;
hence x in dom (R ~) by XTUPLE_0:def 12; :: 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 :: thesis: for x being object holds
( x in rng R iff x in rng (R ~) )
let x be object ; :: thesis: ( x in rng R iff x in rng (R ~) )
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;
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 A2;
then [x,x] in R ~ by RELAT_1:def 7;
hence x in rng (R ~) by XTUPLE_0:def 13; :: 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