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 by Def1; :: thesis: ( Y is anti-discrete & Y is strict & not Y is empty )
tau = {{} ,{{} }} by ZFMISC_1:30;
hence Y is anti-discrete by Def2; :: thesis: ( Y is strict & not Y is empty )
thus ( Y is strict & not Y is empty ) ; :: thesis: verum