:: deftheorem defines 1TopSp COMPTS_1:def 5 :
for D being set holds 1TopSp D = TopStruct(# D,([#] (bool D)) #);