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