let x be Point of (X | C); :: according to COMPACT1:def 6 :: thesis: ex U being a_neighborhood of x st U is compact
reconsider xx = x as Point of X by PRE_TOPC:25;
consider K being a_neighborhood of xx such that
A1: K is compact by Def6;
A2: [#] (X | C) = C by PRE_TOPC:8;
then reconsider KC = K /\ C as Subset of (X | C) by XBOOLE_1:17;
reconsider KC = KC as a_neighborhood of x by A2, TOPMETR:5;
take KC ; :: thesis: KC is compact
A3: xx in Int K by CONNSP_2:def 1;
A4: [#] (X | K) = K by PRE_TOPC:8;
then reconsider KK = K /\ C as Subset of (X | K) by XBOOLE_1:17;
A5: KK is closed by A4, PRE_TOPC:13;
A6: Int K c= K by TOPS_1:16;
then A7: x in KC by A2, A3, XBOOLE_0:def 4;
X | K is compact by A1, A6, A3, COMPTS_1:3;
then KK is compact by A5, COMPTS_1:8;
then (X | K) | KK is compact by A7, COMPTS_1:3;
then X | (K /\ C) is compact by PRE_TOPC:7, XBOOLE_1:17;
then (X | C) | KC is compact by PRE_TOPC:7, XBOOLE_1:17;
hence KC is compact by A7, COMPTS_1:3; :: thesis: verum