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
set S = the correct lower TopAugmentation of R1;
RelStr(# the carrier of the correct lower TopAugmentation of R1, the InternalRel of the correct lower TopAugmentation of R1 #) = RelStr(# the carrier of R1, the InternalRel of R1 #) by YELLOW_9:def 4;
then A2: the correct lower TopAugmentation of R1 is TopAugmentation of R2 by A1, YELLOW_9:def 4;
omega R1 = the topology of the correct lower TopAugmentation of R1 by Def2;
hence omega R1 = omega R2 by A2, Def2; :: thesis: verum