consider O being non empty trivial 1-sorted ;
reconsider tau = bool the carrier of O as Subset-Family of O ;
set Y = TopStruct(# the carrier of O,tau #);
reconsider Y = TopStruct(# the carrier of O,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