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

[#] (One-Point_Compactification X) = succ ([#] X) by Def9;

hence [#] X c= [#] (One-Point_Compactification X) by XBOOLE_1:7; :: thesis: verum