:: Topological Spaces and Continuous Functions
::  by Beata Padlewska and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990-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, TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1,
      RCOMP_1, RELAT_1, FUNCT_1, ORDINAL2, FUNCOP_1, CARD_5, CARD_1, PRE_TOPC;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELSET_1, CARD_1,
      STRUCT_0;
 constructors SETFAM_1, PARTFUN1, STRUCT_0, FUNCOP_1, CARD_1, DOMAIN_1,
      RELSET_1;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, RELSET_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, STRUCT_0, SUBSET_1;
 theorems TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1, XBOOLE_0, XBOOLE_1, FUNCT_1,
      FUNCT_2, RELAT_1, FUNCOP_1, CARD_1;
 schemes SUBSET_1;

begin

definition
  struct(1-sorted) TopStruct (# carrier -> set, topology -> Subset-Family of
    the carrier #);
end;

reserve T for TopStruct;

::
::                   The topological space
::

definition
  let IT be TopStruct;
  attr IT is TopSpace-like means
  :Def1:
  the carrier of IT in the topology of
IT & (for a being Subset-Family of IT st a c= the topology of IT holds union a
in the topology of IT) & for a,b being Subset of IT st a in the topology of IT
  & b in the topology of IT holds a /\ b in the topology of IT;
end;

registration
  cluster non empty strict TopSpace-like for TopStruct;
  existence
  proof
    now
      take X={{}};
      set T={{},X};
      T c= bool X
      proof
        let x be set;
        assume x in T;
        then x= {} or x = X by TARSKI:def 2;
        then x c= X by XBOOLE_1:2;
        hence thesis;
      end;
      then reconsider T as Subset-Family of X;
      take T;
      set Y=TopStruct(#X,T#);
      thus the carrier of Y in the topology of Y by TARSKI:def 2;
      thus for a being Subset-Family of Y st a c= the topology of Y holds
      union a in the topology of Y
      proof
        let a be Subset-Family of Y;
        assume a c= the topology of Y;
        then a={} or a={{}} or a={X} or a={{},X} by ZFMISC_1:36;
        then union a={} or union a=X or union a = {} \/ X by ZFMISC_1:2,25,75;
        hence thesis by TARSKI:def 2;
      end;
      let a,b be Subset of Y such that
A1:   a in the topology of Y and
A2:   b in the topology of Y;
A3:   b={} or b=X by A2,TARSKI:def 2;
      a={} or a=X by A1,TARSKI:def 2;
      hence a /\ b in the topology of Y by A3,TARSKI:def 2;
    end;
    then consider X being non empty set, T being Subset-Family of X such that
A4: ( the carrier of TopStruct(#X,T#) in the topology of TopStruct(#X
,T#) & for a being Subset-Family of TopStruct(#X,T#) st a c= the topology of
TopStruct(#X, T #) holds union a in the topology of TopStruct(#X,T#) )& for a,b
being Subset of TopStruct(#X,T#) st a in the topology of TopStruct(#X,T#) & b
in the topology of TopStruct(#X,T#) holds a /\ b in the topology of TopStruct(#
      X,T#);
    take TopStruct(#X,T#);
    thus TopStruct(#X,T#) is non empty;
    thus thesis by A4,Def1;
  end;
end;

definition
  mode TopSpace is TopSpace-like TopStruct;
end;

definition
  let S be 1-sorted;
  mode Point of S is Element of S;
end;

registration
  let T be TopSpace;
  cluster the topology of T -> non empty;
  coherence by Def1;
end;

reserve GX for TopSpace;

theorem Th1:
  {} in the topology of GX
proof
  reconsider A = {} as Subset-Family of GX by XBOOLE_1:2;
  A c= the topology of GX by XBOOLE_1:2;
  hence thesis by Def1,ZFMISC_1:2;
end;

theorem
  for T being 1-sorted, P being Subset of T holds P \/ P` = [#]T
proof
  let T be 1-sorted, P be Subset of T;
  P \/ P` = [#] the carrier of T by SUBSET_1:10
    .= the carrier of T;
  hence thesis;
end;

theorem Th3:
  for T being 1-sorted, P being Subset of T holds [#]T \ ([#]T \ P ) = P
proof
  let T be 1-sorted, P be Subset of T;
  [#]T \ ([#]T \ P) = P /\ [#]T by XBOOLE_1:48;
  hence thesis by XBOOLE_1:28;
end;

theorem Th4:
  for T being 1-sorted, P being Subset of T holds P <> [#]T iff [#]T \ P <> {}
proof
  let T be 1-sorted, P be Subset of T;
  now
    assume that
A1: P <> [#]T and
A2: [#]T \ P = {};
    [#]T c= P by A2,XBOOLE_1:37;
    hence contradiction by A1,XBOOLE_0:def 10;
  end;
  hence thesis by XBOOLE_1:37;
end;

theorem
  for T being 1-sorted, P,Q being Subset of T st [#]T = P \/ Q & P
  misses Q holds Q = [#]T \ P
proof
  let T be 1-sorted, P,Q be Subset of T;
  assume that
A1: [#]T = P \/ Q and
A2: P misses Q;
  [#]T \ P = Q \ P by A1,XBOOLE_1:40
    .= Q by A2,XBOOLE_1:83;
  hence thesis;
end;

theorem
  for T being 1-sorted holds [#]T = ({}T)`;

definition
  let T be TopStruct, P be Subset of T;

  attr P is open means
  :Def2:
  P in the topology of T;
end;

definition
  let T be TopStruct, P be Subset of T;
  attr P is closed means
  :Def3:
  [#]T \ P is open;
end;

definition

  let T be TopStruct;
  mode SubSpace of T -> TopStruct means
    :Def4:
    [#]it c= [#]T & for P being
Subset of it holds P in the topology of it iff ex Q being Subset of T st Q in
    the topology of T & P = Q /\ [#]it;
  existence
  proof
    take T;
    thus [#]T c= [#]T;
    let P be Subset of T;
    hereby
      assume
A1:   P in the topology of T;
      take Q = P;
      thus Q in the topology of T by A1;
      thus P = Q /\ [#]T by XBOOLE_1:28;
    end;
    given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]T;
    thus thesis by A2,XBOOLE_1:28;
  end;
end;

Lm1: the TopStruct of T is SubSpace of T
proof
  set S = the TopStruct of T;
  thus [#]S c= [#]T;
  let P be Subset of S;
  hereby
    reconsider Q = P as Subset of T;
    assume
A1: P in the topology of S;
    take Q;
    thus Q in the topology of T by A1;
    thus P = Q /\ [#]S by XBOOLE_1:28;
  end;
  given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]S;
  thus thesis by A2,XBOOLE_1:28;
end;

registration
  let T be TopStruct;
  cluster strict for SubSpace of T;
  existence
  proof
    the TopStruct of T is SubSpace of T by Lm1;
    hence thesis;
  end;
end;

registration
  let T be non empty TopStruct;
  cluster strict non empty for SubSpace of T;
  existence
  proof
    the TopStruct of T is SubSpace of T & the TopStruct of T is non empty
    by Lm1;
    hence thesis;
  end;
end;

registration
  let T be TopSpace;
  cluster -> TopSpace-like for SubSpace of T;
  coherence
  proof
    let S be SubSpace of T;
    S is TopSpace-like
    proof
      set P = the carrier of S;
A1:   [#]T in the topology of T by Def1;
A2:   P = [#] S;
      then P c= [#] T by Def4;
      then [#]T /\ P = P by XBOOLE_1:28;
      hence the carrier of S in the topology of S by A2,A1,Def4;
      thus for a being Subset-Family of S st a c= the topology of S holds
      union a in the topology of S
      proof
        let a be Subset-Family of S such that
A3:     a c= the topology of S;
        defpred Q[set] means $1 /\ the carrier of S in a & $1 in the topology
        of T;
        consider b being Subset-Family of T such that
A4:     for Z being Subset of T holds Z in b iff Q[Z] from SUBSET_1:
        sch 3;
A5:     union b /\ P c= union a
        proof
          let x be set;
          assume
A6:       x in union b /\ P;
          then x in union b by XBOOLE_0:def 4;
          then consider Z being set such that
A7:       x in Z and
A8:       Z in b by TARSKI:def 4;
          x in P by A6,XBOOLE_0:def 4;
          then
A9:       x in Z /\ P by A7,XBOOLE_0:def 4;
          Z /\ P in a by A4,A8;
          hence thesis by A9,TARSKI:def 4;
        end;
        b c= the topology of T
        proof
          let y be set;
          assume y in b;
          hence thesis by A4;
        end;
        then
A10:    union b in the topology of T by Def1;
        union a c= union b /\ P
        proof
          let x be set;
          assume
A11:      x in union a;
          then consider Z1 being set such that
A12:      x in Z1 and
A13:      Z1 in a by TARSKI:def 4;
          consider Z3 being Subset of T such that
A14:      Z3 in the topology of T & Z1 = Z3 /\ P by A2,A3,A13,Def4;
          Z3 in b & x in Z3 by A4,A12,A13,A14,XBOOLE_0:def 4;
          then x in union b by TARSKI:def 4;
          hence thesis by A11,XBOOLE_0:def 4;
        end;
        then union a = union b /\ P by A5,XBOOLE_0:def 10;
        hence thesis by A2,A10,Def4;
      end;
      thus for V,Q being Subset of S st V in the topology of S & Q in the
      topology of S holds V /\ Q in the topology of S
      proof
        let V,Q be Subset of S;
        assume that
A15:    V in the topology of S and
A16:    Q in the topology of S;
        consider P1 being Subset of T such that
A17:    P1 in the topology of T and
A18:    V = P1 /\ P by A2,A15,Def4;
        consider Q1 being Subset of T such that
A19:    Q1 in the topology of T and
A20:    Q = Q1 /\ P by A2,A16,Def4;
A21:    V /\ Q = P1 /\ ((Q1 /\ P) /\ P) by A18,A20,XBOOLE_1:16
          .= P1 /\ (Q1 /\ (P /\ P)) by XBOOLE_1:16
          .= (P1 /\ Q1) /\ P by XBOOLE_1:16;
        P1 /\ Q1 in the topology of T by A17,A19,Def1;
        hence thesis by A2,A21,Def4;
      end;
    end;
    hence thesis;
  end;
end;

definition
  let T be TopStruct, P be Subset of T;
  func T|P -> strict SubSpace of T means
  :Def5:
  [#]it = P;
  existence
  proof
    defpred Q[set] means ex Q being Subset of T st Q in the topology of T & $1
    = Q /\ P;
    consider top1 being Subset-Family of P such that
A1: for Z being Subset of P holds Z in top1 iff Q[Z] from SUBSET_1:sch
    3;
    reconsider top1 as Subset-Family of P;
    set Y = TopStruct(#P,top1#);
A2: for Z being Subset of Y holds Z in top1 iff ex Q being Subset of T st
    Q in the topology of T & Z = Q /\ [#]Y
    proof
      let Z be Subset of Y;
      thus Z in top1 implies ex Q being Subset of T st Q in the topology of T
      & Z = Q /\ [#]Y
      proof
        assume Z in top1;
        then Q[Z] by A1;
        hence thesis;
      end;
      thus thesis by A1;
    end;
    [#]Y c= [#]T;
    then reconsider Y as strict SubSpace of T by A2,Def4;
    take Y;
    thus thesis;
  end;
  uniqueness
  proof
    let Z1,Z2 be strict SubSpace of T;
    assume
A3: [#] Z1 = P & [#] Z2 = P;
A4: the topology of Z2 c= the topology of Z1
    proof
      let x be set;
      assume x in the topology of Z2;
      then ex Q being Subset of T st Q in the topology of T & x = Q /\ [#]Z1
      by A3,Def4;
      hence thesis by Def4;
    end;
    the topology of Z1 c= the topology of Z2
    proof
      let x be set;
      assume x in the topology of Z1;
      then ex Q being Subset of T st Q in the topology of T & x = Q /\ [#]Z2
      by A3,Def4;
      hence thesis by Def4;
    end;
    hence thesis by A3,A4,XBOOLE_0:def 10;
  end;
end;

registration
  let T be non empty TopStruct, P be non empty Subset of T;
  cluster T|P -> non empty;
  coherence
  proof
    [#](T|P) = P by Def5;
    hence the carrier of T|P is non empty;
  end;
end;

registration
  let T be TopSpace;
  cluster TopSpace-like strict for SubSpace of T;
  existence
  proof
    set X = the strict SubSpace of T;
    take X;
    thus thesis;
  end;
end;

registration
  let T be TopSpace, P be Subset of T;
  cluster T|P -> TopSpace-like;
  coherence;
end;

theorem
  for S being TopSpace, P1,P2 being Subset of S, P19 being Subset of S|
  P2 st P1=P19 & P1 c= P2 holds S|P1=(S|P2)|P19
proof
  let S be TopSpace, P1,P2 be Subset of S, P19 be Subset of S|P2;
  assume that
A1: P1=P19 and
A2: P1 c= P2;
A3: [#]((S|P2)|P19)=P1 by A1,Def5;
A4: [#](S|P2)=P2 by Def5;
A5: for R being Subset of (S|P2)|P19 holds R in the topology of (S|P2)|P19
  iff ex Q being Subset of S st Q in the topology of S & R=Q/\[#]((S|P2)|P19)
  proof
    let R be Subset of (S|P2)|P19;
A6: now
      given Q being Subset of S such that
A7:   Q in the topology of S and
A8:   R=Q/\[#]((S|P2)|P19);
      reconsider R9=Q/\[#](S|P2) as Subset of S|P2;
A9:   R9 in the topology of (S|P2) by A7,Def4;
      R9/\[#]((S|P2)|P19)=Q/\(P2/\P1) by A4,A3,XBOOLE_1:16
        .=R by A2,A3,A8,XBOOLE_1:28;
      hence R in the topology of (S|P2)|P19 by A9,Def4;
    end;
    now
      assume R in the topology of (S|P2)|P19;
      then consider Q0 being Subset of S|P2 such that
A10:  Q0 in the topology of S|P2 and
A11:  R=Q0/\[#]((S|P2)|P19) by Def4;
      consider Q1 being Subset of S such that
A12:  Q1 in the topology of S and
A13:  Q0=Q1/\[#](S|P2) by A10,Def4;
      R=Q1/\(P2/\P1) by A4,A3,A11,A13,XBOOLE_1:16
        .=Q1/\[#]((S|P2)|P19) by A2,A3,XBOOLE_1:28;
      hence
      ex Q being Subset of S st Q in the topology of S & R=Q/\[#]((S|P2)|
      P19) by A12;
    end;
    hence thesis by A6;
  end;
  [#]((S|P2)|P19) c= [#](S) by A3;
  then (S|P2)|P19 is SubSpace of S by A5,Def4;
  hence thesis by A3,Def5;
end;

theorem Th8: :: JORDAN1:1, AK, 20.02.2006
  for GX being TopStruct, A being Subset of GX holds the carrier of (GX|A) = A
proof
  let GX be TopStruct, A be Subset of GX;
  A=[#](GX|A) by Def5;
  hence thesis;
end;

theorem :: JGRAPH_3:12, AK, 20.02.2006
  for X being TopStruct,Y being non empty TopStruct, f being Function of
  X,Y, P being Subset of X holds f|P is Function of X|P,Y
proof
  let X be TopStruct,Y be non empty TopStruct,f be Function of X,Y, P be
  Subset of X;
  P = the carrier of (X|P) by Th8;
  hence thesis by FUNCT_2:32;
end;

definition
  let S, T be TopStruct, f be Function of S,T;

  attr f is continuous means
  :Def6:
  for P1 being Subset of T st P1 is closed holds f" P1 is closed;
end;

theorem
  for T1, T2, S1, S2 being TopStruct st the TopStruct of T1 = the
  TopStruct of T2 & the TopStruct of S1 = the TopStruct of S2 holds S1 is
  SubSpace of T1 implies S2 is SubSpace of T2
proof
  let T1, T2, S1, S2 be TopStruct such that
A1: the TopStruct of T1 = the TopStruct of T2 & the TopStruct of S1 =
  the TopStruct of S2;
  assume that
A2: [#]S1 c= [#]T1 and
A3: for P being Subset of S1 holds P in the topology of S1 iff ex Q
  being Subset of T1 st Q in the topology of T1 & P = Q /\ [#]S1;
  thus [#]S2 c= [#]T2 by A1,A2;
  thus thesis by A1,A3;
end;

theorem Th11:
  for X9 being SubSpace of T, A being Subset of X9 holds A is Subset of T
proof
  let X9 be SubSpace of T, A be Subset of X9;
  [#]X9 c= [#]T by Def4;
  hence thesis by XBOOLE_1:1;
end;

theorem
  for A being Subset of T st A <> {}T ex x being Point of T st x in A
proof
  let A be Subset of T;
  set x = the Element of A;
  assume
A1: A <> {}T;
  then x is Point of T by TARSKI:def 3;
  hence thesis by A1;
end;

registration
  let T be TopSpace;
  cluster [#]T -> closed;
  coherence
  proof
    {}T in the topology of T by Th1;
    then
A1: {}T is open by Def2;
    [#]T \ [#]T = {}T by Th4;
    hence thesis by A1,Def3;
  end;
end;

registration
  let T be TopSpace;
  cluster closed for Subset of T;
  existence
  proof
    take [#]T;
    thus thesis;
  end;
end;

registration
  let T be non empty TopSpace;
  cluster non empty closed for Subset of T;
  existence
  proof
    take [#]T;
    thus thesis;
  end;
end;

theorem Th13:
  for X9 being SubSpace of T, B being Subset of X9 holds B is
  closed iff ex C being Subset of T st C is closed & C /\ [#](X9) = B
proof
  let X9 be SubSpace of T, B be Subset of X9;
A1: [#]X9 is Subset of T by Th11;
A2: now
    assume B is closed;
    then [#](X9) \ B is open by Def3;
    then [#](X9) \ B in the topology of X9 by Def2;
    then consider V being Subset of T such that
A3: V in the topology of T and
A4: [#](X9) \ B = V /\ [#]X9 by Def4;
A5: ([#](T) \ V) /\ ([#]X9) = [#]X9 /\ V` .= ([#](X9)) \ V by A1,SUBSET_1:13
      .= [#](X9) \ (([#](X9)) /\ V) by XBOOLE_1:47
      .= B by A4,Th3;
    reconsider V1 = V as Subset of T;
A6: [#](T) \ ([#](T) \ V) = V by Th3;
    V1 is open by A3,Def2;
    then [#](T) \ V is closed by A6,Def3;
    hence ex C being Subset of T st C is closed & C /\ ([#]X9) = B by A5;
  end;
  now
    given C being Subset of T such that
A7: C is closed and
A8: C /\ [#]X9 = B;
    [#]T \ C is open by A7,Def3;
    then [#]T \ C in the topology of T by Def2;
    then
A9: ([#]T \ C) /\ [#]X9 in the topology of X9 by Def4;
    [#]X9 \ B = [#]X9 \ C by A8,XBOOLE_1:47
      .= ([#]X9) /\ C` by A1,SUBSET_1:13
      .= ([#]T \ C) /\ ([#]X9);
    then [#]X9 \ B is open by A9,Def2;
    hence B is closed by Def3;
  end;
  hence thesis by A2;
end;

theorem Th14:
  for F being Subset-Family of GX st for A being Subset of GX st A
  in F holds A is closed holds meet F is closed
proof
  let F be Subset-Family of GX such that
A1: for A being Subset of GX st A in F holds A is closed;
  per cases;
  suppose
A2: F <> {};
    defpred Q[set] means [#]GX \ $1 in F;
    consider R1 being Subset-Family of GX such that
A3: for B being Subset of GX holds B in R1 iff Q[B] from SUBSET_1:sch
    3;
A4: for x being set st x in the carrier of GX holds (for A being Subset
of GX st A in F holds x in A) iff for Z being Subset of GX st Z in R1 holds not
    x in Z
    proof
      let x be set;
      assume
A5:   x in the carrier of GX;
      thus (for A being Subset of GX st A in F holds x in A) implies for Z
      being Subset of GX st Z in R1 holds not x in Z
      proof
        assume
A6:     for A being Subset of GX st A in F holds x in A;
        let Z be Subset of GX;
        assume Z in R1;
        then [#]GX \ Z in F by A3;
        then x in [#]GX \ Z by A6;
        hence thesis by XBOOLE_0:def 5;
      end;
      assume
A7:   for Z being Subset of GX st Z in R1 holds not x in Z;
      let A be Subset of GX such that
A8:   A in F;
      [#]GX \ ([#]GX \ A) = A by Th3;
      then [#]GX \ A in R1 by A3,A8;
      then not x in [#]GX \ A by A7;
      hence thesis by A5,XBOOLE_0:def 5;
    end;
A9: for x being set holds x in [#]GX \ (union R1) iff x in meet F
    proof
      let x be set;
      thus x in [#]GX \ (union R1) implies x in meet F
      proof
        assume
A10:    x in [#]GX \ union R1;
        then not x in union R1 by XBOOLE_0:def 5;
        then for Z being Subset of GX st Z in R1 holds not x in Z by
TARSKI:def 4;
        then for A be set st A in F holds x in A by A4,A10;
        hence thesis by A2,SETFAM_1:def 1;
      end;
      assume
A11:  x in meet F;
      then for A being Subset of GX st A in F holds x in A by SETFAM_1:def 1;
      then for Z being set st x in Z holds not Z in R1 by A4;
      then not x in union R1 by TARSKI:def 4;
      hence thesis by A11,XBOOLE_0:def 5;
    end;
    now
      let B be set;
      assume
A12:  B in R1;
      then reconsider B1=B as Subset of GX;
      B1 in R1 iff [#]GX \ B1 in F by A3;
      then
A13:  [#]GX \ B1 is closed by A1,A12;
      [#]GX \ ([#]GX \ B1) = B1 by Th3;
      then B1 is open by A13,Def3;
      hence B in the topology of GX by Def2;
    end;
    then R1 c= the topology of GX by TARSKI:def 3;
    then union R1 in the topology of GX by Def1;
    then
A14: union R1 is open by Def2;
    [#]GX \ ([#]GX \ (union R1)) = union R1 by Th3;
    then [#]GX \ union R1 is closed by A14,Def3;
    hence thesis by A9,TARSKI:1;
  end;
  suppose
A15: F = {};
    the carrier of GX in the topology of GX by Def1;
    then
A16: [#]GX is open by Def2;
    [#]GX = [#]GX \ {}GX;
    then {}GX is closed by A16,Def3;
    hence thesis by A15,SETFAM_1:def 1;
  end;
end;

::
::                    The closure of a set
::

definition
  let GX be TopStruct, A be Subset of GX;
  func Cl A -> Subset of GX means
  :Def7:
  for p being set st p in the carrier
  of GX holds p in it iff for G being Subset of GX st G is open holds p in G
  implies A meets G;
  existence
  proof
    defpred P[set] means for G being Subset of GX st G is open holds $1 in G
    implies A meets G;
    consider P being Subset of GX such that
A1: for x being set holds x in P iff x in the carrier of GX & P[x]
    from SUBSET_1:sch 1;
    take P;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let C1,C2 be Subset of GX;
    assume that
A2: for p being set st p in the carrier of GX holds p in C1 iff for G
    being Subset of GX st G is open holds p in G implies A meets G and
A3: for p being set st p in the carrier of GX holds p in C2 iff for V
    being Subset of GX st V is open holds p in V implies A meets V;
    for x being set holds x in C1 iff x in C2
    proof
      let x be set;
      thus x in C1 implies x in C2
      proof
        assume
A4:     x in C1;
        then
        for G being Subset of GX st G is open holds x in G implies A meets
        G by A2;
        hence thesis by A3,A4;
      end;
      assume
A5:   x in C2;
      then
      for V being Subset of GX st V is open holds x in V implies A meets V
      by A3;
      hence thesis by A2,A5;
    end;
    hence thesis by TARSKI:1;
  end;
  projectivity
  proof
    let r, A be Subset of GX;
    assume
A6: for p being set st p in the carrier of GX holds p in r iff for G
    being Subset of GX st G is open holds p in G implies A meets G;
    let p be set such that
A7: p in the carrier of GX;
    thus p in r implies for G being Subset of GX st G is open & p in G holds r
    meets G by XBOOLE_0:3;
    assume
A8: for G being Subset of GX st G is open holds p in G implies r meets G;
A9: now
      let C be Subset of GX;
      assume C is closed;
      then
A10:  [#]GX \ C is open by Def3;
      now
        assume p in [#]GX \ C;
        then r meets [#]GX \ C by A8,A10;
        then ex x being set st x in r & x in [#]GX \ C by XBOOLE_0:3;
        hence A meets [#]GX \ C by A6,A10;
      end;
      then A c= ([#]GX \ C)` implies p in C or not p in [#]GX by SUBSET_1:23
,XBOOLE_0:def 5;
      hence A c= C implies p in C by A7,Th3;
    end;
    for G being Subset of GX st G is open holds p in G implies A meets G
    proof
      let G be Subset of GX such that
A11:  G is open;
      [#]GX \ ([#]GX \ G) = G by Th3;
      then [#]GX \ G is closed by A11,Def3;
      then A c= G` implies p in [#]GX \ G by A9;
      hence thesis by SUBSET_1:23,XBOOLE_0:def 5;
    end;
    hence thesis by A6,A7;
  end;
end;

theorem Th15:
  for A being Subset of T, p being set st p in the carrier of T
  holds p in Cl A iff for C being Subset of T st C is closed holds (A c= C
  implies p in C)
proof
  let A be Subset of T, p be set such that
A1: p in the carrier of T;
A2: now
    assume
A3: for C being Subset of T st C is closed holds (A c= C implies p in C);
    for G being Subset of T st G is open holds (p in G implies A meets G)
    proof
      let G be Subset of T such that
A4:   G is open;
      [#]T \ ([#]T \ G) = G by Th3;
      then [#]T \ G is closed by A4,Def3;
      then A c= G` implies p in [#]T \ G by A3;
      hence thesis by SUBSET_1:23,XBOOLE_0:def 5;
    end;
    hence p in Cl A by A1,Def7;
  end;
  now
    assume
A5: p in Cl A;
    let C be Subset of T;
    assume C is closed;
    then [#]T \ C is open by Def3;
    then p in [#]T \ C implies A meets ([#]T \ C) by A5,Def7;
    then A c= ([#]T \ C)` implies (p in C or not p in [#]T) by SUBSET_1:23
,XBOOLE_0:def 5;
    hence A c= C implies p in C by A1,Th3;
  end;
  hence thesis by A2;
end;

theorem Th16:
  for A being Subset of GX ex F being Subset-Family of GX st (for
  C being Subset of GX holds C in F iff C is closed & A c= C) & Cl A = meet F
proof
  let A be Subset of GX;
  defpred Q[set] means ex C1 being Subset of GX st C1 = $1 & C1 is closed & A
  c= $1;
  consider F9 being Subset-Family of GX such that
A1: for C being Subset of GX holds C in F9 iff Q[C] from SUBSET_1:sch 3;
  take F=F9;
  thus for C being Subset of GX holds C in F iff C is closed & A c= C
  proof
    let C be Subset of GX;
    thus C in F implies C is closed & A c= C
    proof
      assume C in F;
      then ex C1 being Subset of GX st C1 = C & C1 is closed & A c= C by A1;
      hence thesis;
    end;
    thus thesis by A1;
  end;
  A c= [#]GX;
  then
A2: F <> {} by A1;
  for p being set holds p in Cl A iff p in meet F
  proof
    let p be set;
A3: now
      assume
A4:   p in meet F;
      now
        let C be Subset of GX;
        assume C is closed & A c= C;
        then C in F by A1;
        hence p in C by A4,SETFAM_1:def 1;
      end;
      hence p in Cl A by A4,Th15;
    end;
    now
      assume
A5:   p in Cl A;
      now
        let C be set;
        assume C in F;
        then
        ex C1 being Subset of GX st C1 = C & C1 is closed & A c= C by A1;
        hence p in C by A5,Th15;
      end;
      hence p in meet F by A2,SETFAM_1:def 1;
    end;
    hence thesis by A3;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  for X9 being SubSpace of T, A being Subset of T, A1 being Subset of X9
  st A = A1 holds Cl A1 = (Cl A) /\ ([#]X9)
proof
  let X9 be SubSpace of T, A be Subset of T, A1 be Subset of X9 such that
A1: A = A1;
  for p being set holds p in Cl A1 iff p in (Cl A) /\ ([#]X9)
  proof
    let p be set;
    thus p in Cl A1 implies p in (Cl A) /\ ([#]X9)
    proof
      reconsider DD = Cl A1 as Subset of T by Th11;
      assume
A2:   p in Cl A1;
A3:   for D1 being Subset of T st D1 is closed holds A c= D1 implies p in D1
      proof
        let D1 be Subset of T such that
A4:     D1 is closed;
        set D3 = D1 /\ [#]X9;
        assume A c= D1;
        then
A5:     A1 c= D1 /\ [#]X9 by A1,XBOOLE_1:19;
        D3 is closed by A4,Th13;
        then p in D3 by A2,A5,Th15;
        hence thesis by XBOOLE_0:def 4;
      end;
      p in DD by A2;
      then p in Cl A by A3,Th15;
      hence thesis by A2,XBOOLE_0:def 4;
    end;
    assume
A6: p in (Cl A) /\ ([#]X9);
    then
A7: p in Cl A by XBOOLE_0:def 4;
    now
      let D1 be Subset of X9;
      assume D1 is closed;
      then consider D2 being Subset of T such that
A8:   D2 is closed and
A9:   D1 = D2 /\ [#]X9 by Th13;
A10:  D2 /\ [#]X9 c= D2 by XBOOLE_1:17;
      assume A1 c= D1;
      then A c= D2 by A1,A9,A10,XBOOLE_1:1;
      then p in D2 by A7,A8,Th15;
      hence p in D1 by A6,A9,XBOOLE_0:def 4;
    end;
    hence thesis by A6,Th15;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th18:
  for A being Subset of T holds A c= Cl A
proof
  let A be Subset of T;
  now
    let x be set;
    assume
A1: x in A;
    assume not x in Cl A;
    then ex C being Subset of T st C is closed & A c= C & not x in C by A1,Th15
;
    hence contradiction by A1;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th19:
  for A,B being Subset of T st A c= B holds Cl A c= Cl B
proof
  let A,B be Subset of T such that
A1: A c= B;
  now
    let x be set;
    assume
A2: x in Cl A;
    now
      let D1 be Subset of T;
      assume
A3:   D1 is closed;
      assume B c= D1;
      then A c= D1 by A1,XBOOLE_1:1;
      hence x in D1 by A2,A3,Th15;
    end;
    hence x in Cl B by A2,Th15;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem
  for A,B being Subset of GX holds Cl(A \/ B) = Cl A \/ Cl B
proof
  let A,B be Subset of GX;
  now
    let x be set;
    assume
A1: x in Cl(A \/ B);
    assume
A2: not x in Cl A \/ Cl B;
    then not x in Cl A by XBOOLE_0:def 3;
    then consider G1 being Subset of GX such that
A3: G1 is open and
A4: x in G1 and
A5: A misses G1 by A1,Def7;
A6: A /\ G1 = {} by A5,XBOOLE_0:def 7;
    not x in Cl B by A2,XBOOLE_0:def 3;
    then consider G2 being Subset of GX such that
A7: G2 is open and
A8: x in G2 and
A9: B misses G2 by A1,Def7;
A10: G2 in the topology of GX by A7,Def2;
A11: B /\ G2 = {} by A9,XBOOLE_0:def 7;
    (A \/ B) /\ (G1 /\ G2) = (A /\ (G1 /\ G2)) \/ (B /\ (G2 /\ G1)) by
XBOOLE_1:23
      .= ((A /\ G1) /\ G2) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:16
      .= {} \/ ({} /\ G1) by A6,A11,XBOOLE_1:16
      .= {}GX;
    then
A12: (A \/ B) misses (G1 /\ G2) by XBOOLE_0:def 7;
    G1 in the topology of GX by A3,Def2;
    then G1 /\ G2 in the topology of GX by A10,Def1;
    then
A13: G1 /\ G2 is open by Def2;
    x in G1 /\ G2 by A4,A8,XBOOLE_0:def 4;
    hence contradiction by A1,A13,A12,Def7;
  end;
  then
A14: Cl(A \/ B) c= Cl A \/ Cl B by TARSKI:def 3;
  Cl A c= Cl(A \/ B) & Cl B c= Cl(A \/ B) by Th19,XBOOLE_1:7;
  then Cl A \/ Cl B c= Cl(A \/ B) by XBOOLE_1:8;
  hence thesis by A14,XBOOLE_0:def 10;
end;

theorem
  for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ Cl B
proof
  let A,B be Subset of T;
  Cl(A /\ B) c= Cl A & Cl(A /\ B) c= Cl B by Th19,XBOOLE_1:17;
  hence thesis by XBOOLE_1:19;
end;

theorem Th22:
  for A being Subset of T holds (A is closed implies Cl A = A) & (
  T is TopSpace-like & Cl A = A implies A is closed)
proof
  let A be Subset of T;
  thus A is closed implies Cl A = A
  proof
    assume A is closed;
    then for x be set st x in Cl A holds x in A by Th15;
    then
A1: Cl A c= A by TARSKI:def 3;
    A c= Cl A by Th18;
    hence thesis by A1,XBOOLE_0:def 10;
  end;
  assume
A2: T is TopSpace-like;
  then consider F being Subset-Family of T such that
A3: for C being Subset of T holds C in F iff C is closed & A c= C and
A4: Cl A = meet F by Th16;
  assume
A5: Cl A = A;
  for C being Subset of T st C in F holds C is closed by A3;
  hence thesis by A2,A5,A4,Th14;
end;

theorem
  for A being Subset of T holds (A is open implies Cl([#](T) \ A) = [#](
T) \ A) & (T is TopSpace-like & Cl([#](T) \ A) = [#](T) \ A implies A is open)
proof
  let A be Subset of T;
  [#](T) \([#]T \ A) = A by Th3;
  then
A1: A is open iff [#]T \ A is closed by Def3;
  hence A is open implies Cl ([#]T \ A) = [#]T \ A by Th22;
  assume T is TopSpace-like & Cl([#]T \ A) = [#]T \ A;
  hence thesis by A1,Th22;
end;

theorem
  for A being Subset of T, p being Point of T holds p in Cl A iff T is
non empty & for G being Subset of T st G is open holds p in G implies A meets G
  by Def7;

begin ::Addenda
:: from TOPMETR, 2008.07.06, A.T.

theorem
  for T being non empty TopStruct, A being non empty SubSpace of T for p
  being Point of A holds p is Point of T
proof
  let T be non empty TopStruct,A be non empty SubSpace of T;
  [#] A c= [#] T by Def4;
  hence thesis by TARSKI:def 3;
end;

theorem
  for A,B,C being TopSpace for f being Function of A,C holds f is
  continuous & C is SubSpace of B implies for h being Function of A,B st h = f
  holds h is continuous
proof
  let A,B,C be TopSpace, f be Function of A,C;
  assume that
A1: f is continuous and
A2: C is SubSpace of B;
  let h be Function of A,B such that
A3: h = f;
  for P being Subset of B holds P is closed implies h"P is closed
  proof
    let P be Subset of B such that
A4: P is closed;
A5: rng h c= the carrier of C by A3,RELAT_1:def 19;
A6: h"P = h"(rng h /\ P) by RELAT_1:133
      .= h"(rng h /\ [#] C /\ P) by A5,XBOOLE_1:28
      .= h"(rng h /\ ([#] C /\ P)) by XBOOLE_1:16
      .= h"(P /\ [#] C) by RELAT_1:133;
    reconsider C as SubSpace of B by A2;
    reconsider Q = P /\ [#] C as Subset of C;
    Q is closed by A4,Th13;
    hence thesis by A1,A3,A6,Def6;
  end;
  hence thesis by Def6;
end;

theorem
  for A being TopSpace, B being non empty TopSpace for f being Function
  of A,B for C being SubSpace of B holds f is continuous implies for h being
  Function of A,C st h = f holds h is continuous
proof
  let A be TopSpace, B be non empty TopSpace, f be Function of A,B, C be
  SubSpace of B;
  assume
A1: f is continuous;
  let h be Function of A,C such that
A2: h = f;
A3: rng f c= the carrier of C by A2,RELAT_1:def 19;
  for P being Subset of C holds P is closed implies h"P is closed
  proof
    let P be Subset of C;
    assume P is closed;
    then consider Q being Subset of B such that
A4: Q is closed and
A5: Q /\ ([#] C) = P by Th13;
    h"P = f"Q /\ f"([#] C) by A2,A5,FUNCT_1:68
      .= f"Q /\ f"(rng f /\ [#] C) by RELAT_1:133
      .= f"Q /\ f"(rng f) by A3,XBOOLE_1:28
      .= f"Q /\ dom f by RELAT_1:134
      .= f"Q by RELAT_1:132,XBOOLE_1:28;
    hence thesis by A1,A4,Def6;
  end;
  hence thesis by Def6;
end;

registration
  let T be TopSpace;
  cluster empty -> closed for Subset of T;
  coherence
  proof let S be Subset of T;
    assume S is empty;
    then
A1:  S = {}T;
    the carrier of T in the topology of T by Def1;
    hence [#] T \ S is open by Def2,A1;
  end;
end;

:: from BORSUK_1, 2008.07.07, A.T.

registration
  let X be TopSpace, Y be non empty TopStruct;
  let y be Point of Y;
  cluster X --> y -> continuous;
  coherence
  proof
    let P1 being Subset of Y such that
    P1 is closed;
    set F = X --> y, H = [#] X;
    per cases;
    suppose
      y in P1;
      then F"P1 = H by FUNCOP_1:14;
      hence thesis;
    end;
    suppose
      not y in P1;
      then F"P1 = {}X by FUNCOP_1:16;
      hence thesis;
    end;
  end;
end;

registration
  let S be TopSpace;
  let T be non empty TopSpace;
  cluster continuous for Function of S, T;
  existence
  proof
    set a = the Point of T;
    S --> a is continuous;
    hence thesis;
  end;
end;

reserve T for TopStruct,
  x,y for Point of T;

:: from TSP_1, T_0TOPSP, COMPTS_1, URYSOHN1 2008.07.16, A.T.

definition
  let T;
  attr T is T_0 means
  for x,y st for G being Subset of T st G is open holds x
  in G iff y in G holds x = y;
  attr T is T_1 means
  :Def9:
  for p,q being Point of T st p <> q ex G being
  Subset of T st G is open & p in G & q in G`;
  attr T is T_2 means
  :Def10:
  for p, q being Point of T st p <> q ex G1,G2
being Subset of T st G1 is open &G2 is open & p in G1 & q in G2 & G1 misses G2;
  attr T is regular means
  for p being Point of T, F being Subset of T st F is
  closed & p in F` ex G1,G2 being Subset of T st G1 is open & G2 is open & p in
  G1 & F c= G2 & G1 misses G2;
  attr T is normal means
  for F1,F2 being Subset of T st F1 is closed & F2 is
  closed & F1 misses F2 ex G1,G2 being Subset of T st G1 is open & G2 is open &
  F1 c= G1 & F2 c= G2 & G1 misses G2;
end;

definition
  let T;
  attr T is T_3 means
  :Def13:
  T is T_1 regular;
  attr T is T_4 means
  :Def14:
  T is T_1 normal;
end;

registration
  cluster T_3 -> T_1 regular for TopStruct;
  coherence by Def13;
  cluster T_1 regular -> T_3 for TopStruct;
  coherence by Def13;
  cluster T_4 -> T_1 normal for TopStruct;
  coherence by Def14;
  cluster T_1 normal -> T_4 for TopStruct;
  coherence by Def14;
end;

registration
  cluster T_1 for non empty TopSpace;
  existence
  proof
    set T = TopStruct(#1,[#]bool 1#);
A1: [#]the carrier of T = the carrier of T & for a being Subset-Family of
    T st a c= the topology of T holds union a in the topology of T;
    for a,b being Subset of T st a in the topology of T & b in the
    topology of T holds a /\ b in the topology of T;
    then reconsider T as non empty TopSpace by A1,Def1;
    take T;
    let p,q be Point of T;
    p = 0 by CARD_1:49,TARSKI:def 1;
    hence thesis by CARD_1:49,TARSKI:def 1;
  end;
end;

registration
  cluster T_1 -> T_0 for TopStruct;
  coherence
  proof
    let T;
    assume
A1: T is T_1;
    let x,y;
    assume
A2: for G being Subset of T st G is open holds x in G iff y in G;
    assume x <> y;
    then consider G being Subset of T such that
A3: G is open & x in G and
A4: y in G` by A1,Def9;
    not y in G by A4,XBOOLE_0:def 5;
    hence contradiction by A2,A3;
  end;
  cluster T_2 -> T_1 for TopStruct;
  coherence
  proof
    let T;
    assume
A5: T is T_2;
    let p,q being Point of T;
    assume p <> q;
    then consider G1,G2 being Subset of T such that
A6: G1 is open and
    G2 is open and
A7: p in G1 and
A8: q in G2 and
A9: G1 misses G2 by A5,Def10;
    take G1;
    thus G1 is open by A6;
    thus p in G1 by A7;
    G2 c= G1` by A9,SUBSET_1:23;
    hence thesis by A8;
  end;
end;

:: missing, 2009.02.14, A.T.

registration
  let T be TopSpace;
  cluster the TopStruct of T -> TopSpace-like;
  coherence
  proof
    set S = the TopStruct of T;
    thus the carrier of S in the topology of S & (for a being Subset-Family of
S st a c= the topology of S holds union a in the topology of S) & for a,b being
Subset of S st a in the topology of S & b in the topology of S holds a /\ b in
    the topology of S by Def1;
  end;
end;

registration
  let T be non empty TopStruct;
  cluster the TopStruct of T -> non empty;
  coherence;
end;

theorem
  for T being TopStruct st the TopStruct of T is TopSpace-like holds T
  is TopSpace-like
proof
  let T be TopStruct;
  set S = the TopStruct of T;
  assume ( the carrier of S in the topology of S & for a being Subset-Family
  of S st a c= the topology of S holds union a in the topology of S )& for a,b
being Subset of S st a in the topology of S & b in the topology of S holds a /\
  b in the topology of S;
  hence
  the carrier of T in the topology of T & (for a being Subset-Family of T
  st a c= the topology of T holds union a in the topology of T) & for a,b being
Subset of T st a in the topology of T & b in the topology of T holds a /\ b in
  the topology of T;
end;

theorem
  for T being TopStruct, S being SubSpace of the TopStruct of T holds S
  is SubSpace of T
proof
  let T be TopStruct, S be SubSpace of the TopStruct of T;
  [#]S c= [#]the TopStruct of T by Def4;
  hence
  [#]S c= [#]T & for P being Subset of S holds P in the topology of S iff
  ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by Def4;
end;

registration
  let T be TopSpace;
  cluster open for Subset of T;
  existence
  proof
    take {}T;
    thus {}T in the topology of T by Th1;
  end;
end;

theorem
  for T being TopSpace, X being set holds X is open Subset of T iff X is
  open Subset of the TopStruct of T
proof
  let T be TopSpace, X be set;
  X in the topology of T iff X in the topology of the TopStruct of T;
  hence thesis by Def2;
end;

theorem Th31:
  for T being TopSpace, X being set holds X is closed Subset of T
  iff X is closed Subset of the TopStruct of T
proof
  let T be TopSpace, X be set;
  [#]T \ X in the topology of T iff ([#]the TopStruct of T) \ X in the
  topology of the TopStruct of T;
  then [#]T \ X is open iff ([#]the TopStruct of T) \ X is open by Def2;
  hence thesis by Def3;
end;

theorem Th32:
  for S,T being TopSpace, f being Function of S,T, g being
  Function of the TopStruct of S, T st f = g holds f is continuous iff g is
  continuous
proof
  let S,T be TopSpace, f be Function of S,T, g be Function of the TopStruct of
  S, T such that
A1: f = g;
  thus f is continuous implies g is continuous
  proof
    assume
A2: f is continuous;
    let P1 being Subset of T;
    assume P1 is closed;
    then f"P1 is closed by A2,Def6;
    hence g" P1 is closed by A1,Th31;
  end;
  assume
A3: g is continuous;
  let P1 being Subset of T;
  assume P1 is closed;
  then g"P1 is closed by A3,Def6;
  hence f" P1 is closed by A1,Th31;
end;

theorem Th33:
  for S,T being TopSpace, f being Function of S,T, g being
  Function of S, the TopStruct of T st f = g holds f is continuous iff g is
  continuous
proof
  let S,T be TopSpace, f be Function of S,T, g be Function of S, the TopStruct
  of T such that
A1: f = g;
  thus f is continuous implies g is continuous
  proof
    assume
A2: f is continuous;
    let P1 being Subset of the TopStruct of T;
    reconsider P = P1 as Subset of T;
    assume P1 is closed;
    then P is closed by Th31;
    hence g" P1 is closed by A1,A2,Def6;
  end;
  assume
A3: g is continuous;
  let P1 being Subset of T;
  reconsider P = P1 as Subset of the TopStruct of T;
  assume P1 is closed;
  then P is closed by Th31;
  hence f" P1 is closed by A1,A3,Def6;
end;

theorem
  for S,T being TopSpace, f being Function of S,T, g being Function of
the TopStruct of S, the TopStruct of T st f = g holds f is continuous iff g is
  continuous
proof
  let S,T be TopSpace, f be Function of S,T, g be Function of the TopStruct of
  S, the TopStruct of T such that
A1: f = g;
  reconsider h = f as Function of S, the TopStruct of T;
  h is continuous iff g is continuous by A1,Th32;
  hence f is continuous iff g is continuous by Th33;
end;

:: from BORSUK_3, 2009.03.15, A.T.

registration
  let T be TopStruct, P be empty Subset of T;
  cluster T | P -> empty;
  coherence by Th8;
end;

theorem Th35:
  for S,T being TopStruct holds S is SubSpace of T iff S is
  SubSpace of the TopStruct of T
proof
  let S,T be TopStruct;
  thus S is SubSpace of T implies S is SubSpace of the TopStruct of T
  proof
    assume
A1: S is SubSpace of T;
    then [#]S c= [#]T by Def4;
    hence [#]S c= [#]the TopStruct of T;
    let P be Subset of S;
    thus P in the topology of S implies ex Q being Subset of the TopStruct of
    T st Q in the topology of the TopStruct of T & P = Q /\ [#]S by A1,Def4;
    given Q being Subset of the TopStruct of T such that
A2: Q in the topology of the TopStruct of T & P = Q /\ [#]S;
    thus P in the topology of S by A1,A2,Def4;
  end;
  assume
A3: S is SubSpace of the TopStruct of T;
  then [#]S c= [#]the TopStruct of T by Def4;
  hence [#]S c= [#]T;
  let P be Subset of S;
  thus P in the topology of S implies ex Q being Subset of T st Q in the
  topology of T & P = Q /\ [#]S by A3,Def4;
  given Q being Subset of T such that
A4: Q in the topology of T & P = Q /\ [#]S;
  thus P in the topology of S by A3,A4,Def4;
end;

theorem
  for X being Subset of T, Y being Subset of the TopStruct of T st X = Y
  holds the TopStruct of T|X = (the TopStruct of T)|Y
proof
  let X be Subset of T, Y be Subset of the TopStruct of T;
  assume X = Y;
  then
A1: [#](the TopStruct of T|X) = Y by Def5;
  the TopStruct of T|X is strict SubSpace of the TopStruct of T by Th35;
  hence the TopStruct of T|X = (the TopStruct of T)|Y by A1,Def5;
end;

:: missing, 2009.05.26, A.T.

registration
 cluster strict empty for TopStruct;
  existence
  proof
    set T = the TopStruct;
    take T | {}T;
    thus thesis;
  end;
end;

:: from COMPLSP1, 2010.02.25, A.T.

registration
  let A be non empty set, t be Subset-Family of A;
  cluster TopStruct(#A,t#) -> non empty;
  coherence;
end;

:: from BORSUK_3, 2011.07.08. A.T.

registration
  cluster empty -> T_0 for TopStruct;
  coherence
   proof let T be TopStruct such that
A1:  T is empty;
    let x,y be Point of T such that
  for G being Subset of T st G is open holds x in G iff y in G;
    thus x = {} by A1,SUBSET_1:def 1 .= y by A1,SUBSET_1:def 1;
   end;
end;

registration
  cluster strict empty for TopSpace;
  existence
  proof
    set T = the TopSpace;
    take T | {}T;
    thus thesis;
  end;
end;