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 )
( x in the topology of T & y in the topology of T ) by A2;
then reconsider X = x, Y = y as Subset of T ;
A4: ( X is open & Y is open )

proof

thus ( X in the topology of T & Y in the topology of T ) by A2; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

set VV = { (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } ;
reconsider e = {} T as Subset of T ;
( {} c= Y & {} T is compact & Int ({} T) = {} ) by XBOOLE_1:2;
then A5: e in { (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } ;
{ (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact ) } c= bool the carrier of T

proof

let a be set ; :: 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 A5;
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;
A6: sup A = union VV by YELLOW_1:22;
Y c= union VV

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in union VV )
assume A7: a in Y ; :: thesis: a in union VV
then reconsider a = a as Point of T ;
consider Z being Subset of T such that
A8: ( a in Int Z & Z c= Y & Z is compact ) by A1, A4, A7;
Int Z in VV by A8;
hence a in union VV by A8, TARSKI:def 4; :: thesis: verum

end;

then y <= sup A by A6, YELLOW_1:3;
then consider B being finite Subset of (InclPoset the topology of T) such that
A9: ( B c= A & x <= sup B ) by A3, Th18;
defpred S₁[ set , set ] means ex Z being Subset of T st
( $2 = Z & $1 = Int Z & Z c= Y & Z is compact );

A10: now

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

end;

consider f being Function such that
A12: dom f = B and
A13: for z being set st z in B holds
S₁[z,f . z] from CLASSES1:sch 1(A10);
reconsider W = B as Subset-Family of T by A2, XBOOLE_1:1;
sup B = union W by YELLOW_1:22;
then A14: X c= union W by A9, YELLOW_1:3;

now

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 set such that
A15: ( a in B & z = f . a ) by A12, FUNCT_1:def 5;
ex Z being Subset of T st
( z = Z & a = Int Z & Z c= Y & Z is compact ) by A13, A15;
hence z c= the carrier of T ; :: thesis: verum

end;

then reconsider Z = union (rng f) as Subset of T by ZFMISC_1:94;
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 set ; :: 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
A16: ( z in a & a in W ) by A14, TARSKI:def 4;
consider Z being Subset of T such that
A17: ( f . a = Z & a = Int Z & Z c= Y & Z is compact ) by A13, A16;
Int Z c= Z by TOPS_1:44;
then ( z in Z & Z in rng f ) by A12, A16, A17, FUNCT_1:def 5;
hence z in Z by TARSKI:def 4; :: thesis: verum

end;

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

proof

let z be set ; :: 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
A18: ( z in a & a in rng f ) by TARSKI:def 4;
consider Z being set such that
A19: ( Z in W & a = f . Z ) by A12, A18, FUNCT_1:def 5;
ex S being Subset of T st
( a = S & Z = Int S & S c= Y & S is compact ) by A13, A19;
hence z in y by A18; :: thesis: verum

end;

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

A22: now

let x, B be set ; :: thesis: ( x in rng f & B c= rng f & S₂[B] implies S₂[B \/ {x}] )
assume A23: ( x in rng f & 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
A24: ( A = union B & A is compact ) ;
thus S₂[B \/ {x}] :: thesis: verum

proof

consider Z being set such that
A25: ( Z in W & x = f . Z ) by A12, A23, FUNCT_1:def 5;
consider S being Subset of T such that
A26: ( x = S & Z = Int S & S c= Y & S is compact ) by A13, A25;
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 A24, A26, ZFMISC_1:31
.= union (B \/ {x}) by ZFMISC_1:96 ; :: thesis: Bx is compact
thus Bx is compact by A24, A26, COMPTS_1:19; :: thesis: verum

end;

end;

S₂[ rng f] from FINSET_1:sch 2(A20, A21, A22);
hence Z is compact ; :: thesis: verum