:: On the {B}orel Families of Subsets of Topological Spaces
:: by Adam Grabowski
::
:: Received August 30, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

definition
let T be 1-sorted ;
func TotFam T ->  Subset-Family of T equals :: TOPGEN_4:def 1
 bool the carrier of T;
coherence
 bool the carrier of T is Subset-Family of T by ZFMISC_1:def_1;
end;

:: deftheorem  defines TotFam TOPGEN_4:def_1_:_
 for T being 1-sorted holds TotFam T = bool the carrier of T;

theorem Th1: :: TOPGEN_4:1
for T being set
for F being Subset-Family of T holds
( F is countable iff COMPLEMENT F is countable )
proofend;

registration
cluster RAT  ->  countable ;
coherence
 RAT is countable by CARD_3:def_14, TOPGEN_3:17;
end;

Lm1:  for X being set holds
( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
proofend;

scheme :: TOPGEN_4:sch 1
FraenCoun11{ P1[ set ] } :
  {  {n} where n is Element of RAT : P1[n]  }  is countable
proofend;

theorem :: TOPGEN_4:2
for T being non empty TopSpace
for A being Subset of T holds Der A =  {  x where x is Point of T : x in Cl (A \ {x})  }
proofend;

registration
cluster finite  ->  second-countable for TopStruct ;
coherence
 for b1 being TopStruct st b1 is finite holds
b1 is second-countable
proofend;
end;

registration
cluster REAL  ->  non countable ;
coherence
 not REAL is countable
proofend;
end;

registration
cluster non countable  ->  non finite for set ;
coherence
 for b1 being set st not b1 is countable holds
not b1 is finite ;
cluster non finite  ->  non trivial for set ;
coherence
 for b1 being set st not b1 is finite holds
not b1 is trivial ;
cluster non empty non countable for set ;
existence
 ex b1 being set st
( not b1 is countable & not b1 is empty )
proofend;
end;

theorem :: TOPGEN_4:3
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff Der A c= A )
proofend;

theorem Th4: :: TOPGEN_4:4
for T being non empty TopStruct
for B being Basis of T
for V being Subset of T st V is open &amp; V <> {} holds
ex W being Subset of T st
( W in B &amp; W c= V &amp; W <> {} )
proofend;

begin

:: 1.3.7. Theorem
theorem Th5: :: TOPGEN_4:5
for T being non empty TopSpace holds density T c= weight T
proofend;

theorem :: TOPGEN_4:6
for T being non empty TopSpace holds
( T is separable iff ex A being Subset of T st
( A is dense &amp; A is countable ) )
proofend;

:: 1.3.8. Corollary
theorem Th7: :: TOPGEN_4:7
for T being non empty TopSpace st T is second-countable holds
T is separable
proofend;

registration
cluster non empty TopSpace-like second-countable  ->  non empty separable for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is second-countable holds
b1 is separable by Th7;
end;

:: Exercises
theorem :: TOPGEN_4:8
for T being non empty TopSpace
for A, B being Subset of T st A,B are_separated holds
Fr (A \/ B) = (Fr A) \/ (Fr B)
proofend;

:: Exercise 1.3.B.
theorem :: TOPGEN_4:9
for T being non empty TopSpace
for F being Subset-Family of T st F is locally_finite holds
Fr (union F) c= union (Fr F)
proofend;

theorem Th10: :: TOPGEN_4:10
for T being non empty discrete TopSpace holds
( T is separable iff card ([#] T) c= omega )
proofend;

theorem :: TOPGEN_4:11
for T being non empty discrete TopSpace holds
( T is separable iff T is countable )
proofend;

begin

definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attrF is all-open-containing  means :Def2: :: TOPGEN_4:def 2
 for A being Subset of T st A is open holds
A in F;
end;

:: deftheorem Def2 defines all-open-containing TOPGEN_4:def_2_:_
 for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-open-containing iff for A being Subset of T st A is open holds
A in F );

definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attrF is all-closed-containing  means :Def3: :: TOPGEN_4:def 3
 for A being Subset of T st A is closed holds
A in F;
end;

:: deftheorem Def3 defines all-closed-containing TOPGEN_4:def_3_:_
 for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-closed-containing iff for A being Subset of T st A is closed holds
A in F );

definition
let T be set ;
let F be Subset-Family of T;
attrF is closed_for_countable_unions  means :Def4: :: TOPGEN_4:def 4
 for G being countable Subset-Family of T st G c= F holds
union G in F;
end;

:: deftheorem Def4 defines closed_for_countable_unions TOPGEN_4:def_4_:_
 for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_unions iff for G being countable Subset-Family of T st G c= F holds
union G in F );

Lm2:  for T being set
for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
proofend;

registration
let T be set ;
cluster non empty compl-closed sigma-multiplicative  ->  closed_for_countable_unions for Element of bool (bool T);
coherence
 for b1 being SigmaField of T holds b1 is closed_for_countable_unions by Lm2;
end;

theorem Th12: :: TOPGEN_4:12
for T being set
for F being Subset-Family of T st F is closed_for_countable_unions holds
{} in F
proofend;

registration
let T be set ;
cluster closed_for_countable_unions  ->  non empty for Element of bool (bool T);
coherence
 for b1 being Subset-Family of T st b1 is closed_for_countable_unions holds
not b1 is empty by Th12;
end;

theorem Th13: :: TOPGEN_4:13
for T being set
for F being Subset-Family of T holds
( F is SigmaField of T iff ( F is compl-closed &amp; F is closed_for_countable_unions ) )
proofend;

definition
let T be set ;
let F be Subset-Family of T;
attrF is closed_for_countable_meets  means :Def5: :: TOPGEN_4:def 5
 for G being countable Subset-Family of T st G c= F holds
meet G in F;
end;

:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def_5_:_
 for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_meets iff for G being countable Subset-Family of T st G c= F holds
meet G in F );

theorem Th14: :: TOPGEN_4:14
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-closed-containing &amp; F is compl-closed iff ( F is all-open-containing &amp; F is compl-closed ) )
proofend;

theorem :: TOPGEN_4:15
for T being set
for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F
proofend;

theorem Th16: :: TOPGEN_4:16
for T being set
for F, G being Subset-Family of T st F c= G &amp; G is compl-closed holds
COMPLEMENT F c= G
proofend;

theorem Th17: :: TOPGEN_4:17
for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_meets &amp; F is compl-closed iff ( F is closed_for_countable_unions &amp; F is compl-closed ) )
proofend;

registration
let T be non empty TopSpace;
cluster compl-closed all-open-containing closed_for_countable_unions  ->  all-closed-containing closed_for_countable_meets for Element of bool (bool the carrier of T);
coherence
 for b1 being Subset-Family of T st b1 is all-open-containing &amp; b1 is compl-closed &amp; b1 is closed_for_countable_unions holds
( b1 is all-closed-containing &amp; b1 is closed_for_countable_meets ) by Th14, Th17;
cluster compl-closed all-closed-containing closed_for_countable_meets  ->  all-open-containing closed_for_countable_unions for Element of bool (bool the carrier of T);
coherence
 for b1 being Subset-Family of T st b1 is all-closed-containing &amp; b1 is compl-closed &amp; b1 is closed_for_countable_meets holds
( b1 is all-open-containing &amp; b1 is closed_for_countable_unions ) by Th14, Th17;
end;

begin

registration
let T be set ;
let F be countable Subset-Family of T;
cluster COMPLEMENT F ->  countable ;
coherence
 COMPLEMENT F is countable by Th1;
end;

registration
let T be TopSpace;
cluster empty  ->  open closed for Element of bool (bool the carrier of T);
coherence
 for b1 being Subset-Family of T st b1 is empty holds
( b1 is open &amp; b1 is closed )
proofend;
end;

registration
let T be TopSpace;
cluster countable open closed for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is countable &amp; b1 is open &amp; b1 is closed )
proofend;
end;

theorem Th18: :: TOPGEN_4:18
for T being set holds {} is empty Subset-Family of T
proofend;

registration
cluster empty  ->  countable for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is countable ;
end;

begin

theorem Th19: :: TOPGEN_4:19
for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
proofend;

theorem Th20: :: TOPGEN_4:20
for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )
proofend;

definition
let T be set ;
let F, G be Subset-Family of T;
:: original:INTERSECTION
redefine func INTERSECTION (F,G) ->  Subset-Family of T;
coherence
 INTERSECTION (F,G) is Subset-Family of T
proofend;
:: original:UNION
redefine func UNION (F,G) ->  Subset-Family of T;
coherence
 UNION (F,G) is Subset-Family of T
proofend;
end;

theorem Th21: :: TOPGEN_4:21
for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed &amp; G is closed holds
INTERSECTION (F,G) is closed
proofend;

theorem Th22: :: TOPGEN_4:22
for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed &amp; G is closed holds
UNION (F,G) is closed
proofend;

theorem Th23: :: TOPGEN_4:23
for T being non empty TopSpace
for F, G being Subset-Family of T st F is open &amp; G is open holds
INTERSECTION (F,G) is open
proofend;

theorem Th24: :: TOPGEN_4:24
for T being non empty TopSpace
for F, G being Subset-Family of T st F is open &amp; G is open holds
UNION (F,G) is open
proofend;

theorem Th25: :: TOPGEN_4:25
for T being set
for F, G being Subset-Family of T holds card (INTERSECTION (F,G)) c= card [:F,G:]
proofend;

theorem Th26: :: TOPGEN_4:26
for T being set
for F, G being Subset-Family of T holds card (UNION (F,G)) c= card [:F,G:]
proofend;

theorem Th27: :: TOPGEN_4:27
for F, G being set holds union (UNION (F,G)) c= (union F) \/ (union G)
proofend;

theorem Th28: :: TOPGEN_4:28
for F, G being set st F <> {} &amp; G <> {} holds
(union F) \/ (union G) = union (UNION (F,G))
proofend;

theorem Th29: :: TOPGEN_4:29
for F being set holds UNION ({},F) = {}
proofend;

theorem :: TOPGEN_4:30
for F, G being set holds
( not UNION (F,G) = {} or F = {} or G = {} )
proofend;

theorem :: TOPGEN_4:31
for F, G being set holds
( not INTERSECTION (F,G) = {} or F = {} or G = {} )
proofend;

theorem Th32: :: TOPGEN_4:32
for F, G being set holds meet (UNION (F,G)) c= (meet F) \/ (meet G)
proofend;

theorem :: TOPGEN_4:33
for F, G being set st F <> {} &amp; G <> {} holds
meet (UNION (F,G)) = (meet F) \/ (meet G)
proofend;

theorem Th34: :: TOPGEN_4:34
for F, G being set st F <> {} &amp; G <> {} holds
(meet F) /\ (meet G) = meet (INTERSECTION (F,G))
proofend;

begin

definition
let T be TopSpace;
let A be Subset of T;
attrA is F_sigma  means :Def6: :: TOPGEN_4:def 6
 ex F being countable closed Subset-Family of T st A = union F;
end;

:: deftheorem Def6 defines F_sigma TOPGEN_4:def_6_:_
 for T being TopSpace
for A being Subset of T holds
( A is F_sigma iff ex F being countable closed Subset-Family of T st A = union F );

definition
let T be TopSpace;
let A be Subset of T;
attrA is G_delta  means :Def7: :: TOPGEN_4:def 7
 ex F being countable open Subset-Family of T st A = meet F;
end;

:: deftheorem Def7 defines G_delta TOPGEN_4:def_7_:_
 for T being TopSpace
for A being Subset of T holds
( A is G_delta iff ex F being countable open Subset-Family of T st A = meet F );

registration
let T be non empty TopSpace;
cluster empty  ->  F_sigma G_delta for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is empty holds
( b1 is F_sigma &amp; b1 is G_delta )
proofend;
end;

theorem Th35: :: TOPGEN_4:35
for T being non empty TopSpace holds [#] T is F_sigma
proofend;

theorem Th36: :: TOPGEN_4:36
for T being non empty TopSpace holds [#] T is G_delta
proofend;

registration
let T be non empty TopSpace;
cluster [#] T ->  F_sigma G_delta ;
coherence
 ( [#] T is F_sigma &amp; [#] T is G_delta ) by Th35, Th36;
end;

theorem :: TOPGEN_4:37
for T being non empty TopSpace
for A being Subset of T st A is F_sigma holds
A ` is G_delta
proofend;

theorem :: TOPGEN_4:38
for T being non empty TopSpace
for A being Subset of T st A is G_delta holds
A ` is F_sigma
proofend;

theorem :: TOPGEN_4:39
for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma &amp; B is F_sigma holds
A /\ B is F_sigma
proofend;

theorem :: TOPGEN_4:40
for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma &amp; B is F_sigma holds
A \/ B is F_sigma
proofend;

theorem :: TOPGEN_4:41
for T being non empty TopSpace
for A, B being Subset of T st A is G_delta &amp; B is G_delta holds
A \/ B is G_delta
proofend;

theorem :: TOPGEN_4:42
for T being non empty TopSpace
for A, B being Subset of T st A is G_delta &amp; B is G_delta holds
A /\ B is G_delta
proofend;

theorem :: TOPGEN_4:43
for T being non empty TopSpace
for A being Subset of T st A is closed holds
A is F_sigma
proofend;

theorem :: TOPGEN_4:44
for T being non empty TopSpace
for A being Subset of T st A is open holds
A is G_delta
proofend;

theorem :: TOPGEN_4:45
for A being Subset of R^1 st A = RAT holds
A is F_sigma
proofend;

begin

definition
let T be TopSpace;
attrT is T_1/2  means :Def8: :: TOPGEN_4:def 8
 for A being Subset of T holds Der A is closed ;
end;

:: deftheorem Def8 defines T_1/2 TOPGEN_4:def_8_:_
 for T being TopSpace holds
( T is T_1/2 iff for A being Subset of T holds Der A is closed );

theorem Th46: :: TOPGEN_4:46
for T being TopSpace st T is T_1 holds
T is T_1/2
proofend;

theorem Th47: :: TOPGEN_4:47
for T being non empty TopSpace st T is T_1/2 holds
T is T_0
proofend;

registration
cluster TopSpace-like T_1/2  ->  T_0 for TopStruct ;
coherence
 for b1 being TopSpace st b1 is T_1/2 holds
b1 is T_0
proofend;
cluster TopSpace-like T_1  ->  T_1/2 for TopStruct ;
coherence
 for b1 being TopSpace st b1 is T_1 holds
b1 is T_1/2 by Th46;
end;

begin

:: Page 77 - 1.7.11
definition
let T be non empty TopSpace;
let A be Subset of T;
let x be Point of T;
predx is_a_condensation_point_of A means :Def9: :: TOPGEN_4:def 9
 for N being a_neighborhood of x holds not N /\ A is countable ;
end;

:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def_9_:_
 for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x is_a_condensation_point_of A iff for N being a_neighborhood of x holds not N /\ A is countable );

theorem Th48: :: TOPGEN_4:48
for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T st x is_a_condensation_point_of A &amp; A c= B holds
x is_a_condensation_point_of B
proofend;

definition
let T be non empty TopSpace;
let A be Subset of T;
funcA ^0  ->  Subset of T means :Def10: :: TOPGEN_4:def 10
 for x being Point of T holds
( x in it iff x is_a_condensation_point_of A );
existence
 ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff x is_a_condensation_point_of A )
proofend;
uniqueness
 for b1, b2 being Subset of T st ( for x being Point of T holds
( x in b1 iff x is_a_condensation_point_of A ) ) &amp; ( for x being Point of T holds
( x in b2 iff x is_a_condensation_point_of A ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines ^0 TOPGEN_4:def_10_:_
 for T being non empty TopSpace
for A, b3 being Subset of T holds
( b3 = A ^0 iff for x being Point of T holds
( x in b3 iff x is_a_condensation_point_of A ) );

theorem Th49: :: TOPGEN_4:49
for T being non empty TopSpace
for A being Subset of T
for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
proofend;

theorem :: TOPGEN_4:50
for T being non empty TopSpace
for A being Subset of T holds A ^0 c= Der A
proofend;

theorem :: TOPGEN_4:51
for T being non empty TopSpace
for A being Subset of T holds A ^0 = Cl (A ^0)
proofend;

theorem Th52: :: TOPGEN_4:52
for T being non empty TopSpace
for A, B being Subset of T st A c= B holds
A ^0 c= B ^0
proofend;

theorem Th53: :: TOPGEN_4:53
for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
proofend;

theorem :: TOPGEN_4:54
for T being non empty TopSpace
for A, B being Subset of T holds (A \/ B) ^0 = (A ^0) \/ (B ^0)
proofend;

theorem Th55: :: TOPGEN_4:55
for T being non empty TopSpace
for A being Subset of T st A is countable holds
for x being Point of T holds not x is_a_condensation_point_of A
proofend;

theorem Th56: :: TOPGEN_4:56
for T being non empty TopSpace
for A being Subset of T st A is countable holds
A ^0 = {}
proofend;

registration
let T be non empty TopSpace;
let A be countable Subset of T;
clusterA ^0  ->  empty ;
coherence
 A ^0 is empty by Th56;
end;

theorem :: TOPGEN_4:57
for T being non empty TopSpace st T is second-countable holds
ex B being Basis of T st B is countable
proofend;

registration
cluster non empty TopSpace-like second-countable for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is second-countable &amp; not b1 is empty )
proofend;
end;

begin

registration
let T be non empty TopSpace;
cluster TotFam T ->  non empty compl-closed all-open-containing closed_for_countable_unions ;
coherence
 ( not TotFam T is empty &amp; TotFam T is all-open-containing &amp; TotFam T is compl-closed &amp; TotFam T is closed_for_countable_unions )
proofend;
end;

theorem :: TOPGEN_4:58
for T being set
for A being SetSequence of T holds rng A is non empty countable Subset-Family of T
proofend;

theorem Th59: :: TOPGEN_4:59
for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-open-containing &amp; F c= G holds
G is all-open-containing
proofend;

theorem :: TOPGEN_4:60
for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-closed-containing &amp; F c= G holds
G is all-closed-containing
proofend;

definition
let T be 1-sorted ;
mode SigmaField of T is SigmaField of the carrier of T;
end;

registration
let T be non empty TopSpace;
cluster compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is compl-closed &amp; b1 is closed_for_countable_unions &amp; b1 is closed_for_countable_meets &amp; b1 is all-closed-containing &amp; b1 is all-open-containing )
proofend;
end;

theorem Th61: :: TOPGEN_4:61
for T being non empty TopSpace holds
( sigma (TotFam T) is all-open-containing &amp; sigma (TotFam T) is compl-closed &amp; sigma (TotFam T) is closed_for_countable_unions )
proofend;

registration
let T be non empty TopSpace;
cluster sigma (TotFam T) ->  all-open-containing closed_for_countable_unions ;
coherence
 ( sigma (TotFam T) is all-open-containing &amp; sigma (TotFam T) is compl-closed &amp; sigma (TotFam T) is closed_for_countable_unions ) by Th61;
end;

registration
let T be non empty 1-sorted ;
cluster non empty compl-closed sigma-additive closed_for_countable_unions for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is sigma-additive &amp; b1 is compl-closed &amp; b1 is closed_for_countable_unions &amp; not b1 is empty )
proofend;
end;

registration
let T be non empty TopSpace;
cluster non empty compl-closed sigma-multiplicative  ->  closed_for_countable_unions for Element of bool (bool the carrier of T);
coherence
 for b1 being SigmaField of T holds b1 is closed_for_countable_unions ;
end;

theorem :: TOPGEN_4:62
for T being non empty TopSpace
for F being Subset-Family of T st F is compl-closed &amp; F is closed_for_countable_unions holds
F is SigmaField of T by Th13;

registration
let T be non empty TopSpace;
cluster non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive all-open-containing closed_for_countable_unions for Element of bool (bool the carrier of T);
existence
 ex b1 being SigmaField of T st b1 is all-open-containing
proofend;
end;

registration
let T be non empty TopSpace;
cluster Topology_of T ->  open all-open-containing ;
coherence
 ( Topology_of T is open &amp; Topology_of T is all-open-containing )
proofend;
end;

theorem Th63: :: TOPGEN_4:63
for T being non empty TopSpace
for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y &amp; ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
proofend;

definition
let T be non empty TopSpace;
func BorelSets T ->  compl-closed all-open-containing closed_for_countable_unions Subset-Family of T means :Def11: :: TOPGEN_4:def 11
 for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds it c= G;
existence
 ex b1 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b1 c= G
proofend;
uniqueness
 for b1, b2 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b1 c= G ) &amp; ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b2 c= G ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines BorelSets TOPGEN_4:def_11_:_
 for T being non empty TopSpace
for b2 being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds
( b2 = BorelSets T iff for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b2 c= G );

theorem Th64: :: TOPGEN_4:64
for T being non empty TopSpace
for F being closed Subset-Family of T holds F c= BorelSets T
proofend;

theorem Th65: :: TOPGEN_4:65
for T being non empty TopSpace
for F being open Subset-Family of T holds F c= BorelSets T
proofend;

theorem :: TOPGEN_4:66
for T being non empty TopSpace holds BorelSets T = sigma (Topology_of T)
proofend;

definition
let T be non empty TopSpace;
let A be Subset of T;
attrA is Borel  means :Def12: :: TOPGEN_4:def 12
A in BorelSets T;
end;

:: deftheorem Def12 defines Borel TOPGEN_4:def_12_:_
 for T being non empty TopSpace
for A being Subset of T holds
( A is Borel iff A in BorelSets T );

registration
let T be non empty TopSpace;
cluster F_sigma  ->  Borel for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is F_sigma holds
b1 is Borel
proofend;
end;

registration
let T be non empty TopSpace;
cluster G_delta  ->  Borel for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is G_delta holds
b1 is Borel
proofend;
end;