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 ; :: thesis: ( 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 ) ; :: thesis: verum