let x be Point of (X | P); :: 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 B being basis of xx such that

A1: B is compact by Def3;

A2: [#] (X | P) = P by PRE_TOPC:8;

then xx in P ;

then xx in Int P by TOPS_1:23;

then P is a_neighborhood of xx by CONNSP_2:def 1;

then consider K being a_neighborhood of xx such that

A3: K in B and

A4: K c= P by YELLOW13:def 2;

reconsider KK = K as Subset of (X | P) by A4, PRE_TOPC:8;

K is compact by A1, A3;

then A5: KK is compact by A2, COMPTS_1:2;

A6: Int K c= K by TOPS_1:16;

xx in Int K by CONNSP_2:def 1;

then A7: x in K by A6;

KK = K /\ P by A4, XBOOLE_1:28;

then KK is a_neighborhood of x by A4, A7, TOPMETR:5;

hence ex U being a_neighborhood of x st U is compact by A5; :: thesis: verum

reconsider xx = x as Point of X by PRE_TOPC:25;

consider B being basis of xx such that

A1: B is compact by Def3;

A2: [#] (X | P) = P by PRE_TOPC:8;

then xx in P ;

then xx in Int P by TOPS_1:23;

then P is a_neighborhood of xx by CONNSP_2:def 1;

then consider K being a_neighborhood of xx such that

A3: K in B and

A4: K c= P by YELLOW13:def 2;

reconsider KK = K as Subset of (X | P) by A4, PRE_TOPC:8;

K is compact by A1, A3;

then A5: KK is compact by A2, COMPTS_1:2;

A6: Int K c= K by TOPS_1:16;

xx in Int K by CONNSP_2:def 1;

then A7: x in K by A6;

KK = K /\ P by A4, XBOOLE_1:28;

then KK is a_neighborhood of x by A4, A7, TOPMETR:5;

hence ex U being a_neighborhood of x st U is compact by A5; :: thesis: verum