theorem :: PCOMPS_1:6

for a being set holds 1TopSp {a} is compact ;