set O = the 1 -element 1-sorted ;
reconsider tau = bool the carrier of the 1 -element 1-sorted as Subset-Family of the 1 -element 1-sorted ;
set Y = TopStruct(# the carrier of the 1 -element 1-sorted ,tau #);
reconsider Y = TopStruct(# the carrier of the 1 -element 1-sorted ,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 1 -element & Y is strict )
thus the carrier of Y is 1 -element ; :: according to STRUCT_0:def 19 :: thesis: Y is strict
thus Y is strict ; :: thesis: verum