let T1, T2 be strict TopAugmentation of L; :: thesis: ( T1 is lim-inf & T2 is lim-inf implies T1 = T2 )

assume A1: ( the topology of T1 = xi T1 & the topology of T2 = xi T2 ) ; :: according to WAYBEL33:def 2 :: thesis: T1 = T2

( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;

hence T1 = T2 by A1, Th9; :: thesis: verum

assume A1: ( the topology of T1 = xi T1 & the topology of T2 = xi T2 ) ; :: according to WAYBEL33:def 2 :: thesis: T1 = T2

( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;

hence T1 = T2 by A1, Th9; :: thesis: verum