:: YELLOW_8 semantic presentation

begin

theorem Th1: :: YELLOW_8:1
for X, A, B being set st A in Fin X & B c= A holds
B in Fin X
proof
let X, A, B be set ; ::_thesis: ( A in Fin X & B c= A implies B in Fin X )
assume that
A1: A in Fin X and
A2: B c= A ; ::_thesis: B in Fin X
 A c= X by A1, FINSUB_1:def_5;
then  B c= X by A2, XBOOLE_1:1;
hence  B in Fin X by A1, A2, FINSUB_1:def_5; ::_thesis: verum
end;

theorem Th2: :: YELLOW_8:2
for X being set
for F being Subset-Family of X st F c= Fin X holds
meet F in Fin X
proof
let X be set ; ::_thesis: for F being Subset-Family of X st F c= Fin X holds
meet F in Fin X
let F be Subset-Family of X; ::_thesis: ( F c= Fin X implies meet F in Fin X )
assume A1: F c= Fin X ; ::_thesis: meet F in Fin X
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet F in Fin X
hence  meet F in Fin X by FINSUB_1:7, SETFAM_1:1; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet F in Fin X
then consider A being set  such that
A2: A in F by XBOOLE_0:def_1;
 meet F c= A by A2, SETFAM_1:3;
hence  meet F in Fin X by A1, A2, Th1; ::_thesis: verum
end;
end;
end;

begin

theorem Th3: :: YELLOW_8:3
for X being set
for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent
proof
let X be set ; ::_thesis: for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent
let F be Subset-Family of X; ::_thesis: F, COMPLEMENT F are_equipotent
deffunc H1( set ) ->  Element of bool X = X \ $1;
consider f being Function such that
A1: dom f = F and
A2: for x being set st x in F holds
f . x = H1(x) from FUNCT_1:sch_3();
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = F & rng f = COMPLEMENT F )
thus  f is one-to-one ::_thesis: ( dom f = F & rng f = COMPLEMENT F )
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider X1 = x1, X2 = x2 as Subset of X by A1, A3, A4;
X1 ` = f . x1 by A1, A2, A3
.= X2 ` by A1, A2, A4, A5 ;
hence x1 = (X2 `) `
.= x2 ;
::_thesis: verum
end;
thus  dom f = F by A1; ::_thesis: rng f = COMPLEMENT F
thus  rng f c= COMPLEMENT F :: according to XBOOLE_0:def_10 ::_thesis: COMPLEMENT F c= rng f
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng f or e in COMPLEMENT F )
assume  e in rng f ; ::_thesis: e in COMPLEMENT F
then consider u being set  such that
A6: u in dom f and
A7: e = f . u by FUNCT_1:def_3;
reconsider Y = u as Subset of X by A1, A6;
 e = Y ` by A1, A2, A6, A7;
hence  e in COMPLEMENT F by A1, A6, SETFAM_1:35; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in COMPLEMENT F or e in rng f )
assume A8: e in COMPLEMENT F ; ::_thesis: e in rng f
then reconsider Y = e as Subset of X ;
A9: Y ` in F by A8, SETFAM_1:def_7;
e = (Y `) `
.= f . (Y `) by A2, A9 ;
hence  e in rng f by A1, A9, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th4: :: YELLOW_8:4
for X, Y being set st X,Y are_equipotent & X is countable holds
Y is countable
proof
let X, Y be set ; ::_thesis: ( X,Y are_equipotent & X is countable implies Y is countable )
assume  ( X,Y are_equipotent & card X c= omega ) ; :: according to CARD_3:def_14 ::_thesis: Y is countable
hence  card Y c= omega by CARD_1:5; :: according to CARD_3:def_14 ::_thesis: verum
end;

theorem :: YELLOW_8:5
for X being 1-sorted
for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
proof
let X be 1-sorted ; ::_thesis: for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let F be Subset-Family of X; ::_thesis: for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let P be Subset of X; ::_thesis: ( P ` in COMPLEMENT F iff P in F )
 P = (P `) ` ;
hence  ( P ` in COMPLEMENT F iff P in F ) by SETFAM_1:def_7; ::_thesis: verum
end;

theorem Th6: :: YELLOW_8:6
for X being 1-sorted
for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) `
proof
let X be 1-sorted ; ::_thesis: for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) `
let F be Subset-Family of X; ::_thesis: Intersect (COMPLEMENT F) = (union F) `
percases ( F <> {} or F = {} ) ;
supposeA1: F <> {} ; ::_thesis: Intersect (COMPLEMENT F) = (union F) `
then  COMPLEMENT F <> {} by SETFAM_1:32;
hence  Intersect (COMPLEMENT F) = meet (COMPLEMENT F) by SETFAM_1:def_9
.= ([#] the carrier of X) \ (union F) by A1, SETFAM_1:33
.= (union F) ` ;
::_thesis: verum
end;
suppose F = {} ; ::_thesis: Intersect (COMPLEMENT F) = (union F) `
then reconsider G = F as empty Subset-Family of X ;
 COMPLEMENT G = {} ;
hence  Intersect (COMPLEMENT F) = (union F) ` by SETFAM_1:def_9, ZFMISC_1:2; ::_thesis: verum
end;
end;
end;

theorem Th7: :: YELLOW_8:7
for X being 1-sorted
for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) `
proof
let X be 1-sorted ; ::_thesis: for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) `
let F be Subset-Family of X; ::_thesis: union (COMPLEMENT F) = (Intersect F) `
thus  union (COMPLEMENT F) = ((union (COMPLEMENT F)) `) `
.= (Intersect (COMPLEMENT (COMPLEMENT F))) ` by Th6
.= (Intersect F) ` ; ::_thesis: verum
end;

begin

theorem :: YELLOW_8:8
for T being non empty TopSpace
for A, B being Subset of T st B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) holds
A = Cl B
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) holds
A = Cl B
let A, B be Subset of T; ::_thesis: ( B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) implies A = Cl B )
assume that
A1: ( B c= A & A is closed ) and
A2: for C being Subset of T st B c= C & C is closed holds
A c= C ; ::_thesis: A = Cl B
thus  A c= Cl B by A2, PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl B c= A
thus  Cl B c= A by A1, TOPS_1:5; ::_thesis: verum
end;

theorem Th9: :: YELLOW_8:9
for T being TopStruct
for B being Basis of T
for V being Subset of T st V is open holds
V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
proof
let T be TopStruct ; ::_thesis: for B being Basis of T
for V being Subset of T st V is open holds
V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
let B be Basis of T; ::_thesis: for V being Subset of T st V is open holds
V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
let V be Subset of T; ::_thesis: ( V is open implies V = union  {  G where G is Subset of T : ( G in B & G c= V )  }  )
assume A1: V is open ; ::_thesis: V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
set X =  {  G where G is Subset of T : ( G in B & G c= V )  }  ;
A2: the topology of T c= UniCl B by CANTOR_1:def_2;
 for x being set holds
( x in V iff ex Y being set st
( x in Y & Y in  {  G where G is Subset of T : ( G in B & G c= V )  }  ) )
proof
let x be set ; ::_thesis: ( x in V iff ex Y being set st
( x in Y & Y in  {  G where G is Subset of T : ( G in B & G c= V )  }  ) )
hereby  ::_thesis: ( ex Y being set st
( x in Y & Y in  {  G where G is Subset of T : ( G in B & G c= V )  }  ) implies x in V )
 V in the topology of T by A1, PRE_TOPC:def_2;
then consider Y being Subset-Family of T such that
A3: Y c= B and
A4: V = union Y by A2, CANTOR_1:def_1;
assume  x in V ; ::_thesis: ex W being set st
( x in W & W in  {  G where G is Subset of T : ( G in B & G c= V )  }  )
then consider W being set  such that
A5: x in W and
A6: W in Y by A4, TARSKI:def_4;
take W = W; ::_thesis: ( x in W & W in  {  G where G is Subset of T : ( G in B & G c= V )  }  )
thus  x in W by A5; ::_thesis: W in  {  G where G is Subset of T : ( G in B & G c= V )  }
reconsider G = W as Subset of T by A6;
 G c= V by A4, A6, ZFMISC_1:74;
hence  W in  {  G where G is Subset of T : ( G in B & G c= V )  }  by A3, A6; ::_thesis: verum
end;
given Y being set  such that A7: x in Y and
A8: Y in  {  G where G is Subset of T : ( G in B & G c= V )  }  ; ::_thesis: x in V
 ex G being Subset of T st
( Y = G & G in B & G c= V ) by A8;
hence  x in V by A7; ::_thesis: verum
end;
hence  V = union  {  G where G is Subset of T : ( G in B & G c= V )  }  by TARSKI:def_4; ::_thesis: verum
end;

theorem Th10: :: YELLOW_8:10
for T being TopStruct
for B being Basis of T
for S being Subset of T st S in B holds
S is open
proof
let T be TopStruct ; ::_thesis: for B being Basis of T
for S being Subset of T st S in B holds
S is open
let B be Basis of T; ::_thesis: for S being Subset of T st S in B holds
S is open
let S be Subset of T; ::_thesis: ( S in B implies S is open )
assume A1: S in B ; ::_thesis: S is open
 B c= the topology of T by TOPS_2:64;
hence  S is open by A1, PRE_TOPC:def_2; ::_thesis: verum
end;

theorem :: YELLOW_8:11
for T being non empty TopSpace
for B being Basis of T
for V being Subset of T holds Int V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
proof
let T be non empty TopSpace; ::_thesis: for B being Basis of T
for V being Subset of T holds Int V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
let B be Basis of T; ::_thesis: for V being Subset of T holds Int V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
let V be Subset of T; ::_thesis: Int V = union  {  G where G is Subset of T : ( G in B & G c= V )  }
set X =  {  G where G is Subset of T : ( G in B & G c= V )  }  ;
set Y =  {  G where G is Subset of T : ( G in B & G c= Int V )  }  ;
  {  G where G is Subset of T : ( G in B & G c= V )  }  =  {  G where G is Subset of T : ( G in B & G c= Int V )  }
proof
thus   {  G where G is Subset of T : ( G in B & G c= V )  }  c=  {  G where G is Subset of T : ( G in B & G c= Int V )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  G where G is Subset of T : ( G in B & G c= Int V )  }  c=  {  G where G is Subset of T : ( G in B & G c= V )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  G where G is Subset of T : ( G in B & G c= V )  }  or e in  {  G where G is Subset of T : ( G in B & G c= Int V )  }  )
assume  e in  {  G where G is Subset of T : ( G in B & G c= V )  }  ; ::_thesis: e in  {  G where G is Subset of T : ( G in B & G c= Int V )  }
then consider G being Subset of T such that
A1: e = G and
A2: G in B and
A3: G c= V ;
 G c= Int V by A2, A3, Th10, TOPS_1:24;
hence  e in  {  G where G is Subset of T : ( G in B & G c= Int V )  }  by A1, A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  G where G is Subset of T : ( G in B & G c= Int V )  }  or e in  {  G where G is Subset of T : ( G in B & G c= V )  }  )
assume  e in  {  G where G is Subset of T : ( G in B & G c= Int V )  }  ; ::_thesis: e in  {  G where G is Subset of T : ( G in B & G c= V )  }
then consider G being Subset of T such that
A4: ( e = G & G in B ) and
A5: G c= Int V ;
 Int V c= V by TOPS_1:16;
then  G c= V by A5, XBOOLE_1:1;
hence  e in  {  G where G is Subset of T : ( G in B & G c= V )  }  by A4; ::_thesis: verum
end;
hence  Int V = union  {  G where G is Subset of T : ( G in B & G c= V )  }  by Th9; ::_thesis: verum
end;

begin

definition
let T be non empty TopStruct ;
let x be Point of T;
let F be Subset-Family of T;
attrF is x -quasi_basis  means :Def1: :: YELLOW_8:def 1
( x in Intersect F & ( for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in F & V c= S ) ) );
end;

:: deftheorem Def1 defines -quasi_basis YELLOW_8:def_1_:_
 for T being non empty TopStruct
for x being Point of T
for F being Subset-Family of T holds
( F is x -quasi_basis iff ( x in Intersect F & ( for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in F & V c= S ) ) ) );

registration
let T be non empty TopStruct ;
let x be Point of T;
cluster open x -quasi_basis for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is open & b1 is x -quasi_basis )
proof
defpred S1[ set ] means ( T in the topology of T & x in T );
set IT =  {  S where S is Subset of T : S1[S]  }  ;
  {  S where S is Subset of T : S1[S]  }  is Subset-Family of T from DOMAIN_1:sch_7();
then reconsider IT =  {  S where S is Subset of T : S1[S]  }  as Subset-Family of T ;
take  IT ; ::_thesis: ( IT is open & IT is x -quasi_basis )
 IT c= the topology of T
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in IT or e in the topology of T )
assume  e in IT ; ::_thesis: e in the topology of T
then  ex S being Subset of T st
( S = e & S in the topology of T & x in S ) ;
hence  e in the topology of T ; ::_thesis: verum
end;
hence  IT is open by TOPS_2:64; ::_thesis: IT is x -quasi_basis
now__::_thesis:_for_e_being_set_st_e_in_IT_holds_
x_in_e
let e be set ; ::_thesis: ( e in IT implies x in e )
assume  e in IT ; ::_thesis: x in e
then  ex S being Subset of T st
( S = e & S in the topology of T & x in S ) ;
hence  x in e ; ::_thesis: verum
end;
hence  x in Intersect IT by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in IT & V c= S )
let S be Subset of T; ::_thesis: ( S is open & x in S implies ex V being Subset of T st
( V in IT & V c= S ) )
assume that
A1: S is open and
A2: x in S ; ::_thesis: ex V being Subset of T st
( V in IT & V c= S )
take V = S; ::_thesis: ( V in IT & V c= S )
 V in the topology of T by A1, PRE_TOPC:def_2;
hence  V in IT by A2; ::_thesis: V c= S
thus  V c= S ; ::_thesis: verum
end;
end;

definition
let T be non empty TopStruct ;
let x be Point of T;
mode Basis of x is open x -quasi_basis Subset-Family of T;
end;

theorem Th12: :: YELLOW_8:12
for T being non empty TopStruct
for x being Point of T
for B being Basis of x
for V being Subset of T st V in B holds
( V is open & x in V )
proof
let T be non empty TopStruct ; ::_thesis: for x being Point of T
for B being Basis of x
for V being Subset of T st V in B holds
( V is open & x in V )
let x be Point of T; ::_thesis: for B being Basis of x
for V being Subset of T st V in B holds
( V is open & x in V )
let B be Basis of x; ::_thesis: for V being Subset of T st V in B holds
( V is open & x in V )
let V be Subset of T; ::_thesis: ( V in B implies ( V is open & x in V ) )
assume A1: V in B ; ::_thesis: ( V is open & x in V )
 B c= the topology of T by TOPS_2:64;
hence  V is open by A1, PRE_TOPC:def_2; ::_thesis: x in V
 x in Intersect B by Def1;
hence  x in V by A1, SETFAM_1:43; ::_thesis: verum
end;

theorem :: YELLOW_8:13
for T being non empty TopStruct
for x being Point of T
for B being Basis of x
for V being Subset of T st x in V & V is open holds
ex W being Subset of T st
( W in B & W c= V ) by Def1;

theorem :: YELLOW_8:14
for T being non empty TopStruct
for P being Subset-Family of T st P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) holds
P is Basis of T
proof
let T be non empty TopStruct ; ::_thesis: for P being Subset-Family of T st P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) holds
P is Basis of T
let P be Subset-Family of T; ::_thesis: ( P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) implies P is Basis of T )
assume that
A1: P c= the topology of T and
A2: for x being Point of T ex B being Basis of x st B c= P ; ::_thesis: P is Basis of T
 P is quasi_basis
proof
let e be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not e in the topology of T or e in UniCl P )
assume A3: e in the topology of T ; ::_thesis: e in UniCl P
then reconsider S = e as Subset of T ;
set X =  {  V where V is Subset of T : ( V in P & V c= S )  }  ;
A4:  {  V where V is Subset of T : ( V in P & V c= S )  }  c= P
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  V where V is Subset of T : ( V in P & V c= S )  }  or e in P )
assume  e in  {  V where V is Subset of T : ( V in P & V c= S )  }  ; ::_thesis: e in P
then  ex V being Subset of T st
( e = V & V in P & V c= S ) ;
hence  e in P ; ::_thesis: verum
end;
then reconsider X =  {  V where V is Subset of T : ( V in P & V c= S )  }  as Subset-Family of T by XBOOLE_1:1;
 for u being set holds
( u in S iff ex Z being set st
( u in Z & Z in X ) )
proof
let u be set ; ::_thesis: ( u in S iff ex Z being set st
( u in Z & Z in X ) )
hereby  ::_thesis: ( ex Z being set st
( u in Z & Z in X ) implies u in S )
assume A5: u in S ; ::_thesis: ex Z being set st
( u in Z & Z in X )
then reconsider p = u as Point of T ;
consider B being Basis of p such that
A6: B c= P by A2;
 S is open by A3, PRE_TOPC:def_2;
then consider W being Subset of T such that
A7: W in B and
A8: W c= S by A5, Def1;
reconsider Z = W as set ;
take Z = Z; ::_thesis: ( u in Z & Z in X )
thus  u in Z by A7, Th12; ::_thesis: Z in X
thus  Z in X by A6, A7, A8; ::_thesis: verum
end;
given Z being set  such that A9: u in Z and
A10: Z in X ; ::_thesis: u in S
 ex V being Subset of T st
( V = Z & V in P & V c= S ) by A10;
hence  u in S by A9; ::_thesis: verum
end;
then  S = union X by TARSKI:def_4;
hence  e in UniCl P by A4, CANTOR_1:def_1; ::_thesis: verum
end;
hence  P is Basis of T by A1, TOPS_2:64; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
attrT is Baire  means :Def2: :: YELLOW_8:def 2
 for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) holds
ex I being Subset of T st
( I = Intersect F & I is dense );
end;

:: deftheorem Def2 defines Baire YELLOW_8:def_2_:_
 for T being non empty TopSpace holds
( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) );

theorem :: YELLOW_8:15
for T being non empty TopSpace holds
( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary )
proof
let T be non empty TopSpace; ::_thesis: ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary )
hereby  ::_thesis: ( ( for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary ) implies T is Baire )
assume A1: T is Baire ; ::_thesis: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary
let F be Subset-Family of T; ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) implies union F is boundary )
assume that
A2: F is countable and
A3: for S being Subset of T st S in F holds
S is nowhere_dense ; ::_thesis: union F is boundary
reconsider G = COMPLEMENT F as Subset-Family of T ;
A4: for S being Subset of T st S in G holds
S is everywhere_dense
proof
let S be Subset of T; ::_thesis: ( S in G implies S is everywhere_dense )
assume  S in G ; ::_thesis: S is everywhere_dense
then  S ` in F by SETFAM_1:def_7;
then  S ` is nowhere_dense by A3;
hence  S is everywhere_dense by TOPS_3:39; ::_thesis: verum
end;
 G is countable by A2, Th3, Th4;
then  ex I being Subset of T st
( I = Intersect G & I is dense ) by A1, A4, Def2;
then  (union F) ` is dense by Th6;
hence  union F is boundary by TOPS_1:def_4; ::_thesis: verum
end;
assume A5: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary ; ::_thesis: T is Baire
let F be Subset-Family of T; :: according to YELLOW_8:def_2 ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) implies ex I being Subset of T st
( I = Intersect F & I is dense ) )
assume that
A6: F is countable and
A7: for S being Subset of T st S in F holds
S is everywhere_dense ; ::_thesis: ex I being Subset of T st
( I = Intersect F & I is dense )
reconsider I = Intersect F as Subset of T ;
take  I ; ::_thesis: ( I = Intersect F & I is dense )
thus  I = Intersect F ; ::_thesis: I is dense
reconsider G = COMPLEMENT F as Subset-Family of T ;
A8: for S being Subset of T st S in G holds
S is nowhere_dense
proof
let S be Subset of T; ::_thesis: ( S in G implies S is nowhere_dense )
assume  S in G ; ::_thesis: S is nowhere_dense
then  S ` in F by SETFAM_1:def_7;
then  S ` is everywhere_dense by A7;
hence  S is nowhere_dense by TOPS_3:40; ::_thesis: verum
end;
 G is countable by A6, Th3, Th4;
then  union G is boundary by A5, A8;
then  (Intersect F) ` is boundary by Th7;
hence  I is dense by TOPS_3:18; ::_thesis: verum
end;

begin

definition
let T be TopStruct ;
let S be Subset of T;
attrS is irreducible  means :Def3: :: YELLOW_8:def 3
( not S is empty & S is closed & ( for S1, S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S ) );
end;

:: deftheorem Def3 defines irreducible YELLOW_8:def_3_:_
 for T being TopStruct
for S being Subset of T holds
( S is irreducible iff ( not S is empty & S is closed & ( for S1, S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S ) ) );

registration
let T be TopStruct ;
cluster irreducible  ->  non empty for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is irreducible holds
not b1 is empty by Def3;
end;

definition
let T be non empty TopSpace;
let S be Subset of T;
let p be Point of T;
predp is_dense_point_of S means :Def4: :: YELLOW_8:def 4
( p in S & S c= Cl {p} );
end;

:: deftheorem Def4 defines is_dense_point_of YELLOW_8:def_4_:_
 for T being non empty TopSpace
for S being Subset of T
for p being Point of T holds
( p is_dense_point_of S iff ( p in S & S c= Cl {p} ) );

theorem :: YELLOW_8:16
for T being non empty TopSpace
for S being Subset of T st S is closed holds
for p being Point of T st p is_dense_point_of S holds
S = Cl {p}
proof
let T be non empty TopSpace; ::_thesis: for S being Subset of T st S is closed holds
for p being Point of T st p is_dense_point_of S holds
S = Cl {p}
let S be Subset of T; ::_thesis: ( S is closed implies for p being Point of T st p is_dense_point_of S holds
S = Cl {p} )
assume A1: S is closed ; ::_thesis: for p being Point of T st p is_dense_point_of S holds
S = Cl {p}
let p be Point of T; ::_thesis: ( p is_dense_point_of S implies S = Cl {p} )
assume that
A2: p in S and
A3: S c= Cl {p} ; :: according to YELLOW_8:def_4 ::_thesis: S = Cl {p}
 {p} c= S by A2, ZFMISC_1:31;
then  Cl {p} c= S by A1, TOPS_1:5;
hence  S = Cl {p} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th17: :: YELLOW_8:17
for T being non empty TopSpace
for p being Point of T holds Cl {p} is irreducible
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds Cl {p} is irreducible
let p be Point of T; ::_thesis: Cl {p} is irreducible
assume A1: not Cl {p} is irreducible ; ::_thesis: contradiction
 not Cl {p} is empty by PCOMPS_1:2;
then consider S1, S2 being Subset of T such that
A2: ( S1 is closed & S2 is closed ) and
A3: Cl {p} = S1 \/ S2 and
A4: ( S1 <> Cl {p} & S2 <> Cl {p} ) by A1, Def3;
 ( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def_1;
then  ( p in S1 or p in S2 ) by A3, XBOOLE_0:def_3;
then  ( {p} c= S1 or {p} c= S2 ) by ZFMISC_1:31;
then A5: ( Cl {p} c= S1 or Cl {p} c= S2 ) by A2, TOPS_1:5;
 ( S1 c= Cl {p} & S2 c= Cl {p} ) by A3, XBOOLE_1:7;
hence  contradiction by A4, A5, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster irreducible for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st b1 is irreducible
proof
set p = the Point of T;
 Cl { the Point of T} is irreducible by Th17;
hence  ex b1 being Subset of T st b1 is irreducible ; ::_thesis: verum
end;
end;

definition
let T be non empty TopSpace;
attrT is sober  means :Def5: :: YELLOW_8:def 5
 for S being irreducible Subset of T ex p being Point of T st
( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
p = q ) );
end;

:: deftheorem Def5 defines sober YELLOW_8:def_5_:_
 for T being non empty TopSpace holds
( T is sober iff for S being irreducible Subset of T ex p being Point of T st
( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
p = q ) ) );

theorem Th18: :: YELLOW_8:18
for T being non empty TopSpace
for p being Point of T holds p is_dense_point_of Cl {p}
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds p is_dense_point_of Cl {p}
let p be Point of T; ::_thesis: p is_dense_point_of Cl {p}
 ( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def_1;
hence  p in Cl {p} ; :: according to YELLOW_8:def_4 ::_thesis: Cl {p} c= Cl {p}
thus  Cl {p} c= Cl {p} ; ::_thesis: verum
end;

theorem Th19: :: YELLOW_8:19
for T being non empty TopSpace
for p being Point of T holds p is_dense_point_of {p}
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds p is_dense_point_of {p}
let p be Point of T; ::_thesis: p is_dense_point_of {p}
thus  p in {p} by TARSKI:def_1; :: according to YELLOW_8:def_4 ::_thesis: {p} c= Cl {p}
thus  {p} c= Cl {p} by PRE_TOPC:18; ::_thesis: verum
end;

theorem Th20: :: YELLOW_8:20
for T being non empty TopSpace
for G, F being Subset of T st G is open & F is closed holds
F \ G is closed
proof
let T be non empty TopSpace; ::_thesis: for G, F being Subset of T st G is open & F is closed holds
F \ G is closed
let G, F be Subset of T; ::_thesis: ( G is open & F is closed implies F \ G is closed )
assume A1: ( G is open & F is closed ) ; ::_thesis: F \ G is closed
 F \ G = F /\ (G `) by SUBSET_1:13;
hence  F \ G is closed by A1; ::_thesis: verum
end;

theorem Th21: :: YELLOW_8:21
for T being non empty Hausdorff TopSpace
for S being irreducible Subset of T holds S is trivial
proof
let T be non empty Hausdorff TopSpace; ::_thesis: for S being irreducible Subset of T holds S is trivial
let S be irreducible Subset of T; ::_thesis: S is trivial
assume  not S is trivial ; ::_thesis: contradiction
then consider x, y being Point of T such that
A1: ( x in S & y in S ) and
A2: x <> y by SUBSET_1:45;
consider W, V being Subset of T such that
A3: ( W is open & V is open ) and
A4: ( x in W & y in V ) and
A5: W misses V by A2, PRE_TOPC:def_10;
set S1 = S \ W;
set S2 = S \ V;
A6: ( S \ W <> S & S \ V <> S ) by A4, A1, XBOOLE_0:def_5;
 S is closed by Def3;
then A7: ( S \ W is closed & S \ V is closed ) by A3, Th20;
A8: W /\ V = {} by A5, XBOOLE_0:def_7;
(S \ W) \/ (S \ V) = S \ (W /\ V) by XBOOLE_1:54
.= S by A8 ;
hence  contradiction by A7, A6, Def3; ::_thesis: verum
end;

registration
let T be non empty Hausdorff TopSpace;
cluster irreducible  ->  trivial for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is irreducible holds
b1 is trivial by Th21;
end;

theorem Th22: :: YELLOW_8:22
for T being non empty Hausdorff TopSpace holds T is sober
proof
let T be non empty Hausdorff TopSpace; ::_thesis: T is sober
let S be irreducible Subset of T; :: according to YELLOW_8:def_5 ::_thesis: ex p being Point of T st
( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
p = q ) )
consider d being Element of S such that
A1: S = {d} by SUBSET_1:46;
reconsider d = d as Point of T ;
take  d ; ::_thesis: ( d is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
d = q ) )
thus  d is_dense_point_of S by A1, Th19; ::_thesis: for q being Point of T st q is_dense_point_of S holds
d = q
let p be Point of T; ::_thesis: ( p is_dense_point_of S implies d = p )
assume  p is_dense_point_of S ; ::_thesis: d = p
then  p in S by Def4;
hence  d = p by A1, TARSKI:def_1; ::_thesis: verum
end;

registration
cluster non empty TopSpace-like Hausdorff  ->  non empty sober for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is Hausdorff holds
b1 is sober by Th22;
end;

registration
cluster non empty TopSpace-like sober for TopStruct ;
existence
 ex b1 being non empty TopSpace st b1 is sober
proof
set T = the non empty Hausdorff TopSpace;
take  the non empty Hausdorff TopSpace ; ::_thesis: the non empty Hausdorff TopSpace is sober
thus  the non empty Hausdorff TopSpace is sober ; ::_thesis: verum
end;
end;

theorem Th23: :: YELLOW_8:23
for T being non empty TopSpace holds
( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds
p = q )
proof
let T be non empty TopSpace; ::_thesis: ( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds
p = q )
thus  ( T is T_0 implies for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ) by TSP_1:def_5; ::_thesis: ( ( for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ) implies T is T_0 )
assume  for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ; ::_thesis: T is T_0
then  for p, q being Point of T st p <> q holds
Cl {p} <> Cl {q} ;
hence  T is T_0 by TSP_1:def_5; ::_thesis: verum
end;

theorem Th24: :: YELLOW_8:24
for T being non empty sober TopSpace holds T is T_0
proof
let T be non empty sober TopSpace; ::_thesis: T is T_0
 for p, q being Point of T st Cl {p} = Cl {q} holds
p = q
proof
let p, q be Point of T; ::_thesis: ( Cl {p} = Cl {q} implies p = q )
assume A1: Cl {p} = Cl {q} ; ::_thesis: p = q
 Cl {p} is irreducible by Th17;
then consider r being Point of T such that
 r is_dense_point_of Cl {p} and
A2: for q being Point of T st q is_dense_point_of Cl {p} holds
r = q by Def5;
 p = r by A2, Th18;
hence  p = q by A1, A2, Th18; ::_thesis: verum
end;
hence  T is T_0 by Th23; ::_thesis: verum
end;

registration
cluster non empty TopSpace-like sober  ->  non empty T_0 for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is sober holds
b1 is T_0 by Th24;
end;

definition
let X be set ;
func CofinTop X ->  strict TopStruct  means :Def6: :: YELLOW_8:def 6
( the carrier of it = X & COMPLEMENT the topology of it = {X} \/ (Fin X) );
existence
 ex b1 being strict TopStruct st
( the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) )
proof
 ( {X} c= bool X & Fin X c= bool X ) by FINSUB_1:13, ZFMISC_1:68;
then reconsider F = {X} \/ (Fin X) as Subset-Family of X by XBOOLE_1:8;
reconsider F = F as Subset-Family of X ;
take T = TopStruct(# X,(COMPLEMENT F) #); ::_thesis: ( the carrier of T = X & COMPLEMENT the topology of T = {X} \/ (Fin X) )
thus  the carrier of T = X ; ::_thesis: COMPLEMENT the topology of T = {X} \/ (Fin X)
thus  COMPLEMENT the topology of T = {X} \/ (Fin X) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopStruct st the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) & the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) holds
b1 = b2 by SETFAM_1:38;
end;

:: deftheorem Def6 defines CofinTop YELLOW_8:def_6_:_
 for X being set
for b2 being strict TopStruct holds
( b2 = CofinTop X iff ( the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) ) );

registration
let X be non empty set ;
cluster CofinTop X ->  non empty strict ;
coherence
 not CofinTop X is empty by Def6;
end;

registration
let X be set ;
cluster CofinTop X ->  strict TopSpace-like ;
coherence
 CofinTop X is TopSpace-like
proof
reconsider F = Fin X as Subset-Family of X by FINSUB_1:13;
reconsider XX = {X} as Subset-Family of X by ZFMISC_1:68;
set IT = CofinTop X;
reconsider XX = XX as Subset-Family of X ;
reconsider F = F as Subset-Family of X ;
A1: the carrier of (CofinTop X) = X by Def6;
A2: COMPLEMENT the topology of (CofinTop X) = {X} \/ (Fin X) by Def6;
A3: the topology of (CofinTop X) = COMPLEMENT (COMPLEMENT the topology of (CofinTop X))
.= (COMPLEMENT XX) \/ (COMPLEMENT F) by A1, A2, SETFAM_1:39
.= {{}} \/ (COMPLEMENT F) by SETFAM_1:40 ;
 {}. X in F ;
then  (({} X) `) ` in F ;
then  [#] X in COMPLEMENT F by SETFAM_1:def_7;
hence  the carrier of (CofinTop X) in the topology of (CofinTop X) by A1, A3, XBOOLE_0:def_3; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of (CofinTop X)) holds
( not b1 c= the topology of (CofinTop X) or union b1 in the topology of (CofinTop X) ) ) & ( for b1, b2 being Element of bool the carrier of (CofinTop X) holds
( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) ) ) )
A4: {} in {{}} by TARSKI:def_1;
thus  for a being Subset-Family of (CofinTop X) st a c= the topology of (CofinTop X) holds
union a in the topology of (CofinTop X) ::_thesis: for b1, b2 being Element of bool the carrier of (CofinTop X) holds
( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) )
proof
let a be Subset-Family of (CofinTop X); ::_thesis: ( a c= the topology of (CofinTop X) implies union a in the topology of (CofinTop X) )
assume A5: a c= the topology of (CofinTop X) ; ::_thesis: union a in the topology of (CofinTop X)
set b = a /\ (COMPLEMENT F);
reconsider b = a /\ (COMPLEMENT F) as Subset-Family of X ;
reconsider b = b as Subset-Family of X ;
 a /\ {{}} c= {{}} by XBOOLE_1:17;
then  ( a /\ {{}} = {{}} or a /\ {{}} = {} ) by ZFMISC_1:33;
then A6: union (a /\ {{}}) = {} by ZFMISC_1:2, ZFMISC_1:25;
A7: union a = union (a /\ the topology of (CofinTop X)) by A5, XBOOLE_1:28
.= union ((a /\ {{}}) \/ (a /\ (COMPLEMENT F))) by A3, XBOOLE_1:23
.= (union (a /\ {{}})) \/ (union (a /\ (COMPLEMENT F))) by ZFMISC_1:78
.= union b by A6 ;
percases ( b = {} or b <> {} ) ;
suppose b = {} ; ::_thesis: union a in the topology of (CofinTop X)
hence  union a in the topology of (CofinTop X) by A3, A4, A7, XBOOLE_0:def_3, ZFMISC_1:2; ::_thesis: verum
end;
supposeA8: b <> {} ; ::_thesis: union a in the topology of (CofinTop X)
 b c= COMPLEMENT F by XBOOLE_1:17;
then A9: COMPLEMENT b c= Fin X by SETFAM_1:37;
meet (COMPLEMENT b) = ([#] X) \ (union b) by A8, SETFAM_1:33
.= (union b) ` ;
then  (union b) ` in Fin X by A9, Th2;
then  union b in COMPLEMENT F by SETFAM_1:def_7;
hence  union a in the topology of (CofinTop X) by A3, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let a, b be Subset of (CofinTop X); ::_thesis: ( not a in the topology of (CofinTop X) or not b in the topology of (CofinTop X) or a /\ b in the topology of (CofinTop X) )
assume that
A10: a in the topology of (CofinTop X) and
A11: b in the topology of (CofinTop X) ; ::_thesis: a /\ b in the topology of (CofinTop X)
reconsider a9 = a, b9 = b as Subset of X by Def6;
percases ( a = {} or b = {} or ( a <> {} & b <> {} ) ) ;
suppose ( a = {} or b = {} ) ; ::_thesis: a /\ b in the topology of (CofinTop X)
hence  a /\ b in the topology of (CofinTop X) by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA12: ( a <> {} & b <> {} ) ; ::_thesis: a /\ b in the topology of (CofinTop X)
then  not b in {{}} by TARSKI:def_1;
then  b9 in COMPLEMENT F by A3, A11, XBOOLE_0:def_3;
then A13: b9 ` in Fin X by SETFAM_1:def_7;
 not a in {{}} by A12, TARSKI:def_1;
then  a9 in COMPLEMENT F by A3, A10, XBOOLE_0:def_3;
then  a9 ` in Fin X by SETFAM_1:def_7;
then  (a9 `) \/ (b9 `) in Fin X by A13, FINSUB_1:1;
then  (a9 /\ b9) ` in Fin X by XBOOLE_1:54;
then  a /\ b in COMPLEMENT F by SETFAM_1:def_7;
hence  a /\ b in the topology of (CofinTop X) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;

theorem Th25: :: YELLOW_8:25
for X being non empty set
for P being Subset of (CofinTop X) holds
( P is closed iff ( P = X or P is finite ) )
proof
let X be non empty set ; ::_thesis: for P being Subset of (CofinTop X) holds
( P is closed iff ( P = X or P is finite ) )
let P be Subset of (CofinTop X); ::_thesis: ( P is closed iff ( P = X or P is finite ) )
set T = CofinTop X;
hereby  ::_thesis: ( ( P = X or P is finite ) implies P is closed )
assume that
A1: P is closed and
A2: P <> X ; ::_thesis: P is finite
 P ` in the topology of (CofinTop X) by A1, PRE_TOPC:def_2;
then  P in COMPLEMENT the topology of (CofinTop X) by SETFAM_1:def_7;
then A3: P in {X} \/ (Fin X) by Def6;
 not P in {X} by A2, TARSKI:def_1;
then  P in Fin X by A3, XBOOLE_0:def_3;
hence  P is finite ; ::_thesis: verum
end;
assume A4: ( P = X or P is finite ) ; ::_thesis: P is closed
 the carrier of (CofinTop X) = X by Def6;
then  ( P in {X} or P in Fin X ) by A4, FINSUB_1:def_5, TARSKI:def_1;
then  P in {X} \/ (Fin X) by XBOOLE_0:def_3;
then  P in COMPLEMENT the topology of (CofinTop X) by Def6;
then  P ` in the topology of (CofinTop X) by SETFAM_1:def_7;
then  P ` is open by PRE_TOPC:def_2;
hence  P is closed by TOPS_1:3; ::_thesis: verum
end;

theorem Th26: :: YELLOW_8:26
for T being non empty TopSpace st T is T_1 holds
for p being Point of T holds Cl {p} = {p}
proof
let T be non empty TopSpace; ::_thesis: ( T is T_1 implies for p being Point of T holds Cl {p} = {p} )
assume A1: T is T_1 ; ::_thesis: for p being Point of T holds Cl {p} = {p}
let p be Point of T; ::_thesis: Cl {p} = {p}
 {p} is closed by A1, URYSOHN1:19;
then A2: Cl {p} c= {p} by TOPS_1:5;
 {p} c= Cl {p} by PRE_TOPC:18;
hence  Cl {p} = {p} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let X be non empty set ;
cluster CofinTop X ->  strict T_1 ;
coherence
 CofinTop X is T_1
proof
 for p being Point of (CofinTop X) holds {p} is closed by Th25;
hence  CofinTop X is T_1 by URYSOHN1:19; ::_thesis: verum
end;
end;

registration
let X be infinite set ;
cluster CofinTop X ->  strict non sober ;
coherence
 not CofinTop X is sober
proof
set T = CofinTop X;
reconsider S = [#] X as Subset of (CofinTop X) by Def6;
 S is irreducible
proof
 X = [#] (CofinTop X) by Def6;
hence  ( not S is empty & S is closed ) ; :: according to YELLOW_8:def_3 ::_thesis: for S1, S2 being Subset of (CofinTop X) st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S
let S1, S2 be Subset of (CofinTop X); ::_thesis: ( S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S implies S2 = S )
assume that
A1: ( S1 is closed & S2 is closed ) and
A2: S = S1 \/ S2 ; ::_thesis: ( S1 = S or S2 = S )
assume  ( S1 <> S & S2 <> S ) ; ::_thesis: contradiction
then reconsider S19 = S1, S29 = S2 as finite set by A1, Th25;
 S = S19 \/ S29 by A2;
hence  contradiction ; ::_thesis: verum
end;
then reconsider S = S as irreducible Subset of (CofinTop X) ;
take  S ; :: according to YELLOW_8:def_5 ::_thesis: for p being Point of (CofinTop X) holds
( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) )
let p be Point of (CofinTop X); ::_thesis: ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) )
now__::_thesis:_not_p_is_dense_point_of_S
assume  p is_dense_point_of S ; ::_thesis: contradiction
then  S c= Cl {p} by Def4;
then  Cl {p} is infinite ;
hence  contradiction by Th26; ::_thesis: verum
end;
hence  ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) ) ; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like T_1 non sober for TopStruct ;
existence
 ex b1 being non empty TopSpace st
( b1 is T_1 & not b1 is sober )
proof
set X = the infinite set ;
take  CofinTop the infinite set ; ::_thesis: ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober )
thus  ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober ) ; ::_thesis: verum
end;
end;

begin

theorem Th27: :: YELLOW_8:27
for T being non empty TopSpace holds
( T is regular iff for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) )
proof
let T be non empty TopSpace; ::_thesis: ( T is regular iff for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) )
hereby  ::_thesis: ( ( for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) ) implies T is regular )
assume A1: T is regular ; ::_thesis: for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Element of bool the carrier of T st
( b5 is closed & b5 c= b4 & Q in Int b5 )
let p be Point of T; ::_thesis: for P being Subset of T st p in Int P holds
ex Q being Element of bool the carrier of T st
( b4 is closed & b4 c= b3 & Q in Int b4 )
let P be Subset of T; ::_thesis: ( p in Int P implies ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 ) )
assume  p in Int P ; ::_thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )
then A2: p in ((Int P) `) ` ;
percases ( P = [#] T or P <> [#] T ) ;
supposeA3: P = [#] T ; ::_thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )
take Q = [#] T; ::_thesis: ( Q is closed & Q c= P & p in Int Q )
thus  Q is closed ; ::_thesis: ( Q c= P & p in Int Q )
thus  Q c= P by A3; ::_thesis: p in Int Q
 Int Q = Q by TOPS_1:15;
hence  p in Int Q ; ::_thesis: verum
end;
supposeA4: P <> [#] T ; ::_thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )
now__::_thesis:_not_(Int_P)_`_=_{}
assume  (Int P) ` = {} ; ::_thesis: contradiction
then  ((Int P) `) ` = [#] T ;
then  [#] T c= P by TOPS_1:16;
hence  contradiction by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
then consider W, V being Subset of T such that
A5: W is open and
A6: V is open and
A7: p in W and
A8: (Int P) ` c= V and
A9: W misses V by A1, A2, COMPTS_1:def_2;
A10: Int P c= P by TOPS_1:16;
take Q = V ` ; ::_thesis: ( Q is closed & Q c= P & p in Int Q )
thus  Q is closed by A6; ::_thesis: ( Q c= P & p in Int Q )
 (Int P) ` c= Q ` by A8;
then  Q c= Int P by SUBSET_1:12;
hence  Q c= P by A10, XBOOLE_1:1; ::_thesis: p in Int Q
 W c= Q by A9, SUBSET_1:23;
then  W c= Int Q by A5, TOPS_1:24;
hence  p in Int Q by A7; ::_thesis: verum
end;
end;
end;
assume A11: for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) ; ::_thesis: T is regular
let p be Point of T; :: according to COMPTS_1:def_2 ::_thesis: for b1 being Element of bool the carrier of T holds
( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )
let P be Subset of T; ::_thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )
assume that
 P <> {} and
A12: ( P is closed & p in P ` ) ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
 p in Int (P `) by A12, TOPS_1:23;
then consider Q being Subset of T such that
A13: Q is closed and
A14: Q c= P ` and
A15: p in Int Q by A11;
reconsider W = Int Q as Subset of T ;
take  W ; ::_thesis: ex b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & P c= b1 & W misses b1 )
take V = Q ` ; ::_thesis: ( W is open & V is open & p in W & P c= V & W misses V )
thus  W is open ; ::_thesis: ( V is open & p in W & P c= V & W misses V )
thus  V is open by A13; ::_thesis: ( p in W & P c= V & W misses V )
thus  p in W by A15; ::_thesis: ( P c= V & W misses V )
 (P `) ` c= V by A14, SUBSET_1:12;
hence  P c= V ; ::_thesis: W misses V
 Q misses V by XBOOLE_1:79;
hence  W misses V by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum
end;

theorem :: YELLOW_8:28
for T being non empty TopSpace st T is regular holds
( T is locally-compact iff for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) )
proof
let T be non empty TopSpace; ::_thesis: ( T is regular implies ( T is locally-compact iff for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ) )
assume A1: T is regular ; ::_thesis: ( T is locally-compact iff for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) )
hereby  ::_thesis: ( ( for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ) implies T is locally-compact )
assume A2: T is locally-compact ; ::_thesis: for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact )
let x be Point of T; ::_thesis: ex Y being Subset of T st
( x in Int Y & Y is compact )
 ex Y being Subset of T st
( x in Int Y & Y c= [#] T & Y is compact ) by A2, WAYBEL_3:def_9;
hence  ex Y being Subset of T st
( x in Int Y & Y is compact ) ; ::_thesis: verum
end;
assume A3: for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ; ::_thesis: T is locally-compact
let x be Point of T; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of bool the carrier of T holds
( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of T st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let X be Subset of T; ::_thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of T st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume  ( x in X & X is open ) ; ::_thesis: ex b1 being Element of bool the carrier of T st
( x in Int b1 & b1 c= X & b1 is compact )
then A4: x in Int X by TOPS_1:23;
consider Y being Subset of T such that
A5: x in Int Y and
A6: Y is compact by A3;
 x in (Int X) /\ (Int Y) by A5, A4, XBOOLE_0:def_4;
then  x in Int (X /\ Y) by TOPS_1:17;
then consider Q being Subset of T such that
A7: Q is closed and
A8: Q c= X /\ Y and
A9: x in Int Q by A1, Th27;
take  Q ; ::_thesis: ( x in Int Q & Q c= X & Q is compact )
thus  x in Int Q by A9; ::_thesis: ( Q c= X & Q is compact )
 X /\ Y c= X by XBOOLE_1:17;
hence  Q c= X by A8, XBOOLE_1:1; ::_thesis: Q is compact
 X /\ Y c= Y by XBOOLE_1:17;
hence  Q is compact by A6, A7, A8, COMPTS_1:9, XBOOLE_1:1; ::_thesis: verum
end;