let T be non empty TopSpace; ( 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
; 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); ( x << y implies ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact ) )
assume
x << y
; 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
; ( X = x & Cl X c= y & Cl X is compact )
thus
X = x
; ( 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; verum