:: TOPGEN_4 semantic presentation

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
let T be set ; ::_thesis: for F being Subset-Family of T holds
( F is countable iff COMPLEMENT F is countable )
let F be Subset-Family of T; ::_thesis: ( F is countable iff COMPLEMENT F is countable )
 F, COMPLEMENT F are_equipotent by YELLOW_8:3;
hence  ( F is countable iff COMPLEMENT F is countable ) by YELLOW_8:4; ::_thesis: verum
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
let X be set ; ::_thesis: ( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
thus  ( X is countable implies ex f being Function st
( dom f = RAT & X c= rng f ) ) ::_thesis: ( ex f being Function st
( dom f = RAT & X c= rng f ) implies X is countable )
proof
assume  card X c= omega ; :: according to CARD_3:def_14 ::_thesis: ex f being Function st
( dom f = RAT & X c= rng f )
hence  ex f being Function st
( dom f = RAT & X c= rng f ) by CARD_1:12, TOPGEN_3:17; ::_thesis: verum
end;
assume  ex f being Function st
( dom f = RAT & X c= rng f ) ; ::_thesis: X is countable
hence  card X c= omega by CARD_1:12, TOPGEN_3:17; :: according to CARD_3:def_14 ::_thesis: verum
end;

scheme :: TOPGEN_4:sch 1
FraenCoun11{ P1[ set ] } :
  {  {n} where n is Element of RAT : P1[n]  }  is countable
proof
deffunc H1( set ) ->  set = {$1};
consider f being Function such that
A1: ( dom f = RAT & ( for x being set st x in RAT holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
  {  {n} where n is Element of RAT : P1[n]  }  c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  {n} where n is Element of RAT : P1[n]  }  or x in rng f )
assume  x in  {  {n} where n is Element of RAT : P1[n]  }  ; ::_thesis: x in rng f
then consider n being Element of RAT  such that
A2: x = {n} and
 P1[n] ;
 f . n = x by A1, A2;
hence  x in rng f by A1, FUNCT_1:def_3; ::_thesis: verum
end;
hence   {  {n} where n is Element of RAT : P1[n]  }  is countable by A1, Lm1; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds Der A =  {  x where x is Point of T : x in Cl (A \ {x})  }
let A be Subset of T; ::_thesis: Der A =  {  x where x is Point of T : x in Cl (A \ {x})  }
thus  Der A c=  {  x where x is Point of T : x in Cl (A \ {x})  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x where x is Point of T : x in Cl (A \ {x})  }  c= Der A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Der A or x in  {  x where x is Point of T : x in Cl (A \ {x})  }  )
assume  x in Der A ; ::_thesis: x in  {  x where x is Point of T : x in Cl (A \ {x})  }
then  x is_an_accumulation_point_of A by TOPGEN_1:def_3;
then  x in Cl (A \ {x}) by TOPGEN_1:def_2;
hence  x in  {  x where x is Point of T : x in Cl (A \ {x})  }  ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Point of T : x in Cl (A \ {x})  }  or y in Der A )
assume  y in  {  x where x is Point of T : x in Cl (A \ {x})  }  ; ::_thesis: y in Der A
then consider z being Point of T such that
A1: z = y and
A2: z in Cl (A \ {z}) ;
 z is_an_accumulation_point_of A by A2, TOPGEN_1:def_2;
hence  y in Der A by A1, TOPGEN_1:def_3; ::_thesis: verum
end;

registration
cluster finite  ->  second-countable for TopStruct ;
coherence
 for b1 being TopStruct st b1 is finite holds
b1 is second-countable
proof
let T be TopStruct ; ::_thesis: ( T is finite implies T is second-countable )
assume  T is finite ; ::_thesis: T is second-countable
then reconsider T9 = T as finite TopStruct ;
 weight T9 is finite by TOPGEN_2:def_4;
then  weight T9 c= omega ;
hence  T is second-countable by WAYBEL23:def_6; ::_thesis: verum
end;
end;

registration
cluster REAL  ->  non countable ;
coherence
 not REAL is countable
proof
assume  REAL is countable ; ::_thesis: contradiction
then  card REAL c= omega by CARD_3:def_14;
hence  contradiction by TOPGEN_3:30, TOPGEN_3:def_4; ::_thesis: verum
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
take  REAL ; ::_thesis: ( not REAL is countable & not REAL is empty )
thus  ( not REAL is countable & not REAL is empty ) ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds
( A is closed iff Der A c= A )
let A be Subset of T; ::_thesis: ( A is closed iff Der A c= A )
hereby  ::_thesis: ( Der A c= A implies A is closed )
assume  A is closed ; ::_thesis: Der A c= A
then A1: A = Cl A by PRE_TOPC:22;
 Cl A = A \/ (Der A) by TOPGEN_1:29;
hence  Der A c= A by A1, XBOOLE_1:7; ::_thesis: verum
end;
assume A2: Der A c= A ; ::_thesis: A is closed
Cl A = A \/ (Der A) by TOPGEN_1:29
.= A by A2, XBOOLE_1:12 ;
hence  A is closed ; ::_thesis: verum
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
let T be non empty TopStruct ; ::_thesis: 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 <> {} )
let B be Basis of T; ::_thesis: 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 <> {} )
let V be Subset of T; ::_thesis: ( V is open & V <> {} implies ex W being Subset of T st
( W in B & W c= V & W <> {} ) )
assume that
A1: V is open and
A2: V <> {} ; ::_thesis: ex W being Subset of T st
( W in B & W c= V & W <> {} )
consider x being set  such that
A3: x in V by A2, XBOOLE_0:def_1;
 V = union  {  G where G is Subset of T : ( G in B & G c= V )  }  by A1, YELLOW_8:9;
then consider Y being set  such that
A4: x in Y and
A5: Y in  {  G where G is Subset of T : ( G in B & G c= V )  }  by A3, TARSKI:def_4;
 ex Z being Subset of T st
( Z = Y & Z in B & Z c= V ) by A5;
hence  ex W being Subset of T st
( W in B & W c= V & W <> {} ) by A4; ::_thesis: verum
end;

begin

theorem Th5: :: TOPGEN_4:5
for T being non empty TopSpace holds density T c= weight T
proof
let T be non empty TopSpace; ::_thesis: density T c= weight T
defpred S1[ set ] means $1 <> {} ;
deffunc H1( set ) ->  Element of $1 = choose $1;
set B = the Basis of T;
consider B1 being Basis of T such that
 B1 c= the Basis of T and
A1: card B1 = weight T by TOPGEN_2:18;
set A =  {  H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] )  }  ;
  {  H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] )  }  c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] )  }  or x in the carrier of T )
assume  x in  {  H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] )  }  ; ::_thesis: x in the carrier of T
then consider B2 being Subset of T such that
A2: x = choose B2 and
 B2 in B1 and
A3: B2 <> {} ;
 x in B2 by A2, A3;
hence  x in the carrier of T ; ::_thesis: verum
end;
then reconsider A =  {  H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] )  }  as Subset of T ;
 for Q being Subset of T st Q <> {} & Q is open holds
A meets Q
proof
let Q be Subset of T; ::_thesis: ( Q <> {} & Q is open implies A meets Q )
assume  ( Q <> {} & Q is open ) ; ::_thesis: A meets Q
then consider W being Subset of T such that
A4: W in B1 and
A5: W c= Q and
A6: W <> {} by Th4;
 ( choose W in A & choose W in W ) by A4, A6;
hence  A meets Q by A5, XBOOLE_0:3; ::_thesis: verum
end;
then  A is dense by TOPS_1:45;
then A7: density T c= card A by TOPGEN_1:def_12;
 card  {  H1(w) where w is Element of bool the carrier of T : ( w in B1 & S1[w] )  }  c= card B1 from BORSUK_2:sch_1();
hence  density T c= weight T by A1, A7, XBOOLE_1:1; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: ( T is separable iff ex A being Subset of T st
( A is dense & A is countable ) )
hereby  ::_thesis: ( ex A being Subset of T st
( A is dense & A is countable ) implies T is separable )
consider A being Subset of T such that
A1: A is dense and
A2: density T = card A by TOPGEN_1:def_12;
assume  T is separable ; ::_thesis: ex A being Subset of T st
( A is dense & A is countable )
then  density T c= omega by TOPGEN_1:def_13;
then  A is countable by A2, CARD_3:def_14;
hence  ex A being Subset of T st
( A is dense & A is countable ) by A1; ::_thesis: verum
end;
given A being Subset of T such that A3: ( A is dense & A is countable ) ; ::_thesis: T is separable
 ( density T c= card A & card A c= omega ) by A3, CARD_3:def_14, TOPGEN_1:def_12;
then  density T c= omega by XBOOLE_1:1;
hence  T is separable by TOPGEN_1:def_13; ::_thesis: verum
end;

theorem Th7: :: TOPGEN_4:7
for T being non empty TopSpace st T is second-countable holds
T is separable
proof
let T be non empty TopSpace; ::_thesis: ( T is second-countable implies T is separable )
assume  T is second-countable ; ::_thesis: T is separable
then A1: weight T c= omega by WAYBEL23:def_6;
 density T c= weight T by Th5;
then  density T c= omega by A1, XBOOLE_1:1;
hence  T is separable by TOPGEN_1:def_13; ::_thesis: verum
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;

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
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A,B are_separated holds
Fr (A \/ B) = (Fr A) \/ (Fr B)
let A, B be Subset of T; ::_thesis: ( A,B are_separated implies Fr (A \/ B) = (Fr A) \/ (Fr B) )
A1: ( (Fr A) \/ (Fr B) = ((Fr (A \/ B)) \/ (Fr (A /\ B))) \/ ((Fr A) /\ (Fr B)) & Fr ({} T) = {} ) by TOPS_1:36;
assume A2: A,B are_separated ; ::_thesis: Fr (A \/ B) = (Fr A) \/ (Fr B)
then A3: A misses Cl B by CONNSP_1:def_1;
 A misses B by A2, CONNSP_1:1;
then A4: A /\ B = {} by XBOOLE_0:def_7;
A5: Cl A misses B by A2, CONNSP_1:def_1;
A6: (Fr A) \/ (Fr B) c= Fr (A \/ B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Fr A) \/ (Fr B) or x in Fr (A \/ B) )
assume A7: x in (Fr A) \/ (Fr B) ; ::_thesis: x in Fr (A \/ B)
percases ( x in Fr (A \/ B) or x in (Fr A) /\ (Fr B) ) by A4, A1, A7, XBOOLE_0:def_3;
suppose x in Fr (A \/ B) ; ::_thesis: x in Fr (A \/ B)
hence  x in Fr (A \/ B) ; ::_thesis: verum
end;
supposeA8: x in (Fr A) /\ (Fr B) ; ::_thesis: x in Fr (A \/ B)
then  x in Fr B by XBOOLE_0:def_4;
then  x in (Cl B) /\ (Cl (B `)) by TOPS_1:def_2;
then  x in Cl B by XBOOLE_0:def_4;
then  not x in A by A3, XBOOLE_0:3;
then A9: x in A ` by A7, XBOOLE_0:def_5;
 x in Fr A by A8, XBOOLE_0:def_4;
then  x in (Cl A) /\ (Cl (A `)) by TOPS_1:def_2;
then A10: x in Cl A by XBOOLE_0:def_4;
then  x in (Cl A) \/ (Cl B) by XBOOLE_0:def_3;
then A11: x in Cl (A \/ B) by PRE_TOPC:20;
 not x in B by A5, A10, XBOOLE_0:3;
then  x in B ` by A7, XBOOLE_0:def_5;
then  x in (A `) /\ (B `) by A9, XBOOLE_0:def_4;
then A12: x in (A \/ B) ` by XBOOLE_1:53;
 (A \/ B) ` c= Cl ((A \/ B) `) by PRE_TOPC:18;
then  x in (Cl (A \/ B)) /\ (Cl ((A \/ B) `)) by A11, A12, XBOOLE_0:def_4;
hence  x in Fr (A \/ B) by TOPS_1:def_2; ::_thesis: verum
end;
end;
end;
 Fr (A \/ B) c= (Fr A) \/ (Fr B) by TOPS_1:33;
hence  Fr (A \/ B) = (Fr A) \/ (Fr B) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

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
let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is locally_finite holds
Fr (union F) c= union (Fr F)
let F be Subset-Family of T; ::_thesis: ( F is locally_finite implies Fr (union F) c= union (Fr F) )
assume  F is locally_finite ; ::_thesis: Fr (union F) c= union (Fr F)
then A1: Cl (union F) = union (clf F) by PCOMPS_1:20;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr (union F) or x in union (Fr F) )
assume  x in Fr (union F) ; ::_thesis: x in union (Fr F)
then A2: x in (Cl (union F)) /\ (Cl ((union F) `)) by TOPS_1:def_2;
then A3: x in Cl ((union F) `) by XBOOLE_0:def_4;
 x in Cl (union F) by A2, XBOOLE_0:def_4;
then consider A being set  such that
A4: x in A and
A5: A in clf F by A1, TARSKI:def_4;
consider B being Subset of T such that
A6: A = Cl B and
A7: B in F by A5, PCOMPS_1:def_2;
 B c= union F by A7, ZFMISC_1:74;
then  (union F) ` c= B ` by SUBSET_1:12;
then  Cl ((union F) `) c= Cl (B `) by PRE_TOPC:19;
then  x in (Cl B) /\ (Cl (B `)) by A4, A6, A3, XBOOLE_0:def_4;
then A8: x in Fr B by TOPS_1:def_2;
 Fr B in Fr F by A7, TOPGEN_1:def_1;
hence  x in union (Fr F) by A8, TARSKI:def_4; ::_thesis: verum
end;

theorem Th10: :: TOPGEN_4:10
for T being non empty discrete TopSpace holds
( T is separable iff card ([#] T) c= omega )
proof
let T be non empty discrete TopSpace; ::_thesis: ( T is separable iff card ([#] T) c= omega )
hereby  ::_thesis: ( card ([#] T) c= omega implies T is separable )
assume  T is separable ; ::_thesis: card ([#] T) c= omega
then A1: density T c= omega by TOPGEN_1:def_13;
 ex A being Subset of T st
( A is dense & density T = card A ) by TOPGEN_1:def_12;
hence  card ([#] T) c= omega by A1, TOPS_3:19; ::_thesis: verum
end;
assume  card ([#] T) c= omega ; ::_thesis: T is separable
then  T is countable by TOPGEN_1:2;
hence  T is separable ; ::_thesis: verum
end;

theorem :: TOPGEN_4:11
for T being non empty discrete TopSpace holds
( T is separable iff T is countable )
proof
let T be non empty discrete TopSpace; ::_thesis: ( T is separable iff T is countable )
 ( T is separable iff card ([#] T) c= omega ) by Th10;
hence  ( T is separable iff T is countable ) by TOPGEN_1:2; ::_thesis: verum
end;

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
proof
let T be set ; ::_thesis: for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
let F be Subset-Family of T; ::_thesis: ( F is SigmaField of T implies F is closed_for_countable_unions )
assume A1: F is SigmaField of T ; ::_thesis: F is closed_for_countable_unions
let G be countable Subset-Family of T; :: according to TOPGEN_4:def_4 ::_thesis: ( G c= F implies union G in F )
assume A2: G c= F ; ::_thesis: union G in F
percases ( G is empty or not G is empty ) ;
suppose G is empty ; ::_thesis: union G in F
hence  union G in F by A1, PROB_1:4, ZFMISC_1:2; ::_thesis: verum
end;
suppose not G is empty ; ::_thesis: union G in F
hence  union G in F by A1, A2, MEASURE1:def_5; ::_thesis: verum
end;
end;
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
let T be set ; ::_thesis: for F being Subset-Family of T st F is closed_for_countable_unions holds
{} in F
let F be Subset-Family of T; ::_thesis: ( F is closed_for_countable_unions implies {} in F )
reconsider E = {} as countable Subset-Family of T by XBOOLE_1:2;
A1: E c= F by XBOOLE_1:2;
assume  F is closed_for_countable_unions ; ::_thesis: {} in F
hence  {} in F by A1, Def4, ZFMISC_1:2; ::_thesis: verum
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
let T be set ; ::_thesis: for F being Subset-Family of T holds
( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
let F be Subset-Family of T; ::_thesis: ( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )
thus  ( F is SigmaField of T implies ( F is compl-closed & F is closed_for_countable_unions ) ) ; ::_thesis: ( F is compl-closed & F is closed_for_countable_unions implies F is SigmaField of T )
assume A1: ( F is compl-closed & F is closed_for_countable_unions ) ; ::_thesis: F is SigmaField of T
 F is sigma-additive
proof
let M be N_Sub_set_fam of T; :: according to MEASURE1:def_5 ::_thesis: ( not M c= F or union M in F )
assume  M c= F ; ::_thesis: union M in F
hence  union M in F by A1, Def4; ::_thesis: verum
end;
then reconsider F = F as non empty compl-closed sigma-additive Subset-Family of T by A1;
 F is SigmaField of T ;
hence  F is SigmaField of T ; ::_thesis: verum
end;

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 & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
proof
let T be non empty TopSpace; ::_thesis: 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 ) )
let F be Subset-Family of T; ::_thesis: ( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
hereby  ::_thesis: ( F is all-open-containing & F is compl-closed implies ( F is all-closed-containing & F is compl-closed ) )
assume A1: ( F is all-closed-containing & F is compl-closed ) ; ::_thesis: ( F is all-open-containing & F is compl-closed )
 for A being Subset of T st A is open holds
A in F
proof
let A be Subset of T; ::_thesis: ( A is open implies A in F )
assume  A is open ; ::_thesis: A in F
then  A ` in F by A1, Def3;
then  (A `) ` in F by A1, PROB_1:def_1;
hence  A in F ; ::_thesis: verum
end;
hence  ( F is all-open-containing & F is compl-closed ) by A1, Def2; ::_thesis: verum
end;
assume A2: ( F is all-open-containing & F is compl-closed ) ; ::_thesis: ( F is all-closed-containing & F is compl-closed )
 for A being Subset of T st A is closed holds
A in F
proof
let A be Subset of T; ::_thesis: ( A is closed implies A in F )
assume  A is closed ; ::_thesis: A in F
then  A ` in F by A2, Def2;
then  (A `) ` in F by A2, PROB_1:def_1;
hence  A in F ; ::_thesis: verum
end;
hence  ( F is all-closed-containing & F is compl-closed ) by A2, Def3; ::_thesis: verum
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
let T be set ; ::_thesis: for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F
let F be Subset-Family of T; ::_thesis: ( F is compl-closed implies F = COMPLEMENT F )
assume A1: F is compl-closed ; ::_thesis: F = COMPLEMENT F
thus  F c= COMPLEMENT F :: according to XBOOLE_0:def_10 ::_thesis: COMPLEMENT F c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in COMPLEMENT F )
assume A2: x in F ; ::_thesis: x in COMPLEMENT F
then reconsider x9 = x as Subset of T ;
 x9 ` in F by A1, A2, PROB_1:def_1;
hence  x in COMPLEMENT F by SETFAM_1:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COMPLEMENT F or x in F )
assume A3: x in COMPLEMENT F ; ::_thesis: x in F
then reconsider x9 = x as Subset of T ;
 x9 ` in F by A3, SETFAM_1:def_7;
then  (x9 `) ` in F by A1, PROB_1:def_1;
hence  x in F ; ::_thesis: verum
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
let T be set ; ::_thesis: for F, G being Subset-Family of T st F c= G & G is compl-closed holds
COMPLEMENT F c= G
let F, G be Subset-Family of T; ::_thesis: ( F c= G & G is compl-closed implies COMPLEMENT F c= G )
assume A1: ( F c= G & G is compl-closed ) ; ::_thesis: COMPLEMENT F c= G
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COMPLEMENT F or x in G )
assume A2: x in COMPLEMENT F ; ::_thesis: x in G
then reconsider x9 = x as Subset of T ;
 x9 ` in F by A2, SETFAM_1:def_7;
then  (x9 `) ` in G by A1, PROB_1:def_1;
hence  x in G ; ::_thesis: verum
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
let T be set ; ::_thesis: 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 ) )
let F be Subset-Family of T; ::_thesis: ( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )
hereby  ::_thesis: ( F is closed_for_countable_unions & F is compl-closed implies ( F is closed_for_countable_meets & F is compl-closed ) )
assume A1: ( F is closed_for_countable_meets & F is compl-closed ) ; ::_thesis: ( F is closed_for_countable_unions & F is compl-closed )
 for G being countable Subset-Family of T st G c= F holds
union G in F
proof
let G be countable Subset-Family of T; ::_thesis: ( G c= F implies union G in F )
assume A2: G c= F ; ::_thesis: union G in F
percases ( G = {} or G <> {} ) ;
suppose G = {} ; ::_thesis: union G in F
hence  union G in F by A1, A2, Def5, SETFAM_1:1, ZFMISC_1:2; ::_thesis: verum
end;
suppose G <> {} ; ::_thesis: union G in F
then reconsider G9 = G as non empty Subset-Family of T ;
 ( COMPLEMENT G9 c= F & COMPLEMENT G9 is countable ) by A1, A2, Th1, Th16;
then A3: meet (COMPLEMENT G9) in F by A1, Def5;
(meet (COMPLEMENT G9)) ` = ((union G9) `) ` by TOPS_2:6
.= union G9 ;
hence  union G in F by A1, A3, PROB_1:def_1; ::_thesis: verum
end;
end;
end;
hence  ( F is closed_for_countable_unions & F is compl-closed ) by A1, Def4; ::_thesis: verum
end;
assume A4: ( F is closed_for_countable_unions & F is compl-closed ) ; ::_thesis: ( F is closed_for_countable_meets & F is compl-closed )
 for G being countable Subset-Family of T st G c= F holds
meet G in F
proof
let G be countable Subset-Family of T; ::_thesis: ( G c= F implies meet G in F )
assume A5: G c= F ; ::_thesis: meet G in F
percases ( G = {} or G <> {} ) ;
suppose G = {} ; ::_thesis: meet G in F
hence  meet G in F by A4, A5, Def4, SETFAM_1:1, ZFMISC_1:2; ::_thesis: verum
end;
suppose G <> {} ; ::_thesis: meet G in F
then reconsider G9 = G as non empty Subset-Family of T ;
 ( COMPLEMENT G9 c= F & COMPLEMENT G9 is countable ) by A4, A5, Th1, Th16;
then A6: union (COMPLEMENT G9) in F by A4, Def4;
(union (COMPLEMENT G9)) ` = ((meet G9) `) ` by TOPS_2:7
.= meet G9 ;
hence  meet G in F by A4, A6, PROB_1:def_1; ::_thesis: verum
end;
end;
end;
hence  ( F is closed_for_countable_meets & F is compl-closed ) by A4, Def5; ::_thesis: verum
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
let F be Subset-Family of T; ::_thesis: ( F is empty implies ( F is open & F is closed ) )
assume  F is empty ; ::_thesis: ( F is open & F is closed )
then  ( ( for P being Subset of T st P in F holds
P is open ) & ( for P being Subset of T st P in F holds
P is closed ) ) ;
hence  ( F is open & F is closed ) by TOPS_2:def_1, TOPS_2:def_2; ::_thesis: verum
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
 {} (bool the carrier of T) is open ;
hence  ex b1 being Subset-Family of T st
( b1 is countable & b1 is open & b1 is closed ) ; ::_thesis: verum
end;
end;

theorem Th18: :: TOPGEN_4:18
for T being set holds {} is empty Subset-Family of T
proof
let T be set ; ::_thesis: {} is empty Subset-Family of T
 {} (bool T) = {} ;
hence  {} is empty Subset-Family of T ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
let A be Subset of T; ::_thesis: for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
let F be Subset-Family of T; ::_thesis: ( F = {A} implies ( A is open iff F is open ) )
assume A1: F = {A} ; ::_thesis: ( A is open iff F is open )
hereby  ::_thesis: ( F is open implies A is open )
assume  A is open ; ::_thesis: F is open
then  for A being Subset of T st A in F holds
A is open by A1, TARSKI:def_1;
hence  F is open by TOPS_2:def_1; ::_thesis: verum
end;
assume A2: F is open ; ::_thesis: A is open
 A in F by A1, TARSKI:def_1;
hence  A is open by A2, TOPS_2:def_1; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )
let A be Subset of T; ::_thesis: for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )
let F be Subset-Family of T; ::_thesis: ( F = {A} implies ( A is closed iff F is closed ) )
assume A1: F = {A} ; ::_thesis: ( A is closed iff F is closed )
hereby  ::_thesis: ( F is closed implies A is closed )
assume  A is closed ; ::_thesis: F is closed
then  for A being Subset of T st A in F holds
A is closed by A1, TARSKI:def_1;
hence  F is closed by TOPS_2:def_2; ::_thesis: verum
end;
assume A2: F is closed ; ::_thesis: A is closed
 A in F by A1, TARSKI:def_1;
hence  A is closed by A2, TOPS_2:def_2; ::_thesis: verum
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
 INTERSECTION (F,G) c= bool T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION (F,G) or x in bool T )
assume  x in INTERSECTION (F,G) ; ::_thesis: x in bool T
then consider X, Y being set  such that
A1: X in F and
 Y in G and
A2: x = X /\ Y by SETFAM_1:def_5;
 X /\ Y c= X by XBOOLE_1:17;
then  x is Subset of T by A1, A2, XBOOLE_1:1;
hence  x in bool T ; ::_thesis: verum
end;
hence  INTERSECTION (F,G) is Subset-Family of T ; ::_thesis: verum
end;
:: original: UNION
redefine func UNION (F,G) ->  Subset-Family of T;
coherence
 UNION (F,G) is Subset-Family of T
proof
 UNION (F,G) c= bool T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION (F,G) or x in bool T )
assume  x in UNION (F,G) ; ::_thesis: x in bool T
then consider X, Y being set  such that
A3: ( X in F & Y in G ) and
A4: x = X \/ Y by SETFAM_1:def_4;
 X \/ Y c= T by A3, XBOOLE_1:8;
hence  x in bool T by A4; ::_thesis: verum
end;
hence  UNION (F,G) is Subset-Family of T ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is closed & G is closed holds
INTERSECTION (F,G) is closed
let F, G be Subset-Family of T; ::_thesis: ( F is closed & G is closed implies INTERSECTION (F,G) is closed )
assume A1: ( F is closed & G is closed ) ; ::_thesis: INTERSECTION (F,G) is closed
 for A being Subset of T st A in INTERSECTION (F,G) holds
A is closed
proof
let A be Subset of T; ::_thesis: ( A in INTERSECTION (F,G) implies A is closed )
assume  A in INTERSECTION (F,G) ; ::_thesis: A is closed
then consider X, Y being set  such that
A2: ( X in F & Y in G ) and
A3: A = X /\ Y by SETFAM_1:def_5;
reconsider X = X, Y = Y as Subset of T by A2;
 ( X is closed & Y is closed ) by A1, A2, TOPS_2:def_2;
hence  A is closed by A3; ::_thesis: verum
end;
hence  INTERSECTION (F,G) is closed by TOPS_2:def_2; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is closed & G is closed holds
UNION (F,G) is closed
let F, G be Subset-Family of T; ::_thesis: ( F is closed & G is closed implies UNION (F,G) is closed )
assume A1: ( F is closed & G is closed ) ; ::_thesis: UNION (F,G) is closed
 for A being Subset of T st A in UNION (F,G) holds
A is closed
proof
let A be Subset of T; ::_thesis: ( A in UNION (F,G) implies A is closed )
assume  A in UNION (F,G) ; ::_thesis: A is closed
then consider X, Y being set  such that
A2: ( X in F & Y in G ) and
A3: A = X \/ Y by SETFAM_1:def_4;
reconsider X = X, Y = Y as Subset of T by A2;
 ( X is closed & Y is closed ) by A1, A2, TOPS_2:def_2;
hence  A is closed by A3; ::_thesis: verum
end;
hence  UNION (F,G) is closed by TOPS_2:def_2; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is open & G is open holds
INTERSECTION (F,G) is open
let F, G be Subset-Family of T; ::_thesis: ( F is open & G is open implies INTERSECTION (F,G) is open )
assume A1: ( F is open & G is open ) ; ::_thesis: INTERSECTION (F,G) is open
 for A being Subset of T st A in INTERSECTION (F,G) holds
A is open
proof
let A be Subset of T; ::_thesis: ( A in INTERSECTION (F,G) implies A is open )
assume  A in INTERSECTION (F,G) ; ::_thesis: A is open
then consider X, Y being set  such that
A2: ( X in F & Y in G ) and
A3: A = X /\ Y by SETFAM_1:def_5;
reconsider X = X, Y = Y as Subset of T by A2;
 ( X is open & Y is open ) by A1, A2, TOPS_2:def_1;
hence  A is open by A3; ::_thesis: verum
end;
hence  INTERSECTION (F,G) is open by TOPS_2:def_1; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is open & G is open holds
UNION (F,G) is open
let F, G be Subset-Family of T; ::_thesis: ( F is open & G is open implies UNION (F,G) is open )
assume A1: ( F is open & G is open ) ; ::_thesis: UNION (F,G) is open
 for A being Subset of T st A in UNION (F,G) holds
A is open
proof
let A be Subset of T; ::_thesis: ( A in UNION (F,G) implies A is open )
assume  A in UNION (F,G) ; ::_thesis: A is open
then consider X, Y being set  such that
A2: ( X in F & Y in G ) and
A3: A = X \/ Y by SETFAM_1:def_4;
reconsider X = X, Y = Y as Subset of T by A2;
 ( X is open & Y is open ) by A1, A2, TOPS_2:def_1;
hence  A is open by A3; ::_thesis: verum
end;
hence  UNION (F,G) is open by TOPS_2:def_1; ::_thesis: verum
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
deffunc H1( set ) ->  set = ($1 `1) /\ ($1 `2);
let T be set ; ::_thesis: for F, G being Subset-Family of T holds card (INTERSECTION (F,G)) c= card [:F,G:]
let F, G be Subset-Family of T; ::_thesis: card (INTERSECTION (F,G)) c= card [:F,G:]
set XX = [:F,G:];
set IN =  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  ;
set A = [:(bool T),(bool T):];
set AL = F;
set BL = G;
set C = INTERSECTION (F,G);
A1:  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  c= INTERSECTION (F,G)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  or a in INTERSECTION (F,G) )
assume  a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  ; ::_thesis: a in INTERSECTION (F,G)
then consider X being Element of [:(bool T),(bool T):] such that
A2: a = H1(X) and
A3: X in [:F,G:] ;
 ( X `1 in F & X `2 in G ) by A3, MCART_1:10;
hence  a in INTERSECTION (F,G) by A2, SETFAM_1:def_5; ::_thesis: verum
end;
A4: INTERSECTION (F,G) c=  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in INTERSECTION (F,G) or a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  )
assume  a in INTERSECTION (F,G) ; ::_thesis: a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }
then consider X, Y being set  such that
A5: ( X in F & Y in G ) and
A6: a = X /\ Y by SETFAM_1:def_5;
reconsider X = X, Y = Y as Subset of T by A5;
set XY = [X,Y];
A7: ( [X,Y] `1 = X & [X,Y] `2 = Y ) ;
 [X,Y] in [:F,G:] by A5, ZFMISC_1:87;
hence  a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  by A6, A7; ::_thesis: verum
end;
 card  {  H1(w) where w is Element of [:(bool T),(bool T):] : w in [:F,G:]  }  c= card [:F,G:] from TREES_2:sch_2();
hence  card (INTERSECTION (F,G)) c= card [:F,G:] by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
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
deffunc H1( set ) ->  set = ($1 `1) \/ ($1 `2);
let T be set ; ::_thesis: for F, G being Subset-Family of T holds card (UNION (F,G)) c= card [:F,G:]
let F, G be Subset-Family of T; ::_thesis: card (UNION (F,G)) c= card [:F,G:]
set XX = [:F,G:];
set IN =  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  ;
set A = [:(bool T),(bool T):];
set AL = F;
set BL = G;
set C = UNION (F,G);
A1:  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  = UNION (F,G)
proof
thus   {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  c= UNION (F,G) :: according to XBOOLE_0:def_10 ::_thesis: UNION (F,G) c=  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  or a in UNION (F,G) )
assume  a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  ; ::_thesis: a in UNION (F,G)
then consider X being Element of [:(bool T),(bool T):] such that
A2: a = H1(X) and
A3: X in [:F,G:] ;
 ( X `1 in F & X `2 in G ) by A3, MCART_1:10;
hence  a in UNION (F,G) by A2, SETFAM_1:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in UNION (F,G) or a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  )
assume  a in UNION (F,G) ; ::_thesis: a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }
then consider X, Y being set  such that
A4: ( X in F & Y in G ) and
A5: a = X \/ Y by SETFAM_1:def_4;
reconsider X = X, Y = Y as Subset of T by A4;
set XY = [X,Y];
A6: ( [X,Y] `1 = X & [X,Y] `2 = Y ) ;
 [X,Y] in [:F,G:] by A4, ZFMISC_1:87;
hence  a in  {  H1(X) where X is Element of [:(bool T),(bool T):] : X in [:F,G:]  }  by A5, A6; ::_thesis: verum
end;
 card  {  H1(w) where w is Element of [:(bool T),(bool T):] : w in [:F,G:]  }  c= card [:F,G:] from TREES_2:sch_2();
hence  card (UNION (F,G)) c= card [:F,G:] by A1; ::_thesis: verum
end;

theorem Th27: :: TOPGEN_4:27
for F, G being set holds union (UNION (F,G)) c= (union F) \/ (union G)
proof
let F, G be set ; ::_thesis: union (UNION (F,G)) c= (union F) \/ (union G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (UNION (F,G)) or x in (union F) \/ (union G) )
assume  x in union (UNION (F,G)) ; ::_thesis: x in (union F) \/ (union G)
then consider Y being set  such that
A1: x in Y and
A2: Y in UNION (F,G) by TARSKI:def_4;
consider f, g being set  such that
A3: f in F and
A4: g in G and
A5: Y = f \/ g by A2, SETFAM_1:def_4;
percases ( x in f or x in g ) by A1, A5, XBOOLE_0:def_3;
suppose x in f ; ::_thesis: x in (union F) \/ (union G)
then  x in union F by A3, TARSKI:def_4;
hence  x in (union F) \/ (union G) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in g ; ::_thesis: x in (union F) \/ (union G)
then  x in union G by A4, TARSKI:def_4;
hence  x in (union F) \/ (union G) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;

theorem Th28: :: TOPGEN_4:28
for F, G being set st F <> {} & G <> {} holds
(union F) \/ (union G) = union (UNION (F,G))
proof
let F, G be set ; ::_thesis: ( F <> {} & G <> {} implies (union F) \/ (union G) = union (UNION (F,G)) )
assume that
A1: F <> {} and
A2: G <> {} ; ::_thesis: (union F) \/ (union G) = union (UNION (F,G))
thus  (union F) \/ (union G) c= union (UNION (F,G)) :: according to XBOOLE_0:def_10 ::_thesis: union (UNION (F,G)) c= (union F) \/ (union G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union F) \/ (union G) or x in union (UNION (F,G)) )
assume A3: x in (union F) \/ (union G) ; ::_thesis: x in union (UNION (F,G))
percases ( x in union F or x in union G ) by A3, XBOOLE_0:def_3;
supposeA4: x in union F ; ::_thesis: x in union (UNION (F,G))
consider W being set  such that
A5: W in G by A2, XBOOLE_0:def_1;
consider Y being set  such that
A6: x in Y and
A7: Y in F by A4, TARSKI:def_4;
set YW = Y \/ W;
 ( Y c= Y \/ W & Y \/ W in UNION (F,G) ) by A7, A5, SETFAM_1:def_4, XBOOLE_1:7;
hence  x in union (UNION (F,G)) by A6, TARSKI:def_4; ::_thesis: verum
end;
supposeA8: x in union G ; ::_thesis: x in union (UNION (F,G))
consider W being set  such that
A9: W in F by A1, XBOOLE_0:def_1;
consider Y being set  such that
A10: x in Y and
A11: Y in G by A8, TARSKI:def_4;
set YW = W \/ Y;
 ( Y c= W \/ Y & W \/ Y in UNION (F,G) ) by A11, A9, SETFAM_1:def_4, XBOOLE_1:7;
hence  x in union (UNION (F,G)) by A10, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
thus  union (UNION (F,G)) c= (union F) \/ (union G) by Th27; ::_thesis: verum
end;

theorem Th29: :: TOPGEN_4:29
for F being set holds UNION ({},F) = {}
proof
let F be set ; ::_thesis: UNION ({},F) = {}
 UNION ({},F) c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNION ({},F) or x in {} )
assume  x in UNION ({},F) ; ::_thesis: x in {}
then  ex x1, x2 being set st
( x1 in {} & x2 in F & x = x1 \/ x2 ) by SETFAM_1:def_4;
hence  x in {} ; ::_thesis: verum
end;
hence  UNION ({},F) = {} ; ::_thesis: verum
end;

theorem :: TOPGEN_4:30
for F, G being set holds
( not UNION (F,G) = {} or F = {} or G = {} )
proof
let F, G be set ; ::_thesis: ( not UNION (F,G) = {} or F = {} or G = {} )
assume A1: UNION (F,G) = {} ; ::_thesis: ( F = {} or G = {} )
assume that
A2: F <> {} and
A3: G <> {} ; ::_thesis: contradiction
consider X being set  such that
A4: X in F by A2, XBOOLE_0:def_1;
consider Y being set  such that
A5: Y in G by A3, XBOOLE_0:def_1;
 X \/ Y in UNION (F,G) by A4, A5, SETFAM_1:def_4;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: TOPGEN_4:31
for F, G being set holds
( not INTERSECTION (F,G) = {} or F = {} or G = {} )
proof
let F, G be set ; ::_thesis: ( not INTERSECTION (F,G) = {} or F = {} or G = {} )
assume that
A1: INTERSECTION (F,G) = {} and
A2: F <> {} and
A3: G <> {} ; ::_thesis: contradiction
consider X being set  such that
A4: X in F by A2, XBOOLE_0:def_1;
consider Y being set  such that
A5: Y in G by A3, XBOOLE_0:def_1;
 X /\ Y in INTERSECTION (F,G) by A4, A5, SETFAM_1:def_5;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th32: :: TOPGEN_4:32
for F, G being set holds meet (UNION (F,G)) c= (meet F) \/ (meet G)
proof
let F, G be set ; ::_thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)
percases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
supposeA1: ( F <> {} & G <> {} ) ; ::_thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (UNION (F,G)) or x in (meet F) \/ (meet G) )
assume A2: x in meet (UNION (F,G)) ; ::_thesis: x in (meet F) \/ (meet G)
assume A3: not x in (meet F) \/ (meet G) ; ::_thesis: contradiction
then  not x in meet F by XBOOLE_0:def_3;
then consider Y being set  such that
A4: ( Y in F & not x in Y ) by A1, SETFAM_1:def_1;
 not x in meet G by A3, XBOOLE_0:def_3;
then consider Z being set  such that
A5: ( Z in G & not x in Z ) by A1, SETFAM_1:def_1;
 ( not x in Y \/ Z & Y \/ Z in UNION (F,G) ) by A4, A5, SETFAM_1:def_4, XBOOLE_0:def_3;
hence  contradiction by A2, SETFAM_1:def_1; ::_thesis: verum
end;
suppose ( F = {} or G = {} ) ; ::_thesis: meet (UNION (F,G)) c= (meet F) \/ (meet G)
then  UNION (F,G) = {} by Th29;
then  meet (UNION (F,G)) = {} by SETFAM_1:def_1;
hence  meet (UNION (F,G)) c= (meet F) \/ (meet G) by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;

theorem :: TOPGEN_4:33
for F, G being set st F <> {} & G <> {} holds
meet (UNION (F,G)) = (meet F) \/ (meet G)
proof
let F, G be set ; ::_thesis: ( F <> {} & G <> {} implies meet (UNION (F,G)) = (meet F) \/ (meet G) )
assume A1: ( F <> {} & G <> {} ) ; ::_thesis: meet (UNION (F,G)) = (meet F) \/ (meet G)
thus  meet (UNION (F,G)) c= (meet F) \/ (meet G) by Th32; :: according to XBOOLE_0:def_10 ::_thesis: (meet F) \/ (meet G) c= meet (UNION (F,G))
thus  (meet F) \/ (meet G) c= meet (UNION (F,G)) by A1, SETFAM_1:29; ::_thesis: verum
end;

theorem Th34: :: TOPGEN_4:34
for F, G being set st F <> {} & G <> {} holds
(meet F) /\ (meet G) = meet (INTERSECTION (F,G))
proof
let F, G be set ; ::_thesis: ( F <> {} & G <> {} implies (meet F) /\ (meet G) = meet (INTERSECTION (F,G)) )
assume that
A1: F <> {} and
A2: G <> {} ; ::_thesis: (meet F) /\ (meet G) = meet (INTERSECTION (F,G))
consider y being set  such that
A3: y in F by A1, XBOOLE_0:def_1;
consider z being set  such that
A4: z in G by A2, XBOOLE_0:def_1;
A5: meet (INTERSECTION (F,G)) c= (meet F) /\ (meet G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (INTERSECTION (F,G)) or x in (meet F) /\ (meet G) )
assume A6: x in meet (INTERSECTION (F,G)) ; ::_thesis: x in (meet F) /\ (meet G)
 for Z being set st Z in G holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in G implies x in Z )
assume  Z in G ; ::_thesis: x in Z
then  y /\ Z in INTERSECTION (F,G) by A3, SETFAM_1:def_5;
then  x in y /\ Z by A6, SETFAM_1:def_1;
hence  x in Z by XBOOLE_0:def_4; ::_thesis: verum
end;
then A7: x in meet G by A2, SETFAM_1:def_1;
 for Z being set st Z in F holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in F implies x in Z )
assume  Z in F ; ::_thesis: x in Z
then  Z /\ z in INTERSECTION (F,G) by A4, SETFAM_1:def_5;
then  x in Z /\ z by A6, SETFAM_1:def_1;
hence  x in Z by XBOOLE_0:def_4; ::_thesis: verum
end;
then  x in meet F by A1, SETFAM_1:def_1;
hence  x in (meet F) /\ (meet G) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
A8: y /\ z in INTERSECTION (F,G) by A3, A4, SETFAM_1:def_5;
 (meet F) /\ (meet G) c= meet (INTERSECTION (F,G))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (meet F) /\ (meet G) or x in meet (INTERSECTION (F,G)) )
assume  x in (meet F) /\ (meet G) ; ::_thesis: x in meet (INTERSECTION (F,G))
then A9: ( x in meet F & x in meet G ) by XBOOLE_0:def_4;
 for Z being set st Z in INTERSECTION (F,G) holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in INTERSECTION (F,G) implies x in Z )
assume  Z in INTERSECTION (F,G) ; ::_thesis: x in Z
then consider Z1, Z2 being set  such that
A10: ( Z1 in F & Z2 in G ) and
A11: Z = Z1 /\ Z2 by SETFAM_1:def_5;
 ( x in Z1 & x in Z2 ) by A9, A10, SETFAM_1:def_1;
hence  x in Z by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  x in meet (INTERSECTION (F,G)) by A8, SETFAM_1:def_1; ::_thesis: verum
end;
hence  (meet F) /\ (meet G) = meet (INTERSECTION (F,G)) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;

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 & b1 is G_delta )
proof
let S be Subset of T; ::_thesis: ( S is empty implies ( S is F_sigma & S is G_delta ) )
assume  S is empty ; ::_thesis: ( S is F_sigma & S is G_delta )
then A1: S = {} T ;
thus  S is F_sigma ::_thesis: S is G_delta
proof
reconsider E = {} as empty Subset-Family of T by Th18;
 {} T = union E by ZFMISC_1:2;
hence  S is F_sigma by Def6, A1; ::_thesis: verum
end;
reconsider F = {({} T)} as Subset-Family of T ;
 ( F is open & {} T = meet F ) by Th19, SETFAM_1:10;
hence  S is G_delta by Def7, A1; ::_thesis: verum
end;
end;

theorem Th35: :: TOPGEN_4:35
for T being non empty TopSpace holds [#] T is F_sigma
proof
let T be non empty TopSpace; ::_thesis: [#] T is F_sigma
reconsider F = {([#] T)} as Subset-Family of T ;
 ( F is closed & [#] T = union F ) by Th20, ZFMISC_1:25;
hence  [#] T is F_sigma by Def6; ::_thesis: verum
end;

theorem Th36: :: TOPGEN_4:36
for T being non empty TopSpace holds [#] T is G_delta
proof
let T be non empty TopSpace; ::_thesis: [#] T is G_delta
reconsider F = {([#] T)} as Subset-Family of T ;
 ( F is open & [#] T = meet F ) by Th19, SETFAM_1:10;
hence  [#] T is G_delta by Def7; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is F_sigma holds
A ` is G_delta
let A be Subset of T; ::_thesis: ( A is F_sigma implies A ` is G_delta )
assume  A is F_sigma ; ::_thesis: A ` is G_delta
then consider F being countable closed Subset-Family of T such that
A1: A = union F by Def6;
percases ( F <> {} or F = {} ) ;
supposeA2: F <> {} ; ::_thesis: A ` is G_delta
set G = COMPLEMENT F;
A3: COMPLEMENT F is open by TOPS_2:9;
 (union F) ` = meet (COMPLEMENT F) by A2, TOPS_2:6;
hence  A ` is G_delta by A1, A3, Def7; ::_thesis: verum
end;
suppose F = {} ; ::_thesis: A ` is G_delta
then  A ` = [#] T by A1, ZFMISC_1:2;
hence  A ` is G_delta ; ::_thesis: verum
end;
end;
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is G_delta holds
A ` is F_sigma
let A be Subset of T; ::_thesis: ( A is G_delta implies A ` is F_sigma )
assume  A is G_delta ; ::_thesis: A ` is F_sigma
then consider F being countable open Subset-Family of T such that
A1: A = meet F by Def7;
percases ( F <> {} or F = {} ) ;
supposeA2: F <> {} ; ::_thesis: A ` is F_sigma
set G = COMPLEMENT F;
A3: COMPLEMENT F is closed by TOPS_2:10;
 (meet F) ` = union (COMPLEMENT F) by A2, TOPS_2:7;
hence  A ` is F_sigma by A1, A3, Def6; ::_thesis: verum
end;
suppose F = {} ; ::_thesis: A ` is F_sigma
then  A ` = [#] T by A1, SETFAM_1:1;
hence  A ` is F_sigma ; ::_thesis: verum
end;
end;
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
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A /\ B is F_sigma
let A, B be Subset of T; ::_thesis: ( A is F_sigma & B is F_sigma implies A /\ B is F_sigma )
assume that
A1: A is F_sigma and
A2: B is F_sigma ; ::_thesis: A /\ B is F_sigma
consider F being countable closed Subset-Family of T such that
A3: A = union F by A1, Def6;
consider G being countable closed Subset-Family of T such that
A4: B = union G by A2, Def6;
reconsider H = INTERSECTION (F,G) as Subset-Family of T ;
A5: H is closed by Th21;
 ( card H c= card [:F,G:] & [:F,G:] is countable ) by Th25, CARD_4:7;
then A6: H is countable by WAYBEL12:1;
 A /\ B = union H by A3, A4, SETFAM_1:28;
hence  A /\ B is F_sigma by A5, A6, Def6; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A \/ B is F_sigma
let A, B be Subset of T; ::_thesis: ( A is F_sigma & B is F_sigma implies A \/ B is F_sigma )
assume that
A1: A is F_sigma and
A2: B is F_sigma ; ::_thesis: A \/ B is F_sigma
consider F being countable closed Subset-Family of T such that
A3: A = union F by A1, Def6;
consider G being countable closed Subset-Family of T such that
A4: B = union G by A2, Def6;
reconsider H = UNION (F,G) as Subset-Family of T ;
percases ( ( A <> {} & B <> {} ) or A = {} or B = {} ) ;
supposeA5: ( A <> {} & B <> {} ) ; ::_thesis: A \/ B is F_sigma
A6: H is closed by Th22;
 ( card H c= card [:F,G:] & [:F,G:] is countable ) by Th26, CARD_4:7;
then A7: H is countable by WAYBEL12:1;
 A \/ B = union H by A3, A4, A5, Th28, ZFMISC_1:2;
hence  A \/ B is F_sigma by A6, A7, Def6; ::_thesis: verum
end;
suppose A = {} ; ::_thesis: A \/ B is F_sigma
hence  A \/ B is F_sigma by A2; ::_thesis: verum
end;
suppose B = {} ; ::_thesis: A \/ B is F_sigma
hence  A \/ B is F_sigma by A1; ::_thesis: verum
end;
end;
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
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is G_delta & B is G_delta holds
A \/ B is G_delta
let A, B be Subset of T; ::_thesis: ( A is G_delta & B is G_delta implies A \/ B is G_delta )
assume that
A1: A is G_delta and
A2: B is G_delta ; ::_thesis: A \/ B is G_delta
consider F being countable open Subset-Family of T such that
A3: A = meet F by A1, Def7;
consider G being countable open Subset-Family of T such that
A4: B = meet G by A2, Def7;
reconsider H = UNION (F,G) as Subset-Family of T ;
percases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
supposeA5: ( F <> {} & G <> {} ) ; ::_thesis: A \/ B is G_delta
A6: meet (UNION (F,G)) c= (meet F) \/ (meet G) by Th32;
 (meet F) \/ (meet G) c= meet (UNION (F,G)) by A5, SETFAM_1:29;
then A7: A \/ B = meet H by A3, A4, A6, XBOOLE_0:def_10;
 ( card H c= card [:F,G:] & [:F,G:] is countable ) by Th26, CARD_4:7;
then A8: H is countable by WAYBEL12:1;
 H is open by Th24;
hence  A \/ B is G_delta by A7, A8, Def7; ::_thesis: verum
end;
suppose ( F = {} or G = {} ) ; ::_thesis: A \/ B is G_delta
then  ( A = {} or B = {} ) by A3, A4, SETFAM_1:def_1;
hence  A \/ B is G_delta by A1, A2; ::_thesis: verum
end;
end;
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
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is G_delta & B is G_delta holds
A /\ B is G_delta
let A, B be Subset of T; ::_thesis: ( A is G_delta & B is G_delta implies A /\ B is G_delta )
assume that
A1: A is G_delta and
A2: B is G_delta ; ::_thesis: A /\ B is G_delta
consider F being countable open Subset-Family of T such that
A3: A = meet F by A1, Def7;
consider G being countable open Subset-Family of T such that
A4: B = meet G by A2, Def7;
reconsider H = INTERSECTION (F,G) as Subset-Family of T ;
percases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
supposeA5: ( F <> {} & G <> {} ) ; ::_thesis: A /\ B is G_delta
A6: H is open by Th23;
 ( card H c= card [:F,G:] & [:F,G:] is countable ) by Th25, CARD_4:7;
then A7: H is countable by WAYBEL12:1;
 A /\ B = meet H by A3, A4, A5, Th34;
hence  A /\ B is G_delta by A6, A7, Def7; ::_thesis: verum
end;
suppose ( F = {} or G = {} ) ; ::_thesis: A /\ B is G_delta
then  ( A = {} or B = {} ) by A3, A4, SETFAM_1:def_1;
then  A /\ B = {} T ;
hence  A /\ B is G_delta ; ::_thesis: verum
end;
end;
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is closed holds
A is F_sigma
let A be Subset of T; ::_thesis: ( A is closed implies A is F_sigma )
assume  A is closed ; ::_thesis: A is F_sigma
then reconsider F = {A} as countable closed Subset-Family of T by Th20;
take  F ; :: according to TOPGEN_4:def_6 ::_thesis: A = union F
thus  A = union F by ZFMISC_1:25; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is open holds
A is G_delta
let A be Subset of T; ::_thesis: ( A is open implies A is G_delta )
assume  A is open ; ::_thesis: A is G_delta
then reconsider F = {A} as countable open Subset-Family of T by Th19;
take  F ; :: according to TOPGEN_4:def_7 ::_thesis: A = meet F
thus  A = meet F by SETFAM_1:10; ::_thesis: verum
end;

theorem :: TOPGEN_4:45
for A being Subset of R^1 st A = RAT holds
A is F_sigma
proof
defpred S1[ set ] means  ex a being Element of RAT st a = $1;
defpred S2[ set ] means  ex a being Element of RAT st {a} = $1;
let A be Subset of R^1; ::_thesis: ( A = RAT implies A is F_sigma )
 ex F being set st
for x being set holds
( x in F iff ( x in bool RAT & S2[x] ) ) from XBOOLE_0:sch_1();
then consider F being set  such that
A1: for x being set holds
( x in F iff ( x in bool RAT & S2[x] ) ) ;
A2: bool RAT c= bool REAL by NUMBERS:12, ZFMISC_1:67;
 F c= bool the carrier of R^1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in bool the carrier of R^1 )
assume  x in F ; ::_thesis: x in bool the carrier of R^1
then  x in bool RAT by A1;
hence  x in bool the carrier of R^1 by A2, TOPMETR:17; ::_thesis: verum
end;
then reconsider F = F as Subset-Family of R^1 ;
assume A3: A = RAT ; ::_thesis: A is F_sigma
 ex F being Subset-Family of R^1 st
( F is closed & F is countable & A = union F )
proof
take  F ; ::_thesis: ( F is closed & F is countable & A = union F )
 for B being Subset of R^1 st B in F holds
B is closed
proof
let B be Subset of R^1; ::_thesis: ( B in F implies B is closed )
assume  B in F ; ::_thesis: B is closed
then  ex a being Element of RAT st {a} = B by A1;
hence  B is closed ; ::_thesis: verum
end;
hence  F is closed by TOPS_2:def_2; ::_thesis: ( F is countable & A = union F )
A4: F =  {  {x} where x is Element of RAT : S1[x]  }
proof
thus  F c=  {  {x} where x is Element of RAT : S1[x]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  {x} where x is Element of RAT : S1[x]  }  c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F or y in  {  {x} where x is Element of RAT : S1[x]  }  )
assume  y in F ; ::_thesis: y in  {  {x} where x is Element of RAT : S1[x]  }
then  S2[y] by A1;
hence  y in  {  {x} where x is Element of RAT : S1[x]  }  ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  {x} where x is Element of RAT : S1[x]  }  or y in F )
assume  y in  {  {x} where x is Element of RAT : S1[x]  }  ; ::_thesis: y in F
then  ex z being Element of RAT st
( y = {z} & S1[z] ) ;
hence  y in F by A1; ::_thesis: verum
end;
  {  {x} where x is Element of RAT : S1[x]  }  is countable from TOPGEN_4:sch_1();
hence  F is countable by A4; ::_thesis: A = union F
thus  A c= union F :: according to XBOOLE_0:def_10 ::_thesis: union F c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union F )
assume  x in A ; ::_thesis: x in union F
then reconsider x = x as Element of RAT by A3;
 ( {x} in F & x in {x} ) by A1, TARSKI:def_1;
hence  x in union F by TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in A )
assume  x in union F ; ::_thesis: x in A
then consider Y being set  such that
A5: x in Y and
A6: Y in F by TARSKI:def_4;
 ex a being Element of RAT st {a} = Y by A1, A6;
hence  x in A by A3, A5; ::_thesis: verum
end;
hence  A is F_sigma by Def6; ::_thesis: verum
end;

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
proof
let T be TopSpace; ::_thesis: ( T is T_1 implies T is T_1/2 )
assume A1: T is T_1 ; ::_thesis: T is T_1/2
 for A being Subset of T holds Der A is closed
proof
let A be Subset of T; ::_thesis: Der A is closed
 Der A = Cl (Der A) by A1, TOPGEN_1:33;
hence  Der A is closed ; ::_thesis: verum
end;
hence  T is T_1/2 by Def8; ::_thesis: verum
end;

theorem Th47: :: TOPGEN_4:47
for T being non empty TopSpace st T is T_1/2 holds
T is T_0
proof
let T be non empty TopSpace; ::_thesis: ( T is T_1/2 implies T is T_0 )
assume A1: T is T_1/2 ; ::_thesis: T is T_0
now__::_thesis:_for_x,_y_being_Point_of_T_st_x_<>_y_&_x_in_Cl_{y}_holds_
not_y_in_Cl_{x}
let x, y be Point of T; ::_thesis: ( x <> y & x in Cl {y} implies not y in Cl {x} )
assume A2: x <> y ; ::_thesis: ( x in Cl {y} implies not y in Cl {x} )
assume that
A3: x in Cl {y} and
A4: y in Cl {x} ; ::_thesis: contradiction
 ex G being Subset of T st
( G is open & y in G & not {x} meets G )
proof
set X = (Der {x}) ` ;
 not x in Der {x}
proof
set U = the a_neighborhood of x;
consider V being Subset of T such that
A5: V is open and
 V c= the a_neighborhood of x and
A6: x in V by CONNSP_2:6;
assume  x in Der {x} ; ::_thesis: contradiction
then consider z being Point of T such that
A7: z in {x} /\ V and
A8: x <> z by A5, A6, TOPGEN_1:17;
 z in {x} by A7, XBOOLE_0:def_4;
hence  contradiction by A8, TARSKI:def_1; ::_thesis: verum
end;
then A9: x in (Der {x}) ` by SUBSET_1:29;
assume A10: for G being Subset of T st G is open & y in G holds
{x} meets G ; ::_thesis: contradiction
 for U being open Subset of T st y in U holds
ex r being Point of T st
( r in {x} /\ U & y <> r )
proof
let U be open Subset of T; ::_thesis: ( y in U implies ex r being Point of T st
( r in {x} /\ U & y <> r ) )
assume  y in U ; ::_thesis: ex r being Point of T st
( r in {x} /\ U & y <> r )
then  {x} meets U by A10;
then A11: x in U by ZFMISC_1:50;
 x in {x} by TARSKI:def_1;
then  x in {x} /\ U by A11, XBOOLE_0:def_4;
hence  ex r being Point of T st
( r in {x} /\ U & y <> r ) by A2; ::_thesis: verum
end;
then  y in Der {x} by TOPGEN_1:17;
then A12: not y in (Der {x}) ` by XBOOLE_0:def_5;
 Der {x} is closed by A1, Def8;
then  {y} meets (Der {x}) ` by A3, A9, PRE_TOPC:24;
hence  contradiction by A12, ZFMISC_1:50; ::_thesis: verum
end;
hence  contradiction by A4, PRE_TOPC:24; ::_thesis: verum
end;
hence  T is T_0 by TSP_1:def_6; ::_thesis: verum
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
let T be TopSpace; ::_thesis: ( T is T_1/2 implies T is T_0 )
percases ( not T is empty or T is empty ) ;
suppose not T is empty ; ::_thesis: ( T is T_1/2 implies T is T_0 )
then reconsider T9 = T as non empty TopSpace ;
assume  T is T_1/2 ; ::_thesis: T is T_0
then  T9 is T_1/2 ;
hence  T is T_0 by Th47; ::_thesis: verum
end;
suppose T is empty ; ::_thesis: ( T is T_1/2 implies T is T_0 )
then reconsider T9 = T as empty TopSpace ;
 T9 is T_0 ;
hence  ( T is T_1/2 implies T is T_0 ) ; ::_thesis: verum
end;
end;
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

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 & A c= B holds
x is_a_condensation_point_of B
proof
let T be non empty TopSpace; ::_thesis: 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
let A, B be Subset of T; ::_thesis: 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
let x be Point of T; ::_thesis: ( x is_a_condensation_point_of A & A c= B implies x is_a_condensation_point_of B )
assume that
A1: x is_a_condensation_point_of A and
A2: A c= B ; ::_thesis: x is_a_condensation_point_of B
 for N being a_neighborhood of x holds not N /\ B is countable
proof
let N be a_neighborhood of x; ::_thesis: not N /\ B is countable
 N /\ A c= N /\ B by A2, XBOOLE_1:26;
hence  not N /\ B is countable by A1, Def9; ::_thesis: verum
end;
hence  x is_a_condensation_point_of B by Def9; ::_thesis: verum
end;

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 )
proof
defpred S1[ Point of T] means $1 is_a_condensation_point_of A;
 ex X being Subset of T st
for x being Element of T holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
hence  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 ) ; ::_thesis: verum
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
defpred S1[ Point of T] means $1 is_a_condensation_point_of A;
let A1, A2 be Subset of T; ::_thesis: ( ( for x being Point of T holds
( x in A1 iff x is_a_condensation_point_of A ) ) & ( for x being Point of T holds
( x in A2 iff x is_a_condensation_point_of A ) ) implies A1 = A2 )
assume that
A1: for x being Element of T holds
( x in A1 iff S1[x] ) and
A2: for x being Element of T holds
( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2
thus  A1 = A2 from SUBSET_1:sch_2(A1, A2); ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: 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
let A be Subset of T; ::_thesis: for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
let p be Point of T; ::_thesis: ( p is_a_condensation_point_of A implies p is_an_accumulation_point_of A )
assume A1: p is_a_condensation_point_of A ; ::_thesis: p is_an_accumulation_point_of A
 for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U )
proof
let U be open Subset of T; ::_thesis: ( p in U implies ex q being Point of T st
( q <> p & q in A & q in U ) )
assume  p in U ; ::_thesis: ex q being Point of T st
( q <> p & q in A & q in U )
then reconsider N = U as a_neighborhood of p by CONNSP_2:3;
reconsider NU = N /\ A as non empty non countable set by A1, Def9;
consider q being Element of NU such that
A2: p <> q by BORSUK_4:2;
 q in NU ;
then reconsider q = q as Point of T ;
 ( q in A & q in U ) by XBOOLE_0:def_4;
hence  ex q being Point of T st
( q <> p & q in A & q in U ) by A2; ::_thesis: verum
end;
hence  p is_an_accumulation_point_of A by TOPGEN_1:21; ::_thesis: verum
end;

theorem :: TOPGEN_4:50
for T being non empty TopSpace
for A being Subset of T holds A ^0 c= Der A
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds A ^0 c= Der A
let A be Subset of T; ::_thesis: A ^0 c= Der A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^0 or x in Der A )
assume A1: x in A ^0 ; ::_thesis: x in Der A
then reconsider p = x as Point of T ;
 p is_a_condensation_point_of A by A1, Def10;
then  p is_an_accumulation_point_of A by Th49;
hence  x in Der A by TOPGEN_1:16; ::_thesis: verum
end;

theorem :: TOPGEN_4:51
for T being non empty TopSpace
for A being Subset of T holds A ^0 = Cl (A ^0)
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds A ^0 = Cl (A ^0)
let A be Subset of T; ::_thesis: A ^0 = Cl (A ^0)
thus  A ^0 c= Cl (A ^0) by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl (A ^0) c= A ^0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (A ^0) or x in A ^0 )
assume A1: x in Cl (A ^0) ; ::_thesis: x in A ^0
then reconsider p = x as Point of T ;
 for N being a_neighborhood of p holds not N /\ A is countable
proof
let N be a_neighborhood of p; ::_thesis: not N /\ A is countable
consider N1 being Subset of T such that
A2: N1 is open and
A3: N1 c= N and
A4: p in N1 by CONNSP_2:6;
 A ^0 meets N1 by A1, A2, A4, PRE_TOPC:24;
then consider y being set  such that
A5: y in A ^0 and
A6: y in N1 by XBOOLE_0:3;
reconsider y9 = y as Point of T by A5;
reconsider N1 = N1 as a_neighborhood of y9 by A2, A6, CONNSP_2:6;
A7: N1 /\ A c= N /\ A by A3, XBOOLE_1:26;
 y9 is_a_condensation_point_of A by A5, Def10;
hence  not N /\ A is countable by A7, Def9; ::_thesis: verum
end;
then  p is_a_condensation_point_of A by Def9;
hence  x in A ^0 by Def10; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A c= B holds
A ^0 c= B ^0
let A, B be Subset of T; ::_thesis: ( A c= B implies A ^0 c= B ^0 )
assume A1: A c= B ; ::_thesis: A ^0 c= B ^0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^0 or x in B ^0 )
assume A2: x in A ^0 ; ::_thesis: x in B ^0
then reconsider x9 = x as Point of T ;
 x9 is_a_condensation_point_of A by A2, Def10;
then  x9 is_a_condensation_point_of B by A1, Th48;
hence  x in B ^0 by Def10; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: 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 )
let A, B be Subset of T; ::_thesis: 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 )
let x be Point of T; ::_thesis: ( 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 )
assume A1: x is_a_condensation_point_of A \/ B ; ::_thesis: ( x is_a_condensation_point_of A or x is_a_condensation_point_of B )
assume that
A2: not x is_a_condensation_point_of A and
A3: not x is_a_condensation_point_of B ; ::_thesis: contradiction
consider N1 being a_neighborhood of x such that
A4: N1 /\ A is countable by A2, Def9;
consider N2 being a_neighborhood of x such that
A5: N2 /\ B is countable by A3, Def9;
reconsider N3 = N1 /\ N2 as a_neighborhood of x by CONNSP_2:2;
 ( N3 /\ A c= N1 /\ A & N3 /\ B c= N2 /\ B ) by XBOOLE_1:17, XBOOLE_1:26;
then  (N3 /\ A) \/ (N3 /\ B) is countable by A4, A5, CARD_2:85;
then  N3 /\ (A \/ B) is countable by XBOOLE_1:23;
hence  contradiction by A1, Def9; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T holds (A \/ B) ^0 = (A ^0) \/ (B ^0)
let A, B be Subset of T; ::_thesis: (A \/ B) ^0 = (A ^0) \/ (B ^0)
thus  (A \/ B) ^0 c= (A ^0) \/ (B ^0) :: according to XBOOLE_0:def_10 ::_thesis: (A ^0) \/ (B ^0) c= (A \/ B) ^0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \/ B) ^0 or x in (A ^0) \/ (B ^0) )
assume A1: x in (A \/ B) ^0 ; ::_thesis: x in (A ^0) \/ (B ^0)
then reconsider x9 = x as Point of T ;
 x9 is_a_condensation_point_of A \/ B by A1, Def10;
then  ( x9 is_a_condensation_point_of A or x9 is_a_condensation_point_of B ) by Th53;
then  ( x9 in A ^0 or x9 in B ^0 ) by Def10;
hence  x in (A ^0) \/ (B ^0) by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( A ^0 c= (A \/ B) ^0 & B ^0 c= (A \/ B) ^0 ) by Th52, XBOOLE_1:7;
hence  (A ^0) \/ (B ^0) c= (A \/ B) ^0 by XBOOLE_1:8; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: 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
let A be Subset of T; ::_thesis: ( A is countable implies for x being Point of T holds not x is_a_condensation_point_of A )
assume A1: A is countable ; ::_thesis: for x being Point of T holds not x is_a_condensation_point_of A
given x being Point of T such that A2: x is_a_condensation_point_of A ; ::_thesis: contradiction
set N = the a_neighborhood of x;
 not the a_neighborhood of x /\ A is countable by A2, Def9;
hence  contradiction by A1, CARD_3:94; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for A being Subset of T st A is countable holds
A ^0 = {}
let A be Subset of T; ::_thesis: ( A is countable implies A ^0 = {} )
assume A1: A is countable ; ::_thesis: A ^0 = {}
assume  A ^0 <> {} ; ::_thesis: contradiction
then consider x being set  such that
A2: x in A ^0 by XBOOLE_0:def_1;
reconsider x9 = x as Point of T by A2;
 x9 is_a_condensation_point_of A by A2, Def10;
hence  contradiction by A1, Th55; ::_thesis: verum
end;

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
proof
let T be non empty TopSpace; ::_thesis: ( T is second-countable implies ex B being Basis of T st B is countable )
set B = the Basis of T;
consider B1 being Basis of T such that
 B1 c= the Basis of T and
A1: card B1 = weight T by TOPGEN_2:18;
assume  T is second-countable ; ::_thesis: ex B being Basis of T st B is countable
then  card B1 c= omega by A1, WAYBEL23:def_6;
then  card (card B1) c= card omega by CARD_1:11;
then  B1 is countable by WAYBEL12:1;
hence  ex B being Basis of T st B is countable ; ::_thesis: verum
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
set T = the non empty finite TopSpace;
take  the non empty finite TopSpace ; ::_thesis: ( the non empty finite TopSpace is second-countable & not the non empty finite TopSpace is empty )
thus  ( the non empty finite TopSpace is second-countable & not the non empty finite TopSpace is empty ) ; ::_thesis: verum
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
thus  not TotFam T is empty ; ::_thesis: ( TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
thus  TotFam T is all-open-containing ::_thesis: ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions )
proof
let A be Subset of T; :: according to TOPGEN_4:def_2 ::_thesis: ( A is open implies A in TotFam T )
assume  A is open ; ::_thesis: A in TotFam T
thus  A in TotFam T ; ::_thesis: verum
end;
 for A being Subset of T st A in TotFam T holds
A ` in TotFam T ;
hence  TotFam T is compl-closed by PROB_1:def_1; ::_thesis: TotFam T is closed_for_countable_unions
 for G being countable Subset-Family of T st G c= TotFam T holds
union G in TotFam T ;
hence  TotFam T is closed_for_countable_unions by Def4; ::_thesis: verum
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
let T be set ; ::_thesis: for A being SetSequence of T holds rng A is non empty countable Subset-Family of T
let A be SetSequence of T; ::_thesis: rng A is non empty countable Subset-Family of T
 A . 1 in rng A by FUNCT_2:4;
then reconsider AA = rng A as non empty Subset-Family of T ;
 ( card (rng A) c= card (dom A) & dom A is countable ) by CARD_2:61, FUNCT_2:def_1;
then  AA is countable by WAYBEL12:1;
hence  rng A is non empty countable Subset-Family of T ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is all-open-containing & F c= G holds
G is all-open-containing
let F, G be Subset-Family of T; ::_thesis: ( F is all-open-containing & F c= G implies G is all-open-containing )
assume that
A1: F is all-open-containing and
A2: F c= G ; ::_thesis: G is all-open-containing
 for A being Subset of T st A is open holds
A in G
proof
let A be Subset of T; ::_thesis: ( A is open implies A in G )
assume  A is open ; ::_thesis: A in G
then  A in F by A1, Def2;
hence  A in G by A2; ::_thesis: verum
end;
hence  G is all-open-containing by Def2; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds
G is all-closed-containing
let F, G be Subset-Family of T; ::_thesis: ( F is all-closed-containing & F c= G implies G is all-closed-containing )
assume that
A1: F is all-closed-containing and
A2: F c= G ; ::_thesis: G is all-closed-containing
 for A being Subset of T st A is closed holds
A in G
proof
let A be Subset of T; ::_thesis: ( A is closed implies A in G )
assume  A is closed ; ::_thesis: A in G
then  A in F by A1, Def3;
hence  A in G by A2; ::_thesis: verum
end;
hence  G is all-closed-containing by Def3; ::_thesis: verum
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
take  TotFam T ; ::_thesis: ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions & TotFam T is closed_for_countable_meets & TotFam T is all-closed-containing & TotFam T is all-open-containing )
thus  ( TotFam T is compl-closed & TotFam T is closed_for_countable_unions & TotFam T is closed_for_countable_meets & TotFam T is all-closed-containing & TotFam T is all-open-containing ) ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: ( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
set E = sigma (TotFam T);
 TotFam T c= sigma (TotFam T) by PROB_1:def_9;
hence  sigma (TotFam T) is all-open-containing by Th59; ::_thesis: ( sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )
thus  sigma (TotFam T) is compl-closed ; ::_thesis: sigma (TotFam T) is closed_for_countable_unions
thus  sigma (TotFam T) is closed_for_countable_unions ; ::_thesis: verum
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
take  sigma (TotFam T) ; ::_thesis: ( sigma (TotFam T) is sigma-additive & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions & not sigma (TotFam T) is empty )
thus  ( sigma (TotFam T) is sigma-additive & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions & not sigma (TotFam T) is empty ) ; ::_thesis: verum
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
take  sigma (TotFam T) ; ::_thesis: sigma (TotFam T) is all-open-containing
thus  sigma (TotFam T) is all-open-containing ; ::_thesis: verum
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
set E = Topology_of T;
thus  Topology_of T is open ; ::_thesis: Topology_of T is all-open-containing
 Topology_of T is all-open-containing
proof
let A be Subset of T; :: according to TOPGEN_4:def_2 ::_thesis: ( A is open implies A in Topology_of T )
assume  A is open ; ::_thesis: A in Topology_of T
hence  A in Topology_of T by PRE_TOPC:def_2; ::_thesis: verum
end;
hence  Topology_of T is all-open-containing ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: 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 ) )
let X be Subset-Family of T; ::_thesis: 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 ) )
set V =  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ;
set Y = meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ;
A1: now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
X_c=_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  implies X c= Z )
assume  Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: X c= Z
then  ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
hence  X c= Z ; ::_thesis: verum
end;
A2: bool the carrier of T in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }
proof
set X1 = TotFam T;
 TotFam T in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ;
hence  bool the carrier of T in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: verum
end;
A3: for E being Subset of T st E in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  holds
E ` in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }
proof
let E be Subset of T; ::_thesis: ( E in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  implies E ` in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  )
assume A4: E in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: E ` in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
E_`_in_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  implies E ` in Z )
assume  Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: E ` in Z
then  ( E in Z & ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ) by A4, SETFAM_1:def_1;
hence  E ` in Z by PROB_1:def_1; ::_thesis: verum
end;
hence  E ` in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  by A2, SETFAM_1:def_1; ::_thesis: verum
end;
A5: for BSeq being SetSequence of the carrier of T st rng BSeq c= meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  holds
Intersection BSeq in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }
proof
let BSeq be SetSequence of the carrier of T; ::_thesis: ( rng BSeq c= meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  implies Intersection BSeq in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  )
assume A6: rng BSeq c= meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: Intersection BSeq in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
Intersection_BSeq_in_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  implies Intersection BSeq in Z )
assume A7: Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: Intersection BSeq in Z
then consider S being Subset-Family of T such that
A8: Z = S and
 X c= S and
A9: S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ;
now__::_thesis:_for_n_being_Nat_holds_BSeq_._n_in_Z
let n be Nat; ::_thesis: BSeq . n in Z
 BSeq . n in rng BSeq by NAT_1:51;
hence  BSeq . n in Z by A6, A7, SETFAM_1:def_1; ::_thesis: verum
end;
then A10: rng BSeq c= Z by NAT_1:52;
 S is SigmaField of T by A9, Th13;
hence  Intersection BSeq in Z by A8, A10, PROB_1:def_6; ::_thesis: verum
end;
hence  Intersection BSeq in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  by A2, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_Z_being_set_st_Z_in__{__S_where_S_is_Subset-Family_of_T_:_(_X_c=_S_&_S_is_compl-closed_all-open-containing_closed_for_countable_unions_Subset-Family_of_T_)__}__holds_
{}_in_Z
let Z be set ; ::_thesis: ( Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  implies {} in Z )
assume  Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: {} in Z
then  ex S being Subset-Family of T st
( Z = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
then  Z is Field_Subset of the carrier of T by Th13;
hence  {} in Z by PROB_1:4; ::_thesis: verum
end;
then  {} in meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  by A2, SETFAM_1:def_1;
then reconsider Y = meet  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  as SigmaField of T by A2, A5, A3, PROB_1:15, SETFAM_1:3;
 for A being Subset of T st A is open holds
A in Y
proof
let A be Subset of T; ::_thesis: ( A is open implies A in Y )
assume A11: A is open ; ::_thesis: A in Y
 for Y being set st Y in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  holds
A in Y
proof
let Y be set ; ::_thesis: ( Y in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  implies A in Y )
assume  Y in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  ; ::_thesis: A in Y
then  ex S being Subset-Family of the carrier of T st
( Y = S & X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ) ;
hence  A in Y by A11, Def2; ::_thesis: verum
end;
hence  A in Y by A2, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider Y = Y as compl-closed all-open-containing closed_for_countable_unions Subset-Family of T by Def2;
take  Y ; ::_thesis: ( 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 ) )
 for Z being set st X c= Z & Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds
Y c= Z
proof
let Z be set ; ::_thesis: ( X c= Z & Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T implies Y c= Z )
assume that
A12: X c= Z and
A13: Z is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T ; ::_thesis: Y c= Z
reconsider Z = Z as Subset-Family of T by A13;
 Z in  {  S where S is Subset-Family of T : ( X c= S & S is compl-closed all-open-containing closed_for_countable_unions Subset-Family of T )  }  by A12, A13;
hence  Y c= Z by SETFAM_1:3; ::_thesis: verum
end;
hence  ( 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 ) ) by A2, A1, SETFAM_1:5; ::_thesis: verum
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
reconsider E = {} as Subset-Family of T by Th18;
consider Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T such that
 E c= Y and
A1: for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st E c= Z holds
Y c= Z by Th63;
take  Y ; ::_thesis: for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds Y c= G
let G be compl-closed all-open-containing closed_for_countable_unions Subset-Family of T; ::_thesis: Y c= G
thus  Y c= G by A1, XBOOLE_1:2; ::_thesis: verum
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
let R1, R2 be compl-closed all-open-containing closed_for_countable_unions Subset-Family of T; ::_thesis: ( ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R2 c= G ) implies R1 = R2 )
assume  ( ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R2 c= G ) ) ; ::_thesis: R1 = R2
then  ( R1 c= R2 & R2 c= R1 ) ;
hence  R1 = R2 by XBOOLE_0:def_10; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F being closed Subset-Family of T holds F c= BorelSets T
let F be closed Subset-Family of T; ::_thesis: F c= BorelSets T
 F c= BorelSets T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in BorelSets T )
assume A1: x in F ; ::_thesis: x in BorelSets T
then reconsider xx = x as Subset of T ;
 xx is closed by A1, TOPS_2:def_2;
hence  x in BorelSets T by Def3; ::_thesis: verum
end;
hence  F c= BorelSets T ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for F being open Subset-Family of T holds F c= BorelSets T
let F be open Subset-Family of T; ::_thesis: F c= BorelSets T
 F c= BorelSets T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in BorelSets T )
assume A1: x in F ; ::_thesis: x in BorelSets T
then reconsider xx = x as Subset of T ;
 xx is open by A1, TOPS_2:def_1;
hence  x in BorelSets T by Def2; ::_thesis: verum
end;
hence  F c= BorelSets T ; ::_thesis: verum
end;

theorem :: TOPGEN_4:66
for T being non empty TopSpace holds BorelSets T = sigma (Topology_of T)
proof
let T be non empty TopSpace; ::_thesis: BorelSets T = sigma (Topology_of T)
reconsider BT = BorelSets T as SigmaField of T by Th13;
set X = Topology_of T;
A1: for Z being set st Topology_of T c= Z & Z is SigmaField of T holds
BT c= Z
proof
let Z be set ; ::_thesis: ( Topology_of T c= Z & Z is SigmaField of T implies BT c= Z )
assume that
A2: Topology_of T c= Z and
A3: Z is SigmaField of T ; ::_thesis: BT c= Z
reconsider Z9 = Z as SigmaField of T by A3;
 Z9 is all-open-containing by A2, Th59;
hence  BT c= Z by Def11; ::_thesis: verum
end;
 Topology_of T c= BT by Th65;
hence  BorelSets T = sigma (Topology_of T) by A1, PROB_1:def_9; ::_thesis: verum
end;

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
proof
let A be Subset of T; ::_thesis: ( A is F_sigma implies A is Borel )
assume  A is F_sigma ; ::_thesis: A is Borel
then consider F being countable closed Subset-Family of T such that
A1: A = union F by Def6;
 F c= BorelSets T by Th64;
then  A in BorelSets T by A1, Def4;
hence  A is Borel by Def12; ::_thesis: verum
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
let A be Subset of T; ::_thesis: ( A is G_delta implies A is Borel )
assume  A is G_delta ; ::_thesis: A is Borel
then consider F being countable open Subset-Family of T such that
A1: A = meet F by Def7;
 F c= BorelSets T by Th65;
then  A in BorelSets T by A1, Def5;
hence  A is Borel by Def12; ::_thesis: verum
end;
end;