let R1, R2 be non empty RelStr ; :: thesis: ( RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) implies omega R1 = omega R2 )
assume A1: RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) ; :: thesis: omega R1 = omega R2
consider S being correct lower TopAugmentation of R1;
RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R1,the InternalRel of R1 #) by YELLOW_9:def 4;
then A2: S is TopAugmentation of R2 by A1, YELLOW_9:def 4;
omega R1 = the topology of S by Def2;
hence omega R1 = omega R2 by A2, Def2; :: thesis: verum