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

assume A1: X is locally-relatively-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 Y being a_neighborhood of x such that

A2: Y is relatively-compact by A1;

A3: x in Int Y by CONNSP_2:def 1;

Int Y c= Int (Cl Y) by PRE_TOPC:18, TOPS_1:19;

then Cl Y is a_neighborhood of x by A3, CONNSP_2:def 1;

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

assume A1: X is locally-relatively-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 Y being a_neighborhood of x such that

A2: Y is relatively-compact by A1;

A3: x in Int Y by CONNSP_2:def 1;

Int Y c= Int (Cl Y) by PRE_TOPC:18, TOPS_1:19;

then Cl Y is a_neighborhood of x by A3, CONNSP_2:def 1;

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