let X be TopStruct ; :: thesis: [#] X c= [#] (One-Point_Compactification X)
[#] (One-Point_Compactification X) = succ ([#] X) by Def9;
hence [#] X c= [#] (One-Point_Compactification X) by XBOOLE_1:7; :: thesis: verum