theorem :: COMPTS_1:12
for TS being non empty TopSpace st TS is T_2 & TS is compact holds
TS is regular by Th6, Th8;