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

assume A1: X is locally-closed/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 closed & 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

assume A1: X is locally-closed/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 closed & 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