:: 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 )
proof end;

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 ) )
proof end;

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

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}) }
proof end;

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

registration
cluster REAL -> non countable ;
coherence
not REAL is countable
proof end;
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 )
proof end;
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 )
proof end;

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 & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )
proof end;

begin

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

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 & A is countable ) )
proof end;

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

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)
proof end;

:: 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)
proof end;

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

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

begin

definition
let T be non empty TopSpace;
let F be Subset-Family of T;
attr F 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;
attr F 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;
attr F 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
proof end;

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
proof end;

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 & F is closed_for_countable_unions ) )
proof end;

definition
let T be set ;
let F be Subset-Family of T;
attr F 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 & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
proof end;

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

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

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

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 & b1 is compl-closed & b1 is closed_for_countable_unions holds
( b1 is all-closed-containing & 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 & b1 is compl-closed & b1 is closed_for_countable_meets holds
( b1 is all-open-containing & 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 & b1 is closed )
proof end;
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 & b1 is open & b1 is closed )
proof end;
end;

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

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 )
proof end;

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 )
proof end;

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
proof end;
:: original: UNION
redefine func UNION (F,G) -> Subset-Family of T;
coherence
UNION (F,G) is Subset-Family of T
proof end;
end;

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

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

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

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

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:]
proof end;

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:]
proof end;

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

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

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

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

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

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

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

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

begin

definition
let T be TopSpace;
let A be Subset of T;
attr A 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;
attr A 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 & b1 is G_delta )
proof end;
end;

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

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

registration
let T be non empty TopSpace;
cluster [#] T -> F_sigma G_delta ;
coherence
( [#] T is F_sigma & [#] 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
proof end;

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
proof end;

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

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

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

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

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
proof end;

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
proof end;

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

begin

definition
let T be TopSpace;
attr T 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
proof end;

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

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
proof end;
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;
pred x 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 & A c= B holds
x is_a_condensation_point_of B
proof end;

definition
let T be non empty TopSpace;
let A be Subset of T;
func A ^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 )
proof end;
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 ) ) & ( for x being Point of T holds
( x in b2 iff x is_a_condensation_point_of A ) ) holds
b1 = b2
proof end;
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
proof end;

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

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

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
proof end;

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 )
proof end;

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)
proof end;

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
proof end;

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

registration
let T be non empty TopSpace;
let A be countable Subset of T;
cluster A ^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
proof end;

registration
cluster non empty TopSpace-like second-countable for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is second-countable & not b1 is empty )
proof end;
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 & TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
proof end;
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
proof end;

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 & F c= G holds
G is all-open-containing
proof end;

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

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 & b1 is closed_for_countable_unions & b1 is closed_for_countable_meets & b1 is all-closed-containing & b1 is all-open-containing )
proof end;
end;

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

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 & sigma (TotFam T) is compl-closed & 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 & b1 is compl-closed & b1 is closed_for_countable_unions & not b1 is empty )
proof end;
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 & 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
proof end;
end;

registration
let T be non empty TopSpace;
cluster Topology_of T -> open all-open-containing ;
coherence
( Topology_of T is open & Topology_of T is all-open-containing )
proof end;
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 & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )
proof end;

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
proof end;
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 ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b2 c= G ) holds
b1 = b2
proof end;
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
proof end;

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

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

definition
let T be non empty TopSpace;
let A be Subset of T;
attr A 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
proof end;
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
proof end;
end;