let R1, R2 be real RelStr ; :: thesis: ( the carrier of R1 = the carrier of R2 implies RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )

assume A1: the carrier of R1 = the carrier of R2 ; :: thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

set X = the carrier of R1;

the InternalRel of R1 = the InternalRel of R2

assume A1: the carrier of R1 = the carrier of R2 ; :: thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

set X = the carrier of R1;

the InternalRel of R1 = the InternalRel of R2

proof

hence
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
by A1; :: thesis: verum
let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in the InternalRel of R1 or [a,b] in the InternalRel of R2 ) & ( not [a,b] in the InternalRel of R2 or [a,b] in the InternalRel of R1 ) )

A2: the carrier of R1 c= REAL by Def1;

then A6: ( a in the carrier of R1 & b in the carrier of R1 ) by A1, ZFMISC_1:87;

then reconsider a9 = a, b9 = b as Element of REAL by A2;

a9 <= b9 by A1, A5, A6, Def1;

hence [a,b] in the InternalRel of R1 by A6, Def1; :: thesis: verum

end;A2: the carrier of R1 c= REAL by Def1;

hereby :: thesis: ( not [a,b] in the InternalRel of R2 or [a,b] in the InternalRel of R1 )

assume A5:
[a,b] in the InternalRel of R2
; :: thesis: [a,b] in the InternalRel of R1assume A3:
[a,b] in the InternalRel of R1
; :: thesis: [a,b] in the InternalRel of R2

then A4: ( a in the carrier of R1 & b in the carrier of R1 ) by ZFMISC_1:87;

then reconsider a9 = a, b9 = b as Element of REAL by A2;

a9 <= b9 by A3, A4, Def1;

hence [a,b] in the InternalRel of R2 by A1, A4, Def1; :: thesis: verum

end;then A4: ( a in the carrier of R1 & b in the carrier of R1 ) by ZFMISC_1:87;

then reconsider a9 = a, b9 = b as Element of REAL by A2;

a9 <= b9 by A3, A4, Def1;

hence [a,b] in the InternalRel of R2 by A1, A4, Def1; :: thesis: verum

then A6: ( a in the carrier of R1 & b in the carrier of R1 ) by A1, ZFMISC_1:87;

then reconsider a9 = a, b9 = b as Element of REAL by A2;

a9 <= b9 by A1, A5, A6, Def1;

hence [a,b] in the InternalRel of R1 by A6, Def1; :: thesis: verum