let X be non empty TopSpace; :: thesis: ( X is liminally-compact implies X is locally-compact )

assume A1: X is liminally-compact ; :: thesis: X is locally-compact

let x be Point of X; :: according to COMPACT1:def 6 :: thesis: ex U being a_neighborhood of x st U is compact

consider B being basis of x such that

A2: B is compact by A1;

set V = the a_neighborhood of x;

consider Y being a_neighborhood of x such that

A3: Y in B and

Y c= the a_neighborhood of x by YELLOW13:def 2;

Y is compact by A2, A3;

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

assume A1: X is liminally-compact ; :: thesis: X is locally-compact

let x be Point of X; :: according to COMPACT1:def 6 :: thesis: ex U being a_neighborhood of x st U is compact

consider B being basis of x such that

A2: B is compact by A1;

set V = the a_neighborhood of x;

consider Y being a_neighborhood of x such that

A3: Y in B and

Y c= the a_neighborhood of x by YELLOW13:def 2;

Y is compact by A2, A3;

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