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 & not Y is empty )

now

assume Y is trivial ; :: thesis: contradiction
then consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
d = {} by A1, ZFMISC_1:8;
hence contradiction by A1, ZFMISC_1:8; :: thesis: verum

end;

hence ( not Y is trivial & Y is strict & not Y is empty ) ; :: thesis: verum