set T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #);
A2: RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) ;
then reconsider T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) as strict TopAugmentation of L by YELLOW_9:def 4;
take T ; :: thesis: T is lim-inf
thus the topology of T = xi T by A2, Th9; :: according to WAYBEL33:def 2 :: thesis: verum