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 ( omega R1 = the topology of S & S is TopAugmentation of R2 ) by A1, Def2, YELLOW_9:def 4;
hence omega R1 = omega R2 by Def2; :: thesis: verum