reconsider S = bool the carrier of T as Subset-Family of T by ZFMISC_1:def 1;
reconsider S = S as Subset-Family of T ;
set R = TopStruct(# the carrier of T,S #);
A1: TopStruct(# the carrier of T,S #) is discrete TopStruct by TDLAT_3:def 1;
the topology of T c= S ;
then TopStruct(# the carrier of T,S #) is TopExtension of T by A1, Def5;
hence ex b₁ being TopExtension of T st
( b₁ is strict & b₁ is discrete ) by A1; :: thesis: verum