theorem :: COMPTS_1:13

for TS being non empty TopSpace st TS is T_2 & TS is compact holds
TS is normal