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

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