let X be non empty TopSpace; ( X is locally-relatively-compact implies X is locally-compact )
assume A1:
X is locally-relatively-compact
; X is locally-compact
let x be Point of X; COMPACT1:def 6 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; verum