set O = the non empty trivial 1-sorted ;
reconsider tau = bool the carrier of the non empty trivial 1-sorted as Subset-Family of the non empty trivial 1-sorted ;
set Y = TopStruct(# the carrier of the non empty trivial 1-sorted ,tau #);
reconsider Y = TopStruct(# the carrier of the non empty trivial 1-sorted ,tau #) as non empty discrete TopStruct by TDLAT_3:def 1;
reconsider Y = Y as non empty TopSpace-like TopStruct ;
take Y ; :: thesis: ( Y is trivial & Y is strict & not Y is empty )
thus ( Y is trivial & Y is strict & not Y is empty ) ; :: thesis: verum