let T be non empty TopSpace; ( 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
; T is locally-compact
let x be Point of T; WAYBEL_3:def 9 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; ( 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
; 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; ( 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; ( 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; Z is compact
let F be Subset-Family of T; COMPTS_1:def 4 ( not F is Cover of Z or not F is open or ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of Z & b1 is finite ) )
assume that
A12:
F is Cover of Z
and
A13:
F is open
; ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of Z & b1 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
; ( G c= F & G is Cover of Z & G is finite )
thus
G c= F
by A15, XBOOLE_1:43; ( G is Cover of Z & G is finite )
thus
Z c= union G
SETFAM_1:def 11 G is finite proof
let z be
object ;
TARSKI:def 3 ( not z in Z or z in union G )
assume A18:
z in Z
;
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;
verum
end;
thus
G is finite
; verum