let T1, T2 be strict TopAugmentation of L; :: thesis: ( T1 is lim-inf & T2 is lim-inf implies T1 = T2 )
assume that
A1: the topology of T1 = xi T1 and
A2: 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, A2, Th9; :: thesis: verum