theorem :: PCOMPS_1:4

for a being set holds the topology of (1TopSp a) = bool a ;