set one = {{}};
reconsider tau = bool {{}} as Subset-Family of {{}} ;
take Y = TopStruct(# {{}},tau #); :: thesis: ( Y is discrete & Y is anti-discrete & Y is strict & not Y is empty )
thus Y is discrete ; :: thesis: ( Y is anti-discrete & Y is strict & not Y is empty )
tau = {{},{{}}} by ZFMISC_1:24;
hence Y is anti-discrete ; :: thesis: ( Y is strict & not Y is empty )
thus ( Y is strict & not Y is empty ) ; :: thesis: verum