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

assume A1: X is locally-relatively-compact ; :: thesis: X is locally-closed/compact

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

( U is closed & U is compact )

consider U being a_neighborhood of x such that

A2: U is relatively-compact by A1;

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

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

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

hence ex U being a_neighborhood of x st

( U is closed & U is compact ) by A2; :: thesis: verum

assume A1: X is locally-relatively-compact ; :: thesis: X is locally-closed/compact

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

( U is closed & U is compact )

consider U being a_neighborhood of x such that

A2: U is relatively-compact by A1;

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

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

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

hence ex U being a_neighborhood of x st

( U is closed & U is compact ) by A2; :: thesis: verum