fintopo7.miz



    begin

    reserve X for non empty set;

    theorem :: FINTOPO7:1

    for B,Y be Subset-Family of X st Y c= ( UniCl B) holds ( union Y) in ( UniCl B)

    proof

      let B,Y be Subset-Family of X;

      assume Y c= ( UniCl B);

      then ( union Y) in ( UniCl ( UniCl B)) by CANTOR_1:def 1;

      hence thesis by YELLOW_9: 15;

    end;

    theorem :: FINTOPO7:2

    

     Th1: for B be empty Subset-Family of X st (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB)) & X = ( union B) holds ( FinMeetCl B) c= ( UniCl B)

    proof

      let B be empty Subset-Family of X;

      assume that for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB) and

       A1: X = ( union B);

      ( FinMeetCl B) c= ( UniCl B)

      proof

        let x be object;

        assume

         A2: x in ( FinMeetCl B);

        then

        reconsider x1 = x as Subset of X;

        consider Y be Subset-Family of X such that

         A3: Y c= B and Y is finite and

         A4: x1 = ( Intersect Y) by A2, CANTOR_1:def 3;

        Y = {} & ( meet {} ) = {} by A3, SETFAM_1: 1;

        then x1 = X by A4, SETFAM_1:def 9;

        hence x in ( UniCl B) by A1, CANTOR_1:def 1;

      end;

      hence ( FinMeetCl B) c= ( UniCl B);

    end;

    theorem :: FINTOPO7:3

    

     Th2: for B be non empty Subset-Family of X st (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB)) & X = ( union B) holds ( FinMeetCl B) c= ( UniCl B)

    proof

      let B be non empty Subset-Family of X;

      assume that

       A1: for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB) and

       A2: X = ( union B);

      let x be object;

      assume

       A3: x in ( FinMeetCl B);

      then

      reconsider x0 = x as Subset of X;

      consider Y be Subset-Family of X such that

       A4: Y c= B and

       A5: Y is finite and

       A6: x0 = ( Intersect Y) by A3, CANTOR_1:def 3;

      defpred PP[ Nat] means for Y be Subset-Family of X, x be Subset of X st Y c= B & ( card Y) = $1 & x = ( Intersect Y) holds x in ( UniCl B);

      

       A7: PP[ 0 ]

      proof

        let Y be Subset-Family of X, x be Subset of X;

        assume that Y c= B and

         A8: ( card Y) = 0 and

         A9: x = ( Intersect Y);

        Y = {} by A8;

        then

         A10: x = X by A9, SETFAM_1:def 9;

        reconsider x0 = x as set;

        thus x in ( UniCl B) by A2, A10, CANTOR_1:def 1;

      end;

      

       A11: for k be Nat holds PP[k] implies PP[(k + 1)]

      proof

        let k be Nat;

        assume

         A12: PP[k];

        let Y be Subset-Family of X, x be Subset of X;

        assume that

         A13: Y c= B and

         A14: ( card Y) = (k + 1) and

         A15: x = ( Intersect Y);

        Y is finite set by A14;

        then

        consider x1 be Element of Y, C be Subset of Y such that

         A16: Y = (C \/ {x1}) and

         A17: ( card C) = k by A14, PRE_CIRC: 24;

        

         A18: C c= B & ( card C) = k by A13, A17;

        B c= ( bool X);

        then C c= ( bool X) by A13;

        then

        reconsider C0 = C as Subset-Family of X;

        per cases ;

          suppose

           A19: C = {} ;

          ( meet {x1}) = x1 by SETFAM_1: 10;

          then

           A20: ( Intersect Y) = x1 by A19, A16, SETFAM_1:def 9;

          then x1 in ( bool X);

          then {x1} c= ( bool X) by TARSKI:def 1;

          then

          reconsider B0 = {x1} as Subset-Family of X;

          x1 in Y by A16;

          then

           A21: {x1} c= Y & Y c= B by A13, TARSKI:def 1;

          x in B & B0 c= B & x = ( union B0) by A16, A21, A15, A20;

          hence x in ( UniCl B) by CANTOR_1:def 1;

        end;

          suppose

           A22: C <> {} ;

          then ( meet (C \/ {x1})) = (( meet C) /\ ( meet {x1})) by SETFAM_1: 9;

          then

           A23: ( meet Y) = (( meet C) /\ x1) by A16, SETFAM_1: 10;

          ( meet Y) = ( Intersect Y) by A16, SETFAM_1:def 9;

          then

           A24: ( Intersect Y) = (( Intersect C0) /\ x1) by A22, A23, SETFAM_1:def 9;

          ( Intersect Y) in ( UniCl B)

          proof

            ( Intersect C0) in ( UniCl B) by A18, A12;

            then

            consider Y2 be Subset-Family of X such that

             A25: Y2 c= B and

             A26: ( Intersect C0) = ( union Y2) by CANTOR_1:def 1;

            per cases ;

              suppose

               A27: Y2 is empty;

               {} c= X;

              then

              reconsider x0 = {} as Subset of X;

              

               A28: {} c= ( bool X) & {} c= B & {} = ( union {} ) by ZFMISC_1: 2;

              then

              reconsider S = {} as Subset-Family of X;

              thus thesis by A27, A24, A26, A28, CANTOR_1:def 1;

            end;

              suppose

               A29: Y2 is non empty;

              set Y3 = the set of all (y /\ x1) where y be Element of Y2;

              Y3 c= ( bool X)

              proof

                let x be object;

                assume

                 A30: x in Y3;

                then

                reconsider x as Element of Y3;

                consider y be Element of Y2 such that

                 A31: x = (y /\ x1) by A30;

                

                 A32: x c= x1 by A31, XBOOLE_1: 17;

                x1 in Y & Y c= ( bool X) by A16;

                then x1 c= X;

                then x c= X by A32;

                hence thesis;

              end;

              then

              reconsider Y3 as Subset-Family of X;

              

               A33: ( union Y3) = (( union Y2) /\ x1)

              proof

                hereby

                  let x be object;

                  assume

                   A34: x in ( union Y3);

                  consider a1 be set such that

                   A35: x in a1 and

                   A36: a1 in Y3 by A34, TARSKI:def 4;

                  consider x2 be Element of Y2 such that

                   A37: a1 = (x2 /\ x1) by A36;

                  x in a1 & a1 c= x2 & a1 c= x1 by A35, A37, XBOOLE_1: 17;

                  then x in ( union Y2) & x in x1 by A29, TARSKI:def 4;

                  hence x in (( union Y2) /\ x1) by XBOOLE_0:def 4;

                end;

                let x be object;

                assume x in (( union Y2) /\ x1);

                then

                 A38: x in ( union Y2) & x in x1 by XBOOLE_0:def 4;

                then

                consider a be set such that

                 A39: x in a and

                 A40: a in Y2 by TARSKI:def 4;

                reconsider a as Element of Y2 by A40;

                

                 A41: x in (a /\ x1) by A38, A39, XBOOLE_0:def 4;

                (a /\ x1) in Y3;

                hence x in ( union Y3) by A41, TARSKI:def 4;

              end;

              

               A42: ( Intersect Y) = ( union Y3)

              proof

                hereby

                  let t be object;

                  assume t in ( Intersect Y);

                  then

                   A43: t in ( union Y2) & t in x1 by A24, A26, XBOOLE_0:def 4;

                  then

                  consider t0 be set such that

                   A44: t in t0 and

                   A45: t0 in Y2 by TARSKI:def 4;

                  

                   A46: t in (t0 /\ x1) by A43, A44, XBOOLE_0:def 4;

                  (t0 /\ x1) in Y3 by A45;

                  hence t in ( union Y3) by A46, TARSKI:def 4;

                end;

                let t be object;

                assume t in ( union Y3);

                then t in ( union Y2) & t in x1 by A33, XBOOLE_0:def 4;

                then t in ( meet C0) & t in x1 by A26, A22, SETFAM_1:def 9;

                then t in (( meet C0) /\ x1) by XBOOLE_0:def 4;

                hence t in ( Intersect Y) by A23, A16, SETFAM_1:def 9;

              end;

              Y3 c= ( UniCl B)

              proof

                let t be object;

                assume t in Y3;

                then

                consider a be Element of Y2 such that

                 A47: t = (a /\ x1);

                reconsider a2 = a as Element of B by A29, A25;

                reconsider x2 = x1 as Element of B by A13, A16;

                consider BP be Subset of B such that

                 A48: (a2 /\ x2) = ( union BP) by A1;

                reconsider ax = (a2 /\ x2) as Subset of X;

                BP c= B & B c= ( bool X);

                then

                 A49: BP c= ( bool X);

                thus t in ( UniCl B) by A47, A48, A49, CANTOR_1:def 1;

              end;

              then ( Intersect Y) in ( UniCl ( UniCl B)) by A42, CANTOR_1:def 1;

              hence thesis by YELLOW_9: 15;

            end;

          end;

          hence x in ( UniCl B) by A15;

        end;

      end;

      

       A50: for k be Nat holds PP[k] from NAT_1:sch 2( A7, A11);

      reconsider CY = ( card Y) as Nat by A5;

       PP[CY] by A50;

      hence x in ( UniCl B) by A4, A6;

    end;

    theorem :: FINTOPO7:4

    

     Th3: for B be Subset-Family of X st (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB)) & X = ( union B) holds ( UniCl B) = ( UniCl ( FinMeetCl B)) & TopStruct (# X, ( UniCl B) #) is TopSpace-like

    proof

      let B be Subset-Family of X;

      assume that

       A1: (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB)) and

       A2: X = ( union B);

      thus ( UniCl B) = ( UniCl ( FinMeetCl B))

      proof

        hereby

          let x be object;

          assume

           A3: x in ( UniCl B);

          then

          reconsider x0 = x as Subset of X;

          consider Y be Subset-Family of X such that

           A4: Y c= B and

           A5: x = ( union Y) by A3, CANTOR_1:def 1;

          B c= ( FinMeetCl B) by CANTOR_1: 4;

          then Y c= ( FinMeetCl B) by A4;

          hence x in ( UniCl ( FinMeetCl B)) by A5, CANTOR_1:def 1;

        end;

        let x be object;

        assume

         A6: x in ( UniCl ( FinMeetCl B));

        then

        reconsider x0 = x as Subset of X;

        consider Y1 be Subset-Family of X such that

         A7: Y1 c= ( FinMeetCl B) and

         A8: x = ( union Y1) by A6, CANTOR_1:def 1;

        ( FinMeetCl B) c= ( UniCl B)

        proof

          per cases ;

            suppose B is empty;

            hence thesis by A1, A2, Th1;

          end;

            suppose B is non empty;

            hence thesis by A1, A2, Th2;

          end;

        end;

        then Y1 c= ( UniCl B) by A7;

        then ( union Y1) in ( UniCl ( UniCl B)) by CANTOR_1:def 1;

        hence x in ( UniCl B) by A8, YELLOW_9: 15;

      end;

      hence TopStruct (# X, ( UniCl B) #) is TopSpace-like by CANTOR_1: 15;

    end;

    theorem :: FINTOPO7:5

    for FMT be non empty FMT_Space_Str holds ex S be RelStr st for x be Element of FMT holds ( U_FMT x) is Subset of S

    proof

      let FMT be non empty FMT_Space_Str;

      set S = ( BoolePoset the carrier of FMT);

      take S;

      thus thesis by WAYBEL_7: 2;

    end;

    registration

      let T be non empty TopSpace;

      cluster ( NeighSp T) -> Fo_filled;

      coherence

      proof

        set NT = ( NeighSp T);

        for x be Element of NT, D be Subset of NT st D in ( U_FMT x) holds x in D

        proof

          let x be Element of NT, D be Subset of NT such that

           A1: D in ( U_FMT x);

          ( U_FMT x) = { V where V be Subset of T : V in the topology of T & x in V } by FINTOPO2:def 7;

          then

          consider V0 be Subset of T such that

           A2: D = V0 and V0 in the topology of T and

           A3: x in V0 by A1;

          thus thesis by A2, A3;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let ET be non empty strict FMT_Space_Str, O be Subset of ET;

      :: FINTOPO7:def1

      attr O is open means

      : Def1: for x be Element of ET st x in O holds O in ( U_FMT x);

    end

    definition

      let ET be non empty strict FMT_Space_Str;

      :: FINTOPO7:def2

      attr ET is U_FMT_filter means

      : Def2: for x be Element of ET holds ( U_FMT x) is Filter of the carrier of ET;

      :: FINTOPO7:def3

      attr ET is U_FMT_with_point means

      : Def3: for x be Element of ET, V be Element of ( U_FMT x) holds x in V;

      :: FINTOPO7:def4

      attr ET is U_FMT_local means

      : Def4: for x be Element of ET, V be Element of ( U_FMT x) holds ex W be Element of ( U_FMT x) st for y be Element of ET st y is Element of W holds V is Element of ( U_FMT y);

    end

    theorem :: FINTOPO7:6

    

     Th4: for ET be non empty strict FMT_Space_Str st ET is U_FMT_filter holds for x be Element of ET holds ( U_FMT x) is non empty;

    theorem :: FINTOPO7:7

    for ET be non empty strict FMT_Space_Str st ET is U_FMT_with_point holds ET is Fo_filled;

    theorem :: FINTOPO7:8

    

     Th5: for ET be non empty strict FMT_Space_Str st ET is Fo_filled & for x be Element of ET holds ( U_FMT x) is non empty holds ET is U_FMT_with_point

    proof

      let ET be non empty strict FMT_Space_Str such that

       A1: ET is Fo_filled and

       A2: for x be Element of ET holds ( U_FMT x) is non empty;

      for x be Element of ET, V be Element of ( U_FMT x) holds x in V

      proof

        let x be Element of ET, V be Element of ( U_FMT x);

        ( U_FMT x) is non empty by A2;

        then V in ( U_FMT x);

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO7:9

    for ET be non empty strict FMT_Space_Str st ET is Fo_filled & ET is U_FMT_filter holds ET is U_FMT_with_point

    proof

      let ET be non empty strict FMT_Space_Str such that

       A1: ET is Fo_filled and

       A2: ET is U_FMT_filter;

      for x be Element of ET holds ( U_FMT x) is non empty by A2;

      hence thesis by A1, Th5;

    end;

    registration

      cluster U_FMT_local U_FMT_with_point U_FMT_filter for non empty strict FMT_Space_Str;

      existence

      proof

        set X = { {} }, f = (X --> {X});

        

         A1: { {X}} c= ( bool ( bool X))

        proof

           {X} c= ( bool X)

          proof

            let x be object;

            assume x in {X};

            then

             A2: x = X by TARSKI:def 1;

            X c= X;

            hence thesis by A2;

          end;

          then {X} in ( bool ( bool X));

          hence thesis by TARSKI:def 1;

        end;

        

         A3: ( dom f) = X & ( rng f) = { {X}} by RELAT_1: 160;

        reconsider f as PartFunc of X, ( bool ( bool X)) by A1, A3, FUNCT_2: 2;

        reconsider f as Function of X, ( bool ( bool X));

        reconsider FMT = FMT_Space_Str (# X, f #) as non empty strict FMT_Space_Str;

        

         A4: for x be Element of FMT holds ( U_FMT x) = {X}

        proof

          let x be Element of FMT;

          (the BNbd of FMT . x) in { {X}} by FUNCT_2: 5;

          hence thesis by TARSKI:def 1;

        end;

        FMT is U_FMT_local & FMT is U_FMT_with_point & FMT is U_FMT_filter

        proof

           A5:

          now

            let x be Element of FMT, V be Element of ( U_FMT x);

            ( U_FMT x) is non empty by A4;

            then V in ( U_FMT x);

            then V in {X} by A4;

            then V = X by TARSKI:def 1;

            hence x in V;

          end;

          

           A6: for x be Element of FMT holds ( U_FMT x) is Filter of the carrier of FMT

          proof

            let x be Element of FMT;

            reconsider Z = {X} as Filter of X by CARD_FIL: 4;

            the carrier of FMT = X & Z = {X} & Z is Filter of X;

            hence thesis by A4;

          end;

          for x be Element of FMT, V be Element of ( U_FMT x) holds ex W be Element of ( U_FMT x) st for y be Element of FMT st y is Element of W holds V is Element of ( U_FMT y)

          proof

            let x be Element of FMT, V be Element of ( U_FMT x);

            

             A7: V is Element of {X} by A4;

            take X;

            thus thesis by A7, A4, TARSKI:def 1;

          end;

          hence thesis by A5, A6;

        end;

        hence thesis;

      end;

    end

    theorem :: FINTOPO7:10

    

     Th6: for ET be U_FMT_filter non empty strict FMT_Space_Str, x be Element of ET holds the carrier of ET in ( U_FMT x)

    proof

      let ET be U_FMT_filter non empty strict FMT_Space_Str, x be Element of ET;

      ( U_FMT x) is Filter of the carrier of ET by Def2;

      hence thesis by CARD_FIL: 5;

    end;

    definition

      let ET be U_FMT_filter non empty strict FMT_Space_Str;

      let x be Element of ET;

      :: FINTOPO7:def5

      mode a_neighborhood of x -> Subset of ET means

      : Def5: it in ( U_FMT x);

      existence

      proof

        the carrier of ET in ( U_FMT x) by Th6;

        hence thesis;

      end;

    end

    registration

      let ET be U_FMT_filter non empty strict FMT_Space_Str;

      let x be Element of ET;

      cluster open for a_neighborhood of x;

      existence

      proof

        set S = the carrier of ET;

        take S;

        

         A1: S in ( U_FMT x) by Th6;

        then

        reconsider S as Subset of ET;

        S is open by Th6;

        hence thesis by A1, Def5;

      end;

    end

    definition

      let ET be U_FMT_filter non empty strict FMT_Space_Str;

      let A be Subset of ET;

      :: FINTOPO7:def6

      mode a_neighborhood of A -> Subset of ET means

      : Def6: for x be Element of ET st x in A holds it in ( U_FMT x);

      existence

      proof

        set S = the carrier of ET;

        S c= the carrier of ET;

        then

        reconsider S as Subset of the carrier of ET;

        take S;

        hereby

          let x be Element of ET such that x in A;

          ( U_FMT x) is Filter of the carrier of ET by Def2;

          hence S in ( U_FMT x) by CARD_FIL: 5;

        end;

      end;

    end

    registration

      let ET be U_FMT_filter non empty strict FMT_Space_Str;

      let A be Subset of ET;

      cluster open for a_neighborhood of A;

      existence

      proof

        set S = the carrier of ET;

        S c= the carrier of ET;

        then

        reconsider S as Subset of ET;

        for x be Element of ET st x in A holds S in ( U_FMT x) by Th6;

        then

         A1: S is a_neighborhood of A by Def6;

        S is open by Th6;

        hence thesis by A1;

      end;

    end

    theorem :: FINTOPO7:11

    

     Th7: for ET be U_FMT_filter non empty strict FMT_Space_Str, A be Subset of ET holds for NA be a_neighborhood of A, B be Subset of ET st NA c= B holds B is a_neighborhood of A

    proof

      let ET be U_FMT_filter non empty strict FMT_Space_Str, A be Subset of ET;

      let NA be a_neighborhood of A, B be Subset of ET;

      assume

       A1: NA c= B;

      for x be Element of ET st x in A holds B in ( U_FMT x)

      proof

        let x be Element of ET;

        assume x in A;

        then

         A2: NA in ( U_FMT x) by Def6;

        ( U_FMT x) is Filter of the carrier of ET by Def2;

        hence thesis by A1, A2, CARD_FIL:def 1;

      end;

      hence thesis by Def6;

    end;

    definition

      let ET be U_FMT_filter non empty strict FMT_Space_Str;

      let A be Subset of ET;

      :: FINTOPO7:def7

      func Neighborhood A -> Subset-Family of ET equals the set of all N where N be a_neighborhood of A;

      correctness

      proof

         the set of all N where N be a_neighborhood of A is Subset-Family of the carrier of ET

        proof

           the set of all N where N be a_neighborhood of A c= ( bool the carrier of ET)

          proof

            let t be object;

            assume t in the set of all N where N be a_neighborhood of A;

            then

            consider N0 be a_neighborhood of A such that

             A1: t = N0;

            thus thesis by A1;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: FINTOPO7:12

    

     Th7bis: for ET be U_FMT_filter non empty strict FMT_Space_Str, A be non empty Subset of ET holds ( Neighborhood A) is Filter of the carrier of ET

    proof

      let ET be U_FMT_filter non empty strict FMT_Space_Str, A be non empty Subset of ET;

      set S = the set of all F where F be a_neighborhood of A;

      S is Filter of the carrier of ET

      proof

        

         A1: S is non empty Subset-Family of the carrier of ET

        proof

          

           A2: S is non empty

          proof

            set Sq = the carrier of ET;

            Sq c= the carrier of ET;

            then

            reconsider Sq as Subset of the carrier of ET;

            Sq is a_neighborhood of A

            proof

              for x be Element of ET st x in A holds Sq in ( U_FMT x) by Th6;

              hence thesis by Def6;

            end;

            then Sq in S;

            hence thesis;

          end;

          S is Subset-Family of the carrier of ET

          proof

            S c= ( bool the carrier of ET)

            proof

              let t be object;

              assume t in S;

              then

              consider F0 be a_neighborhood of A such that

               A3: t = F0;

              thus t in ( bool the carrier of ET) by A3;

            end;

            hence thesis;

          end;

          hence thesis by A2;

        end;

        

         A4: not {} in S

        proof

          assume {} in S;

          then

          consider F0 be a_neighborhood of A such that

           A5: {} = F0;

          A is non empty;

          then

          consider a be object such that

           A6: a in A;

          reconsider a0 = a as Element of ET by A6;

          

           A7: {} in ( U_FMT a0) by A5, A6, Def6;

          ( U_FMT a0) is Filter of the carrier of ET by Def2;

          hence thesis by A7, CARD_FIL:def 1;

        end;

        for Y1,Y2 be Subset of ET holds (Y1 in S & Y2 in S implies (Y1 /\ Y2) in S) & (Y1 in S & Y1 c= Y2 implies Y2 in S)

        proof

          let Y1,Y2 be Subset of ET;

          now

            assume that

             A8: Y1 in S and

             A9: Y2 in S;

            consider F1 be a_neighborhood of A such that

             A10: Y1 = F1 by A8;

            consider F2 be a_neighborhood of A such that

             A11: Y2 = F2 by A9;

            

             A12: for x be Element of ET st x in A holds (Y1 /\ Y2) in ( U_FMT x)

            proof

              let x be Element of ET;

              assume x in A;

              then

               A13: Y1 in ( U_FMT x) & Y2 in ( U_FMT x) by A10, A11, Def6;

              ( U_FMT x) is Filter of the carrier of ET by Def2;

              hence thesis by A13, CARD_FIL:def 1;

            end;

            (Y1 /\ Y2) is a_neighborhood of A by A12, Def6;

            hence (Y1 /\ Y2) in S;

          end;

          hence Y1 in S & Y2 in S implies (Y1 /\ Y2) in S;

          now

            assume that

             A14: Y1 in S and

             A15: Y1 c= Y2;

            consider y1 be a_neighborhood of A such that

             A16: y1 = Y1 by A14;

            for x be Element of ET st x in A holds Y2 in ( U_FMT x)

            proof

              let x be Element of ET;

              assume x in A;

              then

               A17: Y1 in ( U_FMT x) by A16, Def6;

              ( U_FMT x) is Filter of the carrier of ET by Def2;

              hence thesis by A17, A15, CARD_FIL:def 1;

            end;

            then Y2 is a_neighborhood of A by Def6;

            hence Y1 in S & Y1 c= Y2 implies Y2 in S;

          end;

          hence thesis;

        end;

        hence thesis by A1, A4, CARD_FIL:def 1;

      end;

      hence thesis;

    end;

    definition

      let ET be non empty strict FMT_Space_Str;

      :: FINTOPO7:def8

      attr ET is U_FMT_filter_base means for x be Element of the carrier of ET holds ( U_FMT x) is filter_base of the carrier of ET;

    end

    definition

      let ET be non empty FMT_Space_Str;

      :: FINTOPO7:def9

      func <.ET.] -> Function of the carrier of ET, ( bool ( bool the carrier of ET)) means

      : Def7: for x be Element of the carrier of ET holds (it . x) = <.( U_FMT x).];

      existence

      proof

        deffunc FF( Element of the carrier of ET) = <.( U_FMT $1).];

        consider f be Function of the carrier of ET, ( bool ( bool the carrier of ET)) such that

         A1: for x be Element of the carrier of ET holds (f . x) = FF(x) from FUNCT_2:sch 4;

        thus thesis by A1;

      end;

      uniqueness

      proof

        for Y1,Y2 be Function of the carrier of ET, ( bool ( bool the carrier of ET)) st (for x be Element of the carrier of ET holds (Y1 . x) = <.( U_FMT x).] & for y be Element of the carrier of ET holds (Y2 . y) = <.( U_FMT y).]) holds Y1 = Y2

        proof

          let Y1,Y2 be Function of the carrier of ET, ( bool ( bool the carrier of ET)) such that

           A2: for x be Element of the carrier of ET holds (Y1 . x) = <.( U_FMT x).] & for y be Element of the carrier of ET holds (Y2 . y) = <.( U_FMT y).];

          for t be object st t in the carrier of ET holds (Y1 . t) = (Y2 . t)

          proof

            let t be object such that

             A3: t in the carrier of ET;

            reconsider t as Element of the carrier of ET by A3;

            (Y1 . t) = <.( U_FMT t).] & (Y2 . t) = <.( U_FMT t).] by A2;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let ET be non empty strict FMT_Space_Str;

      :: FINTOPO7:def10

      func gen_filter (ET) -> non empty strict FMT_Space_Str equals FMT_Space_Str (# the carrier of ET, <.ET.] #);

      correctness ;

    end

    theorem :: FINTOPO7:13

    

     Th8: for ET be non empty strict FMT_Space_Str st ET is U_FMT_filter_base holds ( gen_filter ET) is U_FMT_filter

    proof

      let ET be non empty strict FMT_Space_Str such that

       A1: ET is U_FMT_filter_base;

      for x be Element of ( gen_filter ET) holds ( U_FMT x) is Filter of the carrier of ( gen_filter ET)

      proof

        let x be Element of ( gen_filter ET);

        reconsider x0 = x as Element of ET;

        ( U_FMT x0) is filter_base of the carrier of ET by A1;

        then <.( U_FMT x0).] is Filter of the carrier of ET by CARDFIL2: 25;

        hence thesis by Def7;

      end;

      hence thesis;

    end;

    begin

    definition

      mode FMT_TopSpace is U_FMT_local U_FMT_with_point U_FMT_filter non empty strict FMT_Space_Str;

    end

    notation

      let ET be FMT_TopSpace, x be Element of ET;

      synonym NeighborhoodSystem x for U_FMT x;

    end

    registration

      let ET be FMT_TopSpace;

      cluster open for Subset of ET;

      existence

      proof

        

         A1: ET is U_FMT_filter;

        set S = the carrier of ET;

        S c= the carrier of ET;

        then

        reconsider S = the carrier of ET as Subset of ET;

        take S;

        for x be Element of ET st x in S holds S in ( U_FMT x)

        proof

          let x be Element of ET;

          assume x in S;

          ( U_FMT x) is Filter of the carrier of ET by A1;

          hence S in ( U_FMT x) by CARD_FIL: 5;

        end;

        hence thesis;

      end;

    end

    definition

      let ET be FMT_TopSpace;

      :: FINTOPO7:def11

      func Family_open_set (ET) -> non empty Subset-Family of the carrier of ET equals the set of all O where O be open Subset of ET;

      correctness

      proof

        set OO = the set of all O where O be open Subset of ET;

        

         A1: OO is non empty

        proof

          the carrier of ET is open Subset of ET

          proof

            

             A2: ET is U_FMT_filter;

            set S = the carrier of ET;

            S c= the carrier of ET;

            then

            reconsider S as Subset of ET;

            for x be Element of ET st x in S holds S in ( U_FMT x)

            proof

              let x be Element of ET;

              assume x in S;

              ( U_FMT x) is Filter of the carrier of ET by A2;

              hence S in ( U_FMT x) by CARD_FIL: 5;

            end;

            hence thesis by Def1;

          end;

          then the carrier of ET in OO;

          hence thesis;

        end;

        now

          let t be object;

          assume t in OO;

          then

          consider OO1 be open Subset of ET such that

           A3: t = OO1;

          thus t in ( bool the carrier of ET) by A3;

        end;

        then OO c= ( bool the carrier of ET);

        hence thesis by A1;

      end;

    end

    theorem :: FINTOPO7:14

    

     Th9: for ET be FMT_TopSpace holds {} in ( Family_open_set ET) & the carrier of ET in ( Family_open_set ET) & (for a be Subset-Family of ET st a c= ( Family_open_set ET) holds ( union a) in ( Family_open_set ET)) & (for a,b be Subset of ET st a in ( Family_open_set ET) & b in ( Family_open_set ET) holds (a /\ b) in ( Family_open_set ET))

    proof

      let ET be FMT_TopSpace;

      

       A1: ET is U_FMT_filter;

      thus {} in ( Family_open_set ET)

      proof

        set S = {} ;

        S c= the carrier of ET;

        then

        reconsider S as Subset of ET;

        S is open;

        then

        reconsider S as open Subset of ET;

        S in the set of all O where O be open Subset of ET;

        hence thesis;

      end;

      thus the carrier of ET in ( Family_open_set ET)

      proof

        set S = the carrier of ET;

        S c= the carrier of ET;

        then

        reconsider S as Subset of ET;

        for x be Element of ET st x in S holds S in ( U_FMT x)

        proof

          let x be Element of ET;

          assume x in S;

          ( U_FMT x) is Filter of the carrier of ET by A1;

          hence S in ( U_FMT x) by CARD_FIL: 5;

        end;

        then S is open;

        then

        reconsider S as open Subset of ET;

        S in the set of all O where O be open Subset of ET;

        hence thesis;

      end;

      thus (for a be Subset-Family of ET st a c= ( Family_open_set ET) holds ( union a) in ( Family_open_set ET))

      proof

        let a be Subset-Family of ET such that

         A2: a c= ( Family_open_set ET);

        reconsider UA = ( union a) as Subset of ET;

        now

          let x be Element of ET;

          assume x in UA;

          then

          consider Y be set such that

           A3: x in Y and

           A4: Y in a by TARSKI:def 4;

          Y in the set of all O where O be open Subset of ET by A2, A4;

          then

          consider Y0 be open Subset of ET such that

           A5: Y = Y0;

          

           A6: Y in ( U_FMT x) by A3, A5, Def1;

          

           A7: Y c= UA by A4, ZFMISC_1: 74;

          ( U_FMT x) is Filter of the carrier of ET by A1;

          hence UA in ( U_FMT x) by A6, A7, CARD_FIL:def 1;

        end;

        then UA is open;

        hence thesis;

      end;

      thus for a,b be Subset of ET st a in ( Family_open_set ET) & b in ( Family_open_set ET) holds (a /\ b) in ( Family_open_set ET)

      proof

        let a,b be Subset of ET such that

         A9: a in ( Family_open_set ET) and

         A10: b in ( Family_open_set ET);

        now

          let x be Element of ET such that

           A11: x in (a /\ b);

          

           A12: x in a & x in b by A11, XBOOLE_0:def 4;

          consider a0 be open Subset of ET such that

           A13: a = a0 by A9;

          

           A14: a in ( U_FMT x) by A12, A13, Def1;

          consider b0 be open Subset of ET such that

           A15: b = b0 by A10;

          

           A16: b in ( U_FMT x) by A12, A15, Def1;

          ( U_FMT x) is Filter of the carrier of ET by A1;

          hence (a /\ b) in ( U_FMT x) by A14, A16, CARD_FIL:def 1;

        end;

        then (a /\ b) is open;

        then

        reconsider AB = (a /\ b) as open Subset of ET;

        AB in the set of all O where O be open Subset of ET;

        hence thesis;

      end;

    end;

    theorem :: FINTOPO7:15

    

     Th10: for ET be FMT_TopSpace, a be Element of ET, V be a_neighborhood of a holds ex O be open Subset of ET st a in O & O c= V

    proof

      let ET be FMT_TopSpace, a be Element of ET, V be a_neighborhood of a;

      set O = { x where x be Element of ET : V is a_neighborhood of x };

      O is Subset of ET

      proof

        O c= the carrier of ET

        proof

          let x be object;

          assume x in O;

          then

          consider t be Element of ET such that

           A1: x = t and V is a_neighborhood of t;

          thus thesis by A1;

        end;

        hence thesis;

      end;

      then

      reconsider O as Subset of ET;

      

       A2: O is open Subset of ET

      proof

        for x be Element of ET st x in O holds O in ( U_FMT x)

        proof

          let x be Element of ET;

          assume x in O;

          then

          consider t be Element of ET such that

           A3: x = t and

           A4: V is a_neighborhood of t;

          x is Element of ET & V is Element of ( U_FMT x) by A3, A4, Def5;

          then

          consider W be Element of ( U_FMT x) such that

           A5: for y be Element of ET st y is Element of W holds V is Element of ( U_FMT y) by Def4;

          

           A6: W c= O

          proof

            let v be object such that

             E1: v in W;

            ( U_FMT x) is non empty by Th4;

            then W in ( U_FMT x);

            then

            reconsider v as Element of ET by E1;

            

             A7: v is Element of ET & V is Element of ( U_FMT v) by E1, A5;

            ( U_FMT v) is non empty by Th4;

            then V is a_neighborhood of v by A7, Def5;

            hence thesis;

          end;

          W in ( U_FMT x) & ( U_FMT x) is Filter of the carrier of ET

          proof

            hereby

              ( U_FMT x) is non empty by Th4;

              hence W in ( U_FMT x);

            end;

            thus ( U_FMT x) is Filter of the carrier of ET by Def2;

          end;

          hence thesis by A6, CARD_FIL:def 1;

        end;

        hence thesis by Def1;

      end;

      

       A8: a in O;

      O c= V

      proof

        let x be object;

        assume x in O;

        then

        consider x0 be Element of ET such that

         A9: x = x0 and

         A10: V is a_neighborhood of x0;

        V in ( U_FMT x0) by A10, Def5;

        hence x in V by A9, Def3;

      end;

      hence thesis by A2, A8;

    end;

    theorem :: FINTOPO7:16

    

     Th11: for ET be FMT_TopSpace, A be non empty Subset of ET holds for V be Subset of ET holds V is a_neighborhood of A iff ex O be open Subset of ET st A c= O & O c= V

    proof

      let ET be FMT_TopSpace, A be non empty Subset of ET;

      let V be Subset of ET;

      thus V is a_neighborhood of A implies ex O be open Subset of ET st A c= O & O c= V

      proof

        assume

         A1: V is a_neighborhood of A;

         A2:

        now

          let a be Element of ET;

          assume a in A;

          then V in ( U_FMT a) by A1, Def6;

          then V is a_neighborhood of a by Def5;

          hence ex O be open Subset of ET st a in O & O c= V by Th10;

        end;

        defpred P[ object, object] means ex x be Element of ET, y be open Subset of ET st x = $1 & y = $2 & x in y & y c= V;

        

         A3: for x be object st x in A holds ex y be object st y in ( bool the carrier of ET) & P[x, y]

        proof

          let x be object such that

           A4: x in A;

          reconsider x as Element of A by A4;

          consider O be open Subset of ET such that

           A5: x in O and

           A6: O c= V by A2;

          thus thesis by A5, A6;

        end;

        ex f be Function of A, ( bool the carrier of ET) st for x be object st x in A holds P[x, (f . x)] from FUNCT_2:sch 1( A3);

        then

        consider f be Function of A, ( bool the carrier of ET) such that

         A7: for x be object st x in A holds P[x, (f . x)];

        set OO = ( union ( rng f));

        OO is open Subset of ET & A c= OO & OO c= V

        proof

          reconsider OO as Subset of ET;

          

           A8: OO is open Subset of ET & OO c= V

          proof

            

             A9: for a be Element of ET st a in A holds (f . a) is open Subset of ET & (f . a) c= V

            proof

              let a be Element of ET;

              assume a in A;

              then P[a, (f . a)] by A7;

              then

              consider x1 be set, y1 be open Subset of ET such that a = x1 and

               A10: (f . a) = y1 and x1 in y1 and

               A11: y1 c= V;

              thus thesis by A11, A10;

            end;

            

             A12: OO c= V

            proof

              let t be object;

              assume t in OO;

              then

              consider T be set such that

               A13: t in T and

               A14: T in ( rng f) by TARSKI:def 4;

              consider x be object such that

               A15: x in ( dom f) and

               A16: T = (f . x) by A14, FUNCT_1:def 3;

              x in A by A15;

              then (f . x) c= V by A9;

              hence thesis by A13, A16;

            end;

            ( rng f) c= ( Family_open_set ET)

            proof

              let t be object;

              assume t in ( rng f);

              then

              consider x be object such that

               A17: x in ( dom f) and

               A18: t = (f . x) by FUNCT_1:def 3;

              

               A19: x in A by A17;

              (f . x) is open Subset of ET by A19, A9;

              hence thesis by A18;

            end;

            then ( union ( rng f)) in the set of all O where O be open Subset of ET by Th9;

            then

            consider O1 be open Subset of ET such that

             A20: ( union ( rng f)) = O1;

            thus thesis by A20, A12;

          end;

          A c= OO

          proof

            let t be object;

            assume

             A21: t in A;

            then P[t, (f . t)] by A7;

            then

            consider x1,y1 be set such that

             A22: t = x1 and

             A23: (f . t) = y1 and

             A24: x1 in y1 and y1 c= V;

            y1 in ( rng f) by A23, A21, FUNCT_2: 4;

            hence thesis by A22, A24, TARSKI:def 4;

          end;

          hence thesis by A8;

        end;

        hence thesis;

      end;

      thus (ex O be open Subset of ET st A c= O & O c= V) implies V is a_neighborhood of A

      proof

        given O be open Subset of ET such that

         A25: A c= O and

         A26: O c= V;

        for x be Element of ET st x in A holds O in ( U_FMT x) by A25, Def1;

        then O is a_neighborhood of A by Def6;

        hence thesis by A26, Th7;

      end;

    end;

    theorem :: FINTOPO7:17

    for ET be FMT_TopSpace, A be non empty Subset of ET holds ( Neighborhood A) is Filter of the carrier of ET by Th7bis;

    definition

      let ET be FMT_TopSpace, A be non empty Subset of ET;

      :: FINTOPO7:def12

      func OpenNeighborhoods A -> Subset-Family of the carrier of ET equals the set of all N where N be open a_neighborhood of A;

      correctness

      proof

         the set of all N where N be open a_neighborhood of A c= ( bool the carrier of ET)

        proof

          let t be object;

          assume t in the set of all N where N be open a_neighborhood of A;

          then

          consider N be open a_neighborhood of A such that

           A1: t = N;

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: FINTOPO7:18

    for ET be FMT_TopSpace, cF be Filter of the carrier of ET, cS be non empty Subset of cF holds for A be non empty Subset of ET st cF = ( Neighborhood A) & cS = ( OpenNeighborhoods A) holds cS is filter_basis

    proof

      let ET be FMT_TopSpace, cF be Filter of the carrier of ET, cS be non empty Subset of cF;

      let A be non empty Subset of ET such that

       A1: cF = ( Neighborhood A) and

       A2: cS = ( OpenNeighborhoods A);

      for f be Element of cF holds ex b be Element of cS st b c= f

      proof

        let f be Element of cF;

        f in the set of all N where N be a_neighborhood of A by A1;

        then

        consider N be a_neighborhood of A such that

         A3: f = N;

        consider O be open Subset of ET such that

         A4: A c= O & O c= N by Th11;

        O is open;

        then for x be Element of ET st x in A holds O in ( U_FMT x) by A4;

        then O is open a_neighborhood of A by Def6;

        then O in the set of all N where N be open a_neighborhood of A;

        hence thesis by A2, A3, A4;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO7:19

    

     Th12: for T be non empty TopSpace holds ex ET be FMT_TopSpace st the carrier of T = the carrier of ET & ( Family_open_set ET) = the topology of T

    proof

      let T be non empty TopSpace;

      ex ET be non empty strict FMT_Space_Str st ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT be FMT_TopSpace st TT = ET & ( Family_open_set TT) = the topology of T

      proof

        deffunc F( object) = { O where O be Element of the topology of T : $1 in O };

        

         A1: for x be object st x in the carrier of T holds F(x) in ( bool ( bool the carrier of T))

        proof

          let x be object such that

           A2: x in the carrier of T;

          reconsider x as Element of T by A2;

           F(x) c= ( bool the carrier of T)

          proof

            let t be object such that

             A3: t in F(x);

            consider O1 be Element of the topology of T such that

             A4: t = O1 and x in O1 by A3;

            thus thesis by A4;

          end;

          hence thesis;

        end;

        ex f be Function of the carrier of T, ( bool ( bool the carrier of T)) st for x be object st x in the carrier of T holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

        then

        consider f be Function of the carrier of T, ( bool ( bool the carrier of T)) such that

         A5: for x be object st x in the carrier of T holds (f . x) = F(x);

        reconsider TMP = FMT_Space_Str (# the carrier of T, f #) as non empty strict FMT_Space_Str;

        

         A6: for t be Element of TMP holds ( U_FMT t) is non empty

        proof

          let t be Element of TMP;

          take TT = the carrier of T;

          TT in the topology of T by PRE_TOPC:def 1;

          then TT in F(t);

          hence thesis by A5;

        end;

        

         A7: TMP is U_FMT_filter_base

        proof

          for x be Element of the carrier of TMP holds ( U_FMT x) is non empty & ( U_FMT x) is with_non-empty_elements & for B1,B2 be Element of ( U_FMT x) holds ex B be Element of ( U_FMT x) st B c= (B1 /\ B2)

          proof

            let x be Element of the carrier of TMP;

            thus

             A8: ( U_FMT x) is non empty by A6;

            thus ( U_FMT x) is with_non-empty_elements

            proof

              assume that

               A9: not (( U_FMT x) is with_non-empty_elements);

               {} in F(x) by A9, A5;

              then

              consider O be Element of the topology of T such that

               A10: O = {} and

               A11: x in O;

              thus thesis by A10, A11;

            end;

            thus for B1,B2 be Element of ( U_FMT x) holds ex B be Element of ( U_FMT x) st B c= (B1 /\ B2)

            proof

              let B1,B2 be Element of ( U_FMT x);

              B1 in ( U_FMT x) & B2 in ( U_FMT x) by A8;

              then

               A12: B1 in F(x) & B2 in F(x) by A5;

              then

              consider O1 be Element of the topology of T such that

               A13: B1 = O1 and

               A14: x in O1;

              consider O2 be Element of the topology of T such that

               A15: B2 = O2 and

               A16: x in O2 by A12;

              

               A17: x in (O1 /\ O2) by A14, A16, XBOOLE_0:def 4;

              reconsider OO = (O1 /\ O2) as Element of the topology of T by PRE_TOPC:def 1;

              OO in F(x) by A17;

              then

              reconsider OO as Element of ( U_FMT x) by A5;

              take OO;

              thus thesis by A13, A15;

            end;

          end;

          then for x be Element of the carrier of TMP holds ( U_FMT x) is non empty & ( U_FMT x) is with_non-empty_elements & ( U_FMT x) is quasi_basis;

          hence thesis;

        end;

        reconsider ET = ( gen_filter TMP) as non empty strict FMT_Space_Str;

        take ET;

        thus ET is U_FMT_filter by A7, Th8;

        thus

         A18: ET is U_FMT_with_point

        proof

          for x be Element of ET, V be Element of ( U_FMT x) holds x in V

          proof

            let x be Element of ET, V be Element of ( U_FMT x);

            set Z = (the BNbd of ( gen_filter TMP) . x);

            reconsider x0 = x as Element of TMP;

            

             A20: ( U_FMT x) = <.( U_FMT x0).] by Def7;

            

             A21: ( U_FMT x0) = F(x0) by A5;

            then

            reconsider FX0 = F(x0) as Subset-Family of the carrier of TMP;

            

             A22: V is Element of <.FX0.] by A5, A20;

             <.FX0.] is non empty

            proof

              the carrier of T in the topology of T by PRE_TOPC:def 1;

              then the carrier of T in FX0;

              then

              reconsider XX = the carrier of T as Element of FX0;

              FX0 c= <.FX0.] by CARDFIL2:def 8;

              hence thesis by A21, A6;

            end;

            then V in <.FX0.] by A22;

            then

            consider b be Element of FX0 such that

             A23: b c= V by CARDFIL2:def 8;

             F(x0) is non empty

            proof

              the carrier of T in the topology of T by PRE_TOPC:def 1;

              then the carrier of T in F(x0);

              hence thesis;

            end;

            then b in F(x0);

            then

            consider OO be Element of the topology of T such that

             A24: b = OO and

             A25: x0 in OO;

            thus thesis by A23, A24, A25;

          end;

          hence thesis;

        end;

        thus

         A26: ET is U_FMT_local

        proof

          for x be Element of ET holds for V be Element of ( U_FMT x) holds ex W be Element of ( U_FMT x) st for y be Element of ET st y is Element of W holds V is Element of ( U_FMT y)

          proof

            let t be Element of ET;

            set Z = (the BNbd of ( gen_filter TMP) . t);

            reconsider t0 = t as Element of TMP;

            

             A28: ( U_FMT t) = <.( U_FMT t0).] by Def7;

            

             A29: ( U_FMT t0) = F(t0) by A5;

            then

            reconsider FT0 = F(t0) as Subset-Family of the carrier of TMP;

            for V be Element of ( U_FMT t) holds ex W be Element of ( U_FMT t) st for y be Element of ET st y is Element of W holds V is Element of ( U_FMT y)

            proof

              let V be Element of ( U_FMT t);

              

               A30: <.FT0.] is non empty

              proof

                the carrier of T in the topology of T by PRE_TOPC:def 1;

                then the carrier of T in FT0;

                then

                reconsider XX = the carrier of T as Element of FT0;

                XX in <.FT0.]

                proof

                  XX is Element of FT0 & XX c= XX;

                  hence thesis by CARDFIL2:def 8;

                end;

                hence thesis;

              end;

              

               A31: V in <.FT0.] by A30, A28, A29;

              consider V0 be Element of FT0 such that

               A32: V0 c= V by A31, CARDFIL2:def 8;

              

               A33: F(t0) is non empty

              proof

                the carrier of T in the topology of T by PRE_TOPC:def 1;

                then the carrier of T in F(t0);

                hence thesis;

              end;

              then V0 in F(t0);

              then

              consider OUV be Element of the topology of T such that

               A34: V0 = OUV and

               A35: t0 in OUV;

              reconsider W = OUV as Element of ( U_FMT t) by A28, A29, A34, CARDFIL2:def 8;

              take W;

              for y be Element of ET st y is Element of W holds V is Element of ( U_FMT y)

              proof

                let y be Element of ET such that

                 A36: y is Element of W;

                set Z = (the BNbd of ( gen_filter TMP) . y);

                reconsider y0 = y as Element of TMP;

                

                 A38: ( U_FMT y0) = F(y0) by A5;

                then

                reconsider FY0 = F(y0) as Subset-Family of the carrier of TMP;

                

                 A39: V0 in F(y0) by A34, A36, A35;

                V0 in FT0 & FT0 c= ( bool the carrier of TMP) by A33;

                then

                reconsider VV0 = V0 as Subset of the carrier of TMP;

                V in <.FY0.] by A39, A32, A31, CARDFIL2:def 8;

                hence thesis by Def7, A38;

              end;

              hence thesis;

            end;

            hence thesis;

          end;

          hence thesis;

        end;

        thus the carrier of T = the carrier of ET;

        ex TT be FMT_TopSpace st TT = ET & ( Family_open_set TT) = the topology of T

        proof

          reconsider TT = ET as FMT_TopSpace by A7, Th8, A18, A26;

          ( Family_open_set TT) = the topology of T

          proof

            

             A41: ( Family_open_set TT) c= the topology of T

            proof

              for t be object st t in ( Family_open_set TT) holds t in the topology of T

              proof

                let t be object;

                assume t in ( Family_open_set TT);

                then

                consider O be open Subset of TT such that

                 A42: t = O;

                per cases ;

                  suppose O is empty;

                  hence thesis by A42, PRE_TOPC: 1;

                end;

                  suppose not O is empty;

                  reconsider O as Subset of T;

                  

                   A44: for x be Point of T st x in O holds ex b be Subset of T st b is a_neighborhood of x & b c= O

                  proof

                    let x be Point of T;

                    assume

                     A45: x in O;

                    reconsider x0 = x as Element of ET;

                    

                     A46: O in ( U_FMT x0) by A45, Def1;

                    set Z = (the BNbd of ( gen_filter TMP) . x0);

                    reconsider x1 = x0 as Element of TMP;

                    O in <.( U_FMT x1).] by A46, Def7;

                    then

                    consider b be Element of ( U_FMT x1) such that

                     A48: b c= O by CARDFIL2:def 8;

                    ( U_FMT x1) is non empty & b is Element of ( U_FMT x1) by A6;

                    then b in ( U_FMT x1);

                    then b in F(x1) by A5;

                    then

                    consider b0 be Element of the topology of T such that

                     A49: b = b0 and

                     A50: x1 in b0;

                    b0 is open;

                    hence thesis by A48, A49, A50, CONNSP_2: 3;

                  end;

                  thus thesis by A44, CONNSP_2: 7, A42, PRE_TOPC:def 2;

                end;

              end;

              hence thesis;

            end;

            the topology of T c= ( Family_open_set TT)

            proof

              let t be object;

              assume

               A51: t in the topology of T;

              then

              reconsider t as Subset of TT;

              t is open

              proof

                for x be Element of ET st x in t holds t in ( U_FMT x)

                proof

                  let x be Element of ET;

                  assume

                   A53: x in t;

                  set Z = (the BNbd of ( gen_filter TMP) . x);

                  reconsider x0 = x as Element of TMP;

                  

                   A55: ( U_FMT x) = <.( U_FMT x0).] by Def7;

                  ( U_FMT x0) = F(x0) by A5;

                  then

                  reconsider FX0 = F(x0) as Subset-Family of the carrier of TMP;

                  t in F(x0) by A51, A53;

                  then t in ( U_FMT x0) by A5;

                  hence thesis by A55, CARDFIL2:def 8;

                end;

                hence thesis;

              end;

              hence thesis;

            end;

            hence thesis by A41;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      then

      consider ET be non empty strict FMT_Space_Str such that

       A56: the carrier of T = the carrier of ET and ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local and

       A57: ex TT be FMT_TopSpace st TT = ET & ( Family_open_set TT) = the topology of T;

      consider TT be FMT_TopSpace such that

       A58: TT = ET and ( Family_open_set TT) = the topology of T by A57;

      take TT;

      thus thesis by A56, A57, A58;

    end;

    theorem :: FINTOPO7:20

    

     Th13: for T be non empty TopSpace, ET be FMT_TopSpace st the carrier of T = the carrier of ET & ( Family_open_set ET) = the topology of T holds for x be Element of ET holds ( U_FMT x) = { V where V be Subset of ET : ex O be Subset of T st O in the topology of T & x in O & O c= V }

    proof

      let T be non empty TopSpace, ET be FMT_TopSpace;

      assume that the carrier of T = the carrier of ET and

       A1: ( Family_open_set ET) = the topology of T;

      

       A2: for o be set st o in ( Family_open_set ET) holds for x be Element of ET st x in o holds o in ( U_FMT x)

      proof

        let o be set;

        assume o in ( Family_open_set ET);

        then

        consider O be open Subset of ET such that

         A3: o = O;

        thus thesis by A3, Def1;

      end;

      for x be Element of ET holds ( U_FMT x) = { V where V be Subset of ET : ex O be Subset of T st O in the topology of T & x in O & O c= V }

      proof

        let x be Element of ET;

        

         A4: ( U_FMT x) c= { V where V be Subset of ET : ex O be Subset of T st O in the topology of T & x in O & O c= V }

        proof

          let t be object;

          assume

           A5: t in ( U_FMT x);

          then

           A6: t is a_neighborhood of x by Def5;

          reconsider t as Subset of ET by A5;

          consider OO be open Subset of ET such that

           A7: x in OO and

           A8: OO c= t by A6, Th10;

          

           A9: OO in ( Family_open_set ET);

          then

          reconsider OO as Subset of T by A1;

          thus thesis by A7, A8, A9, A1;

        end;

        { V where V be Subset of ET : ex O be Subset of T st O in the topology of T & x in O & O c= V } c= ( U_FMT x)

        proof

          let t be object;

          assume t in { V where V be Subset of ET : ex O be Subset of T st O in the topology of T & x in O & O c= V };

          then

          consider V be Subset of ET such that

           A10: t = V and

           A11: ex O be Subset of T st O in the topology of T & x in O & O c= V;

          consider O2 be Subset of T such that

           A12: O2 in the topology of T and

           A13: x in O2 and

           A14: O2 c= V by A11;

          

           A15: O2 in ( U_FMT x) by A12, A1, A2, A13;

          ( U_FMT x) is Filter of the carrier of ET by Def2;

          hence thesis by A14, CARD_FIL:def 1, A15, A10;

        end;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    begin

    definition

      let ET be FMT_TopSpace, F be Subset-Family of ET;

      :: FINTOPO7:def13

      attr F is quasi_basis means

      : Def8: ( Family_open_set ET) c= ( UniCl F);

    end

    registration

      let ET be FMT_TopSpace;

      cluster ( Family_open_set ET) -> quasi_basis;

      coherence

      proof

        reconsider F = ( Family_open_set ET) as Subset-Family of ET;

        let x be object;

        assume

         A1: x in ( Family_open_set ET);

        then

        reconsider B = {x} as Subset-Family of ET by SUBSET_1: 41;

        

         A2: B c= ( Family_open_set ET) by A1, ZFMISC_1: 31;

        x = ( union B);

        hence thesis by A2, CANTOR_1:def 1;

      end;

    end

    registration

      let ET be FMT_TopSpace;

      cluster quasi_basis for Subset-Family of ET;

      existence

      proof

        reconsider OP = ( Family_open_set ET) as Subset-Family of ET;

        for x be Subset of ET holds x in OP iff ex Y be Subset-Family of ET st Y c= OP & x = ( union Y)

        proof

          let x be Subset of ET;

          hereby

            assume

             A1: x in OP;

            reconsider B = {x} as Subset-Family of ET;

            x = ( union B);

            hence ex Y be Subset-Family of ET st Y c= OP & x = ( union Y) by A1, ZFMISC_1: 31;

          end;

          given Y be Subset-Family of ET such that

           A2: Y c= OP & x = ( union Y);

          thus x in OP by A2, Th9;

        end;

        hence thesis;

      end;

    end

    definition

      let ET be FMT_TopSpace;

      let S be Subset-Family of ET;

      :: FINTOPO7:def14

      attr S is open means S c= ( Family_open_set ET);

    end

    registration

      let ET be FMT_TopSpace;

      cluster open for Subset-Family of ET;

      existence

      proof

        take ( Family_open_set ET);

        thus thesis;

      end;

    end

    registration

      let ET be FMT_TopSpace;

      cluster open quasi_basis for Subset-Family of ET;

      existence

      proof

        take ( Family_open_set ET);

        thus thesis;

      end;

    end

    definition

      let ET be FMT_TopSpace;

      mode Basis of ET is open quasi_basis Subset-Family of ET;

    end

    theorem :: FINTOPO7:21

    for ET be FMT_TopSpace, B be Basis of ET holds ( Family_open_set ET) = ( UniCl B)

    proof

      let X be FMT_TopSpace, B be Basis of X;

      thus ( Family_open_set X) c= ( UniCl B) by Def8;

      hereby

        let t be object;

        assume t in ( UniCl B);

        then

        consider Y be Subset-Family of X such that

         A1: Y c= B & t = ( union Y) by CANTOR_1:def 1;

        B is open;

        then B c= ( Family_open_set X);

        then Y c= ( Family_open_set X) by A1;

        hence t in ( Family_open_set X) by A1, Th9;

      end;

    end;

    theorem :: FINTOPO7:22

    for B be non empty Subset-Family of X st (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB)) & X = ( union B) holds ex ET be FMT_TopSpace st the carrier of ET = X & B is Basis of ET

    proof

      let B be non empty Subset-Family of X such that

       A1: (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB)) and

       A2: X = ( union B);

      set O = ( UniCl B);

      set T = TopStruct (# X, O #);

      T is TopSpace by A1, A2, Th3;

      then

      consider ET be FMT_TopSpace such that

       A3: the carrier of T = the carrier of ET and

       A4: ( Family_open_set ET) = the topology of T by Th12;

      reconsider B1 = B as Subset-Family of ET by A3;

      

       A5: B1 is open by A4, CANTOR_1: 1;

      B1 is quasi_basis by A3, A4;

      hence thesis by A3, A5;

    end;

    theorem :: FINTOPO7:23

    for ET be FMT_TopSpace, B be Basis of ET holds (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB)) & (the carrier of ET = ( union B))

    proof

      let X be FMT_TopSpace, B be Basis of X;

      

       A1: B is quasi_basis;

      thus (for B1,B2 be Element of B holds ex BB be Subset of B st (B1 /\ B2) = ( union BB))

      proof

        let B1,B2 be Element of B;

        per cases ;

          suppose B is empty;

          then

           A2: ( UniCl B) = { {} } by YELLOW_9: 16;

          the carrier of X in ( Family_open_set X) by Th9;

          hence thesis by A1, A2, TARSKI:def 1;

        end;

          suppose

           A3: not B is empty;

          B is open;

          then B c= ( Family_open_set X);

          then B1 in ( Family_open_set X) & B2 in ( Family_open_set X) by A3;

          then (B1 /\ B2) in ( Family_open_set X) & B is quasi_basis by Th9;

          then

          consider Y be Subset-Family of X such that

           A4: Y c= B & (B1 /\ B2) = ( union Y) by CANTOR_1:def 1;

          reconsider Y as Subset of B by A4;

          thus ex BB be Subset of B st (B1 /\ B2) = ( union BB) by A4;

        end;

      end;

      the carrier of X in ( Family_open_set X) by Th9;

      then

      consider Y be Subset-Family of X such that

       A5: Y c= B & the carrier of X = ( union Y) by A1, CANTOR_1:def 1;

      thus the carrier of X c= ( union B) by A5, ZFMISC_1: 77;

      thus ( union B) c= the carrier of X;

    end;

    begin

    definition

      let T be non empty TopSpace;

      :: FINTOPO7:def15

      func TopSpace2FMT T -> FMT_TopSpace means

      : Def9: the carrier of it = the carrier of T & ( Family_open_set it ) = the topology of T;

      existence by Th12;

      uniqueness

      proof

        let S1,S2 be FMT_TopSpace such that

         A1: the carrier of S1 = the carrier of T & ( Family_open_set S1) = the topology of T and

         A2: the carrier of S2 = the carrier of T & ( Family_open_set S2) = the topology of T;

        set F1 = the BNbd of S1;

        set F2 = the BNbd of S2;

        F1 = F2

        proof

          reconsider F2 as Function of the carrier of S1, ( bool ( bool the carrier of S1)) by A1, A2;

          for x be object st x in the carrier of S1 holds (F1 . x) = (F2 . x)

          proof

            let x be object;

            assume x in the carrier of S1;

            then

            reconsider x as Element of S1;

            (F1 . x) = (F2 . x)

            proof

              hereby

                let t be object;

                assume t in (F1 . x);

                then t in ( U_FMT x);

                then t in { V where V be Subset of S1 : ex O be Subset of T st O in the topology of T & x in O & O c= V } by A1, Th13;

                then

                consider V1 be Subset of S1 such that

                 A3: t = V1 and

                 A4: ex O be Subset of T st O in the topology of T & x in O & O c= V1;

                consider O1 be Subset of T such that

                 A5: O1 in the topology of T & x in O1 & O1 c= V1 by A4;

                reconsider V2 = V1 as Subset of S2 by A1, A2;

                reconsider x2 = x as Element of S2 by A1, A2;

                O1 in the topology of T & x2 in O1 & O1 c= V2 by A5;

                then t in { V where V be Subset of S2 : ex O be Subset of T st O in the topology of T & x in O & O c= V } by A3;

                then t in ( U_FMT x2) by A2, Th13;

                hence t in (F2 . x);

              end;

              let t be object;

              assume

               A6: t in (F2 . x);

              consider x3 be Element of S2 such that

               A7: x = x3 by A1, A2;

              t in ( U_FMT x3) by A7, A6;

              then t in { V where V be Subset of S2 : ex O be Subset of T st O in the topology of T & x3 in O & O c= V } by A2, Th13;

              then

              consider V2 be Subset of S2 such that

               A8: t = V2 and

               A9: ex O be Subset of T st O in the topology of T & x3 in O & O c= V2;

              consider O2 be Subset of T such that

               A10: O2 in the topology of T & x3 in O2 & O2 c= V2 by A9;

              reconsider V1 = V2 as Subset of S1 by A1, A2;

              reconsider x1 = x3 as Element of S1 by A1, A2;

              O2 in the topology of T & x1 in O2 & O2 c= V1 by A10;

              then t in { V where V be Subset of S1 : ex O be Subset of T st O in the topology of T & x in O & O c= V } by A7, A8;

              then t in ( U_FMT x1) by A7, A1, Th13;

              hence t in (F1 . x) by A7;

            end;

            hence thesis;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        hence S1 = S2;

      end;

    end

    definition

      let ET be FMT_TopSpace;

      :: FINTOPO7:def16

      func FMT2TopSpace ET -> strict TopSpace means

      : Def10: the carrier of it = the carrier of ET & ( Family_open_set ET) = the topology of it ;

      existence

      proof

        set T = TopStruct (# the carrier of ET, ( Family_open_set ET) #);

        

         A1: (for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T) by Th9;

        (for a,b be Subset of ET st a in the topology of T & b in the topology of T holds (a /\ b) in ( Family_open_set ET)) by Th9;

        then T is TopSpace by A1, Th9, PRE_TOPC:def 1;

        hence thesis;

      end;

      uniqueness ;

    end

    registration

      let ET be FMT_TopSpace;

      cluster ( FMT2TopSpace ET) -> non empty;

      coherence by Def10;

    end

    theorem :: FINTOPO7:24

    for T be non empty strict TopSpace holds T = ( FMT2TopSpace ( TopSpace2FMT T))

    proof

      let T be non empty strict TopSpace;

      ( TopSpace2FMT T) is FMT_TopSpace & the carrier of ( TopSpace2FMT T) = the carrier of T & ( Family_open_set ( TopSpace2FMT T)) = the topology of T by Def9;

      hence thesis by Def10;

    end;

    theorem :: FINTOPO7:25

    for ET be FMT_TopSpace holds ET = ( TopSpace2FMT ( FMT2TopSpace ET))

    proof

      let ET be FMT_TopSpace;

      ( FMT2TopSpace ET) is strict TopSpace & the carrier of ( FMT2TopSpace ET) = the carrier of ET & ( Family_open_set ET) = the topology of ( FMT2TopSpace ET) by Def10;

      hence thesis by Def9;

    end;