theorem :: PCOMPS_1:5

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