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
proof
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;
hereby :: thesis: ( not [a,b] in the InternalRel of R2 or [a,b] in the InternalRel of R1 )
assume 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;
assume A5: [a,b] in the InternalRel of R2 ; :: thesis: [a,b] in the InternalRel of R1
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;
hence RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by A1; :: thesis: verum