consider O being non empty non trivial 1-sorted ;
reconsider tau = {} as Subset-Family of O by XBOOLE_1:2;
take Y = TopStruct(# the carrier of O,tau #); :: thesis: ( not Y is trivial & Y is strict & not Y is empty )
thus ( not Y is trivial & Y is strict & not Y is empty ) ; :: thesis: verum