set T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #);
A1: 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 TopAugmentation of L by YELLOW_9:def 4;
take T ; :: thesis: ( T is strict & T is lim-inf )
thus T is strict ; :: thesis: T is lim-inf
thus the topology of T = xi T by A1, Th9; :: according to WAYBEL33:def 2 :: thesis: verum