let T be non empty TopSpace; :: thesis: ( T is regular & InclPoset the topology of T is continuous implies T is locally-compact )
set L = InclPoset the topology of T;
A1: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
assume that
A2: T is regular and
A3: InclPoset the topology of T is continuous ; :: thesis: T is locally-compact
let x be Point of T; :: according to WAYBEL_3:def 9 :: thesis: 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 )
let X be Subset of T; :: thesis: ( x in X & X is open implies ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact ) )
assume that
A4: x in X and
A5: X is open ; :: thesis: ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
reconsider a = X as Element of (InclPoset the topology of T) by A1, A5;
a = sup (waybelow a) by A3, Def5
.= union (waybelow a) by YELLOW_1:22 ;
then consider Y being set such that
A6: x in Y and
A7: Y in waybelow a by A4, TARSKI:def 4;
Y in the carrier of (InclPoset the topology of T) by A7;
then reconsider Y = Y as Subset of T by A1;
consider y being Element of (InclPoset the topology of T) such that
A8: Y = y and
A9: y << a by A7;
Y is open by A1, A7;
then consider W being open Subset of T such that
A10: x in W and
A11: Cl W c= Y by A2, A6, URYSOHN1:21;
take Z = Cl W; :: thesis: ( x in Int Z & Z c= X & Z is compact )
W c= Z by PRE_TOPC:18;
hence x in Int Z by A10, TOPS_1:22; :: thesis: ( Z c= X & Z is compact )
y <= a by A9, Th1;
then Y c= X by A8, YELLOW_1:3;
hence Z c= X by A11; :: thesis: Z is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( not F is Cover of Z or not F is open or ex b₁ being Element of K10(K10( the carrier of T)) st
( b₁ c= F & b₁ is Cover of Z & b₁ is finite ) )
assume that
A12: F is Cover of Z and
A13: F is open ; :: thesis: ex b₁ being Element of K10(K10( the carrier of T)) st
( b₁ c= F & b₁ is Cover of Z & b₁ is finite )
reconsider ZZ = {(Z `)} as Subset-Family of T ;
reconsider ZZ = ZZ as Subset-Family of T ;
reconsider FZ = F \/ ZZ as Subset-Family of T ;
for x being Subset of T st x in ZZ holds
x is open by TARSKI:def 1;
then ZZ is open ;
then FZ is open by A13, TOPS_2:13;
then reconsider FF = FZ as Subset of (InclPoset the topology of T) by YELLOW_1:25;
A14: sup FF = union FZ by YELLOW_1:22
.= (union F) \/ (union ZZ) by ZFMISC_1:78
.= (union F) \/ (Z `) by ZFMISC_1:25 ;
Z c= union F by A12, SETFAM_1:def 11;
then Z \/ (Z `) c= sup FF by A14, XBOOLE_1:9;
then [#] T c= sup FF by PRE_TOPC:2;
then X c= sup FF ;
then a <= sup FF by YELLOW_1:3;
then consider A being finite Subset of (InclPoset the topology of T) such that
A15: A c= FF and
A16: y <= sup A by A9, Th18;
A17: sup A = union A by YELLOW_1:22;
reconsider G = A \ ZZ as Subset-Family of T by A1, XBOOLE_1:1;
take G ; :: thesis: ( G c= F & G is Cover of Z & G is finite )
thus G c= F by A15, XBOOLE_1:43; :: thesis: ( G is Cover of Z & G is finite )
thus Z c= union G :: according to SETFAM_1:def 11 :: thesis: G is finite

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in union G )
assume A18: z in Z ; :: thesis: z in union G
then A19: z in Y by A11;
A20: Y c= union A by A8, A16, A17, YELLOW_1:3;
A21: not z in Z ` by A18, XBOOLE_0:def 5;
consider B being set such that
A22: z in B and
A23: B in A by A19, A20, TARSKI:def 4;
not B in ZZ by A21, A22, TARSKI:def 1;
then B in G by A23, XBOOLE_0:def 5;
hence z in union G by A22, TARSKI:def 4; :: thesis: verum

end;

thus G is finite ; :: thesis: verum