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