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 A2: ( T is regular & InclPoset the topology of T is continuous ) ; :: thesis: T is locally-compact
then A3: InclPoset the topology of T is continuous LATTICE ;
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 A4: ( x in X & X is open ) ; :: thesis: ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
then reconsider a = X as Element of (InclPoset the topology of T) by A1, PRE_TOPC:def 5;
a = sup (waybelow a) by A3, Def5
.= union (waybelow a) by YELLOW_1:22 ;
then consider Y being set such that
A5: ( x in Y & Y in waybelow a ) by A4, TARSKI:def 4;
Y in the carrier of (InclPoset the topology of T) by A5;
then reconsider Y = Y as Subset of T by A1;
consider y being Element of (InclPoset the topology of T) such that
A6: ( Y = y & y << a ) by A5;
Y is open by A1, A5, PRE_TOPC:def 5;
then consider W being open Subset of T such that
A7: ( x in W & Cl W c= Y ) by A2, A5, URYSOHN1:29;
take Z = Cl W; :: thesis: ( x in Int Z & Z c= X & Z is compact )
W c= Z by PRE_TOPC:48;
hence x in Int Z by A7, TOPS_1:54; :: thesis: ( Z c= X & Z is compact )
y <= a by A6, Th1;
then Y c= X by A6, YELLOW_1:3;
hence Z c= X by A7, XBOOLE_1:1; :: thesis: Z is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 7 :: 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 A8: ( F is Cover of Z & 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 by TOPS_2:def 1;
then FZ is open by A8, TOPS_2:20;
then reconsider FF = FZ as Subset of (InclPoset the topology of T) by YELLOW_1:25;
A9: sup FF = union FZ by YELLOW_1:22
.= (union F) \/ (union ZZ) by ZFMISC_1:96
.= (union F) \/ (Z ` ) by ZFMISC_1:31 ;
Z c= union F by A8, SETFAM_1:def 12;
then Z \/ (Z ` ) c= sup FF by A9, XBOOLE_1:9;
then [#] T c= sup FF by PRE_TOPC:18;
then X c= sup FF by XBOOLE_1:1;
then a <= sup FF by YELLOW_1:3;
then consider A being finite Subset of (InclPoset the topology of T) such that
A10: ( A c= FF & y <= sup A ) by A6, Th18;
A11: 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 A10, XBOOLE_1:43; :: thesis: ( G is Cover of Z & G is finite )
thus Z c= union G :: according to SETFAM_1:def 12 :: thesis: G is finite

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in union G )
assume z in Z ; :: thesis: z in union G
then A12: ( z in Y & Y c= union A & not z in Z ` ) by A6, A7, A10, A11, XBOOLE_0:def 5, YELLOW_1:3;
then consider B being set such that
A13: ( z in B & B in A ) by TARSKI:def 4;
not B in ZZ by A12, A13, TARSKI:def 1;
then B in G by A13, XBOOLE_0:def 5;
hence z in union G by A13, TARSKI:def 4; :: thesis: verum

end;

thus G is finite ; :: thesis: verum