let T be non empty TopSpace; ( T is locally-compact implies for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) )
assume A1:
for x being Point of T
for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
; WAYBEL_3:def 9 for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact )
set L = InclPoset the topology of T;
A2:
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
( x c= Z & Z c= y & Z is compact ) )
assume A3:
x << y
; ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact )
A4:
x in the topology of T
by A2;
y in the topology of T
by A2;
then reconsider X = x, Y = y as Subset of T by A4;
A5:
Y is open
by A2;
set VV = { (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } ;
reconsider e = {} T as Subset of T ;
A6:
{} c= Y
;
Int ({} T) = {}
;
then A7:
e in { (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) }
by A6;
{ (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } c= bool the carrier of T
then reconsider VV = { (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } as non empty Subset-Family of T by A7;
set V = union VV;
VV is open
then reconsider A = VV as Subset of (InclPoset the topology of T) by YELLOW_1:25;
A8:
sup A = union VV
by YELLOW_1:22;
Y c= union VV
then
y <= sup A
by A8, YELLOW_1:3;
then consider B being finite Subset of (InclPoset the topology of T) such that
A13:
B c= A
and
A14:
x <= sup B
by A3, Th18;
defpred S1[ object , object ] means ex Z being Subset of T st
( $2 = Z & $1 = Int Z & Z c= Y & Z is compact );
consider f being Function such that
A19:
dom f = B
and
A20:
for z being object st z in B holds
S1[z,f . z]
from CLASSES1:sch 1(A15);
reconsider W = B as Subset-Family of T by A2, XBOOLE_1:1;
sup B = union W
by YELLOW_1:22;
then A21:
X c= union W
by A14, YELLOW_1:3;
then reconsider Z = union (rng f) as Subset of T by ZFMISC_1:76;
take
Z
; ( x c= Z & Z c= y & Z is compact )
thus
x c= Z
( Z c= y & Z is compact )
thus
Z c= y
Z is compact
A33:
rng f is finite
by A19, FINSET_1:8;
defpred S2[ set ] means ex A being Subset of T st
( A = union $1 & A is compact );
union {} = {} T
by ZFMISC_1:2;
then A34:
S2[ {} ]
;
S2[ rng f]
from FINSET_1:sch 2(A33, A34, A35);
hence
Z is compact
; verum