pre_topc.miz



    begin

    definition

      struct ( 1-sorted) TopStruct (# the carrier -> set,

the topology -> Subset-Family of the carrier #)

       attr strict strict;

    end

    reserve T for TopStruct;

    definition

      let IT be TopStruct;

      :: PRE_TOPC:def1

      attr IT is TopSpace-like means

      : Def1: the carrier of IT in the topology of IT & (for a be Subset-Family of IT st a c= the topology of IT holds ( union a) in the topology of IT) & for a,b be 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 object;

            reconsider xx = x as set by TARSKI: 1;

            assume x in T;

            then x = {} or x = X by TARSKI:def 2;

            then xx c= X;

            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 be 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, ZFMISC_1: 25, ZFMISC_1: 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 be non empty set, T be Subset-Family of X such that

         A4: (the carrier of TopStruct (# X, T #) in the topology of TopStruct (# X, T #) & for a be 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 be 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;

      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 :: PRE_TOPC:1

    

     Th1: {} in the topology of GX

    proof

      reconsider A = {} as Subset-Family of GX by XBOOLE_1: 2;

      A c= the topology of GX;

      hence thesis by Def1, ZFMISC_1: 2;

    end;

    theorem :: PRE_TOPC:2

    for T be 1-sorted, P be 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 :: PRE_TOPC:3

    

     Th3: for T be 1-sorted, P be 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 :: PRE_TOPC:4

    

     Th4: for T be 1-sorted, P be 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 :: PRE_TOPC:5

    for T be 1-sorted, P,Q be 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 :: PRE_TOPC:6

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

    definition

      let T be TopStruct, P be Subset of T;

      :: PRE_TOPC:def2

      attr P is open means

      : Def2: P in the topology of T;

    end

    definition

      let T be TopStruct, P be Subset of T;

      :: PRE_TOPC:def3

      attr P is closed means

      : Def3: (( [#] T) \ P) is open;

    end

    definition

      let T be TopStruct;

      :: PRE_TOPC:def4

      mode SubSpace of T -> TopStruct means

      : Def4: ( [#] it ) c= ( [#] T) & for P be Subset of it holds P in the topology of it iff ex Q be 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 be 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 be 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 be 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 be Subset-Family of T such that

             A4: for Z be 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 object;

              assume

               A6: x in (( union b) /\ P);

              then x in ( union b) by XBOOLE_0:def 4;

              then

              consider Z be 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 by A4;

            then

             A10: ( union b) in the topology of T by Def1;

            ( union a) c= (( union b) /\ P)

            proof

              let x be object;

              assume

               A11: x in ( union a);

              then

              consider Z1 be set such that

               A12: x in Z1 and

               A13: Z1 in a by TARSKI:def 4;

              consider Z3 be 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 be 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 be Subset of T such that

             A17: P1 in the topology of T and

             A18: V = (P1 /\ P) by A2, A15, Def4;

            consider Q1 be 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;

      :: PRE_TOPC:def5

      func T | P -> strict SubSpace of T means

      : Def5: ( [#] it ) = P;

      existence

      proof

        defpred Q[ set] means ex Q be Subset of T st Q in the topology of T & $1 = (Q /\ P);

        consider top1 be Subset-Family of P such that

         A1: for Z be 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 be Subset of Y holds Z in top1 iff ex Q be 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 be 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 object;

          assume x in the topology of Z2;

          then ex Q be 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 object;

          assume x in the topology of Z1;

          then ex Q be 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 :: PRE_TOPC:7

    for S be TopSpace, P1,P2 be Subset of S, P19 be 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 be Subset of ((S | P2) | P19) holds R in the topology of ((S | P2) | P19) iff ex Q be 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 be 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 be 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 be 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 be 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 :: PRE_TOPC:8

    

     Th8: for GX be TopStruct, A be 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 :: PRE_TOPC:9

    for X be TopStruct, Y be non empty TopStruct, f be Function of X, Y, P be 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;

      :: PRE_TOPC:def6

      attr f is continuous means for P1 be Subset of T st P1 is closed holds (f " P1) is closed;

    end

    theorem :: PRE_TOPC:10

    for T1,T2,S1,S2 be 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 be Subset of S1 holds P in the topology of S1 iff ex Q be 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 :: PRE_TOPC:11

    

     Th11: for X9 be SubSpace of T, A be 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 :: PRE_TOPC:12

    for A be Subset of T st A <> ( {} T) holds ex x be 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;

        (( [#] T) \ ( [#] T)) = ( {} T) by Th4;

        hence thesis by A1;

      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 :: PRE_TOPC:13

    

     Th13: for X9 be SubSpace of T, B be Subset of X9 holds B is closed iff ex C be 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;

        then (( [#] X9) \ B) in the topology of X9;

        then

        consider V be 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;

        then (( [#] T) \ V) is closed by A6;

        hence ex C be Subset of T st C is closed & (C /\ ( [#] X9)) = B by A5;

      end;

      now

        given C be Subset of T such that

         A7: C is closed and

         A8: (C /\ ( [#] X9)) = B;

        (( [#] T) \ C) is open by A7;

        then (( [#] T) \ C) in the topology of T;

        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;

        hence B is closed;

      end;

      hence thesis by A2;

    end;

    theorem :: PRE_TOPC:14

    

     Th14: for F be Subset-Family of GX st for A be 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 be 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 be Subset-Family of GX such that

         A3: for B be Subset of GX holds B in R1 iff Q[B] from SUBSET_1:sch 3;

        

         A4: for x be set st x in the carrier of GX holds (for A be Subset of GX st A in F holds x in A) iff for Z be 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 be Subset of GX st A in F holds x in A) implies for Z be Subset of GX st Z in R1 holds not x in Z

          proof

            assume

             A6: for A be 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 be 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 be object holds x in (( [#] GX) \ ( union R1)) iff x in ( meet F)

        proof

          let x be object;

          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 be 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 be Subset of GX st A in F holds x in A by SETFAM_1:def 1;

          then for Z be 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 object;

          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;

          hence B in the topology of GX;

        end;

        then R1 c= the topology of GX;

        then ( union R1) in the topology of GX by Def1;

        then

         A14: ( union R1) is open;

        (( [#] GX) \ (( [#] GX) \ ( union R1))) = ( union R1) by Th3;

        then (( [#] GX) \ ( union R1)) is closed by A14;

        hence thesis by A9, TARSKI: 2;

      end;

        suppose

         A15: F = {} ;

        the carrier of GX in the topology of GX by Def1;

        then

         A16: ( [#] GX) is open;

        ( {} GX) is closed by A16;

        hence thesis by A15, SETFAM_1:def 1;

      end;

    end;

    definition

      let GX be TopStruct, A be Subset of GX;

      :: PRE_TOPC:def7

      func Cl A -> Subset of GX means

      : Def7: for p be set st p in the carrier of GX holds p in it iff for G be Subset of GX st G is open holds p in G implies A meets G;

      existence

      proof

        defpred P[ set] means for G be Subset of GX st G is open holds $1 in G implies A meets G;

        consider P be Subset of GX such that

         A1: for x be 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 be set st p in the carrier of GX holds p in C1 iff for G be Subset of GX st G is open holds p in G implies A meets G and

         A3: for p be set st p in the carrier of GX holds p in C2 iff for V be Subset of GX st V is open holds p in V implies A meets V;

        for x be object holds x in C1 iff x in C2

        proof

          let x be object;

          thus x in C1 implies x in C2

          proof

            assume

             A4: x in C1;

            then for G be 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 be 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: 2;

      end;

      projectivity

      proof

        let r,A be Subset of GX;

        assume

         A6: for p be set st p in the carrier of GX holds p in r iff for G be 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 be Subset of GX st G is open & p in G holds r meets G by XBOOLE_0: 3;

        assume

         A8: for G be 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;

          now

            assume p in (( [#] GX) \ C);

            then r meets (( [#] GX) \ C) by A8, A10;

            then ex x be object 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 be 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;

          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 :: PRE_TOPC:15

    

     Th15: for A be Subset of T, p be set st p in the carrier of T holds p in ( Cl A) iff for C be 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 be Subset of T st C is closed holds (A c= C implies p in C);

        for G be 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;

          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;

        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 :: PRE_TOPC:16

    

     Th16: for A be Subset of GX holds ex F be Subset-Family of GX st (for C be 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 be Subset of GX st C1 = $1 & C1 is closed & A c= $1;

      consider F9 be Subset-Family of GX such that

       A1: for C be Subset of GX holds C in F9 iff Q[C] from SUBSET_1:sch 3;

      take F = F9;

      thus for C be 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 be 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 be object holds p in ( Cl A) iff p in ( meet F)

      proof

        let p be object;

         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 be 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: 2;

    end;

    theorem :: PRE_TOPC:17

    for X9 be SubSpace of T, A be Subset of T, A1 be 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 be object holds p in ( Cl A1) iff p in (( Cl A) /\ ( [#] X9))

      proof

        let p be object;

        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 be 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 be 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;

          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: 2;

    end;

    theorem :: PRE_TOPC:18

    

     Th18: for A be Subset of T holds A c= ( Cl A)

    proof

      let A be Subset of T;

      now

        let x be object;

        assume

         A1: x in A;

        assume not x in ( Cl A);

        then ex C be Subset of T st C is closed & A c= C & not x in C by A1, Th15;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: PRE_TOPC:19

    

     Th19: for A,B be 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;

      let x be object;

      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;

        hence x in D1 by A2, A3, Th15;

      end;

      hence x in ( Cl B) by A2, Th15;

    end;

    theorem :: PRE_TOPC:20

    for A,B be Subset of GX holds ( Cl (A \/ B)) = (( Cl A) \/ ( Cl B))

    proof

      let A,B be Subset of GX;

      now

        let x be object;

        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 be 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 be 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;

        

         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;

        then (G1 /\ G2) in the topology of GX by A10, Def1;

        then

         A13: (G1 /\ G2) is open;

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

      ( 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 :: PRE_TOPC:21

    for A,B be 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 :: PRE_TOPC:22

    

     Th22: for A be 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 object st x in ( Cl A) holds x in A by Th15;

        then

         A1: ( Cl A) c= A;

        A c= ( Cl A) by Th18;

        hence thesis by A1, XBOOLE_0:def 10;

      end;

      assume

       A2: T is TopSpace-like;

      then

      consider F be Subset-Family of T such that

       A3: for C be 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 be Subset of T st C in F holds C is closed by A3;

      hence thesis by A2, A5, A4, Th14;

    end;

    theorem :: PRE_TOPC:23

    for A be 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;

      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 :: PRE_TOPC:24

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

    begin

    theorem :: PRE_TOPC:25

    for T be non empty TopStruct, A be non empty SubSpace of T holds for p be 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;

    end;

    theorem :: PRE_TOPC:26

    for A,B,C be TopSpace holds for f be Function of A, C holds f is continuous & C is SubSpace of B implies for h be 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 be 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;

      end;

      hence thesis;

    end;

    theorem :: PRE_TOPC:27

    for A be TopSpace, B be non empty TopSpace holds for f be Function of A, B holds for C be SubSpace of B holds f is continuous implies for h be 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 be 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 be 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;

      end;

      hence thesis;

    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 A1;

      end;

    end

    registration

      let X be TopSpace, Y be non empty TopStruct;

      let y be Point of Y;

      cluster (X --> y) -> continuous;

      coherence

      proof

        let P1 be 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;

    definition

      let T;

      :: PRE_TOPC:def8

      attr T is T_0 means for x, y st for G be Subset of T st G is open holds x in G iff y in G holds x = y;

      :: PRE_TOPC:def9

      attr T is T_1 means for p,q be Point of T st p <> q holds ex G be Subset of T st G is open & p in G & q in (G ` );

      :: PRE_TOPC:def10

      attr T is T_2 means for p,q be Point of T st p <> q holds ex G1,G2 be Subset of T st G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2;

      :: PRE_TOPC:def11

      attr T is regular means for p be Point of T, F be Subset of T st F is closed & p in (F ` ) holds ex G1,G2 be Subset of T st G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2;

      :: PRE_TOPC:def12

      attr T is normal means for F1,F2 be Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds ex G1,G2 be Subset of T st G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2;

    end

    definition

      let T;

      :: PRE_TOPC:def13

      attr T is T_3 means T is T_1 regular;

      :: PRE_TOPC:def14

      attr T is T_4 means T is T_1 normal;

    end

    registration

      cluster T_3 -> T_1 regular for TopStruct;

      coherence ;

      cluster T_1 regular -> T_3 for TopStruct;

      coherence ;

      cluster T_4 -> T_1 normal for TopStruct;

      coherence ;

      cluster T_1 normal -> T_4 for TopStruct;

      coherence ;

    end

    registration

      cluster T_1 for non empty TopSpace;

      existence

      proof

        set T = TopStruct (# { {} }, ( [#] ( bool { {} })) #);

        

         A1: ( [#] the carrier of T) = the carrier of T & for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T;

        for a,b be 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 = {} by TARSKI:def 1;

        hence thesis by 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 be Subset of T st G is open holds x in G iff y in G;

        assume x <> y;

        then

        consider G be Subset of T such that

         A3: G is open & x in G and

         A4: y in (G ` ) by A1;

         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 be Point of T;

        assume p <> q;

        then

        consider G1,G2 be 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;

        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

    registration

      let T be TopSpace;

      cluster the TopStruct of T -> TopSpace-like;

      coherence by Def1;

    end

    registration

      let T be non empty TopStruct;

      cluster the TopStruct of T -> non empty;

      coherence ;

    end

    theorem :: PRE_TOPC:28

    for T be TopStruct st the TopStruct of T is TopSpace-like holds T is TopSpace-like;

    theorem :: PRE_TOPC:29

    for T be TopStruct, S be 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 be Subset of S holds P in the topology of S iff ex Q be 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 :: PRE_TOPC:30

    for T be TopSpace, X be 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 :: PRE_TOPC:31

    

     Th31: for T be TopSpace, X be 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) is open iff (( [#] the TopStruct of T) \ X) is open;

      hence thesis by Def3;

    end;

    theorem :: PRE_TOPC:32

    

     Th32: for S,T be TopSpace, f be Function of S, T, g be 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 by A1, Th31;

      assume

       A2: g is continuous;

      let P1 be Subset of T;

      assume P1 is closed;

      then (g " P1) is closed by A2;

      hence (f " P1) is closed by A1, Th31;

    end;

    theorem :: PRE_TOPC:33

    

     Th33: for S,T be TopSpace, f be Function of S, T, g be 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 by Th31, A1;

      assume

       A2: g is continuous;

      let P1 be 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, A2;

    end;

    theorem :: PRE_TOPC:34

    for S,T be TopSpace, f be Function of S, T, g be 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;

    registration

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

      cluster (T | P) -> empty;

      coherence by Th8;

    end

    theorem :: PRE_TOPC:35

    

     Th35: for S,T be 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 be Subset of the TopStruct of T st Q in the topology of the TopStruct of T & P = (Q /\ ( [#] S)) by A1, Def4;

        given Q be 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 be Subset of T st Q in the topology of T & P = (Q /\ ( [#] S)) by A3, Def4;

      given Q be 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 :: PRE_TOPC:36

    for X be Subset of T, Y be 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;

    registration

      cluster strict empty for TopStruct;

      existence

      proof

        set T = the TopStruct;

        take (T | ( {} T));

        thus thesis;

      end;

    end

    registration

      let A be non empty set, t be Subset-Family of A;

      cluster TopStruct (# A, t #) -> non empty;

      coherence ;

    end

    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 be 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