set O = the 1 -element 1-sorted ;
reconsider tau = {} as Subset-Family of the 1 -element 1-sorted by XBOOLE_1:2;
reconsider tau = tau as Subset-Family of the 1 -element 1-sorted ;
take TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) ; :: thesis: ( TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is 1 -element & TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is strict )
thus the carrier of TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is 1 -element ; :: according to STRUCT_0:def 19 :: thesis: TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is strict
thus TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is strict ; :: thesis: verum