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