:: On the {B}orel Families of Subsets of Topological Spaces
::  by Adam Grabowski
::
:: Received August 30, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, SETFAM_1, ZFMISC_1, CARD_3, TARSKI, NUMBERS, FUNCT_1,
      RELAT_1, CARD_1, ORDINAL1, SUBSET_1, XBOOLE_0, PRE_TOPC, TOPGEN_1,
      FINSET_1, WAYBEL23, RCOMP_1, RLVECT_3, TOPS_1, CONNSP_1, PCOMPS_1,
      NATTRA_1, PROB_1, MEASURE1, MCART_1, TOPMETR, CONNSP_2, WAYBEL30,
      OPENLATT, EQREL_1, NAT_1, TOPGEN_4;
 notations TARSKI, XBOOLE_0,
      XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, ORDINAL1,
      NUMBERS, CARD_3, MCART_1, WELLORD2, FINSET_1, SETFAM_1, DOMAIN_1,
      CONNSP_2, ZFMISC_1, STRUCT_0, OPENLATT, MEASURE1, PRE_TOPC, TOPS_1,
      TOPS_2, CONNSP_1, TDLAT_3, WAYBEL23, PROB_1, TOPMETR, CANTOR_1, ORDERS_4,
      TOPGEN_1, TOPGEN_3, PCOMPS_1;
 constructors MEASURE1, TOPS_1, CONNSP_1, COMPTS_1, TDLAT_3, TOPMETR, OPENLATT,
      WAYBEL23, TOPGEN_2, ORDERS_4, TOPGEN_1, TOPGEN_3, PCOMPS_1, XTUPLE_0;
 registrations SUBSET_1, RELSET_1, FINSET_1, NUMBERS, CARD_1, MEASURE1,
      STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TOPMETR, TOPREAL6, TOPGEN_2,
      TOPGEN_1, CARD_3, COMPTS_1, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, CARD_3, MEASURE1, SUBSET_1, STRUCT_0, OPENLATT,
      XTUPLE_0;
 theorems TARSKI, SETFAM_1, FUNCT_1, FUNCT_2, ZFMISC_1, PRE_TOPC, TOPS_1,
      XBOOLE_1, SUBSET_1, YELLOW_8, WAYBEL23, TOPMETR, NUMBERS, CONNSP_1,
      CONNSP_2, CARD_4, CARD_1, PCOMPS_1, XBOOLE_0, TOPGEN_1, TOPS_2, MEASURE1,
      WAYBEL12, MCART_1, BORSUK_4, TSP_1, TOPGEN_2, TOPGEN_3, PROB_1, CARD_2,
      TOPS_3, NAT_1, CARD_3;
 schemes FUNCT_1, TREES_2, BORSUK_2, SUBSET_1, XBOOLE_0;

begin :: Preliminaries

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

theorem Th1:
  for T being set, F being Subset-Family of T holds F is countable
  iff COMPLEMENT F is countable
proof
  let T be set, F be Subset-Family of T;
  F, COMPLEMENT F are_equipotent by YELLOW_8:3;
  hence thesis by YELLOW_8:4;
end;

registration
  cluster RAT -> countable;
  coherence 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;
  thus X is countable implies ex f be Function st dom f = RAT & X c= rng f
  proof
    assume card X c= omega;
    hence thesis by CARD_1:12,TOPGEN_3:17;
  end;
  assume ex f be Function st dom f = RAT & X c= rng f;
  hence card X c= omega by CARD_1:12,TOPGEN_3:17;
end;

scheme FraenCoun11 { P[set] } :
  { {n} where n is Element of RAT : P[n] } is countable
  proof
  deffunc g(set) = { $1 };
  consider f being Function such that
A1: dom f = RAT & for x being set st x in RAT holds f.x = g(x) from
  FUNCT_1:sch 3;
  { {n} where n is Element of RAT : P[n] } c= rng f
  proof
    let x be set;
    assume x in { {n} where n is Element of RAT : P[n] };
    then consider n be Element of RAT such that
A2: x = {n} and
    P[n];
    f.n = x by A1,A2;
    hence thesis by A1,FUNCT_1:def 3;
  end;
  hence thesis by A1,Lm1;
end;

theorem
  for T being non empty TopSpace, 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, A be Subset of T;
  thus Der A c= { x where x is Point of T : x in Cl (A \ {x}) }
  proof
    let x be set;
    assume x in Der A;
    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 thesis;
  end;
  let y be set;
  assume y in { x where x is Point of T : x in Cl (A \ {x}) };
  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 thesis by A1,TOPGEN_1:def 3;
end;

registration
  cluster finite -> second-countable for TopStruct;
  coherence
  proof
    let T be TopStruct;
    assume T is finite;
    then reconsider T9 = T as finite TopStruct;
    weight T9 is finite by TOPGEN_2:def 4;
    then weight T9 c= omega;
    hence thesis by WAYBEL23:def 6;
  end;
end;

registration
  cluster REAL -> non countable;
  coherence
  proof
    assume REAL is countable;
    then card REAL c= omega by CARD_3:def 14;
    hence thesis by TOPGEN_3:30,def 4;
  end;
end;

registration
  cluster non countable -> non finite for set;
  coherence;
  cluster non finite -> non trivial for set;
  coherence;
  cluster non countable non empty for set;
  existence
  proof
    take REAL;
    thus thesis;
  end;
end;

reserve T for non empty TopSpace,
  A, B for Subset of T,
  F, G for Subset-Family of T;

theorem
  A is closed iff Der A c= A
proof
  hereby
    assume A is closed;
    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;
  end;
  assume
A2: Der A c= A;
  Cl A = A \/ Der A by TOPGEN_1:29
    .= A by A2,XBOOLE_1:12;
  hence thesis;
end;

theorem Th4:
  for T being non empty TopStruct, B being Basis of T, V being
Subset of T st V is open & V <> {} ex W being Subset of T st W in B & W c= V &
  W <> {}
proof
  let T be non empty TopStruct, B be Basis of T, V be Subset of T;
  assume that
A1: V is open and
A2: V <> {};
  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 thesis by A4;
end;

begin :: Regular Formalization: Separable Spaces
:: 1.3.7. Theorem

theorem Th5:
  density T c= weight T
proof
  defpred P[set] means $1 <> {};
  deffunc F(set) = choose $1;
  set B = the Basis of T;
  consider B1 being Basis of T such that
  B1 c= B and
A1: card B1 = weight T by TOPGEN_2:18;
  set A = { F(BB) where BB is Element of bool the carrier of T : BB in B1 & P[
  BB] };
  A c= the carrier of T
  proof
    let x be set;
    assume x in A;
    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 thesis;
  end;
  then reconsider A 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;
    assume Q <> {} & Q is open;
    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 thesis by A5,XBOOLE_0:3;
  end;
  then A is dense by TOPS_1:45;
  then
A7: density T c= card A by TOPGEN_1:def 12;
  card { F(w) where w is Element of bool the carrier of T : w in B1 & P[w
  ] } c= card B1 from BORSUK_2:sch 1;
  hence thesis by A1,A7,XBOOLE_1:1;
end;

theorem
  T is separable iff ex A being Subset of T st A is dense countable
proof
  hereby
    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;
    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 countable by A1;
  end;
  given A being Subset of T such that
A3: A is dense countable;
  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 thesis by TOPGEN_1:def 13;
end;

:: 1.3.8. Corollary

theorem Th7:
  T is second-countable implies T is separable
proof
  assume T is second-countable;
  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 thesis by TOPGEN_1:def 13;
end;

registration
  cluster second-countable -> separable for non empty TopSpace;
  coherence by Th7;
end;

:: Exercises

theorem :: Exercise 1.3.A.
  for T being non empty TopSpace, 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, A, B be Subset of T;
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;
  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;
    assume
A7: x in Fr A \/ Fr B;
    per cases by A4,A1,A7,XBOOLE_0:def 3;
    suppose
      x in Fr (A \/ B);
      hence thesis;
    end;
    suppose
A8:   x in Fr A /\ Fr 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 thesis by TOPS_1:def 2;
    end;
  end;
  Fr (A \/ B) c= Fr A \/ Fr B by TOPS_1:33;
  hence thesis by A6,XBOOLE_0:def 10;
end;

:: Exercise 1.3.B.

theorem :: Ex. 1.3.B. a)
  F is locally_finite implies Fr union F c= union Fr F
proof
  assume F is locally_finite;
  then
A1: Cl union F = union clf F by PCOMPS_1:20;
  let x be set;
  assume x in Fr union 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 thesis by A8,TARSKI:def 4;
end;

theorem Th10: :: also for empty TopSpaces
  for T being discrete non empty TopSpace holds T is separable iff
  card [#]T c= omega
proof
  let T be discrete non empty TopSpace;
  hereby
    assume T is separable;
    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;
  end;
  assume card [#]T c= omega;
  then T is countable by TOPGEN_1:2;
  hence thesis;
end;

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

begin :: Families of Subsets Closed for Countable Unions and Complement

definition
  let T, F;
  attr F is all-open-containing means
  :Def2:
  for A being Subset of T st A is open holds A in F;
end;

definition
  let T, F;
  attr F is all-closed-containing means
  :Def3:
  for A being Subset of T st A is closed holds A in F;
end;

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

Lm2: for T being set, F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
proof
  let T be set, F be Subset-Family of T;
  assume
A1: F is SigmaField of T;
  let G be countable Subset-Family of T;
  assume
A2: G c= F;
  per cases;
  suppose
    G is empty;
    hence thesis by A1,PROB_1:4,ZFMISC_1:2;
  end;
  suppose
    G is non empty;
    hence thesis by A1,A2,MEASURE1:def 5;
  end;
end;

registration
  let T be set;
  cluster -> closed_for_countable_unions for SigmaField of T;
  coherence by Lm2;
end;

theorem Th12:
  for T being set, F being Subset-Family of T st F is
  closed_for_countable_unions holds {} in F
proof
  let T be set, F be Subset-Family of T;
  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;
  hence thesis by A1,Def4,ZFMISC_1:2;
end;

registration
  let T be set;
  cluster closed_for_countable_unions -> non empty for Subset-Family of T;
  coherence by Th12;
end;

theorem Th13:
  for T being set, F being Subset-Family of T holds F is
  SigmaField of T iff F is compl-closed closed_for_countable_unions
proof
  let T be set, F be Subset-Family of T;
  thus F is SigmaField of T implies F is compl-closed
  closed_for_countable_unions;
  assume
A1: F is compl-closed closed_for_countable_unions;
  F is sigma-additive
  proof
    let M be N_Sub_set_fam of T;
    assume M c= F;
    hence thesis by A1,Def4;
  end;
  then reconsider
  F as non empty compl-closed sigma-additive Subset-Family of T by A1;
  F is SigmaField of T;
  hence thesis;
end;

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

theorem Th14:
  for F being Subset-Family of T holds F is all-closed-containing
  compl-closed iff F is all-open-containing compl-closed
proof
  let F be Subset-Family of T;
  hereby
    assume
A1: F is all-closed-containing compl-closed;
    for A being Subset of T st A is open holds A in F
    proof
      let A be Subset of T;
      assume A is open;
      then A` in F by A1,Def3;
      then A`` in F by A1,PROB_1:def 1;
      hence thesis;
    end;
    hence F is all-open-containing compl-closed by A1,Def2;
  end;
  assume
A2: F is all-open-containing compl-closed;
  for A being Subset of T st A is closed holds A in F
  proof
    let A be Subset of T;
    assume A is closed;
    then A` in F by A2,Def2;
    then A`` in F by A2,PROB_1:def 1;
    hence thesis;
  end;
  hence thesis by A2,Def3;
end;

theorem
  for T being set, F being Subset-Family of T st F is compl-closed holds
  F = COMPLEMENT F
proof
  let T be set, F be Subset-Family of T;
  assume
A1: F is compl-closed;
  thus F c= COMPLEMENT F
  proof
    let x be set;
    assume
A2: x in F;
    then reconsider x9 = x as Subset of T;
    x9` in F by A1,A2,PROB_1:def 1;
    hence thesis by SETFAM_1:def 7;
  end;
  let x be set;
  assume
A3: x in COMPLEMENT 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 thesis;
end;

theorem Th16:
  for T being set, 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, F, G be Subset-Family of T;
  assume
A1: F c= G & G is compl-closed;
  let x be set;
  assume
A2: x in COMPLEMENT F;
  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 thesis;
end;

theorem Th17:
  for T being set, F being Subset-Family of T holds F is
  closed_for_countable_meets compl-closed iff F is closed_for_countable_unions
  compl-closed
proof
  let T be set, F be Subset-Family of T;
  hereby
    assume
A1: F is closed_for_countable_meets 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;
      assume
A2:   G c= F;
      per cases;
      suppose
        G = {};
        hence thesis by A1,A2,Def5,SETFAM_1:1,ZFMISC_1:2;
      end;
      suppose
        G <> {};
        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 thesis by A1,A3,PROB_1:def 1;
      end;
    end;
    hence F is closed_for_countable_unions compl-closed by A1,Def4;
  end;
  assume
A4: F is closed_for_countable_unions 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;
    assume
A5: G c= F;
    per cases;
    suppose
      G = {};
      hence thesis by A4,A5,Def4,SETFAM_1:1,ZFMISC_1:2;
    end;
    suppose
      G <> {};
      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 thesis by A4,A6,PROB_1:def 1;
    end;
  end;
  hence thesis by A4,Def5;
end;

registration
  let T;
  cluster all-open-containing compl-closed closed_for_countable_unions ->
    all-closed-containing closed_for_countable_meets for Subset-Family of T;
  coherence by Th14,Th17;
  cluster all-closed-containing compl-closed closed_for_countable_meets ->
    all-open-containing closed_for_countable_unions for Subset-Family of T;
  coherence by Th14,Th17;
end;

begin :: On the Families of Subsets

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

registration
  let T be TopSpace;
  cluster empty -> open closed for Subset-Family of T;
  coherence
  proof
    let F be Subset-Family of T;
    assume F is empty; then
    ( for P being Subset of T holds P in F implies P is open)& for P being
    Subset of T holds P in F implies P is closed;
    hence thesis by TOPS_2:def 1,def 2;
  end;
end;

registration
  let T be TopSpace;
  cluster countable open closed for Subset-Family of T;
  existence
  proof
    {}bool the carrier of T is open;
    hence thesis;
  end;
end;

theorem Th18:
  for T being set holds {} is empty Subset-Family of T
proof
  let T be set;
  {}bool T = {};
  hence thesis;
end;

registration
  cluster empty -> countable for set;
  coherence;
end;

begin :: Collective Properties of Families

theorem Th19:
  F = { A } implies (A is open iff F is open)
proof
  assume
A1: F = { A };
  hereby
    assume A 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;
  end;
  assume
A2: F is open;
  A in F by A1,TARSKI:def 1;
  hence thesis by A2,TOPS_2:def 1;
end;

theorem Th20:
  F = { A } implies (A is closed iff F is closed)
proof
  assume
A1: F = { A };
  hereby
    assume A 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;
  end;
  assume
A2: F is closed;
  A in F by A1,TARSKI:def 1;
  hence thesis by A2,TOPS_2:def 2;
end;

definition
  let T be set, F, G be Subset-Family of T;
  redefine func INTERSECTION (F,G) -> Subset-Family of T;
  coherence
  proof
    INTERSECTION (F,G) c= bool T
    proof
      let x be set;
      assume x in INTERSECTION (F,G);
      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 thesis;
    end;
    hence thesis;
  end;
  redefine func UNION (F,G) -> Subset-Family of T;
  coherence
  proof
    UNION (F,G) c= bool T
    proof
      let x be set;
      assume x in UNION (F,G);
      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 thesis by A4;
    end;
    hence thesis;
  end;
end;

theorem Th21:
  F is closed & G is closed implies INTERSECTION (F,G) is closed
proof
  assume
A1: F is closed & 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;
    assume A in INTERSECTION (F,G);
    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, Y as Subset of T by A2;
    X is closed & Y is closed by A1,A2,TOPS_2:def 2;
    hence thesis by A3;
  end;
  hence thesis by TOPS_2:def 2;
end;

theorem Th22:
  F is closed & G is closed implies UNION (F,G) is closed
proof
  assume
A1: F is closed & 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;
    assume A in UNION (F,G);
    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, Y as Subset of T by A2;
    X is closed & Y is closed by A1,A2,TOPS_2:def 2;
    hence thesis by A3;
  end;
  hence thesis by TOPS_2:def 2;
end;

theorem Th23:
  F is open & G is open implies INTERSECTION (F,G) is open
proof
  assume
A1: F is open & 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;
    assume A in INTERSECTION (F,G);
    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, Y as Subset of T by A2;
    X is open & Y is open by A1,A2,TOPS_2:def 1;
    hence thesis by A3;
  end;
  hence thesis by TOPS_2:def 1;
end;

theorem Th24:
  F is open & G is open implies UNION (F,G) is open
proof
  assume
A1: F is open & 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;
    assume A in UNION (F,G);
    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, Y as Subset of T by A2;
    X is open & Y is open by A1,A2,TOPS_2:def 1;
    hence thesis by A3;
  end;
  hence thesis by TOPS_2:def 1;
end;

theorem Th25:
  for T being set, F, G being Subset-Family of T holds card
  INTERSECTION (F,G) c= card [:F,G:]
proof
  deffunc F(set) = $1`1 /\ $1`2;
  let T be set, F, G be Subset-Family of T;
  set XX = [:F,G:];
  set IN = { F(X) where X is Element of [:bool T, bool T:] : X in XX };
  set A = [:bool T, bool T:];
  set AL = F, BL = G;
  set C = INTERSECTION(AL,BL);
A1: IN c= C
  proof
    let a be set;
    assume a in IN;
    then consider X being Element of [:bool T, bool T:] such that
A2: a = F(X) and
A3: X in XX;
    X`1 in F & X`2 in G by A3,MCART_1:10;
    hence thesis by A2,SETFAM_1:def 5;
  end;
A4: C c= IN
  proof
    let a be set;
    assume a in C;
    then consider X,Y be set such that
A5: X in AL & Y in BL and
A6: a = X /\ Y by SETFAM_1:def 5;
    reconsider X,Y as Subset of T by A5;
    set XY = [X,Y];
A7: XY`1 = X & XY`2 = Y;
    XY in XX by A5,ZFMISC_1:87;
    hence thesis by A6,A7;
  end;
  card { F(w) where w is Element of A : w in XX } c= card XX from TREES_2:
  sch 2;
  hence thesis by A1,A4,XBOOLE_0:def 10;
end;

theorem Th26:
  for T being set, F, G being Subset-Family of T holds card UNION
  (F,G) c= card [:F,G:]
proof
  deffunc F(set) = $1`1 \/ $1`2;
  let T be set, F, G be Subset-Family of T;
  set XX = [:F,G:];
  set IN = { F(X) where X is Element of [:bool T, bool T:] : X in XX };
  set A = [:bool T, bool T:];
  set AL = F, BL = G;
  set C = UNION(AL,BL);
A1: IN = C
  proof
    thus IN c= C
    proof
      let a be set;
      assume a in IN;
      then consider X being Element of [:bool T, bool T:] such that
A2:   a = F(X) and
A3:   X in XX;
      X`1 in F & X`2 in G by A3,MCART_1:10;
      hence thesis by A2,SETFAM_1:def 4;
    end;
    let a be set;
    assume a in C;
    then consider X,Y be set such that
A4: X in AL & Y in BL and
A5: a = X \/ Y by SETFAM_1:def 4;
    reconsider X,Y as Subset of T by A4;
    set XY = [X,Y];
A6: XY`1 = X & XY`2 = Y;
    XY in XX by A4,ZFMISC_1:87;
    hence thesis by A5,A6;
  end;
  card { F(w) where w is Element of A : w in XX } c= card XX from TREES_2:
  sch 2;
  hence thesis by A1;
end;

theorem Th27:
  for F, G being set holds union UNION (F,G) c= union F \/ union G
proof
  let F, G be set;
  let x be set;
  assume x in union UNION (F,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;
  per cases by A1,A5,XBOOLE_0:def 3;
  suppose
    x in f;
    then x in union F by A3,TARSKI:def 4;
    hence thesis by XBOOLE_0:def 3;
  end;
  suppose
    x in g;
    then x in union G by A4,TARSKI:def 4;
    hence thesis by XBOOLE_0:def 3;
  end;
end;

theorem Th28:
  for F, G being set st F <> {} & G <> {} holds union F \/ union G
  = union UNION (F,G)
proof
  let F, G be set;
  assume that
A1: F <> {} and
A2: G <> {};
  thus union F \/ union G c= union UNION (F,G)
  proof
    let x be set;
    assume
A3: x in union F \/ union G;
    per cases by A3,XBOOLE_0:def 3;
    suppose
A4:   x in union F;
      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= YW & YW in UNION (F,G) by A7,A5,SETFAM_1:def 4,XBOOLE_1:7;
      hence thesis by A6,TARSKI:def 4;
    end;
    suppose
A8:   x in union 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= YW & YW in UNION (F,G) by A11,A9,SETFAM_1:def 4,XBOOLE_1:7;
      hence thesis by A10,TARSKI:def 4;
    end;
  end;
  thus thesis by Th27;
end;

theorem Th29:
  for F being set holds UNION ({},F) = {}
proof
  let F be set;
  UNION ({},F) c= {}
  proof
    let x be set;
    assume x in UNION ({},F);
    then ex x1, x2 being set st x1 in {} & x2 in F & x = x1 \/ x2 by
SETFAM_1:def 4;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  for F, G being set holds UNION (F, G) = {} implies F = {} or G = {}
proof
  let F, G be set;
  assume
A1: UNION (F,G) = {};
  assume that
A2: F <> {} and
A3: G <> {};
  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 thesis by A1;
end;

theorem
  for F, G being set st INTERSECTION (F, G) = {} holds F = {} or G = {}
proof
  let F, G be set;
  assume that
A1: INTERSECTION (F,G) = {} and
A2: F <> {} and
A3: G <> {};
  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 thesis by A1;
end;

theorem Th32:
  for F, G being set holds meet UNION (F,G) c= meet F \/ meet G
proof
  let F, G be set;
  per cases;
  suppose
A1: F <> {} & G <> {};
    let x be set;
    assume
A2: x in meet UNION (F,G);
    assume
A3: not x in meet F \/ meet G;
    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 thesis by A2,SETFAM_1:def 1;
  end;
  suppose
    F = {} or G = {};
    then UNION (F,G) = {} by Th29;
    then meet UNION (F,G) = {} by SETFAM_1:def 1;
    hence thesis by XBOOLE_1:2;
  end;
end;

theorem
  for F, G being set st F <> {} & G <> {} holds meet UNION(F,G) = meet F
  \/ meet G
proof
  let F, G be set;
  assume
A1: F <> {} & G <> {};
  thus meet UNION(F,G) c= meet F \/ meet G by Th32;
  thus thesis by A1,SETFAM_1:29;
end;

theorem Th34:
  for F, G being set st F <> {} & G <> {} holds meet F /\ meet G =
  meet INTERSECTION(F,G)
proof
  let F, G be set;
  assume that
A1: F <> {} and
A2: 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 such that
A6: x in meet INTERSECTION(F,G);
    for Z be set st Z in G holds x in Z
    proof
      let Z be set;
      assume Z in G;
      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 thesis by XBOOLE_0:def 4;
    end;
    then
A7: x in meet G by A2,SETFAM_1:def 1;
    for Z be set st Z in F holds x in Z
    proof
      let Z be set;
      assume Z in F;
      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 thesis by XBOOLE_0:def 4;
    end;
    then x in meet F by A1,SETFAM_1:def 1;
    hence thesis by A7,XBOOLE_0:def 4;
  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;
    assume x in meet F /\ meet G;
    then
A9: x in meet F & x in meet G by XBOOLE_0:def 4;
    for Z be set st Z in INTERSECTION(F,G) holds x in Z
    proof
      let Z be set;
      assume Z in INTERSECTION(F,G);
      then consider Z1,Z2 be 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 thesis by A11,XBOOLE_0:def 4;
    end;
    hence thesis by A8,SETFAM_1:def 1;
  end;
  hence thesis by A5,XBOOLE_0:def 10;
end;

begin :: F_sigma and G_delta Types of Subsets

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

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

registration
  let T;
  cluster empty -> F_sigma G_delta for Subset of T;
  coherence
   proof let S be Subset of T;
    assume S is empty;
    then
A1:  S = {}T;
    thus S is F_sigma
proof
  reconsider E = {} as empty Subset-Family of T by Th18;
  {}T = union E by ZFMISC_1:2;
  hence thesis by Def6,A1;
end;
  reconsider F = { {}T } as Subset-Family of T;
  F is open & {}T = meet F by Th19,SETFAM_1:10;
  hence thesis by Def7,A1;
   end;
end;

theorem Th35:
  [#]T is F_sigma
proof
  reconsider F = { [#]T } as Subset-Family of T;
  F is closed & [#]T = union F by Th20,ZFMISC_1:25;
  hence thesis by Def6;
end;

theorem Th36:
  [#]T is G_delta
proof
  reconsider F = { [#]T } as Subset-Family of T;
  F is open & [#]T = meet F by Th19,SETFAM_1:10;
  hence thesis by Def7;
end;

registration
  let T;
  cluster [#]T -> F_sigma G_delta;
  coherence by Th35,Th36;
end;

theorem
  A is F_sigma implies A` is G_delta
proof
  assume A is F_sigma;
  then consider F being closed countable Subset-Family of T such that
A1: A = union F by Def6;
  per cases;
  suppose
A2: F <> {};
    set G = COMPLEMENT F;
A3: G is open by TOPS_2:9;
    (union F)` = meet COMPLEMENT F by A2,TOPS_2:6;
    hence thesis by A1,A3,Def7;
  end;
  suppose
    F = {};
    then A` = [#]T by A1,ZFMISC_1:2;
    hence thesis;
  end;
end;

theorem
  A is G_delta implies A` is F_sigma
proof
  assume A is G_delta;
  then consider F being open countable Subset-Family of T such that
A1: A = meet F by Def7;
  per cases;
  suppose
A2: F <> {};
    set G = COMPLEMENT F;
A3: G is closed by TOPS_2:10;
    (meet F)` = union COMPLEMENT F by A2,TOPS_2:7;
    hence thesis by A1,A3,Def6;
  end;
  suppose
    F = {};
    then A` = [#]T by A1,SETFAM_1:1;
    hence thesis;
  end;
end;

theorem
  A is F_sigma & B is F_sigma implies A /\ B is F_sigma
proof
  assume that
A1: A is F_sigma and
A2: B is F_sigma;
  consider F being closed countable Subset-Family of T such that
A3: A = union F by A1,Def6;
  consider G being closed countable 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 thesis by A5,A6,Def6;
end;

theorem
  A is F_sigma & B is F_sigma implies A \/ B is F_sigma
proof
  assume that
A1: A is F_sigma and
A2: B is F_sigma;
  consider F being closed countable Subset-Family of T such that
A3: A = union F by A1,Def6;
  consider G being closed countable Subset-Family of T such that
A4: B = union G by A2,Def6;
  reconsider H = UNION (F,G) as Subset-Family of T;
  per cases;
  suppose
A5: A <> {} & B <> {};
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 thesis by A6,A7,Def6;
  end;
  suppose
    A = {};
    hence thesis by A2;
  end;
  suppose
    B = {};
    hence thesis by A1;
  end;
end;

theorem
  A is G_delta & B is G_delta implies A \/ B is G_delta
proof
  assume that
A1: A is G_delta and
A2: B is G_delta;
  consider F being open countable Subset-Family of T such that
A3: A = meet F by A1,Def7;
  consider G being open countable Subset-Family of T such that
A4: B = meet G by A2,Def7;
  reconsider H = UNION (F,G) as Subset-Family of T;
  per cases;
  suppose
A5: F <> {} & G <> {};
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 thesis by A7,A8,Def7;
  end;
  suppose
    F = {} or G = {};
    then A = {} or B = {} by A3,A4,SETFAM_1:def 1;
    hence thesis by A1,A2;
  end;
end;

theorem
  A is G_delta & B is G_delta implies A /\ B is G_delta
proof
  assume that
A1: A is G_delta and
A2: B is G_delta;
  consider F being open countable Subset-Family of T such that
A3: A = meet F by A1,Def7;
  consider G being open countable Subset-Family of T such that
A4: B = meet G by A2,Def7;
  reconsider H = INTERSECTION (F,G) as Subset-Family of T;
  per cases;
  suppose
A5: F <> {} & G <> {};
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 thesis by A6,A7,Def7;
  end;
  suppose
    F = {} or G = {};
    then A = {} or B = {} by A3,A4,SETFAM_1:def 1;
    then A /\ B = {}T;
    hence thesis;
  end;
end;

theorem
  for A being Subset of T st A is closed holds A is F_sigma
proof
  let A be Subset of T;
  assume A is closed;
  then reconsider F = {A} as closed countable Subset-Family of T by Th20;
  take F;
  thus thesis by ZFMISC_1:25;
end;

theorem
  for A being Subset of T st A is open holds A is G_delta
proof
  let A be Subset of T;
  assume A is open;
  then reconsider F = {A} as open countable Subset-Family of T by Th19;
  take F;
  thus thesis by SETFAM_1:10;
end;

theorem
  for A being Subset of R^1 st A = RAT holds A is F_sigma
proof
  defpred R[set] means ex a being Element of RAT st a = $1;
  defpred P[set] means ex a being Element of RAT st {a} = $1;
  let A be Subset of R^1;
  ex F being set st for x being set holds x in F iff x in bool RAT & P[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 & P[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;
    assume x in F;
    then x in bool RAT by A1;
    hence thesis by A2,TOPMETR:17;
  end;
  then reconsider F as Subset-Family of R^1;
  assume
A3: A = RAT;
  ex F being Subset-Family of R^1 st F is closed countable & A = union F
  proof
    take F;
    for B being Subset of R^1 st B in F holds B is closed
    proof
      let B be Subset of R^1;
      assume B in F;
      then ex a being Element of RAT st {a} = B by A1;
      hence thesis;
    end;
    hence F is closed by TOPS_2:def 2;
A4: F = { {x} where x is Element of RAT : R[x] }
    proof
      thus F c= { {x} where x is Element of RAT : R[x] }
      proof
        let y be set;
        assume y in F;
        then P[y] by A1;
        hence thesis;
      end;
      let y be set;
      assume y in { {x} where x is Element of RAT : R[x] };
      then ex z being Element of RAT st y = {z} & R[z];
      hence thesis by A1;
    end;
    { {x} where x is Element of RAT : R[x] } is countable from
    FraenCoun11;
    hence F is countable by A4;
    thus A c= union F
    proof
      let x be set;
      assume x in A;
      then reconsider x as Element of RAT by A3;
      {x} in F & x in {x} by A1,TARSKI:def 1;
      hence thesis by TARSKI:def 4;
    end;
    let x be set;
    assume x in union F;
    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 thesis by A3,A5;
  end;
  hence thesis by Def6;
end;

begin :: T_1/2 Topological Spaces

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

theorem Th46:
  for T being TopSpace st T is T_1 holds T is T_1/2
proof
  let T be TopSpace;
  assume
A1: T is T_1;
  for A being Subset of T holds Der A is closed
  proof
    let A be Subset of T;
    Der A = Cl Der A by A1,TOPGEN_1:33;
    hence thesis;
  end;
  hence thesis by Def8;
end;

theorem Th47:
  for T being non empty TopSpace st T is T_1/2 holds T is T_0
proof
  let T be non empty TopSpace;
  assume
A1: T is T_1/2;
  now
    let x, y be Point of T;
    assume
A2: x <> y;
    assume that
A3: x in Cl {y} and
A4: y in Cl {x};
    not for G being Subset of T st G is open holds y in G implies {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= U and
A6:     x in V by CONNSP_2:6;
        assume x in Der {x};
        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 thesis by A8,TARSKI:def 1;
      end;
      then
A9:   x in (Der {x})` by SUBSET_1:29;
      assume
A10:  for G being Subset of T st G is open holds y in G implies {x} meets G;
      for U being open Subset of T st y in U ex r being Point of T st r in
      {x} /\ U & y <> r
      proof
        let U be open Subset of T;
        assume y in U;
        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 thesis by A2;
      end;
      then y in Der {x} by TOPGEN_1:17;
      then
A12:  not y in X by XBOOLE_0:def 5;
      Der {x} is closed by A1,Def8;
      then {y} meets X by A3,A9,PRE_TOPC:24;
      hence thesis by A12,ZFMISC_1:50;
    end;
    hence contradiction by A4,PRE_TOPC:24;
  end;
  hence thesis by TSP_1:def 6;
end;

registration
  cluster T_1/2 -> T_0 for TopSpace;
  coherence
  proof
    let T be TopSpace;
    per cases;
    suppose
      T is non empty;
      then reconsider T9 = T as non empty TopSpace;
      assume T is T_1/2;
      then T9 is T_1/2;
      hence thesis by Th47;
    end;
    suppose
      T is empty;
      then reconsider T9 = T as empty TopSpace;
      T9 is T_0;
      hence thesis;
    end;
  end;
  cluster T_1 -> T_1/2 for TopSpace;
  coherence by Th46;
end;

begin :: Condensation Points
:: Page 77 - 1.7.11

definition
  let T, A;
  let x be Point of T;
  pred x is_a_condensation_point_of A means
  :Def9:
  for N being a_neighborhood of x holds N /\ A is not countable;
end;

reserve x for Point of T;

theorem Th48:
  x is_a_condensation_point_of A & A c= B implies x
  is_a_condensation_point_of B
proof
  assume that
A1: x is_a_condensation_point_of A and
A2: A c= B;
  for N being a_neighborhood of x holds N /\ B is not countable
  proof
    let N be a_neighborhood of x;
    N /\ A c= N /\ B by A2,XBOOLE_1:26;
    hence thesis by A1,Def9;
  end;
  hence thesis by Def9;
end;

definition
  let T, A;
  func A^0 -> Subset of T means
  :Def10:
  for x being Point of T holds x in it iff x is_a_condensation_point_of A;
  existence
  proof
    defpred P[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 P[x
    ] from SUBSET_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    defpred P[Point of T] means $1 is_a_condensation_point_of A;
    let A1, A2 be Subset of T such that
A1: for x being Element of T holds x in A1 iff P[x] and
A2: for x being Element of T holds x in A2 iff P[x];
    thus A1 = A2 from SUBSET_1:sch 2(A1,A2);
  end;
end;

theorem Th49:
  for p being Point of T st p is_a_condensation_point_of A holds p
  is_an_accumulation_point_of A
proof
  let p be Point of T;
  assume
A1: p is_a_condensation_point_of A;
  for U being open Subset of T st p in U ex q being Point of T st q <> p &
  q in A & q in U
  proof
    let U be open Subset of T;
    assume p 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 as Point of T;
    q in A & q in U by XBOOLE_0:def 4;
    hence thesis by A2;
  end;
  hence thesis by TOPGEN_1:21;
end;

theorem
  A^0 c= Der A
proof
  let x be set;
  assume
A1: x in A^0;
  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 thesis by TOPGEN_1:16;
end;

theorem
  A^0 = Cl (A^0)
proof
  thus A^0 c= Cl (A^0) by PRE_TOPC:18;
  let x be set;
  assume
A1: x in Cl (A^0);
  then reconsider p = x as Point of T;
  for N being a_neighborhood of p holds N /\ A is not countable
  proof
    let N be a_neighborhood of p;
    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 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 thesis by A7,Def9;
  end;
  then p is_a_condensation_point_of A by Def9;
  hence thesis by Def10;
end;

theorem Th52:
  A c= B implies A^0 c= B^0
proof
  assume
A1: A c= B;
  let x be set;
  assume
A2: x in A^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 thesis by Def10;
end;

theorem Th53:
  x is_a_condensation_point_of A \/ B implies x
  is_a_condensation_point_of A or x is_a_condensation_point_of B
proof
  assume
A1: x is_a_condensation_point_of A \/ B;
  assume that
A2: not x is_a_condensation_point_of A and
A3: not x is_a_condensation_point_of B;
  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,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 thesis by A1,Def9;
end;

theorem
  (A \/ B)^0 = (A^0) \/ (B^0)
proof
  thus (A \/ B)^0 c= (A^0) \/ (B^0)
  proof
    let x be set;
    assume
A1: x in (A \/ 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 thesis by XBOOLE_0:def 3;
  end;
  A^0 c= (A \/ B)^0 & B^0 c= (A \/ B)^0 by Th52,XBOOLE_1:7;
  hence thesis by XBOOLE_1:8;
end;

theorem Th55:
  A is countable implies not ex x being Point of T st x
  is_a_condensation_point_of A
proof
  assume
A1: A is countable;
  given x being Point of T such that
A2: x is_a_condensation_point_of A;
  set N = the a_neighborhood of x;
  N /\ A is not countable by A2,Def9;
  hence thesis by A1,CARD_3:94;
end;

theorem Th56:
  A is countable implies A^0 = {}
proof
  assume
A1: A is countable;
  assume A^0 <> {};
  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 thesis by A1,Th55;
end;

registration
  let T;
  let A be countable Subset of T;
  cluster A^0 -> empty;
  coherence by Th56;
end;

theorem
  T is second-countable implies ex B being Basis of T st B is countable
proof
  set B = the Basis of T;
  consider B1 being Basis of T such that
  B1 c= B and
A1: card B1 = weight T by TOPGEN_2:18;
  assume T is second-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 thesis;
end;

registration
  cluster second-countable non empty for TopSpace;
  existence
  proof
    set T = the finite non empty TopSpace;
    take T;
    thus thesis;
  end;
end;

begin :: Borel Families of Subsets

registration
  let T;
  cluster TotFam T -> non empty all-open-containing compl-closed
    closed_for_countable_unions;
  coherence
  proof
    thus TotFam T is non empty;
    thus TotFam T is all-open-containing
    proof
      let A be Subset of T;
      assume A is open;
      thus thesis;
    end;
    for A be Subset of T st A in TotFam T holds A` in TotFam T;
    hence TotFam T is compl-closed by PROB_1:def 1;
    for G being countable Subset-Family of T st G c= TotFam T holds union
    G in TotFam T;
    hence thesis by Def4;
  end;
end;

theorem
  for T being set, A being SetSequence of T holds
  rng A is countable non empty Subset-Family of T
proof
  let T be set, A be SetSequence 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 thesis;
end;

theorem Th59:
  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 F, G be Subset-Family of T;
  assume that
A1: F is all-open-containing and
A2: F c= G;
  for A being Subset of T st A is open holds A in G
  proof
    let A be Subset of T;
    assume A is open;
    then A in F by A1,Def2;
    hence thesis by A2;
  end;
  hence thesis by Def2;
end;

theorem
  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 F, G be Subset-Family of T;
  assume that
A1: F is all-closed-containing and
A2: F c= G;
  for A being Subset of T st A is closed holds A in G
  proof
    let A be Subset of T;
    assume A is closed;
    then A in F by A1,Def3;
    hence thesis by A2;
  end;
  hence thesis by Def3;
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 closed_for_countable_unions closed_for_countable_meets
    all-closed-containing all-open-containing for Subset-Family of T;
  existence
  proof
    take TotFam T;
    thus thesis;
  end;
end;

theorem Th61:
  sigma TotFam T is all-open-containing compl-closed
  closed_for_countable_unions
proof
  set E = sigma TotFam T;
  TotFam T c= sigma TotFam T by PROB_1:def 9;
  hence E is all-open-containing by Th59;
  thus E is compl-closed;
  thus thesis;
end;

registration
  let T;
  cluster sigma TotFam T -> all-open-containing compl-closed
    closed_for_countable_unions;
  coherence by Th61;
end;

registration
  let T be non empty 1-sorted;
  cluster sigma-additive compl-closed closed_for_countable_unions non empty
    for Subset-Family of T;
  existence
  proof
    take sigma TotFam T;
    thus thesis;
  end;
end;

registration
  let T be non empty TopSpace;
  cluster -> closed_for_countable_unions for SigmaField of T;
  coherence;
end;

theorem
  for T being non empty TopSpace, F being Subset-Family of T st F is
  compl-closed closed_for_countable_unions holds F is SigmaField of T by Th13;

registration
  let T be non empty TopSpace;
  cluster all-open-containing for SigmaField of T;
  existence
  proof
    take sigma TotFam T;
    thus thesis;
  end;
end;

registration
  let T be non empty TopSpace;
  cluster Topology_of T -> open all-open-containing;
  coherence
  proof
    set E = Topology_of T;
    thus E is open;
    E is all-open-containing
    proof
      let A be Subset of T;
      assume A is open;
      hence thesis by PRE_TOPC:def 2;
    end;
    hence thesis;
  end;
end;

theorem Th63:
  for X being Subset-Family of T ex Y being all-open-containing
  compl-closed closed_for_countable_unions Subset-Family of T st X c= Y & for Z
  be all-open-containing compl-closed closed_for_countable_unions Subset-Family
  of T st X c= Z holds Y c= Z
proof
  let X be Subset-Family of T;
  set V = { S where S is Subset-Family of T : X c= S & S is
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
  };
  set Y = meet V;
A1: now
    let Z be set;
    assume Z in V;
    then ex S be Subset-Family of T st Z = S & X c= S & S is
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
    ;
    hence X c= Z;
  end;
A2: bool the carrier of T in V
  proof
    set X1 = TotFam T;
    X1 in V;
    hence thesis;
  end;
A3: for E being Subset of T st E in Y holds E` in Y
  proof
    let E be Subset of T such that
A4: E in Y;
    now
      let Z be set;
      assume Z in V;
      then E in Z & ex S being Subset-Family of T st Z = S & X c= S & S is
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
      by A4,SETFAM_1:def 1;
      hence E` in Z by PROB_1:def 1;
    end;
    hence thesis by A2,SETFAM_1:def 1;
  end;
A5: for BSeq be SetSequence of the carrier of T st rng BSeq c= Y holds
  Intersection BSeq in Y
  proof
    let BSeq be SetSequence of the carrier of T such that
A6: rng BSeq c= Y;
    now
      let Z be set;
      assume
A7:   Z in V;
      then consider S be Subset-Family of T such that
A8:   Z = S and
      X c= S and
A9:   S is all-open-containing compl-closed
      closed_for_countable_unions Subset-Family of T;
      now
        let n be Nat;
        BSeq.n in rng BSeq by NAT_1:51;
        hence BSeq.n in Z by A6,A7,SETFAM_1:def 1;
      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;
    end;
    hence thesis by A2,SETFAM_1:def 1;
  end;
  now
    let Z be set;
    assume Z in V;
    then ex S being Subset-Family of T st Z = S & X c= S & S is
all-open-containing compl-closed 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;
  end;
  then {} in Y by A2,SETFAM_1:def 1;
  then reconsider Y 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;
    assume
A11: A is open;
    for Y being set holds Y in V implies A in Y
    proof
      let Y be set;
      assume Y in V;
      then ex S being Subset-Family of the carrier of T st Y = S & X c= S & S
is all-open-containing compl-closed closed_for_countable_unions Subset-Family
      of T;
      hence thesis by A11,Def2;
    end;
    hence thesis by A2,SETFAM_1:def 1;
  end;
  then reconsider
  Y as all-open-containing compl-closed closed_for_countable_unions
  Subset-Family of T by Def2;
  take Y;
  for Z be set st X c= Z & Z is all-open-containing compl-closed
  closed_for_countable_unions Subset-Family of T holds Y c= Z
  proof
    let Z be set;
    assume that
A12: X c= Z and
A13: Z is all-open-containing compl-closed closed_for_countable_unions
    Subset-Family of T;
    reconsider Z as Subset-Family of T by A13;
    Z in V by A12,A13;
    hence thesis by SETFAM_1:3;
  end;
  hence thesis by A2,A1,SETFAM_1:5;
end;

definition
  let T;
  func BorelSets T -> all-open-containing compl-closed
  closed_for_countable_unions Subset-Family of T means
  :Def11:
  for G being
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
  holds it c= G;
  existence
  proof
    reconsider E = {} as Subset-Family of T by Th18;
    consider Y being all-open-containing compl-closed
    closed_for_countable_unions Subset-Family of T such that
    E c= Y and
A1: for Z be all-open-containing compl-closed
closed_for_countable_unions Subset-Family of T st E c= Z holds Y c= Z by Th63;
    take Y;
    let G be all-open-containing compl-closed closed_for_countable_unions
    Subset-Family of T;
    thus thesis by A1,XBOOLE_1:2;
  end;
  uniqueness
  proof
    let R1,R2 be all-open-containing compl-closed closed_for_countable_unions
    Subset-Family of T;
    assume ( for G being all-open-containing compl-closed
    closed_for_countable_unions Subset-Family of T holds R1 c= G)& for G being
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
    holds R2 c= G;
    then R1 c= R2 & R2 c= R1;
    hence thesis by XBOOLE_0:def 10;
  end;
end;

theorem Th64:
  for F being closed Subset-Family of T holds F c= BorelSets T
proof
  let F be closed Subset-Family of T;
  F c= BorelSets T
  proof
    let x be set;
    assume
A1: x in F;
    then reconsider xx = x as Subset of T;
    xx is closed by A1,TOPS_2:def 2;
    hence thesis by Def3;
  end;
  hence thesis;
end;

theorem Th65:
  for F being open Subset-Family of T holds F c= BorelSets T
proof
  let F be open Subset-Family of T;
  F c= BorelSets T
  proof
    let x be set;
    assume
A1: x in F;
    then reconsider xx = x as Subset of T;
    xx is open by A1,TOPS_2:def 1;
    hence thesis by Def2;
  end;
  hence thesis;
end;

theorem
  BorelSets T = sigma Topology_of T
proof
  reconsider BT = BorelSets T as SigmaField of T by Th13;
  set X = Topology_of T;
A1: for Z being set st X c= Z & Z is SigmaField of T holds BT c= Z
  proof
    let Z be set;
    assume that
A2: X c= Z and
A3: Z is SigmaField of T;
    reconsider Z9 = Z as SigmaField of T by A3;
    Z9 is all-open-containing by A2,Th59;
    hence thesis by Def11;
  end;
  X c= BT by Th65;
  hence thesis by A1,PROB_1:def 9;
end;

definition
  let T, A;
  attr A is Borel means
  :Def12:
  A in BorelSets T;
end;

registration
  let T;
  cluster F_sigma -> Borel for Subset of T;
  coherence
  proof
    let A be Subset of T;
    assume A is F_sigma;
    then consider F being closed countable 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 thesis by Def12;
  end;
end;

registration
  let T;
  cluster G_delta -> Borel for Subset of T;
  coherence
  proof
    let A be Subset of T;
    assume A is G_delta;
    then consider F being open countable 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 thesis by Def12;
  end;
end;