reconsider BB = bool the carrier of R as Subset-Family of R ;
set T = TopRelStr(# the carrier of R, the InternalRel of R,BB #);
RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,BB #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,BB #) #)
;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,BB #) as TopAugmentation of R by Def4;
take
T
; ( T is correct & T is discrete & T is strict )
T is discrete TopStruct
by TDLAT_3:def 1;
hence
( T is correct & T is discrete & T is strict )
; verum