let X be non empty Hausdorff TopSpace; :: thesis: ( X is locally-compact implies X is locally-relatively-compact )
assume A1: X is locally-compact ; :: thesis: X is locally-relatively-compact
let x be Point of X; :: according to COMPACT1:def 4 :: thesis: ex U being a_neighborhood of x st U is relatively-compact
consider U being a_neighborhood of x such that
A2: U is compact by A1;
Cl U = U by A2, PRE_TOPC:22;
then U is relatively-compact by A2;
hence ex U being a_neighborhood of x st U is relatively-compact ; :: thesis: verum