let T be non empty TopSpace; :: thesis: ( 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 ) ; :: according to WAYBEL_3:def 9 :: thesis: 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); :: thesis: ( x << y implies ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) )
assume A3: x << y ; :: thesis: 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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } or a in bool the carrier of T )
assume a in { (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } ; :: thesis: a in bool the carrier of T
then ex Z being Subset of T st
( a = Int Z & Z c= Y & Z is compact ) ;
hence a in bool the carrier of T ; :: thesis: verum

end;

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

proof

let a be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not a in VV or a is open )
assume a in VV ; :: thesis: a is open
then ex Z being Subset of T st
( a = Int Z & Z c= Y & Z is compact ) ;
hence a is open ; :: thesis: verum

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in union VV )
assume A9: a in Y ; :: thesis: a in union VV
then reconsider a = a as Point of T ;
consider Z being Subset of T such that
A10: a in Int Z and
A11: Z c= Y and
A12: Z is compact by A1, A5, A9;
Int Z in VV by A11, A12;
hence a in union VV by A10, TARSKI:def 4; :: thesis: verum

end;

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 S₁[ object , object ] means ex Z being Subset of T st
( $2 = Z & $1 = Int Z & Z c= Y & Z is compact );

A15: now :: thesis: for z being object st z in B holds
ex s being object st S₁[z,s]

let z be object ; :: thesis: ( z in B implies ex s being object st S₁[z,s] )
assume z in B ; :: thesis: ex s being object st S₁[z,s]
then z in A by A13;
then consider Z being Subset of T such that
A16: z = Int Z and
A17: Z c= Y and
A18: Z is compact ;
reconsider s = Z as object ;
take s = s; :: thesis: S₁[z,s]
thus S₁[z,s] by A16, A17, A18; :: thesis: verum

end;

consider f being Function such that
A19: dom f = B and
A20: for z being object st z in B holds
S₁[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;

now :: thesis: for z being set st z in rng f holds
z c= the carrier of T

let z be set ; :: thesis: ( z in rng f implies z c= the carrier of T )
assume z in rng f ; :: thesis: z c= the carrier of T
then consider a being object such that
A22: a in B and
A23: z = f . a by A19, FUNCT_1:def 3;
ex Z being Subset of T st
( z = Z & a = Int Z & Z c= Y & Z is compact ) by A20, A22, A23;
hence z c= the carrier of T ; :: thesis: verum

end;

then reconsider Z = union (rng f) as Subset of T by ZFMISC_1:76;
take Z ; :: thesis: ( x c= Z & Z c= y & Z is compact )
thus x c= Z :: thesis: ( Z c= y & Z is compact )

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in Z )
assume z in x ; :: thesis: z in Z
then consider a being set such that
A24: z in a and
A25: a in W by A21, TARSKI:def 4;
consider Z being Subset of T such that
A26: f . a = Z and
A27: a = Int Z and
Z c= Y and
Z is compact by A20, A25;
A28: Int Z c= Z by TOPS_1:16;
Z in rng f by A19, A25, A26, FUNCT_1:def 3;
hence z in Z by A24, A27, A28, TARSKI:def 4; :: thesis: verum

end;

thus Z c= y :: thesis: Z is compact

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in y )
assume z in Z ; :: thesis: z in y
then consider a being set such that
A29: z in a and
A30: a in rng f by TARSKI:def 4;
consider Z being object such that
A31: Z in W and
A32: a = f . Z by A19, A30, FUNCT_1:def 3;
ex S being Subset of T st
( a = S & Z = Int S & S c= Y & S is compact ) by A20, A31, A32;
hence z in y by A29; :: thesis: verum

end;

A33: rng f is finite by A19, FINSET_1:8;
defpred S₂[ set ] means ex A being Subset of T st
( A = union $1 & A is compact );
union {} = {} T by ZFMISC_1:2;
then A34: S₂[ {} ] ;

A35: now :: thesis: for x, B being set st x in rng f & B c= rng f & S₂[B] holds
S₂[B \/ {x}]

let x, B be set ; :: thesis: ( x in rng f & B c= rng f & S₂[B] implies S₂[B \/ {x}] )
assume that
A36: x in rng f and
B c= rng f ; :: thesis: ( S₂[B] implies S₂[B \/ {x}] )
assume S₂[B] ; :: thesis: S₂[B \/ {x}]
then consider A being Subset of T such that
A37: A = union B and
A38: A is compact ;
thus S₂[B \/ {x}] :: thesis: verum

proof

consider Z being object such that
A39: Z in W and
A40: x = f . Z by A19, A36, FUNCT_1:def 3;
consider S being Subset of T such that
A41: x = S and
Z = Int S and
S c= Y and
A42: S is compact by A20, A39, A40;
reconsider Bx = A \/ S as Subset of T ;
take Bx ; :: thesis: ( Bx = union (B \/ {x}) & Bx is compact )
thus Bx = (union B) \/ (union {x}) by A37, A41, ZFMISC_1:25
.= union (B \/ {x}) by ZFMISC_1:78 ; :: thesis: Bx is compact
thus Bx is compact by A38, A42, COMPTS_1:10; :: thesis: verum

end;

end;

S₂[ rng f] from FINSET_1:sch 2(A33, A34, A35);
hence Z is compact ; :: thesis: verum