theorem :: COMPACT1:8

for X being non empty TopSpace st not X is compact holds
incl (X,(One-Point_Compactification X)) is compactification