set D = {{},1};
reconsider tau = bool {{},1} as Subset-Family of {{},1} ;
reconsider tau = tau as Subset-Family of {{},1} ;
reconsider Y = TopStruct(# {{},1},tau #) as non empty discrete TopStruct by TDLAT_3:def 1;
take Y ; :: thesis: ( not Y is trivial & Y is strict )
now :: thesis: not Y is trivial
assume Y is trivial ; :: thesis: contradiction
then consider d being Element of Y such that
A1: the carrier of Y = {d} ;
d = {} by A1, ZFMISC_1:4;
hence contradiction by A1, ZFMISC_1:4; :: thesis: verum
end;
hence ( not Y is trivial & Y is strict ) ; :: thesis: verum