:: deftheorem defines compactification COMPACT1:def 8 :
for X, Y being TopSpace
for h being Function of X,Y holds
( h is compactification iff ( h is embedding & Y is compact & h .: ([#] X) is dense ) );