cardfil2.miz



    begin

    reserve X for non empty set,

FX for Filter of X,

SFX for Subset-Family of X;

    definition

      let X be set, SFX be Subset-Family of X;

      :: CARDFIL2:def1

      attr SFX is upper means

      : def1: for Y1,Y2 be Subset of X st Y1 in SFX & Y1 c= Y2 holds Y2 in SFX;

    end

    registration

      let X be set;

      cluster non empty for cap-closed Subset-Family of X;

      existence

      proof

        reconsider SFX = { {} } as non empty Subset-Family of X by SETFAM_1: 46;

        now

          let x,y be set;

          assume x in { {} } & y in { {} };

          then x = {} & y = {} by TARSKI:def 1;

          hence (x /\ y) in { {} } by TARSKI:def 1;

        end;

        then SFX is cap-closed;

        hence thesis;

      end;

    end

    registration

      let X be set;

      cluster upper for non empty cap-closed Subset-Family of X;

      existence

      proof

        per cases ;

          suppose X is non empty;

          then

          reconsider B = {X} as non empty Subset-Family of X by CARD_FIL: 2;

           A1:

          now

            let x,y be set;

            assume x in {X} & y in {X};

            then x = X & y = X by TARSKI:def 1;

            hence (x /\ y) in {X} by TARSKI:def 1;

          end;

          now

            let Y1,Y2 be Subset of X;

            assume

             A2: Y1 in B & Y1 c= Y2;

            then Y1 = X & Y2 = X by TARSKI:def 1;

            hence Y2 in B by A2;

          end;

          then B is cap-closed & B is upper by A1;

          hence thesis;

        end;

          suppose

           A3: X is empty;

          now

            let x,y be set;

            assume x in { {} } & y in { {} };

            then x = {} & y = {} by TARSKI:def 1;

            hence (x /\ y) in { {} } by TARSKI:def 1;

          end;

          then { {} } is cap-closed;

          then

          reconsider B = { {} } as non empty cap-closed Subset-Family of {} by SETFAM_1: 46;

          B is upper;

          hence thesis by A3;

        end;

      end;

    end

    registration

      let X be non empty set;

      cluster with_non-empty_elements for non empty upper cap-closed Subset-Family of X;

      existence

      proof

        now

          let x,y be set;

          assume that

           A1: x in {X} and

           A2: y in {X};

          x = X & y = X by A1, A2, TARSKI:def 1;

          hence (x /\ y) in {X} by TARSKI:def 1;

        end;

        then {X} is cap-closed;

        then

        reconsider B = {X} as non empty cap-closed Subset-Family of X by CARD_FIL: 2;

        now

          let Y1,Y2 be Subset of X;

          assume

           A3: Y1 in B & Y1 c= Y2;

          Y1 = X & Y2 = X by A3, TARSKI:def 1;

          hence Y2 in B by A3;

        end;

        then B is upper;

        hence thesis;

      end;

    end

    

     Lm01: for SFX be non empty with_non-empty_elements upper cap-closed Subset-Family of X holds SFX is Filter of X

    proof

      let SFX be non empty with_non-empty_elements upper cap-closed Subset-Family of X;

      now

        thus not {} in SFX;

        SFX is cap-closed;

        hence for Y1,Y2 be Subset of X st Y1 in SFX & Y2 in SFX holds (Y1 /\ Y2) in SFX;

        thus for Y1,Y2 be Subset of X st Y1 in SFX & Y1 c= Y2 holds Y2 in SFX by def1;

      end;

      hence thesis by CARD_FIL:def 1;

    end;

    

     Lm02: FX is non empty with_non-empty_elements upper cap-closed Subset-Family of X

    proof

      FX is non empty with_non-empty_elements cap-closed upper by CARD_FIL:def 1;

      hence thesis;

    end;

    theorem :: CARDFIL2:1

    SFX is non empty with_non-empty_elements upper cap-closed Subset-Family of X iff SFX is Filter of X by Lm01, Lm02;

    theorem :: CARDFIL2:2

    for X1,X2 be non empty set, F1 be Filter of X1, F2 be Filter of X2 holds the set of all [:f1, f2:] where f1 be Element of F1, f2 be Element of F2 is non empty Subset-Family of [:X1, X2:]

    proof

      let X1,X2 be non empty set, F1 be Filter of X1, F2 be Filter of X2;

      set F1xF2 = the set of all [:f1, f2:] where f1 be Element of F1, f2 be Element of F2;

      

       A0: [: the Element of F1, the Element of F2:] in F1xF2;

      F1xF2 c= ( bool [:X1, X2:])

      proof

        let x be object;

        assume x in F1xF2;

        then

        consider f1 be Element of F1, f2 be Element of F2 such that

         A1: x = [:f1, f2:];

        thus thesis by A1;

      end;

      hence thesis by A0;

    end;

    definition

      let X be non empty set;

      :: CARDFIL2:def2

      attr X is cap-finite-closed means for SX be finite non empty Subset of X holds ( meet SX) in X;

    end

    registration

      cluster cap-finite-closed for non empty set;

      existence

      proof

        take X = { {} };

        now

          let SX be finite non empty Subset of X;

          ( meet SX) = ( meet { {} }) or ( meet SX) = ( meet {} ) by ZFMISC_1: 33;

          then ( meet SX) = {} by SETFAM_1: 10, SETFAM_1: 1;

          hence ( meet SX) in X by TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: CARDFIL2:3

    

     Th01: for X be non empty set st X is cap-finite-closed holds X is cap-closed

    proof

      let X be non empty set;

      assume

       A1: X is cap-finite-closed;

      now

        let a,b be set;

        assume a in X & b in X;

        then {a, b} c= X by TARSKI:def 2;

        then ( meet {a, b}) in X by A1;

        hence (a /\ b) in X by SETFAM_1: 11;

      end;

      hence thesis;

    end;

    registration

      cluster cap-finite-closed -> cap-closed for non empty set;

      coherence by Th01;

    end

    theorem :: CARDFIL2:4

    

     Th02: for X be set, SFX be Subset-Family of X holds SFX is cap-closed & X in SFX iff ( FinMeetCl SFX) c= SFX

    proof

      let X be set, F be Subset-Family of X;

      hereby

        assume that

         A1: F is cap-closed and

         A2: X in F;

        now

          let x be object;

          assume

           A3: x in ( FinMeetCl F);

          then

          reconsider x1 = x as Subset of X;

          consider Y be Subset-Family of X such that

           A4: Y c= F and

           A5: Y is finite and

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

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

          

           A7: P[ 0 ]

          proof

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

            assume that Y c= F and

             A8: ( card Y) = 0 and

             A9: x = ( Intersect Y);

            

             A10: Y = {} by A8;

            reconsider x0 = x as set;

            thus x in F by A9, A10, SETFAM_1:def 9, A2;

          end;

          

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

          proof

            let k be Nat;

            assume

             A12: P[k];

            now

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

              assume that

               A13: Y c= F 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= F & ( card C) = k by A13, A17;

              F 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 x = x1 by A15, A16, A19, SETFAM_1:def 9;

                hence x in F by A13, A16;

              end;

                suppose

                 A20: C <> {} ;

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

                then

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

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

                then

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

                

                 A23: ( Intersect C0) in F by A12, A18;

                x1 in F by A13, A16;

                hence x in F by A22, A15, A23, A1;

              end;

            end;

            hence P[(k + 1)];

          end;

          

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

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

           P[CY] by A24;

          hence x in F by A4, A6;

        end;

        hence ( FinMeetCl F) c= F;

      end;

      assume

       A25: ( FinMeetCl F) c= F;

      now

        let A,B be set;

        assume

         A26: A in F & B in F;

        then A in ( bool X) & B in ( bool X);

        then {A, B} c= ( bool X) by TARSKI:def 2;

        then

        reconsider AB = {A, B} as finite Subset-Family of X;

        AB c= F & AB is finite & ( meet AB) = ( Intersect AB) by A26, TARSKI:def 2, SETFAM_1:def 9;

        then ( meet AB) in ( FinMeetCl F) by CANTOR_1:def 3;

        then (A /\ B) in ( FinMeetCl F) by SETFAM_1: 11;

        hence (A /\ B) in F by A25;

      end;

      hence F is cap-closed & X in F by A25, CANTOR_1: 8;

    end;

    theorem :: CARDFIL2:5

    for X be non empty set, A be non empty Subset of X holds { B where B be Subset of X : A c= B } is Filter of X

    proof

      let X be non empty set, A be non empty Subset of X;

      set C = { B where B be Subset of X : A c= B };

      

       A1: C is non empty Subset-Family of X

      proof

        

         A2: A in C;

        now

          let x be object such that

           A3: x in C;

          consider b0 be Subset of X such that

           A4: x = b0 and A c= b0 by A3;

          thus x in ( bool X) by A4;

        end;

        then C c= ( bool X);

        hence thesis by A2;

      end;

      

       A5: not {} in C

      proof

        assume {} in C;

        then

        consider b0 be Subset of X such that

         A6: {} = b0 & A c= b0;

        thus thesis by A6;

      end;

      

       A7: for Y1,Y2 be Subset of X holds Y1 in C & Y2 in C implies (Y1 /\ Y2) in C

      proof

        let Y1,Y2 be Subset of X such that

         A8: Y1 in C and

         A9: Y2 in C;

        consider b1 be Subset of X such that

         A10: Y1 = b1 & A c= b1 by A8;

        consider b2 be Subset of X such that

         A11: Y2 = b2 & A c= b2 by A9;

        A c= (Y1 /\ Y2) by A10, A11, XBOOLE_1: 19;

        hence thesis;

      end;

      for Y1,Y2 be Subset of X holds Y1 in C & Y1 c= Y2 implies Y2 in C

      proof

        let Y1,Y2 be Subset of X such that

         A12: Y1 in C and

         A13: Y1 c= Y2;

        consider b1 be Subset of X such that

         A14: b1 = Y1 & A c= b1 by A12;

        A c= Y2 by A13, A14;

        hence thesis;

      end;

      hence thesis by A1, A5, A7, CARD_FIL:def 1;

    end;

    registration

      let X be non empty set;

      cluster -> cap-closed for Filter of X;

      coherence by CARD_FIL:def 1;

    end

    theorem :: CARDFIL2:6

    for X be set, B be Subset-Family of X st B = {X} holds B is upper

    proof

      let X be set, B be Subset-Family of X;

      assume

       A1: B = {X};

      now

        let Y1,Y2 be Subset of X;

        assume

         A3: Y1 in B & Y1 c= Y2;

        Y1 = X & Y2 = X by A1, A3, TARSKI:def 1;

        hence Y2 in B by A3;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:7

    for X be non empty set, F be Filter of X holds F <> ( bool X)

    proof

      let X be non empty set, F be Filter of X;

      assume

       A1: F = ( bool X);

       {} c= X;

      hence contradiction by A1, CARD_FIL:def 1;

    end;

    definition

      let X be non empty set;

      :: CARDFIL2:def3

      func Filt X -> non empty set equals the set of all F where F be Filter of X;

      correctness

      proof

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

        FX in the set of all F where F be Filter of X;

        hence thesis;

      end;

    end

    definition

      let X be non empty set, I be non empty set, M be ( Filt X) -valued ManySortedSet of I;

      :: CARDFIL2:def4

      func Filter_Intersection M -> Filter of X equals ( meet ( rng M));

      coherence

      proof

        set F = ( meet ( rng M));

         A1:

        now

          let Y be set;

          assume Y in ( rng M);

          then

          consider a be object such that

           A2: a in ( dom M) and

           A3: (M . a) = Y by FUNCT_1:def 3;

          (M . a) in ( Filt X) by A2, FUNCT_1: 102;

          then

          consider FF be Filter of X such that

           A4: (M . a) = FF;

          thus X in Y by A3, A4, CARD_FIL: 5;

        end;

        now

          let x be object;

          assume

           A5: x in F;

          set i0 = the Element of I;

          i0 in I & I is non empty;

          then

           A6: i0 in ( dom M) by PARTFUN1:def 2;

          then (M . i0) in ( rng M) by FUNCT_1:def 3;

          then

           A7: x in (M . i0) by A5, SETFAM_1:def 1;

          (M . i0) in ( Filt X) by A6, FUNCT_1: 102;

          then

          consider F0 be Filter of X such that

           A8: (M . i0) = F0;

          thus x in ( bool X) by A7, A8;

        end;

        then F c= ( bool X);

        then

        reconsider F as non empty Subset-Family of X by A1, SETFAM_1:def 1;

        

         A9: not {} in F

        proof

          assume

           A10: {} in F;

          set i0 = the Element of I;

          i0 in I & I is non empty;

          then

           A11: i0 in ( dom M) by PARTFUN1:def 2;

          then

           A12: (M . i0) in ( rng M) by FUNCT_1:def 3;

          (M . i0) in ( Filt X) by A11, FUNCT_1: 102;

          then

          consider F0 be Filter of X such that

           A13: (M . i0) = F0;

           {} in F0 by A12, A10, SETFAM_1:def 1, A13;

          hence contradiction by CARD_FIL:def 1;

        end;

        now

          hereby

            let Y1,Y2 be Subset of X;

            assume that

             A14: Y1 in F and

             A15: Y2 in F;

            now

              let Y be set;

              assume

               A16: Y in ( rng M);

              then Y in ( Filt X);

              then

              consider F0 be Filter of X such that

               A17: Y = F0;

              Y1 in F0 & Y2 in F0 by A14, A15, A16, A17, SETFAM_1:def 1;

              hence (Y1 /\ Y2) in Y by A17, CARD_FIL:def 1;

            end;

            hence (Y1 /\ Y2) in F by SETFAM_1:def 1;

          end;

          let Y1,Y2 be Subset of X;

          assume that

           A18: Y1 in F and

           A19: Y1 c= Y2;

          now

            let Y be set;

            assume

             A20: Y in ( rng M);

            then Y in ( Filt X);

            then

            consider F0 be Filter of X such that

             A21: Y = F0;

            Y1 in Y by A18, A20, SETFAM_1:def 1;

            hence Y2 in Y by A19, A21, CARD_FIL:def 1;

          end;

          hence Y2 in F by SETFAM_1:def 1;

        end;

        hence thesis by A9, CARD_FIL:def 1;

      end;

    end

    definition

      let X be non empty set, F1,F2 be Filter of X;

      :: CARDFIL2:def5

      pred F1 is_filter-coarser_than F2 means F1 c= F2;

      reflexivity ;

      :: CARDFIL2:def6

      pred F1 is_filter-finer_than F2 means F2 c= F1;

      reflexivity ;

    end

    theorem :: CARDFIL2:8

    for X be non empty set, F be Filter of X, FX be Filter of X st FX = {X} holds FX is_coarser_than F

    proof

      let X be non empty set, F be Filter of X, FX be Filter of X;

      assume

       A1: FX = {X};

      X in F by CARD_FIL: 5;

      then {X} c= F by TARSKI:def 1;

      hence thesis by A1;

    end;

    theorem :: CARDFIL2:9

    for X be non empty set, I be non empty set, M be ( Filt X) -valued ManySortedSet of I holds for i be Element of I, F be Filter of X st F = (M . i) holds ( Filter_Intersection M) is_filter-coarser_than F

    proof

      let X be non empty set, I be non empty set, M be ( Filt X) -valued ManySortedSet of I;

      let i be Element of I, F be Filter of X;

      set FIM = ( Filter_Intersection M);

      assume

       A1: F = (M . i);

      now

        let a be object;

        assume

         A2: a in ( Filter_Intersection M);

        i in I;

        then i in ( dom M) by PARTFUN1:def 2;

        then (M . i) in ( rng M) by FUNCT_1:def 3;

        hence a in F by A1, A2, SETFAM_1:def 1;

      end;

      then FIM c= F;

      hence FIM is_filter-coarser_than F;

    end;

    theorem :: CARDFIL2:10

    for X be set, S be Subset-Family of X st ( FinMeetCl S) is with_non-empty_elements holds S is with_non-empty_elements

    proof

      let X be set, S be Subset-Family of X;

      assume

       A1: ( FinMeetCl S) is with_non-empty_elements;

      assume not S is with_non-empty_elements;

      then {} in S & S c= ( FinMeetCl S) by CANTOR_1: 4;

      hence contradiction by A1;

    end;

    theorem :: CARDFIL2:11

    for X be non empty set, G be Subset-Family of X, F be Filter of X st G c= F holds ( FinMeetCl G) c= F & ( FinMeetCl G) is with_non-empty_elements

    proof

      let X be non empty set, G be Subset-Family of X, F be Filter of X;

      assume

       A1: G c= F;

      

       A2: ( FinMeetCl G) c= ( FinMeetCl F) by A1, CANTOR_1: 14;

      ( FinMeetCl F) c= F by Th02, CARD_FIL: 5;

      hence ( FinMeetCl G) c= F by A2;

      hence ( FinMeetCl G) is with_non-empty_elements by CARD_FIL:def 1;

    end;

    definition

      let X be non empty set;

      let F be Filter of X;

      let B be non empty Subset of F;

      :: CARDFIL2:def7

      attr B is filter_basis means

      : def2: for f be Element of F holds ex b be Element of B st b c= f;

    end

    theorem :: CARDFIL2:12

    for X be non empty set, F be Filter of X, B be non empty Subset of F holds F is_coarser_than B iff B is filter_basis

    proof

      let X be non empty set, F be Filter of X, B be non empty Subset of F;

      hereby

        assume

         A1: F is_coarser_than B;

        now

          let f be Element of F;

          consider b be set such that

           A2: b in B and

           A3: b c= f by A1;

          reconsider b1 = b as Element of B by A2;

          b1 is Element of B & b1 c= f by A3;

          hence ex b be Element of B st b c= f;

        end;

        hence B is filter_basis;

      end;

      assume

       A4: B is filter_basis;

      for f be set st f in F holds ex b be set st b in B & b c= f

      proof

        let f be set;

        assume f in F;

        then

        consider b be Element of B such that

         A5: b c= f by A4;

        thus thesis by A5;

      end;

      hence thesis;

    end;

    registration

      let X be non empty set;

      let F be Filter of X;

      cluster filter_basis for non empty Subset of F;

      existence

      proof

        reconsider F2 = F as non empty Subset of F by XBOOLE_0:def 10;

        take F2;

        thus thesis;

      end;

    end

    definition

      let X be non empty set;

      let F be Filter of X;

      mode basis of F is filter_basis non empty Subset of F;

    end

    theorem :: CARDFIL2:13

    

     Th03: for X be non empty set, F be Filter of X holds F is basis of F

    proof

      let X be non empty set, F be Filter of X;

      thus F is filter_basis non empty Subset of F

      proof

        F is non empty & F c= F;

        then

        reconsider F0 = F as non empty Subset of F;

        F0 is filter_basis;

        hence thesis;

      end;

    end;

    definition

      let X be set, B be Subset-Family of X;

      :: CARDFIL2:def8

      func <.B.] -> Subset-Family of X means

      : def3: for x be Subset of X holds x in it iff ex b be Element of B st b c= x;

      existence

      proof

        defpred P[ set] means ex b be Element of B st b c= $1;

        ex Z be Subset-Family of X st for x be Subset of X holds x in Z iff P[x] from SUBSET_1:sch 3;

        hence thesis;

      end;

      correctness

      proof

        let B1,B2 be Subset-Family of X such that

         A1: for x be Subset of X holds x in B1 iff ex b be Element of B st b c= x and

         A2: for x be Subset of X holds x in B2 iff ex b be Element of B st b c= x;

        thus B1 c= B2

        proof

          let x be object;

          assume

           A3: x in B1;

          then

          reconsider x as Subset of X;

          ex b be Element of B st b c= x by A1, A3;

          hence thesis by A2;

        end;

        let x be object;

        assume

         A4: x in B2;

        then

        reconsider x as Subset of X;

        ex b be Element of B st b c= x by A2, A4;

        hence thesis by A1;

      end;

    end

    theorem :: CARDFIL2:14

    for X be set, S be Subset-Family of X holds <.S.] = { x where x be Subset of X : ex b be Element of S st b c= x }

    proof

      let X be set, S be Subset-Family of X;

      set SX = { x where x be Subset of X : ex b be Element of S st b c= x };

      hereby

        let x be object;

        assume

         A1: x in <.S.];

        then

        reconsider x1 = x as Subset of X;

        ex b be Element of S st b c= x1 by A1, def3;

        hence x in SX;

      end;

      let x be object;

      assume x in SX;

      then

      consider x0 be Subset of X such that

       A2: x = x0 and

       A3: ex b be Element of S st b c= x0;

      reconsider x1 = x as Subset of X by A2;

      thus x in <.S.] by A2, A3, def3;

    end;

    theorem :: CARDFIL2:15

    for X be set, B be empty Subset-Family of X holds <.B.] = ( bool X)

    proof

      let X be set, B be empty Subset-Family of X;

      thus <.B.] c= ( bool X);

      let x be object;

      assume x in ( bool X);

      then

      reconsider x0 = x as Subset of X;

       {} is Element of B & {} c= x0 by SUBSET_1:def 1;

      hence x in <.B.] by def3;

    end;

    theorem :: CARDFIL2:16

    for X be set, B be Subset-Family of X st {} in B holds <.B.] = ( bool X)

    proof

      let X be set, B be Subset-Family of X;

      assume

       A1: {} in B;

      thus <.B.] c= ( bool X);

      let x be object;

      assume x in ( bool X);

      then

      reconsider x0 = x as Subset of X;

       {} is Element of B & {} c= x0 by A1;

      hence x in <.B.] by def3;

    end;

    begin

    theorem :: CARDFIL2:17

    

     Th04: for X be set, B be non empty Subset-Family of X, L be Subset of ( BoolePoset X) st B = L holds <.B.] = ( uparrow L)

    proof

      let X be set, B be non empty Subset-Family of X, L be Subset of ( BoolePoset X);

      assume

       A1: B = L;

      hereby

        let x be object;

        assume

         A2: x in <.B.];

        then

        reconsider x0 = x as Subset of X;

        consider b be Element of B such that

         A3: b c= x0 by A2, def3;

        reconsider b1 = b as Element of ( BoolePoset X) by LATTICE3:def 1;

        reconsider x1 = x0 as Element of ( BoolePoset X) by LATTICE3:def 1;

        b1 <= x1 & b1 in L by A3, A1, YELLOW_1: 2;

        hence x in ( uparrow L) by WAYBEL_0:def 16;

      end;

      let x be object;

      assume

       A4B1: x in ( uparrow L);

      then

      reconsider x0 = x as Element of ( BoolePoset X);

      consider y be Element of ( BoolePoset X) such that

       A5B2: y <= x0 and

       A6B3: y in L by A4B1, WAYBEL_0:def 16;

      

       A7B4: y c= x0 by A5B2, YELLOW_1: 2;

      x0 is Element of ( bool X) by LATTICE3:def 1;

      then

      reconsider x1 = x as Subset of X;

      x1 in <.B.] by A1, A6B3, A7B4, def3;

      hence x in <.B.];

    end;

    theorem :: CARDFIL2:18

    for X be set, B be Subset-Family of X holds B c= <.B.] by def3;

    definition

      let X be set;

      let B1,B2 be Subset-Family of X;

      :: CARDFIL2:def9

      pred B1,B2 are_equivalent_generators means (for b1 be Element of B1 holds ex b2 be Element of B2 st b2 c= b1) & (for b2 be Element of B2 holds ex b1 be Element of B1 st b1 c= b2);

      reflexivity ;

      symmetry ;

    end

    theorem :: CARDFIL2:19

    

     Th05: for X be set, B1,B2 be Subset-Family of X st (B1,B2) are_equivalent_generators holds <.B1.] c= <.B2.]

    proof

      let X be set, B1,B2 be Subset-Family of X;

      assume

       A1: (B1,B2) are_equivalent_generators ;

      let x be object;

      assume

       A2: x in <.B1.];

      then

      reconsider x0 = x as Subset of X;

      consider b1 be Element of B1 such that

       A3: b1 c= x0 by A2, def3;

      consider b2 be Element of B2 such that

       A4: b2 c= b1 by A1;

      b2 c= x0 by A3, A4;

      hence thesis by def3;

    end;

    theorem :: CARDFIL2:20

    for X be set, B1,B2 be Subset-Family of X st (B1,B2) are_equivalent_generators holds <.B1.] = <.B2.] by Th05;

    definition

      let X be non empty set;

      let F be Filter of X;

      let B be non empty Subset of F;

      :: CARDFIL2:def10

      func # B -> non empty Subset-Family of X equals B;

      coherence by XBOOLE_1: 1;

    end

    theorem :: CARDFIL2:21

    

     Th06: for X be non empty set, F be Filter of X, B be basis of F holds F = <.( # B).]

    proof

      let X be non empty set, F be Filter of X, B be basis of F;

      hereby

        let x be object;

        assume x in F;

        then

        reconsider x0 = x as Element of F;

        consider b0 be Element of B such that

         A1: b0 c= x0 by def2;

        reconsider x0 as Subset of X;

        thus x in <.( # B).] by A1, def3;

      end;

      let x be object;

      assume

       A2: x in <.( # B).];

      then

      reconsider x0 = x as Subset of X;

      reconsider B2 = ( # B) as Subset-Family of X;

      consider b0 be Element of B such that

       A3: b0 c= x0 by A2, def3;

      thus x in F by A3, CARD_FIL:def 1;

    end;

    theorem :: CARDFIL2:22

    

     Th07: for X be non empty set, F be Filter of X, B be Subset-Family of X st F = <.B.] holds B is basis of F

    proof

      let X be non empty set, F be Filter of X, B be Subset-Family of X;

      assume

       A1: F = <.B.];

      then

       A2: B c= F by def3;

      B is non empty

      proof

        assume

         A3I1: B is empty;

        

         A4I2A: {} c= X;

         {} is Element of B by A3I1, SUBSET_1:def 1;

        then {} in <.B.] by A4I2A, def3;

        hence contradiction by A1, CARD_FIL:def 1;

      end;

      then

      reconsider B1 = B as non empty Subset of F by A2;

      B1 is filter_basis by A1, def3;

      hence thesis;

    end;

    theorem :: CARDFIL2:23

    for X be non empty set, F be Filter of X, B be basis of F, S be Subset-Family of X, S1 be Subset of F st S = S1 & (( # B),S) are_equivalent_generators holds S1 is basis of F

    proof

      let X be non empty set, F be Filter of X, B be basis of F, S be Subset-Family of X, S1 be Subset of F such that

       A1: S = S1 and

       A2: (( # B),S) are_equivalent_generators ;

       <.( # B).] = <.S.] by A2, Th05;

      hence thesis by A1, Th06, Th07;

    end;

    theorem :: CARDFIL2:24

    for X be non empty set, F be Filter of X, B1,B2 be basis of F holds (( # B1),( # B2)) are_equivalent_generators

    proof

      let X be non empty set, F be Filter of X, B1,B2 be basis of F;

      hereby

        let b1 be Element of ( # B1);

        b1 in ( # B1);

        then b1 in F;

        then b1 in <.( # B2).] by Th06;

        hence ex b2 be Element of ( # B2) st b2 c= b1 by def3;

      end;

      let b2 be Element of ( # B2);

      b2 in ( # B2);

      then b2 in F;

      then b2 in <.( # B1).] by Th06;

      hence ex b1 be Element of ( # B1) st b1 c= b2 by def3;

    end;

    definition

      let X be set;

      let B be Subset-Family of X;

      :: CARDFIL2:def11

      attr B is quasi_basis means

      : def4: for b1,b2 be Element of B holds ex b be Element of B st b c= (b1 /\ b2);

    end

    registration

      let X be non empty set;

      cluster quasi_basis for non empty Subset-Family of X;

      existence

      proof

        take S = {X};

        thus S is non empty Subset-Family of X by CARD_FIL: 2;

        reconsider S1 = S as Subset-Family of X by CARD_FIL: 2;

        now

          let b1,b2 be Element of S1;

          set b = (b1 /\ b2);

          b1 = X & b2 = X by TARSKI:def 1;

          hence ex b be Element of S1 st b c= (b1 /\ b2);

        end;

        then S1 is quasi_basis;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster with_non-empty_elements for non empty quasi_basis Subset-Family of X;

      existence

      proof

        set S = {X};

        reconsider S1 = S as Subset-Family of X by CARD_FIL: 2;

        now

          let b1,b2 be Element of S1;

          set b = (b1 /\ b2);

          b1 = X & b2 = X by TARSKI:def 1;

          hence ex b be Element of S1 st b c= (b1 /\ b2);

        end;

        then S1 is quasi_basis;

        then

        reconsider S2 = S1 as quasi_basis non empty Subset-Family of X;

        S2 is with_non-empty_elements;

        hence thesis;

      end;

    end

    definition

      let X be non empty set;

      mode filter_base of X is with_non-empty_elements non empty quasi_basis Subset-Family of X;

    end

    theorem :: CARDFIL2:25

    

     Th08: for X be non empty set, B be filter_base of X holds <.B.] is Filter of X

    proof

      let X be non empty set, B be filter_base of X;

      consider b0 be object such that

       A1: b0 in B by XBOOLE_0:def 1;

      now

        thus <.B.] is non empty by A1, def3;

        hereby

          assume

           A2: {} in <.B.];

          then

          reconsider x0 = {} as Subset of X;

          consider b0 be Element of B such that

           A3: b0 c= x0 by A2, def3;

          thus not {} in <.B.] by A3;

        end;

        let Y1,Y2 be Subset of X;

        hereby

          assume that

           A4: Y1 in <.B.] and

           A5: Y2 in <.B.];

          reconsider y1 = Y1, y2 = Y2 as Subset of X;

          consider b1 be Element of B such that

           A6: b1 c= y1 by A4, def3;

          consider b2 be Element of B such that

           A7: b2 c= y2 by A5, def3;

          consider b3 be Element of B such that

           A8: b3 c= (b1 /\ b2) by def4;

          (b1 /\ b2) c= (Y1 /\ Y2) by A6, A7, XBOOLE_1: 27;

          then b3 c= (Y1 /\ Y2) by A8;

          hence (Y1 /\ Y2) in <.B.] by def3;

        end;

        assume that

         A9: Y1 in <.B.] and

         A10: Y1 c= Y2;

        reconsider y1 = Y1 as Subset of X;

        consider b1 be Element of B such that

         A11: b1 c= y1 by A9, def3;

        b1 c= Y2 by A10, A11;

        hence Y2 in <.B.] by def3;

      end;

      hence thesis by CARD_FIL:def 1;

    end;

    definition

      let X be non empty set, B be filter_base of X;

      :: CARDFIL2:def12

      func <.B.) -> Filter of X equals <.B.];

      coherence by Th08;

    end

    theorem :: CARDFIL2:26

    for X be non empty set, B1,B2 be filter_base of X st <.B1.) = <.B2.) holds (B1,B2) are_equivalent_generators

    proof

      let X be non empty set, B1,B2 be filter_base of X;

      assume

       A1: <.B1.) = <.B2.);

      

       A2: for b1 be Element of B1 holds ex b2 be Element of B2 st b2 c= b1

      proof

        let b1 be Element of B1;

        b1 in <.B2.] by A1, def3;

        then

        consider b2 be Element of B2 such that

         A3: b2 c= b1 by def3;

        thus thesis by A3;

      end;

      for b2 be Element of B2 holds ex b1 be Element of B1 st b1 c= b2

      proof

        let b2 be Element of B2;

        b2 in <.B1.] by A1, def3;

        then

        consider b1 be Element of B1 such that

         A4: b1 c= b2 by def3;

        thus thesis by A4;

      end;

      hence thesis by A2;

    end;

    theorem :: CARDFIL2:27

    for X be non empty set, FB be filter_base of X, F be Filter of X st FB c= F holds <.FB.) is_coarser_than F

    proof

      let X be non empty set, FB be filter_base of X, F be Filter of X;

      assume

       A1: FB c= F;

      now

        let x be object;

        assume

         A2: x in <.FB.);

        then

        reconsider x1 = x as Subset of X;

        consider b be Element of FB such that

         A4: b c= x1 by A2, def3;

        

         A5: b in F by A1;

        reconsider x2 = x1 as Subset of X;

        consider c be Element of F such that

         A6: c c= x2 by A4, A5;

        thus x in F by A6, CARD_FIL:def 1;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:28

    for X be non empty set, G be Subset-Family of X st ( FinMeetCl G) is with_non-empty_elements holds ( FinMeetCl G) is filter_base of X & ex F be Filter of X st ( FinMeetCl G) c= F

    proof

      let X be non empty set, G be Subset-Family of X;

      assume

       A1: ( FinMeetCl G) is with_non-empty_elements;

      reconsider FG = ( FinMeetCl G) as Subset-Family of X;

      now

        let b1,b2 be Element of FG;

        ( FinMeetCl FG) c= FG by CANTOR_1: 11;

        then FG is cap-closed by Th02;

        then

        reconsider b = (b1 /\ b2) as Element of FG;

        b is Element of FG & b c= (b1 /\ b2);

        hence ex b be Element of FG st b c= (b1 /\ b2);

      end;

      then FG is quasi_basis;

      then

      reconsider FG as filter_base of X by A1;

      FG c= <.FG.) by def3;

      hence thesis;

    end;

    theorem :: CARDFIL2:29

    

     Th09: for X be non empty set, F be Filter of X, B be basis of F holds B is filter_base of X

    proof

      let X be non empty set, F be Filter of X, B be basis of F;

      for b1,b2 be Element of B holds ex b be Element of B st b c= (b1 /\ b2)

      proof

        let b1,b2 be Element of B;

        (b1 /\ b2) in F by CARD_FIL:def 1;

        then

        consider b0 be Element of B such that

         A1: b0 c= (b1 /\ b2) by def2;

        thus thesis by A1;

      end;

      then

       A2: ( # B) is quasi_basis;

      B is with_non-empty_elements by CARD_FIL:def 1;

      hence thesis by A2;

    end;

    theorem :: CARDFIL2:30

    

     Th10: for X be non empty set, B be filter_base of X holds B is basis of <.B.)

    proof

      let X be non empty set, B be filter_base of X;

      reconsider B2 = <.B.) as Filter of X;

      B is filter_basis non empty Subset of B2

      proof

        B is non empty Subset of B2

        proof

          B c= B2 by def3;

          hence thesis;

        end;

        then

        reconsider B3 = B as non empty Subset of B2;

        B3 is filter_basis by def3;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:31

    for X be non empty set, F be Filter of X, B be basis of F, L be Subset of ( BoolePoset X) st L = ( # B) holds F = ( uparrow L)

    proof

      let X be non empty set, F be Filter of X, B be basis of F, L be Subset of ( BoolePoset X);

      assume

       A1: L = ( # B);

      F = <.( # B).] by Th06;

      hence F = ( uparrow L) by Th04, A1;

    end;

    theorem :: CARDFIL2:32

    for X be non empty set, B be filter_base of X, L be Subset of ( BoolePoset X) st L = B holds <.B.) = ( uparrow L) by Th04;

    theorem :: CARDFIL2:33

    

     Th11: for X be non empty set, F1,F2 be Filter of X, B1 be basis of F1, B2 be basis of F2 holds F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2

    proof

      let X be non empty set, F1,F2 be Filter of X, B1 be basis of F1, B2 be basis of F2;

      hereby

        assume F1 is_filter-coarser_than F2;

        then

         A1: F1 c= F2;

        now

          let x be set;

          assume x in B1;

          then x in F2 by A1;

          then ex b be Element of B2 st b c= x by def2;

          hence ex y be set st y in B2 & y c= x;

        end;

        hence B1 is_coarser_than B2;

      end;

      assume

       A2: B1 is_coarser_than B2;

      now

        let x be object;

        assume

         A3: x in F1;

        then

        reconsider x1 = x as Subset of X;

        consider b1 be Element of B1 such that

         A4: b1 c= x1 by A3, def2;

        consider b2 be set such that

         A5: b2 in B2 and

         A6: b2 c= b1 by A2;

        reconsider b2 as Element of B2 by A5;

        

         A7: b2 c= x1 by A4, A6;

        x1 in <.( # B2).] by A7, def3;

        hence x in F2 by Th06;

      end;

      then F1 c= F2;

      hence F1 is_filter-coarser_than F2;

    end;

    theorem :: CARDFIL2:34

    

     Th12: for X,Y be non empty set, f be Function of X, Y, F be Filter of X, B be basis of F holds (f .: ( # B)) is filter_base of Y & <.(f .: ( # B)).] is Filter of Y & <.(f .: ( # B)).] = { M where M be Subset of Y : (f " M) in F }

    proof

      let X,Y be non empty set, f be Function of X, Y, F be Filter of X, B be basis of F;

      set FB = (f .: ( # B));

      now

        set b0 = the Element of B;

        (f .: b0) in FB by FUNCT_2:def 10;

        hence FB is non empty;

      end;

      then

      reconsider FB1 = FB as non empty Subset-Family of Y;

      

       A1: FB is quasi_basis non empty Subset-Family of Y

      proof

        now

          let b1,b2 be Element of FB;

          b1 in FB1;

          then

          consider M be Subset of X such that

           A2: M in ( # B) and

           A3: b1 = (f .: M) by FUNCT_2:def 10;

          b2 in FB1;

          then

          consider N be Subset of X such that

           A4: N in ( # B) and

           A5: b2 = (f .: N) by FUNCT_2:def 10;

          ( # B) is quasi_basis & M in ( # B) & N in ( # B) by A2, A4, Th09;

          then

          consider P be Element of B such that

           A6: P c= (M /\ N);

          

           A7: (f .: P) c= (f .: (M /\ N)) by A6, RELAT_1: 123;

          (f .: (M /\ N)) c= ((f .: M) /\ (f .: N)) by RELAT_1: 121;

          then

           A8: (f .: P) c= (b1 /\ b2) by A3, A5, A7;

          (f .: P) is Element of FB by FUNCT_2:def 10;

          hence ex b be Element of FB st b c= (b1 /\ b2) by A8;

        end;

        then FB1 is quasi_basis;

        hence thesis;

      end;

      

       A9: FB is with_non-empty_elements

      proof

        assume not FB is with_non-empty_elements;

        then

        consider x be Subset of X such that

         A10: x in ( # B) and

         A11: {} = (f .: x) by FUNCT_2:def 10;

        ( dom f) = X by FUNCT_2:def 1;

        then X misses x by A11, RELAT_1: 118;

        then {} in B by A10, XBOOLE_1: 67;

        hence contradiction by CARD_FIL:def 1;

      end;

      hence FB is filter_base of Y by A1;

      thus <.FB.] is Filter of Y by A1, A9, Th08;

      thus <.FB.] = { M where M be Subset of Y : (f " M) in F }

      proof

        hereby

          let y be object;

          assume

           A12: y in <.FB.];

          then

          reconsider y0 = y as Subset of Y;

          consider b be Element of FB such that

           A13: b c= y0 by A12, def3;

          b in FB1;

          then

          consider M be Subset of X such that

           A14: M in ( # B) and

           A15: b = (f .: M) by FUNCT_2:def 10;

          

           A16: (f " (f .: M)) c= (f " y0) by A13, A15, RELAT_1: 143;

          M c= (f " (f .: M)) by FUNCT_2: 42;

          then M c= (f " y0) by A16;

          then (f " y0) in <.( # B).] by A14, def3;

          then (f " y0) in F by Th06;

          hence y in { M where M be Subset of Y : (f " M) in F };

        end;

        let x be object;

        assume x in { M where M be Subset of Y : (f " M) in F };

        then

        consider M0 be Subset of Y such that

         A17: x = M0 and

         A18: (f " M0) in F;

        (f " M0) in <.( # B).] by A18, Th06;

        then

        consider b0 be Element of ( # B) such that

         A19: b0 c= (f " M0) by def3;

        

         A20: (f .: b0) c= (f .: (f " M0)) by A19, RELAT_1: 123;

        reconsider fb = (f .: b0) as Element of FB by FUNCT_2:def 10;

        (f .: (f " M0)) c= M0 by FUNCT_1: 75;

        then fb c= M0 by A20;

        hence x in <.FB.] by A17, def3;

      end;

    end;

    definition

      let X,Y be non empty set, f be Function of X, Y, F be Filter of X;

      :: CARDFIL2:def13

      func filter_image (f,F) -> Filter of Y equals { M where M be Subset of Y : (f " M) in F };

      correctness

      proof

        reconsider F0 = F as basis of F by Th03;

         <.(f .: ( # F0)).] is Filter of Y & <.(f .: ( # F0)).] = { M where M be Subset of Y : (f " M) in F } by Th12;

        hence thesis;

      end;

    end

    theorem :: CARDFIL2:35

    

     Th13: for X,Y be non empty set, f be Function of X, Y, F be Filter of X holds (f .: F) is filter_base of Y & <.(f .: F).] = ( filter_image (f,F))

    proof

      let X,Y be non empty set, f be Function of X, Y, F be Filter of X;

      reconsider F1 = F as basis of F by Th03;

      (f .: ( # F1)) is filter_base of Y & <.(f .: ( # F1)).] = ( filter_image (f,F)) by Th12;

      hence thesis;

    end;

    theorem :: CARDFIL2:36

    for X be non empty set, B be filter_base of X st B = <.B.) holds B is Filter of X;

    theorem :: CARDFIL2:37

    

     Th13bThmBA2: for X,Y be non empty set, f be Function of X, Y, F be Filter of X, B be basis of F holds (f .: ( # B)) is basis of ( filter_image (f,F)) & <.(f .: ( # B)).] = ( filter_image (f,F))

    proof

      let X,Y be non empty set, f be Function of X, Y, F be Filter of X, B be basis of F;

      reconsider FB = (f .: ( # B)) as filter_base of Y by Th12;

      reconsider FB2 = <.FB.) as Filter of Y;

      FB2 = ( filter_image (f,F)) by Th12;

      hence thesis by Th10;

    end;

    theorem :: CARDFIL2:38

    for X,Y be non empty set, f be Function of X, Y, B1,B2 be filter_base of X st B1 is_coarser_than B2 holds <.B1.) is_filter-coarser_than <.B2.)

    proof

      let X,Y be non empty set, f be Function of X, Y, B1,B2 be filter_base of X;

      assume

       A1: B1 is_coarser_than B2;

      B1 is basis of <.B1.) & B2 is basis of <.B2.) by Th10;

      hence thesis by A1, Th11;

    end;

    theorem :: CARDFIL2:39

    for X,Y be non empty set, f be Function of X, Y, F be Filter of X holds (f .: F) is Filter of Y iff Y = ( rng f)

    proof

      let X,Y be non empty set, f be Function of X, Y, F be Filter of X;

      hereby

        assume (f .: F) is Filter of Y;

        then Y in (f .: F) by CARD_FIL: 5;

        then

        consider B be Subset of X such that B in F and

         A1: Y = (f .: B) by FUNCT_2:def 10;

        now

          let y be object;

          assume y in Y;

          then

          consider x be object such that

           A2: x in ( dom f) and x in B and

           A3: y = (f . x) by A1, FUNCT_1:def 6;

          thus y in ( rng f) by A2, A3, FUNCT_1:def 3;

        end;

        then Y c= ( rng f);

        hence Y = ( rng f);

      end;

      assume

       A4: Y = ( rng f);

      reconsider fF = (f .: F) as filter_base of Y by Th13;

      

       A5: fF c= <.fF.) by def3;

       <.fF.) c= fF

      proof

        let x be object;

        assume

         A6: x in <.fF.);

        then

        reconsider x1 = x as Subset of Y;

        consider b2 be Element of fF such that

         A7: b2 c= x1 by A6, def3;

        consider bx be Subset of X such that

         A8: bx in F and

         A9: b2 = (f .: bx) by FUNCT_2:def 10;

        reconsider fx1 = (f " x1) as Subset of X;

        

         A10: ( dom f) = X by FUNCT_2:def 1;

        

         A11: (f " (f .: bx)) c= (f " x1) by A7, A9, RELAT_1: 143;

        bx c= (f " (f .: bx)) by A10, FUNCT_1: 76;

        then bx c= (f " x1) by A11;

        then fx1 in F by A8, CARD_FIL:def 1;

        then (f .: fx1) in fF by FUNCT_2:def 10;

        hence thesis by A4, FUNCT_1: 77;

      end;

      then fF = <.fF.) by A5;

      hence thesis;

    end;

    theorem :: CARDFIL2:40

    for X be non empty set, A be non empty Subset of X holds for F be Filter of A, B be basis of F holds (( incl A) .: ( # B)) is filter_base of X & <.(( incl A) .: ( # B)).] is Filter of X & <.(( incl A) .: ( # B)).] = { M where M be Subset of X : (( incl A) " M) in F } by Th12;

    definition

      let L be non empty RelStr;

      :: CARDFIL2:def14

      func Tails L -> non empty Subset-Family of L equals the set of all ( uparrow i) where i be Element of L;

      coherence

      proof

        

         A1: the set of all ( uparrow i) where i be Element of L is non empty

        proof

          set l0 = the Element of L;

          take ( uparrow the Element of L);

          thus thesis;

        end;

         the set of all ( uparrow i) where i be Element of L c= ( bool the carrier of L)

        proof

          let t be object;

          assume t in the set of all ( uparrow i) where i be Element of L;

          then

          consider i0 be Element of L such that

           A2: t = ( uparrow i0);

          thus thesis by A2;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: CARDFIL2:41

    

     Th14: for L be non empty transitive reflexive RelStr st ( [#] L) is directed holds <.( Tails L).] is Filter of ( [#] L)

    proof

      let L be non empty transitive reflexive RelStr;

      assume

       A1: ( [#] L) is directed;

      ( Tails L) is non empty Subset-Family of L & ( Tails L) is with_non-empty_elements & ( Tails L) is quasi_basis

      proof

        

         A2: ( Tails L) is with_non-empty_elements

        proof

          assume not ( Tails L) is with_non-empty_elements;

          then

          consider i0 be Element of L such that

           A3: {} = ( uparrow i0);

          thus contradiction by A3;

        end;

        (for x,y be Element of ( Tails L) holds ex z be Element of ( Tails L) st z c= (x /\ y))

        proof

          let x,y be Element of ( Tails L);

          x in ( Tails L);

          then

          consider lx be Element of L such that

           A4: x = ( uparrow lx);

          y in ( Tails L);

          then

          consider ly be Element of L such that

           A5: y = ( uparrow ly);

          consider lz be Element of L such that lz in the carrier of L and

           A6: lx <= lz and

           A7: ly <= lz by A1;

          set z = ( uparrow lz);

          z in ( Tails L);

          then

          reconsider z as Element of ( Tails L);

          take z;

          ( uparrow lz) c= ( uparrow lx) & ( uparrow lz) c= ( uparrow ly) by A6, A7, WAYBEL_0: 22;

          hence thesis by A4, A5, XBOOLE_1: 19;

        end;

        hence thesis by A2;

      end;

      hence thesis by Th08;

    end;

    definition

      let L be non empty transitive reflexive RelStr;

      assume

       A1: ( [#] L) is directed;

      :: CARDFIL2:def15

      func Tails_Filter (L) -> Filter of ( [#] L) equals

      : DefL9: <.( Tails L).];

      coherence by A1, Th14;

    end

    theorem :: CARDFIL2:42

    

     Th15: for L be non empty transitive reflexive RelStr st ( [#] L) is directed holds ( Tails L) is basis of ( Tails_Filter L)

    proof

      let L be non empty transitive reflexive RelStr;

      assume ( [#] L) is directed;

      then ( Tails_Filter L) = <.( Tails L).] by DefL9;

      hence thesis by Th07;

    end;

    definition

      let L be RelStr;

      let x be Subset-Family of L;

      :: CARDFIL2:def16

      func # x -> Subset-Family of ( [#] L) equals x;

      coherence ;

    end

    theorem :: CARDFIL2:43

    

     Th16: for X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X st ( [#] L) is directed holds (f .: ( # ( Tails L))) is basis of ( filter_image (f,( Tails_Filter L)))

    proof

      let X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X such that

       A1: ( [#] L) is directed;

      reconsider SL = ( Tails L) as basis of ( Tails_Filter L) by A1, Th15;

      (f .: ( # SL)) is basis of ( filter_image (f,( Tails_Filter L))) by Th13bThmBA2;

      hence thesis;

    end;

    theorem :: CARDFIL2:44

    

     Th17: for X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, x be Subset of X st ( [#] L) is directed & x in (f .: ( # ( Tails L))) holds ex j be Element of L st for i be Element of L st i >= j holds (f . i) in x

    proof

      let X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, x be Subset of X;

      assume that ( [#] L) is directed and

       A2: x in (f .: ( # ( Tails L)));

      reconsider x0 = x as Subset of X;

      consider b0 be Subset of ( [#] L) such that

       A3: b0 in ( # ( Tails L)) and

       A4: x0 = (f .: b0) by A2, FUNCT_2:def 10;

      consider i be Element of L such that

       A5: b0 = ( uparrow i) by A3;

      now

        let j be Element of L;

        assume j >= i;

        then

         C1: i <= j & i in {i} by TARSKI:def 1;

        j in ( [#] L);

        then j in ( uparrow i) & j in ( dom f) by C1, WAYBEL_0:def 16, FUNCT_2:def 1;

        hence (f . j) in x by A4, A5, FUNCT_1:def 6;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:45

    

     Th18: for X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, x be Subset of X st ( [#] L) is directed & (ex j be Element of L st for i be Element of L st i >= j holds (f . i) in x) holds ex b be Element of ( Tails L) st (f .: b) c= x

    proof

      let X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, x be Subset of X;

      assume that ( [#] L) is directed and

       A1: ex j be Element of L st for i be Element of L st i >= j holds (f . i) in x;

      consider j0 be Element of L such that

       A2: for i be Element of L st i >= j0 holds (f . i) in x by A1;

      set b0 = ( uparrow {j0});

      b0 = ( uparrow j0);

      then

       A3: b0 in ( # ( Tails L));

      now

        let t be object;

        assume t in (f .: b0);

        then

        consider x0 be object such that

         A4: x0 in ( dom f) and

         A5: x0 in ( uparrow j0) and

         A6: t = (f . x0) by FUNCT_1:def 6;

        reconsider x1 = x0 as Element of L by A4;

        consider y1 be Element of L such that

         A7: y1 <= x1 and

         A8: y1 in {j0} by A5, WAYBEL_0:def 16;

        y1 = j0 by A8, TARSKI:def 1;

        hence t in x by A2, A6, A7;

      end;

      then (f .: b0) c= x;

      hence thesis by A3;

    end;

    theorem :: CARDFIL2:46

    

     Th19: for X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, F be Filter of X, B be basis of F st ( [#] L) is directed holds F is_filter-coarser_than ( filter_image (f,( Tails_Filter L))) iff B is_coarser_than (f .: ( # ( Tails L)))

    proof

      let X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, F be Filter of X, B be basis of F;

      assume ( [#] L) is directed;

      then (f .: ( # ( Tails L))) is basis of ( filter_image (f,( Tails_Filter L))) by Th16;

      hence thesis by Th11;

    end;

    theorem :: CARDFIL2:47

    

     Th20: for X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, B be filter_base of X st ( [#] L) is directed holds B is_coarser_than (f .: ( # ( Tails L))) iff for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b

    proof

      let X be non empty set, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), X, B be filter_base of X;

      assume

       A1: ( [#] L) is directed;

      hereby

        assume

         A2: B is_coarser_than (f .: ( # ( Tails L)));

        hereby

          let b be Element of B;

          consider x0 be set such that

           A3: x0 in (f .: ( # ( Tails L))) and

           A4: x0 c= b by A2;

          reconsider x1 = x0 as Subset of X by A4, XBOOLE_1: 1;

          consider j0 be Element of L such that

           A5: for i be Element of L st i >= j0 holds (f . i) in x1 by A1, A3, Th17;

          for i be Element of L st i >= j0 holds (f . i) in b by A4, A5;

          hence ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b;

        end;

      end;

      assume

       A6: for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b;

      now

        let Y be set;

        assume

         A7: Y in B;

        then

        consider i0 be Element of L such that

         A8: for j be Element of L st i0 <= j holds (f . j) in Y by A6;

        reconsider b = Y as Subset of X by A7;

        consider b0 be Element of ( Tails L) such that

         A9: (f .: b0) c= b by A1, A8, Th18;

        (f .: b0) in (f .: ( # ( Tails L))) by FUNCT_2:def 10;

        hence ex X be set st X in (f .: ( # ( Tails L))) & X c= Y by A9;

      end;

      hence B is_coarser_than (f .: ( # ( Tails L)));

    end;

    definition

      let X be non empty set, s be sequence of X;

      :: CARDFIL2:def17

      func elementary_filter (s) -> Filter of X equals ( filter_image (s,( Frechet_Filter NAT )));

      correctness ;

    end

    theorem :: CARDFIL2:48

    

     Th21: ex F be sequence of ( bool NAT ) st for x be Element of NAT holds (F . x) = { y where y be Element of NAT : x <= y }

    proof

      deffunc FF( object) = { y where y be Element of NAT : ex x0 be Element of NAT st x0 = $1 & x0 <= y };

       A1:

      now

        let x be object;

        assume x in NAT ;

        now

          let t be object;

          assume t in { y where y be Element of NAT : ex x0 be Element of NAT st x0 = x & x0 <= y };

          then

          consider y0 be Element of NAT such that

           A2: t = y0 and ex x0 be Element of NAT st x0 = x & x0 <= y0;

          thus t in NAT by A2;

        end;

        then { y where y be Element of NAT : ex x0 be Element of NAT st x0 = x & x0 <= y } c= NAT ;

        hence FF(x) in ( bool NAT );

      end;

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

      then

      consider F be Function of NAT , ( bool NAT ) such that

       A3: for x be object st x in NAT holds (F . x) = FF(x);

      for x be Element of NAT holds (F . x) = { y where y be Element of NAT : x <= y }

      proof

        let x be Element of NAT ;

        { y where y be Element of NAT : ex x0 be Element of NAT st x0 = x & x0 <= y } = { y where y be Element of NAT : x <= y }

        proof

          hereby

            let t be object;

            assume t in { y where y be Element of NAT : ex x0 be Element of NAT st x0 = x & x0 <= y };

            then

            consider y0 be Element of NAT such that

             A4: t = y0 and

             A5: ex x0 be Element of NAT st x0 = x & x0 <= y0;

            consider x1 be Element of NAT such that

             A6: x1 = x and

             A7: x1 <= y0 by A5;

            thus t in { y where y be Element of NAT : x <= y } by A4, A6, A7;

          end;

          let t be object;

          assume t in { y where y be Element of NAT : x <= y };

          then

          consider y0 be Element of NAT such that

           A8: t = y0 and

           A9: x <= y0;

          thus t in { y where y be Element of NAT : ex x0 be Element of NAT st x0 = x & x0 <= y } by A8, A9;

        end;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:49

    

     Th22: for n be natural number holds ( NAT \ { t where t be Element of NAT : n <= t }) is finite

    proof

      let n be natural number;

      ( NAT \ { t where t be Element of NAT : n <= t }) c= (n + 1)

      proof

        ( NAT \ { t where t be Element of NAT : n <= t }) c= (( Seg n) \/ { 0 })

        proof

          set S = ( NAT \ { t where t be Element of NAT : n <= t });

          per cases ;

            suppose

             A1: n = 0 ;

            S is empty

            proof

              let x be object such that

               A2: x in S;

              x in NAT & not x in { t where t be Element of NAT : 0 <= t } by A1, A2, XBOOLE_0:def 5;

              hence thesis;

            end;

            hence thesis;

          end;

            suppose n > 0 ;

            let x be object such that

             A3: x in S;

            

             A4: x in NAT & not x in { t where t be Element of NAT : n <= t } by A3, XBOOLE_0:def 5;

            reconsider x as Element of NAT by A3;

            

             A5: x = 0 or x in ( Seg x) by FINSEQ_1: 3;

            x <= n by A4;

            then ( Seg x) c= ( Seg n) by FINSEQ_1: 5;

            then x in { 0 } or x in ( Seg n) by A5, TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        hence thesis by AFINSQ_1: 4;

      end;

      hence thesis;

    end;

    

     Lm3: for p be Element of OrderedNAT , p0 be Element of NAT st p = p0 holds { x where x be Element of NAT : p0 <= x } = { x where x be Element of OrderedNAT : p <= x }

    proof

      let p be Element of OrderedNAT , p0 be Element of NAT ;

      assume

       A1: p = p0;

      hereby

        let t be object;

        assume t in { x where x be Element of NAT : p0 <= x };

        then

        consider x0 be Element of NAT such that

         A2: t = x0 and

         A3: p0 <= x0;

        reconsider x1 = x0 as Element of OrderedNAT ;

        p <= x1 by A3, A1;

        hence t in { x where x be Element of OrderedNAT : p <= x } by A2;

      end;

      let t be object;

      assume t in { x where x be Element of OrderedNAT : p <= x };

      then

      consider x0 be Element of OrderedNAT such that

       A4: t = x0 and

       A5: p <= x0;

      consider a,b be Element of NAT such that

       A6: [p0, x0] = [a, b] and

       A7: a <= b by A1, A5;

      p0 = a & x0 = b by A6, XTUPLE_0: 1;

      hence t in { x where x be Element of NAT : p0 <= x } by A4, A7;

    end;

    

     Lm4: for p be Element of OrderedNAT holds { x where x be Element of NAT : ex p0 be Element of NAT st p = p0 & p0 <= x } = { x where x be Element of OrderedNAT : p <= x }

    proof

      let p be Element of OrderedNAT ;

      hereby

        let t be object;

        assume t in { x where x be Element of NAT : ex p0 be Element of NAT st p = p0 & p0 <= x };

        then

        consider x0 be Element of NAT such that

         A1: t = x0 and

         A2: ex p0 be Element of NAT st p = p0 & p0 <= x0;

        consider p0 be Element of NAT such that

         A3: p = p0 and

         A4: p0 <= x0 by A2;

        reconsider x1 = x0 as Element of OrderedNAT ;

        p <= x1 by A4, A3;

        hence t in { x where x be Element of OrderedNAT : p <= x } by A1;

      end;

      let t be object;

      assume t in { x where x be Element of OrderedNAT : p <= x };

      then

      consider x0 be Element of OrderedNAT such that

       A5: t = x0 and

       A6: p <= x0;

      reconsider p0 = p as Element of NAT ;

      consider a,b be Element of NAT such that

       A7: [p0, x0] = [a, b] and

       A8: a <= b by A6;

      p0 = a & x0 = b by A7, XTUPLE_0: 1;

      hence t in { x where x be Element of NAT : ex p0 be Element of NAT st p = p0 & p0 <= x } by A5, A8;

    end;

    theorem :: CARDFIL2:50

    

     Th23: for p be Element of OrderedNAT holds { x where x be Element of NAT : ex p0 be Element of NAT st p = p0 & p0 <= x } = ( uparrow p)

    proof

      let p be Element of OrderedNAT ;

      reconsider p0 = p as Element of NAT ;

      

       A1: for p be Element of the carrier of OrderedNAT holds { x where x be Element of the carrier of OrderedNAT : p <= x } = ( uparrow p)

      proof

        let p be Element of OrderedNAT ;

        hereby

          let t be object;

          assume t in { x where x be Element of OrderedNAT : p <= x };

          then

          consider x0 be Element of OrderedNAT such that

           A2: t = x0 and

           A3: p <= x0;

          thus t in ( uparrow p) by A2, A3, WAYBEL_0: 18;

        end;

        let t be object;

        assume

         A4: t in ( uparrow p);

        then

        reconsider t0 = t as Element of OrderedNAT ;

        p <= t0 by A4, WAYBEL_0: 18;

        hence t in { x where x be Element of OrderedNAT : p <= x };

      end;

      { x where x be Element of NAT : ex p0 be Element of NAT st p = p0 & p0 <= x } = { x where x be Element of OrderedNAT : p <= x } by Lm4;

      hence thesis by A1;

    end;

    registration

      cluster ( [#] OrderedNAT ) -> directed;

      coherence ;

      cluster OrderedNAT -> reflexive;

      coherence by DICKSON:def 3;

    end

    theorem :: CARDFIL2:51

    

     Th24: for X be denumerable set holds ( Frechet_Filter X) = the set of all (X \ A) where A be finite Subset of X

    proof

      let X be denumerable set;

      

       A1: ( card X) = omega by CARD_3:def 15;

      hereby

        let x be object such that

         A2: x in ( Frechet_Filter X);

        reconsider x0 = x as Subset of X by A2;

        ( card (X \ x0)) in ( card X) by A2, CARD_FIL: 18;

        then

         A3: (X \ x0) is finite Subset of X by A1;

        (X \ (X \ x0)) = (X /\ x0) & (X /\ x0) c= X by XBOOLE_1: 48;

        then (X \ (X \ x0)) = x0 by XBOOLE_1: 28;

        hence x in the set of all (X \ A) where A be finite Subset of X by A3;

      end;

      let x be object such that

       A4: x in the set of all (X \ A) where A be finite Subset of X;

      consider a0 be finite Subset of X such that

       A5: x = (X \ a0) by A4;

      reconsider x0 = x as Subset of X by A5;

      (X \ (X \ a0)) = (X /\ a0) & (X /\ a0) c= X by XBOOLE_1: 48;

      then ( card (X \ x0)) = ( card a0) by A5, XBOOLE_1: 28;

      hence thesis by A1;

    end;

    theorem :: CARDFIL2:52

    

     Th25: for F be sequence of ( bool NAT ) st for x be Element of NAT holds (F . x) = { y where y be Element of NAT : x <= y } holds ( rng F) is basis of ( Frechet_Filter NAT )

    proof

      let F be sequence of ( bool NAT );

      assume

       A1: for x be Element of NAT holds (F . x) = { y where y be Element of NAT : x <= y };

      

       A2: ( Frechet_Filter NAT ) = the set of all ( NAT \ A) where A be finite Subset of NAT by Th24;

      for t be object st t in ( rng F) holds t in ( Frechet_Filter NAT )

      proof

        let t be object;

        assume

         A3: t in ( rng F);

        then

        consider x0 be object such that

         A4: x0 in ( dom F) & t = (F . x0) by FUNCT_1:def 3;

        reconsider x2 = x0 as natural number by A4;

        reconsider t1 = t as Subset of NAT by A3;

         A5:

        now

          ( NAT \ t1) = ( NAT \ { y where y be Element of NAT : x2 <= y }) by A1, A4;

          hence ( NAT \ t1) is finite by Th22;

          thus ( NAT \ t1) is Subset of NAT ;

        end;

        ( NAT \ ( NAT \ t1)) = (t1 /\ NAT ) by XBOOLE_1: 48;

        then t1 = ( NAT \ ( NAT \ t1)) by XBOOLE_1: 17, XBOOLE_1: 19;

        hence thesis by A2, A5;

      end;

      then ( rng F) c= ( Frechet_Filter NAT );

      then

      reconsider F1 = ( rng F) as non empty Subset of ( Frechet_Filter NAT );

      

       A7: F1 is filter_basis

      proof

        for f be Element of ( Frechet_Filter NAT ) holds ex b be Element of F1 st b c= f

        proof

          let f be Element of ( Frechet_Filter NAT );

          f in the set of all ( NAT \ A) where A be finite Subset of NAT by A2;

          then

          consider A0 be finite Subset of NAT such that

           A8: f = ( NAT \ A0);

          reconsider A1 = A0 as natural-membered set;

          consider n0 be natural number such that

           A9: A1 c= ( Segm n0) by AFINSQ_2: 2;

          reconsider n1 = n0 as Element of NAT by ORDINAL1:def 12;

          

           A10: ( dom F) = NAT by FUNCT_2:def 1;

          set b = ( NAT \ ( Segm n0));

          b is Element of ( rng F)

          proof

            b = { y where y be Element of NAT : n0 <= y }

            proof

              hereby

                let x be object;

                assume

                 A11: x in b;

                then

                reconsider x1 = x as Element of NAT ;

                for n0 be natural number, t be Element of ( NAT \ ( Segm n0)) holds n0 <= t

                proof

                  let n0 be natural number, t be Element of ( NAT \ ( Segm n0));

                  ( Segm n0) c< NAT ;

                  then ( NAT \ ( Segm n0)) is non empty by XBOOLE_1: 105;

                  then not t in ( Segm n0) by XBOOLE_0:def 5;

                  hence thesis by NAT_1: 44;

                end;

                then n0 <= x1 by A11;

                hence x in { y where y be Element of NAT : n0 <= y };

              end;

              let x be object;

              assume x in { y where y be Element of NAT : n0 <= y };

              then

              consider y0 be Element of NAT such that

               A12: x = y0 and

               A13: n0 <= y0;

              reconsider x1 = x as Element of NAT by A12;

              x1 in NAT & not x1 in ( Segm n0) by A12, A13, NAT_1: 44;

              hence x in b by XBOOLE_0:def 5;

            end;

            then b = (F . n1) by A1;

            hence thesis by A10, FUNCT_1: 3;

          end;

          hence thesis by A8, A9, XBOOLE_1: 34;

        end;

        hence thesis;

      end;

      thus thesis by A7;

    end;

    theorem :: CARDFIL2:53

    

     Th26: for F be sequence of ( bool NAT ) st for x be Element of NAT holds (F . x) = { y where y be Element of NAT : x <= y } holds ( # ( Tails OrderedNAT )) = ( rng F)

    proof

      let F be sequence of ( bool NAT ) such that

       A1: for x be Element of NAT holds (F . x) = { y where y be Element of NAT : x <= y };

      set F1 = ( rng F);

      set F2 = the set of all ( uparrow p) where p be Element of OrderedNAT ;

      now

        hereby

          let t be object;

          assume t in F1;

          then

          consider x0 be object such that

           A2: x0 in ( dom F) & t = (F . x0) by FUNCT_1:def 3;

          reconsider x1 = x0 as Element of NAT by A2;

          reconsider x2 = x0 as Element of OrderedNAT by A2;

          t = { y where y be Element of NAT : x1 <= y } by A1, A2;

          then t = { x where x be Element of OrderedNAT : x2 <= x } by Lm3;

          then t = { x where x be Element of NAT : ex p0 be Element of NAT st x2 = p0 & p0 <= x } by Lm4;

          then t = ( uparrow x2) by Th23;

          hence t in F2;

        end;

        let t be object;

        assume t in F2;

        then

        consider p0 be Element of OrderedNAT such that

         A3: t = ( uparrow p0);

        t = { x where x be Element of NAT : ex p1 be Element of NAT st p0 = p1 & p1 <= x } by A3, Th23;

        then

         A4: t = { y where y be Element of OrderedNAT : p0 <= y } by Lm4;

        reconsider p2 = p0 as Element of NAT ;

        t = { x where x be Element of NAT : p2 <= x } by A4, Lm3;

        then

         A5: t = (F . p2) by A1;

        ( dom F) = NAT by FUNCT_2:def 1;

        hence t in F1 by A5, FUNCT_1: 3;

      end;

      then F1 c= F2 & F2 c= F1;

      hence thesis;

    end;

    theorem :: CARDFIL2:54

    

     Th27: ( # ( Tails OrderedNAT )) is basis of ( Frechet_Filter NAT ) & ( Tails_Filter OrderedNAT ) = ( Frechet_Filter NAT )

    proof

      consider F be sequence of ( bool NAT ) such that

       A1: for x be Element of NAT holds (F . x) = { y where y be Element of NAT : x <= y } by Th21;

      set F1 = ( rng F);

      set F2 = the set of all ( uparrow p) where p be Element of OrderedNAT ;

      

       A2: F1 = F2 by A1, Th26;

      hence ( # ( Tails OrderedNAT )) is basis of ( Frechet_Filter NAT ) by A1, Th25;

      reconsider BFF = ( # ( Tails OrderedNAT )) as basis of ( Frechet_Filter NAT ) by A1, A2, Th25;

       <.( # BFF).] = ( Frechet_Filter NAT ) by Th06;

      hence thesis by DefL9;

    end;

    definition

      :: CARDFIL2:def18

      func base_of_frechet_filter -> filter_base of NAT equals ( # ( Tails OrderedNAT ));

      coherence by Th27, Th09;

    end

    theorem :: CARDFIL2:55

     NAT in base_of_frechet_filter

    proof

      reconsider n0 = 0 as Element of OrderedNAT ;

      

       A1: ( uparrow n0) = ( uparrow {n0});

      ( uparrow {n0}) = NAT

      proof

         NAT c= ( uparrow {n0})

        proof

          let t be object;

          assume t in NAT ;

          then

          reconsider t0 = t as Element of OrderedNAT ;

          n0 <= t0 & n0 in {n0} by TARSKI:def 1;

          hence thesis by WAYBEL_0:def 16;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: CARDFIL2:56

     base_of_frechet_filter is basis of ( Frechet_Filter NAT ) by Th27;

    theorem :: CARDFIL2:57

    for X be non empty set, F1,F2 be Filter of X, F be Filter of X st F is_filter-finer_than F1 & F is_filter-finer_than F2 holds for M1 be Element of F1, M2 be Element of F2 holds (M1 /\ M2) is non empty

    proof

      let X be non empty set, F1,F2 be Filter of X, F be Filter of X such that

       A1: F is_filter-finer_than F1 and

       A2: F is_filter-finer_than F2;

      hereby

        let M1 be Element of F1, M2 be Element of F2;

        M1 in F1 & M2 in F2;

        then (M1 /\ M2) in F by A1, A2, CARD_FIL:def 1;

        hence (M1 /\ M2) is non empty by CARD_FIL:def 1;

      end;

    end;

    theorem :: CARDFIL2:58

    for X be non empty set, F1,F2 be Filter of X st for M1 be Element of F1, M2 be Element of F2 holds (M1 /\ M2) is non empty holds ex F be Filter of X st F is_filter-finer_than F1 & F is_filter-finer_than F2

    proof

      let X be non empty set, F1,F2 be Filter of X;

      assume

       A1: for M1 be Element of F1, M2 be Element of F2 holds (M1 /\ M2) is non empty;

      set F = the set of all (M1 /\ M2) where M1 be Element of F1, M2 be Element of F2;

      take F;

      F is non empty Subset-Family of X

      proof

        set M1 = the Element of F1;

        set M2 = the Element of F2;

        

         A2: (M1 /\ M2) in F;

        F c= ( bool X)

        proof

          let x be object;

          assume x in F;

          then

          consider M1 be Element of F1, M2 be Element of F2 such that

           A3: x = (M1 /\ M2);

          thus x in ( bool X) by A3;

        end;

        hence thesis by A2;

      end;

      then

      reconsider F as non empty Subset-Family of X;

      now

        hereby

          assume {} in F;

          then

          consider M1 be Element of F1, M2 be Element of F2 such that

           A4: {} = (M1 /\ M2);

          thus not {} in F by A4, A1;

        end;

        hereby

          let Y1,Y2 be Subset of X;

          hereby

            assume that

             A5: Y1 in F and

             A6: Y2 in F;

            consider M1 be Element of F1, M2 be Element of F2 such that

             A7: Y1 = (M1 /\ M2) by A5;

            consider M3 be Element of F1, M4 be Element of F2 such that

             A8: Y2 = (M3 /\ M4) by A6;

            (Y1 /\ Y2) = (M1 /\ (M2 /\ (M3 /\ M4))) by A7, A8, XBOOLE_1: 16;

            then (Y1 /\ Y2) = (M1 /\ (M3 /\ (M4 /\ M2))) by XBOOLE_1: 16;

            then

             A9: (Y1 /\ Y2) = ((M1 /\ M3) /\ (M2 /\ M4)) by XBOOLE_1: 16;

            (M1 /\ M3) is Element of F1 & (M2 /\ M4) is Element of F2 by CARD_FIL:def 1;

            hence (Y1 /\ Y2) in F by A9;

          end;

          assume that

           A10: Y1 in F and

           A11: Y1 c= Y2;

          consider M1 be Element of F1, M2 be Element of F2 such that

           A12: Y1 = (M1 /\ M2) by A10;

          (Y2 \/ (M1 /\ M2)) = Y2 by A11, A12, XBOOLE_1: 12;

          then

           A13: Y2 = ((M1 \/ Y2) /\ (M2 \/ Y2)) by XBOOLE_1: 24;

          M1 c= (M1 \/ Y2) & M2 c= (M2 \/ Y2) by XBOOLE_1: 7;

          then (M1 \/ Y2) is Element of F1 & (M2 \/ Y2) is Element of F2 by CARD_FIL:def 1;

          hence Y2 in F by A13;

        end;

      end;

      then

      reconsider F0 = F as Filter of X by CARD_FIL:def 1;

      

       A14: X in F1 & X in F2 by CARD_FIL: 5;

      F1 c= F0

      proof

        let x be object;

        assume

         A15: x in F1;

        then

        reconsider x as Subset of X;

        x = (x /\ X) by XBOOLE_1: 17, XBOOLE_1: 19;

        hence thesis by A14, A15;

      end;

      then

       A16: F0 is_filter-finer_than F1;

      F2 c= F0

      proof

        let x be object;

        assume

         A17: x in F2;

        then

        reconsider x as Subset of X;

        x = (x /\ X) by XBOOLE_1: 17, XBOOLE_1: 19;

        hence thesis by A14, A17;

      end;

      then F0 is_filter-finer_than F2;

      hence thesis by A16;

    end;

    definition

      let X be set;

      let x be Subset of X;

      :: CARDFIL2:def19

      func PLO2bis (x) -> Element of ( BoolePoset X) equals x;

      coherence by LATTICE3:def 1;

    end

    theorem :: CARDFIL2:59

    

     Th28: for X be infinite set holds X in the set of all (X \ A) where A be finite Subset of X

    proof

      let X be infinite set;

      set Z = {} ;

      Z is finite Subset of X

      proof

         {} c= X;

        hence thesis;

      end;

      then

      reconsider Z as finite Subset of X;

      (X \ Z) in { (X \ A) where A be finite Subset of X : not contradiction };

      hence thesis;

    end;

    theorem :: CARDFIL2:60

    

     Th29: for X be set, A be Subset of X holds { B where B be Element of ( BoolePoset X) : A c= B } = { B where B be Subset of X : A c= B }

    proof

      let X be set, A be Subset of X;

      set C = { B where B be Element of ( BoolePoset X) : A c= B };

      set D = { B where B be Subset of X : A c= B };

      now

        hereby

          let x be object;

          assume x in C;

          then

          consider b0 be Element of ( BoolePoset X) such that

           A1: x = b0 and

           A2: A c= b0;

          x is Subset of X by A1, WAYBEL_8: 26;

          hence x in D by A1, A2;

        end;

        let x be object;

        assume x in D;

        then

        consider b0 be Subset of X such that

         A3: x = b0 and

         A4: A c= b0;

        x is Element of ( BoolePoset X) by A3, WAYBEL_8: 26;

        hence x in C by A3, A4;

      end;

      then C c= D & D c= C;

      hence thesis;

    end;

    theorem :: CARDFIL2:61

    for X be set, a be Element of ( BoolePoset X) holds ( uparrow a) = { Y where Y be Subset of X : a c= Y } by WAYBEL15: 2;

    theorem :: CARDFIL2:62

    for X be set, A be Subset of X holds { B where B be Element of ( BoolePoset X) : A c= B } = ( uparrow ( PLO2bis A))

    proof

      let X be set, A be Subset of X;

      reconsider Z = ( PLO2bis A) as Element of ( BoolePoset X);

      set S1 = { Y where Y be Subset of X : Z c= Y };

      set S2 = { B where B be Subset of X : A c= B };

      { B where B be Element of ( BoolePoset X) : A c= B } = { B where B be Subset of X : A c= B } by Th29;

      hence thesis by WAYBEL15: 2;

    end;

    theorem :: CARDFIL2:63

    for X be non empty set, F be Filter of X holds ( union F) = X by CARD_FIL: 5, ZFMISC_1: 74;

    theorem :: CARDFIL2:64

    for X be infinite set holds the set of all (X \ A) where A be finite Subset of X is Filter of X

    proof

      let X be infinite set;

      set FF = the set of all (X \ A) where A be finite Subset of X;

      now

        let x be object;

        assume x in FF;

        then

        consider a1 be finite Subset of X such that

         A1: x = (X \ a1);

        thus x in ( bool X) by A1;

      end;

      then FF c= ( bool X);

      then

      reconsider FF as non empty Subset-Family of X by Th28;

      

       A2: not {} in FF

      proof

        assume {} in FF;

        then

        consider a be finite Subset of X such that

         A3: {} = (X \ a);

        X c= a by A3, XBOOLE_1: 37;

        hence contradiction;

      end;

      

       A4: for Y1,Y2 be Subset of X st Y1 in FF & Y2 in FF holds (Y1 /\ Y2) in FF

      proof

        let Y1,Y2 be Subset of X such that

         A5: Y1 in FF and

         A6: Y2 in FF;

        consider a1 be finite Subset of X such that

         A7: Y1 = (X \ a1) by A5;

        consider a2 be finite Subset of X such that

         A8: Y2 = (X \ a2) by A6;

        (Y1 /\ Y2) = (X \ (a1 \/ a2)) by A7, A8, XBOOLE_1: 53;

        hence thesis;

      end;

      for Y1,Y2 be Subset of X st Y1 in FF & Y1 c= Y2 holds Y2 in FF

      proof

        let Y1,Y2 be Subset of X such that

         A9: Y1 in FF and

         A10: Y1 c= Y2;

        consider a1 be finite Subset of X such that

         A11: Y1 = (X \ a1) by A9;

        (X \ Y2) c= (X \ (X \ a1)) by A10, A11, XBOOLE_1: 34;

        then

         A12: (X \ Y2) c= (X /\ a1) by XBOOLE_1: 48;

        (X \ (X \ Y2)) = (X /\ Y2) & (X /\ Y2) c= Y2 by XBOOLE_1: 17, XBOOLE_1: 48;

        then (X \ (X \ Y2)) = Y2 by XBOOLE_1: 28;

        hence thesis by A12;

      end;

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

    end;

    theorem :: CARDFIL2:65

    for X be set holds ( bool X) is Filter of ( BoolePoset X) by WAYBEL16: 11;

    theorem :: CARDFIL2:66

    for X be set holds {X} is Filter of ( BoolePoset X) by WAYBEL16: 12;

    theorem :: CARDFIL2:67

    for X be non empty set holds {X} is Filter of X by CARD_FIL: 4;

    theorem :: CARDFIL2:68

    

     Th30Thm70: for A be Element of ( BoolePoset X) holds { Y where Y be Subset of X : A c= Y } is Filter of ( BoolePoset X)

    proof

      let A be Element of ( BoolePoset X);

      { Y where Y be Subset of X : A c= Y } = ( uparrow A) by WAYBEL15: 2;

      hence thesis;

    end;

    theorem :: CARDFIL2:69

    for A be Element of ( BoolePoset X) holds { B where B be Element of ( BoolePoset X) : A c= B } is Filter of ( BoolePoset X)

    proof

      let A be Element of ( BoolePoset X);

      reconsider A as Subset of X by WAYBEL_8: 26;

      { B where B be Element of ( BoolePoset X) : A c= B } = { B where B be Subset of X : A c= B } by Th29;

      hence thesis by Th30Thm70;

    end;

    theorem :: CARDFIL2:70

    for X be non empty set, B be non empty Subset of ( BoolePoset X) holds (for x,y be Element of B holds ex z be Element of B st z c= (x /\ y)) iff B is filtered

    proof

      let X be non empty set, B be non empty Subset of ( BoolePoset X);

      hereby

        assume

         A1: (for x,y be Element of B holds ex z be Element of B st z c= (x /\ y));

        for x,y be Element of ( BoolePoset X) st x in B & y in B holds ex z be Element of ( BoolePoset X) st z in B & z <= x & z <= y

        proof

          let x,y be Element of ( BoolePoset X) such that

           A2: x in B & y in B;

          reconsider x, y as Element of B by A2;

          consider z0 be Element of B such that

           A3: z0 c= (x /\ y) by A1;

          reconsider z0 as Element of ( BoolePoset X);

          take z0;

          (x /\ y) c= x & (x /\ y) c= y by XBOOLE_1: 17;

          then z0 c= x & z0 c= y by A3;

          hence thesis by YELLOW_1: 2;

        end;

        hence B is filtered;

      end;

      assume

       A4: B is filtered;

      for x,y be Element of B holds ex z be Element of B st z c= (x /\ y)

      proof

        let x,y be Element of B;

        consider z0 be Element of ( BoolePoset X) such that

         A5: z0 in B and

         A6: z0 <= x and

         A7: z0 <= y by A4;

        

         A8: z0 c= x & z0 c= y by A6, A7, YELLOW_1: 2;

        reconsider z0 as Element of B by A5;

        take z0;

        thus thesis by A8, XBOOLE_1: 19;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:71

    

     Th31: for X be non empty set, F be non empty Subset of ( BooleLatt X) holds F is Filter of ( BooleLatt X) iff (for p,q be Element of F holds (p /\ q) in F) & (for p be Element of F, q be Element of ( BooleLatt X) st p c= q holds q in F)

    proof

      let X be non empty set, F be non empty Subset of ( BooleLatt X);

      hereby

        assume

         A1: F is Filter of ( BooleLatt X);

        then

         A2: for p,q be Element of ( BooleLatt X) st p in F & p [= q holds q in F by FILTER_0: 9;

        now

          let p,q be Element of ( BooleLatt X);

          now

            assume p in F & q in F;

            then (p "/\" q) in F by A1, FILTER_0: 9;

            hence (p /\ q) in F;

          end;

          hence (p in F & q in F implies (p /\ q) in F) & (p in F & p c= q implies q in F) by A2, LATTICE3: 2;

        end;

        hence (for p,q be Element of F holds (p /\ q) in F) & (for p be Element of F, q be Element of ( BooleLatt X) st p c= q holds q in F);

      end;

      assume that

       A3: for p,q be Element of F holds (p /\ q) in F and

       A4: for p be Element of F, q be Element of ( BooleLatt X) st p c= q holds q in F;

      

       A5: (for p,q be Element of ( BooleLatt X) st p in F & q in F holds (p "/\" q) in F) by A3;

      for p,q be Element of ( BooleLatt X) st p in F & p [= q holds q in F by A4, LATTICE3: 2;

      hence F is Filter of ( BooleLatt X) by A5, FILTER_0: 9;

    end;

    theorem :: CARDFIL2:72

    

     Th32: for X be non empty set, F be non empty Subset of ( BooleLatt X) holds F is Filter of ( BooleLatt X) iff for Y1,Y2 be Subset of X holds (Y1 in F & Y2 in F implies (Y1 /\ Y2) in F) & (Y1 in F & Y1 c= Y2 implies Y2 in F)

    proof

      let X be non empty set, F be non empty Subset of ( BooleLatt X);

      hereby

        assume

         A1: F is Filter of ( BooleLatt X);

        hereby

          let Y1,Y2 be Subset of X;

          Y1 is Element of the carrier of ( BooleLatt X) & Y2 is Element of the carrier of ( BooleLatt X) by LATTICE3:def 1;

          hence (Y1 in F & Y2 in F implies (Y1 /\ Y2) in F) & (Y1 in F & Y1 c= Y2 implies Y2 in F) by A1, Th31;

        end;

      end;

      assume that

       A2: for Y1,Y2 be Subset of X holds (Y1 in F & Y2 in F implies (Y1 /\ Y2) in F) & (Y1 in F & Y1 c= Y2 implies Y2 in F);

      now

        hereby

          let p,q be Element of F;

          reconsider p1 = p, q1 = q as Subset of X by LATTICE3:def 1;

          p1 in F & q1 in F implies (p1 /\ q1) in F by A2;

          hence (p /\ q) in F;

        end;

        let p be Element of F, q be Element of ( BooleLatt X) such that

         A3: p c= q;

        reconsider p1 = p, q1 = q as Subset of X by LATTICE3:def 1;

        p1 in F & p1 c= q & (p1 in F & p1 c= q1 implies q1 in F) by A2, A3;

        hence q in F;

      end;

      hence F is Filter of ( BooleLatt X) by Th31;

    end;

    theorem :: CARDFIL2:73

    

     Th33: for X be non empty set, FF be non empty Subset-Family of X st FF is Filter of ( BooleLatt X) holds FF is Filter of ( BoolePoset X)

    proof

      let X be non empty set, FF be non empty Subset-Family of X such that

       A1: FF is Filter of ( BooleLatt X);

      now

        set Z = ( LattPOSet ( BooleLatt X));

        reconsider FF as Subset of Z by A1;

        

         A2: FF is filtered

        proof

          for x,y be Element of Z st x in FF & y in FF holds ex z be Element of Z st z in FF & z <= x & z <= y

          proof

            let x,y be Element of Z such that

             A3: x in FF & y in FF;

            reconsider x1 = x, y1 = y as Element of ( BooleLatt X);

            set z = (x1 "/\" y1);

             A4:

            now

              (x1 /\ y1) c= x1 & (x1 /\ y1) c= y1 by XBOOLE_1: 17;

              hence (z % ) <= (x1 % ) & (z % ) <= (y1 % ) by LATTICE3: 2, LATTICE3: 7;

            end;

            (x /\ y) in FF by A1, A3, Th31;

            hence thesis by A4;

          end;

          hence thesis;

        end;

        FF is upper

        proof

          for x,y be Element of Z st x in FF & x <= y holds y in FF

          proof

            let x,y be Element of Z such that

             A5: x in FF & x <= y;

            reconsider x, y as Element of ( BooleLatt X);

            

             A6: (x % ) <= (y % ) by A5;

            x in FF & x c= y by A5, A6, LATTICE3: 2, LATTICE3: 7;

            hence thesis by A1, Th31;

          end;

          hence thesis;

        end;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:74

    

     Th34: for X be non empty set, F be Filter of ( BoolePoset X) holds F is Filter of ( BooleLatt X)

    proof

      let X be non empty set, F be Filter of ( BoolePoset X);

      now

        let Y1,Y2 be Subset of X;

        hereby

          assume that

           A1: Y1 in F and

           A2: Y2 in F;

          reconsider Z1 = Y1, Z2 = Y2 as Element of ( BoolePoset X) by LATTICE3:def 1;

          

           A3: (Z1 "/\" Z2) in F by A1, A2, WAYBEL_0: 41;

          set W = (Z1 "/\" Z2);

          reconsider Z1, Z2 as Element of ( BooleLatt X);

          thus (Y1 /\ Y2) in F by A3, YELLOW_1: 17;

        end;

        hereby

          assume that

           A4: Y1 in F and

           A5: Y1 c= Y2;

          reconsider Z1 = Y1, Z2 = Y2 as Element of ( BoolePoset X) by LATTICE3:def 1;

          Z1 <= Z2 by YELLOW_1: 2, A5;

          hence Y2 in F by A4, WAYBEL_0:def 20;

        end;

      end;

      hence thesis by Th32;

    end;

    theorem :: CARDFIL2:75

    

     Th35: for X be non empty set, F be non empty Subset of ( BooleLatt X) holds F is with_non-empty_elements & F is Filter of ( BooleLatt X) iff F is Filter of X

    proof

      let X be non empty set, F be non empty Subset of ( BooleLatt X);

      hereby

        assume that

         A1: F is with_non-empty_elements and

         A2: F is Filter of ( BooleLatt X);

        

         A3: F is non empty Subset-Family of X by LATTICE3:def 1;

        for Y1,Y2 be Subset of X holds (Y1 in F & Y2 in F implies (Y1 /\ Y2) in F) & (Y1 in F & Y1 c= Y2 implies Y2 in F) by A2, Th32;

        hence F is Filter of X by A1, A3, CARD_FIL:def 1;

      end;

      assume F is Filter of X;

      then F is with_non-empty_elements & for Y1,Y2 be Subset of X holds (Y1 in F & Y2 in F implies (Y1 /\ Y2) in F) & (Y1 in F & Y1 c= Y2 implies Y2 in F) by CARD_FIL:def 1;

      hence F is with_non-empty_elements & F is Filter of ( BooleLatt X) by Th32;

    end;

    theorem :: CARDFIL2:76

    

     Th36: for X be non empty set, F be proper Filter of ( BoolePoset X) holds F is Filter of X

    proof

      let X be non empty set, F be proper Filter of ( BoolePoset X);

      

       A1: F is with_non-empty_elements

      proof

        assume not F is with_non-empty_elements;

        then ( Bottom ( BoolePoset X)) in F by YELLOW_1: 18;

        hence contradiction by WAYBEL_7: 4;

      end;

      reconsider F as non empty Subset of ( BooleLatt X);

      thus thesis by A1, Th34, Th35;

    end;

    theorem :: CARDFIL2:77

    for T be non empty TopSpace, x be Point of T holds ( NeighborhoodSystem x) is Filter of the carrier of T by Th36;

    definition

      let T be non empty TopSpace, F be proper Filter of ( BoolePoset ( [#] T));

      :: CARDFIL2:def20

      func BOOL2F F -> Filter of the carrier of T equals F;

      coherence by Th36;

    end

    definition

      let T be non empty TopSpace, F1 be Filter of the carrier of T, F2 be proper Filter of ( BoolePoset ( [#] T));

      :: CARDFIL2:def21

      pred F1 is_filter-finer_than F2 means ( BOOL2F F2) c= F1;

    end

    begin

    definition

      let T be non empty TopSpace, F be Filter of the carrier of T;

      :: CARDFIL2:def22

      func lim_filter F -> Subset of T equals { x where x be Point of T : F is_filter-finer_than ( NeighborhoodSystem x) };

      correctness

      proof

        set Z = { x where x be Point of T : F is_filter-finer_than ( NeighborhoodSystem x) };

        now

          let x be object;

          assume x in Z;

          then

          consider x0 be Point of T such that

           A1: x = x0 and F is_filter-finer_than ( NeighborhoodSystem x0);

          thus x in the carrier of T by A1;

        end;

        then Z c= the carrier of T;

        hence thesis;

      end;

    end

    definition

      let T be non empty TopSpace, B be filter_base of the carrier of T;

      :: CARDFIL2:def23

      func Lim B -> Subset of T equals ( lim_filter <.B.));

      correctness ;

    end

    theorem :: CARDFIL2:78

    

     Th37: for T be non empty TopSpace, F be Filter of the carrier of T holds ex F1 be proper Filter of ( BoolePoset the carrier of T) st F = F1

    proof

      let T be non empty TopSpace, F be Filter of the carrier of T;

      reconsider F1 = F as non empty Subset of ( BooleLatt the carrier of T) by LATTICE3:def 1;

      

       A1: F1 is Filter of ( BoolePoset the carrier of T) by Th33, Th35;

       not {} in F by CARD_FIL:def 1;

      then not ( Bottom ( BoolePoset the carrier of T)) in F1 by YELLOW_1: 18;

      then F1 is proper;

      hence thesis by A1;

    end;

    definition

      let T be non empty TopSpace, F be Filter of the carrier of T;

      :: CARDFIL2:def24

      func F2BOOL (F,T) -> proper Filter of ( BoolePoset ( [#] T)) equals F;

      coherence

      proof

        consider F2 be proper Filter of ( BoolePoset the carrier of T) such that

         A1: F = F2 by Th37;

        thus thesis by A1;

      end;

    end

    theorem :: CARDFIL2:79

    for T be non empty TopSpace, x be Point of T, F be Filter of the carrier of T holds x is_a_convergence_point_of (F,T) iff x is_a_convergence_point_of (( F2BOOL (F,T)),T);

    theorem :: CARDFIL2:80

    for T be non empty TopSpace, x be Point of T, F be Filter of the carrier of T holds x is_a_convergence_point_of (F,T) iff x in ( lim_filter F)

    proof

      let T be non empty TopSpace, x be Point of T, F be Filter of the carrier of T;

      consider F2 be proper Filter of ( BoolePoset the carrier of T) such that

       A1: F = F2 by Th37;

      F is_filter-finer_than ( NeighborhoodSystem x) iff x in { x where x be Point of T : F is_filter-finer_than ( NeighborhoodSystem x) }

      proof

        thus F is_filter-finer_than ( NeighborhoodSystem x) implies x in { x where x be Point of T : F is_filter-finer_than ( NeighborhoodSystem x) };

        assume x in { x where x be Point of T : F is_filter-finer_than ( NeighborhoodSystem x) };

        then

        consider x0 be Point of T such that

         A2: x = x0 and

         A3: F is_filter-finer_than ( NeighborhoodSystem x0);

        thus F is_filter-finer_than ( NeighborhoodSystem x) by A2, A3;

      end;

      hence thesis by A1, YELLOW19: 3;

    end;

    definition

      let T be non empty TopSpace, F be Filter of ( BoolePoset ( [#] T));

      :: CARDFIL2:def25

      func lim_filterb F -> Subset of T equals { x where x be Point of T : ( NeighborhoodSystem x) c= F };

      correctness

      proof

        set Z = { x where x be Point of T : ( NeighborhoodSystem x) c= F };

        now

          let x be object;

          assume x in Z;

          then

          consider x0 be Point of T such that

           A1: x = x0 and ( NeighborhoodSystem x0) c= F;

          thus x in the carrier of T by A1;

        end;

        then Z c= the carrier of T;

        hence thesis;

      end;

    end

    theorem :: CARDFIL2:81

    for T be non empty TopSpace, F be Filter of the carrier of T holds ( lim_filter F) = ( lim_filterb ( F2BOOL (F,T)))

    proof

      let T be non empty TopSpace, F be Filter of the carrier of T;

      now

        hereby

          let x be object;

          assume x in ( lim_filter F);

          then

          consider x0 be Point of T such that

           A1: x = x0 and

           A2: F is_filter-finer_than ( NeighborhoodSystem x0);

          thus x in ( lim_filterb ( F2BOOL (F,T))) by A1, A2;

        end;

        let x be object;

        assume x in ( lim_filterb ( F2BOOL (F,T)));

        then

        consider x0 be Point of T such that

         A3: x = x0 and

         A4: ( NeighborhoodSystem x0) c= F;

        F is_filter-finer_than ( NeighborhoodSystem x0) by A4;

        hence x in ( lim_filter F) by A3;

      end;

      then ( lim_filter F) c= ( lim_filterb ( F2BOOL (F,T))) & ( lim_filterb ( F2BOOL (F,T))) c= ( lim_filter F);

      hence thesis;

    end;

    theorem :: CARDFIL2:82

    for T be non empty TopSpace, F be Filter of the carrier of T holds ( Lim ( a_net ( F2BOOL (F,T)))) = ( lim_filter F)

    proof

      let T be non empty TopSpace, F be Filter of the carrier of T;

      now

        hereby

          let x be object;

          assume

           A1: x in ( Lim ( a_net ( F2BOOL (F,T))));

          then

          reconsider x0 = x as Point of T;

          F is_filter-finer_than ( NeighborhoodSystem x0) by A1, YELLOW19: 3, YELLOW19: 17;

          hence x in ( lim_filter F);

        end;

        let x be object;

        assume

         A2: x in ( lim_filter F);

        then

        reconsider x0 = x as Point of T;

        consider x1 be Point of T such that

         A3: x0 = x1 and

         A4: F is_filter-finer_than ( NeighborhoodSystem x1) by A2;

        thus x in ( Lim ( a_net ( F2BOOL (F,T)))) by A3, A4, YELLOW19: 3, YELLOW19: 17;

      end;

      then ( Lim ( a_net ( F2BOOL (F,T)))) c= ( lim_filter F) & ( lim_filter F) c= ( Lim ( a_net ( F2BOOL (F,T))));

      hence thesis;

    end;

    theorem :: CARDFIL2:83

    

     Th38: for T be Hausdorff non empty TopSpace, F be Filter of the carrier of T, p,q be Point of T st p in ( lim_filter F) & q in ( lim_filter F) holds p = q

    proof

      let T be Hausdorff non empty TopSpace, F be Filter of the carrier of T, p,q be Point of T such that

       A1: p in ( lim_filter F) and

       A2: q in ( lim_filter F);

      consider p0 be Point of T such that

       A3: p = p0 and

       A4: F is_filter-finer_than ( NeighborhoodSystem p0) by A1;

      consider q0 be Point of T such that

       A5: q = q0 and

       A6: F is_filter-finer_than ( NeighborhoodSystem q0) by A2;

      now

        assume p <> q;

        then

        consider G1,G2 be Subset of T such that

         A7: G1 is open and

         A8: G2 is open and

         A9: p in G1 and

         A10: q in G2 and

         A11: G1 misses G2 by PRE_TOPC:def 10;

        G1 in ( NeighborhoodSystem p) & G2 in ( NeighborhoodSystem q) by A7, A8, A9, A10, CONNSP_2: 3, YELLOW19: 2;

        then {} in F by A3, A4, A5, A6, A11, CARD_FIL:def 1;

        hence contradiction by CARD_FIL:def 1;

      end;

      hence thesis;

    end;

    registration

      let T be Hausdorff non empty TopSpace, F be Filter of the carrier of T;

      cluster ( lim_filter F) -> trivial;

      coherence

      proof

        for p,q be Point of T st p in ( lim_filter F) & q in ( lim_filter F) holds p = q by Th38;

        hence thesis by SUBSET_1: 45;

      end;

    end

    definition

      let X be non empty set, T be non empty TopSpace, f be Function of X, the carrier of T, F be Filter of X;

      :: CARDFIL2:def26

      func lim_filter (f,F) -> Subset of ( [#] T) equals ( lim_filter ( filter_image (f,F)));

      coherence ;

    end

    definition

      let T be non empty TopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T;

      :: CARDFIL2:def27

      func lim_f f -> Subset of ( [#] T) equals ( lim_filter ( filter_image (f,( Tails_Filter L))));

      coherence ;

    end

    theorem :: CARDFIL2:84

    for T be non empty TopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) st ( [#] L) is directed holds x in ( lim_f f) iff for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b

    proof

      let T be non empty TopSpace, L be non empty transitive reflexive RelStr, f be Function of ( [#] L), the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) such that

       A1: ( [#] L) is directed;

      hereby

        assume x in ( lim_f f);

        then

        consider x0 be Element of T such that

         A2: x = x0 and

         A3: ( filter_image (f,( Tails_Filter L))) is_filter-finer_than ( NeighborhoodSystem x0);

        ( BOOL2F ( NeighborhoodSystem x)) is_filter-coarser_than ( filter_image (f,( Tails_Filter L))) by A2, A3;

        then

         A4: B is_coarser_than (f .: ( # ( Tails L))) by A1, Th19;

        reconsider B1 = B as filter_base of ( [#] T) by Th09;

        for b be Element of B1 holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b by A1, A4, Th20;

        hence for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b;

      end;

      assume

       A5: for b be Element of B holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b;

      reconsider B1 = B as filter_base of ( [#] T) by Th09;

      for b be Element of B1 holds ex i be Element of L st for j be Element of L st i <= j holds (f . j) in b by A5;

      then B is_coarser_than (f .: ( # ( Tails L))) by A1, Th20;

      then ( BOOL2F ( NeighborhoodSystem x)) is_filter-coarser_than ( filter_image (f,( Tails_Filter L))) by A1, Th19;

      then x is Element of T & ( filter_image (f,( Tails_Filter L))) is_filter-finer_than ( NeighborhoodSystem x);

      hence x in ( lim_f f);

    end;

    definition

      let T be non empty TopSpace, s be sequence of T;

      :: CARDFIL2:def28

      func lim_f s -> Subset of T equals ( lim_filter ( elementary_filter s));

      coherence ;

    end

    theorem :: CARDFIL2:85

    for T be non empty TopSpace, s be sequence of T holds ( lim_filter (s,( Frechet_Filter NAT ))) = ( lim_f s);

    theorem :: CARDFIL2:86

    for T be non empty TopSpace, x be Point of T holds ( NeighborhoodSystem x) is filter_base of ( [#] T)

    proof

      let T be non empty TopSpace, x be Point of T;

      reconsider Nx = ( NeighborhoodSystem x) as Filter of ( [#] T) by Th36;

      Nx is basis of Nx by Th03;

      hence thesis by Th09;

    end;

    theorem :: CARDFIL2:87

    for T be non empty TopSpace, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds B is filter_base of ( [#] T) by Th09;

    theorem :: CARDFIL2:88

    for X be non empty set, s be sequence of X, B be filter_base of X holds B is_coarser_than (s .: base_of_frechet_filter ) iff for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b by Th20;

    theorem :: CARDFIL2:89

    

     Th39: for T be non empty TopSpace, s be sequence of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s,( Frechet_Filter NAT ))) iff B is_coarser_than (s .: base_of_frechet_filter )

    proof

      let T be non empty TopSpace, s be sequence of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      set F = ( filter_image (s,( Frechet_Filter NAT )));

      hereby

        assume x in ( lim_filter (s,( Frechet_Filter NAT )));

        then

        consider x0 be Element of T such that

         A1: x = x0 and

         A2: F is_filter-finer_than ( NeighborhoodSystem x0);

        ( BOOL2F ( NeighborhoodSystem x)) is_filter-coarser_than F by A1, A2;

        hence B is_coarser_than (s .: base_of_frechet_filter ) by Th19, Th27;

      end;

      assume

       A3: B is_coarser_than (s .: base_of_frechet_filter );

      ( BOOL2F ( NeighborhoodSystem x)) is_filter-coarser_than F by A3, Th19, Th27;

      then F is_filter-finer_than ( NeighborhoodSystem x);

      hence x in ( lim_filter (s,( Frechet_Filter NAT )));

    end;

    theorem :: CARDFIL2:90

    

     Th40: for T be non empty TopSpace, s be sequence of ( [#] T), x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds B is_coarser_than (s .: base_of_frechet_filter ) iff for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b

    proof

      let T be non empty TopSpace, s be sequence of ( [#] T), x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      reconsider B as filter_base of ( [#] T) by Th09;

      B is_coarser_than (s .: base_of_frechet_filter ) iff for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b by Th20;

      hence thesis;

    end;

    theorem :: CARDFIL2:91

    

     Th41: for T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_filter (s,( Frechet_Filter NAT ))) iff for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b

    proof

      let T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      x in ( lim_filter (s,( Frechet_Filter NAT ))) iff B is_coarser_than (s .: base_of_frechet_filter ) by Th39;

      hence thesis by Th40;

    end;

    theorem :: CARDFIL2:92

    

     Th42: for T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f s) iff for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b

    proof

      let T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      x in ( lim_filter (s,( Frechet_Filter NAT ))) iff for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b by Th41;

      hence thesis;

    end;

    begin

    definition

      let L be 1-sorted, s be sequence of the carrier of L;

      :: CARDFIL2:def29

      func sequence_to_net (s) -> non empty strict NetStr over L equals NetStr (# NAT , NATOrd , s #);

      coherence ;

    end

    registration

      let L be non empty 1-sorted, s be sequence of the carrier of L;

      cluster ( sequence_to_net s) -> non empty;

      coherence ;

    end

    theorem :: CARDFIL2:93

    

     Th43: for L be non empty 1-sorted, B be set, s be sequence of the carrier of L holds ( sequence_to_net s) is_eventually_in B iff ex i be Element of ( sequence_to_net s) st for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in B;

    theorem :: CARDFIL2:94

    

     Th44: for T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds (for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b) iff (for b be Element of B holds ex i be Element of ( sequence_to_net s) st for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in b)

    proof

      let T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      

       A1: (for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b) implies (for b be Element of B holds ex i be Element of ( sequence_to_net s) st for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in b)

      proof

        assume

         A2: for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b;

        for b be Element of B holds ex i be Element of ( sequence_to_net s) st for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in b

        proof

          let b be Element of B;

          consider i be Element of OrderedNAT such that

           A3: for j be Element of OrderedNAT st i <= j holds (s . j) in b by A2;

          reconsider i0 = i as Element of ( sequence_to_net s);

          for j be Element of ( sequence_to_net s) st i0 <= j holds (( sequence_to_net s) . j) in b

          proof

            let j be Element of ( sequence_to_net s);

            assume

             A4: i0 <= j;

            reconsider j0 = j as Element of OrderedNAT ;

            (the mapping of ( sequence_to_net s) . j) = (s . j0) & i <= j0 by A4;

            hence thesis by A3;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      (for b be Element of B holds ex i be Element of ( sequence_to_net s) st for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in b) implies (for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b)

      proof

        assume

         A5: for b be Element of B holds ex i be Element of ( sequence_to_net s) st for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in b;

        (for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b)

        proof

          let b be Element of B;

          consider i be Element of ( sequence_to_net s) such that

           A6: for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in b by A5;

          reconsider i0 = i as Element of OrderedNAT ;

          for j be Element of OrderedNAT st i0 <= j holds (s . j) in b

          proof

            let j be Element of OrderedNAT ;

            assume

             A7: i0 <= j;

            reconsider j0 = j as Element of ( sequence_to_net s);

            (the mapping of ( sequence_to_net s) . j0) = (s . j) & i <= j0 by A7;

            then (( sequence_to_net s) . j0) in b & i <= j0 by A6;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: CARDFIL2:95

    for T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f s) iff for b be Element of B holds ( sequence_to_net s) is_eventually_in b

    proof

      let T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume x in ( lim_f s);

        then for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b by Th42;

        hence for b be Element of B holds ( sequence_to_net s) is_eventually_in b by Th44;

      end;

      assume for b be Element of B holds ( sequence_to_net s) is_eventually_in b;

      then (for b be Element of B holds ex i be Element of ( sequence_to_net s) st for j be Element of ( sequence_to_net s) st i <= j holds (( sequence_to_net s) . j) in b) by Th43;

      then for b be Element of B holds ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b by Th44;

      hence x in ( lim_f s) by Th42;

    end;

    theorem :: CARDFIL2:96

    

     Th45: for T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f s) iff for b be Element of B holds ex i be Element of NAT st for j be Element of NAT st i <= j holds (s . j) in b

    proof

      let T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      now

        hereby

          assume

           A1: x in ( lim_filter (s,( Frechet_Filter NAT )));

          now

            let b be Element of B;

            consider i0 be Element of OrderedNAT such that

             A2: for j be Element of OrderedNAT st i0 <= j holds (s . j) in b by A1, Th41;

            reconsider i1 = i0 as Element of NAT ;

            now

              let j be Element of NAT ;

              assume

               A3: i1 <= j;

              reconsider j1 = j as Element of OrderedNAT ;

              i0 <= j1 by A3;

              hence (s . j) in b by A2;

            end;

            hence ex i be Element of NAT st for j be Element of NAT st i <= j holds (s . j) in b;

          end;

          hence for b be Element of B holds ex i be Element of NAT st for j be Element of NAT st i <= j holds (s . j) in b;

        end;

        assume

         A4: for b be Element of B holds ex i be Element of NAT st for j be Element of NAT st i <= j holds (s . j) in b;

        now

          let b be Element of B;

          consider i0 be Element of NAT such that

           A5: for j be Element of NAT st i0 <= j holds (s . j) in b by A4;

          reconsider i1 = i0 as Element of OrderedNAT ;

          now

            let j be Element of OrderedNAT ;

            assume

             A6: i1 <= j;

            consider x,y be Element of NAT such that

             A7: [i1, j] = [x, y] and

             A8: x <= y by A6;

            i1 = x & j = y & x <= y by A7, A8, XTUPLE_0: 1;

            hence (s . j) in b by A5;

          end;

          hence ex i be Element of OrderedNAT st for j be Element of OrderedNAT st i <= j holds (s . j) in b;

        end;

        hence x in ( lim_filter (s,( Frechet_Filter NAT ))) by Th41;

      end;

      hence thesis;

    end;

    theorem :: CARDFIL2:97

    for T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x)) holds x in ( lim_f s) iff for b be Element of B holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b

    proof

      let T be non empty TopSpace, s be sequence of the carrier of T, x be Point of T, B be basis of ( BOOL2F ( NeighborhoodSystem x));

      hereby

        assume

         A1: x in ( lim_f s);

        now

          let b be Element of B;

          consider i0 be Element of NAT such that

           A2: for j be Element of NAT st i0 <= j holds (s . j) in b by A1, Th45;

          reconsider i1 = i0 as Nat;

          take i1;

          now

            let k be Nat;

            assume

             A3: i1 <= k;

            reconsider k0 = k as Element of NAT by ORDINAL1:def 12;

            i0 <= k0 by A3;

            hence (s . k) in b by A2;

          end;

          hence for k be Nat st i1 <= k holds (s . k) in b;

        end;

        hence for b be Element of B holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b;

      end;

      assume

       A4: for b be Element of B holds ex i be Nat st for j be Nat st i <= j holds (s . j) in b;

      now

        let b be Element of B;

        consider i0 be Nat such that

         A5: for j be Nat st i0 <= j holds (s . j) in b by A4;

        reconsider i1 = i0 as Element of NAT by ORDINAL1:def 12;

        take i1;

        thus for j be Element of NAT st i1 <= j holds (s . j) in b by A5;

      end;

      hence x in ( lim_f s) by Th45;

    end;