let T be non empty TopSpace; :: thesis: ( T is locally-compact & T is T_2 implies for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact ) )
assume that
A1: T is locally-compact and
A2: T is T_2 ; :: thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact )
set L = InclPoset the topology of T;
A3: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
let x, y be Element of (InclPoset the topology of T); :: thesis: ( x << y implies ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact ) )
assume x << y ; :: thesis: ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact )
then consider Z being Subset of T such that
A4: x c= Z and
A5: Z c= y and
A6: Z is compact by A1, Th39;
x in the topology of T by A3;
then reconsider X = x as Subset of T ;
take X ; :: thesis: ( X = x & Cl X c= y & Cl X is compact )
thus X = x ; :: thesis: ( Cl X c= y & Cl X is compact )
Cl X c= Z by A2, A4, A6, TOPS_1:5;
hence ( Cl X c= y & Cl X is compact ) by A5, A6, COMPTS_1:9; :: thesis: verum