yellow19.miz

    begin

    reserve x,y,X for set;

    theorem :: YELLOW19:1



     Th1: for X be non empty set holds for F be proper Filter of ( BoolePoset X) holds for A be set st A in F holds not A is empty

    proof

      let X be non empty set;

      ( Bottom ( BoolePoset X)) = {} by YELLOW_1: 18;

      hence thesis by WAYBEL_7: 4;

    end;

    definition

      let T be non empty TopSpace;

      let x be Point of T;

      :: YELLOW19:def1

      func NeighborhoodSystem x -> Subset of ( BoolePoset ( [#] T)) equals the set of all A where A be a_neighborhood of x;

      coherence

      proof

        set Y = the set of all A where A be a_neighborhood of x;

        set X = the carrier of T;

        Y c= ( bool X)

        proof

          let y be object;

          assume y in Y;

          then ex A be a_neighborhood of x st y = A;

          hence thesis;

        end;

        hence thesis by WAYBEL_7: 2;

      end;

    end

    theorem :: YELLOW19:2



     Th2: for T be non empty TopSpace, x be Point of T, A be set holds A in ( NeighborhoodSystem x) iff A is a_neighborhood of x

    proof

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

      B in ( NeighborhoodSystem x) iff ex A be a_neighborhood of x st B = A;

      hence thesis;

    end;

    registration

      let T be non empty TopSpace;

      let x be Point of T;

      cluster ( NeighborhoodSystem x) -> non empty proper upper filtered;

      coherence

      proof

        set Y = ( NeighborhoodSystem x);

        set X = the carrier of T, L = ( BoolePoset ( [#] T));

        set A0 = the a_neighborhood of x;

        A0 in ( NeighborhoodSystem x);

        hence ( NeighborhoodSystem x) is non empty;

         {} c= X;

        then

         A1: {} in ( bool X);

         not {} is a_neighborhood of x by CONNSP_2: 4;

        then

         A2: not {} in ( NeighborhoodSystem x) by Th2;

        the carrier of ( BoolePoset X) = ( bool X) by WAYBEL_7: 2;

        hence ( NeighborhoodSystem x) is proper by A1, A2;

        thus ( NeighborhoodSystem x) is upper

        proof

          let a,b be Element of L;

          reconsider B = b as Subset of T by WAYBEL_7: 2;

          assume a in Y;

          then

          reconsider A = a as a_neighborhood of x by Th2;

          assume a <= b;

          then A c= B by YELLOW_1: 2;

          then

           A3: ( Int A) c= ( Int B) by TOPS_1: 19;

          x in ( Int A) by CONNSP_2:def 1;

          then b is a_neighborhood of x by A3, CONNSP_2:def 1;

          hence thesis;

        end;

        let a,b be Element of L;

        assume that

         A4: a in Y and

         A5: b in Y;

        reconsider A = a, B = b as a_neighborhood of x by A4, A5, Th2;



         A6: (A /\ B) is a_neighborhood of x by CONNSP_2: 2;

        then (A /\ B) in ( NeighborhoodSystem x);

        then

        reconsider z = (A /\ B) as Element of L;

        take z;



         A7: z c= B by XBOOLE_1: 17;

        z c= A by XBOOLE_1: 17;

        hence thesis by A6, A7, YELLOW_1: 2;

      end;

    end

    theorem :: YELLOW19:3



     Th3: for T be non empty TopSpace, x be Point of T holds for F be upper Subset of ( BoolePoset ( [#] T)) holds x is_a_convergence_point_of (F,T) iff ( NeighborhoodSystem x) c= F

    proof

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

      let F be upper Subset of ( BoolePoset ( [#] T));

      hereby

        assume

         A1: x is_a_convergence_point_of (F,T);

        thus ( NeighborhoodSystem x) c= F

        proof

          let y be object;

          assume y in ( NeighborhoodSystem x);

          then

          reconsider y as a_neighborhood of x by Th2;

          x in ( Int y) by CONNSP_2:def 1;

          then

           A2: ( Int y) in F by A1;

          ( Int y) c= y by TOPS_1: 16;

          hence thesis by A2, WAYBEL_7: 7;

        end;

      end;

      assume

       A3: ( NeighborhoodSystem x) c= F;

      let A be Subset of T;

      assume that

       A4: A is open and

       A5: x in A;

      A is a_neighborhood of x by A4, A5, CONNSP_2: 3;

      then A in ( NeighborhoodSystem x);

      hence thesis by A3;

    end;

    theorem :: YELLOW19:4

    for T be non empty TopSpace, x be Point of T holds x is_a_convergence_point_of (( NeighborhoodSystem x),T) by Th3;

    theorem :: YELLOW19:5

    for T be non empty TopSpace holds for A be Subset of T holds A is open iff for x be Point of T st x in A holds for F be Filter of ( BoolePoset ( [#] T)) st x is_a_convergence_point_of (F,T) holds A in F

    proof

      let T be non empty TopSpace, A be Subset of T;

      thus A is open implies for x be Point of T st x in A holds for F be Filter of ( BoolePoset ( [#] T)) st x is_a_convergence_point_of (F,T) holds A in F;

      assume

       A1: for x be Point of T st x in A holds for F be Filter of ( BoolePoset ( [#] T)) st x is_a_convergence_point_of (F,T) holds A in F;

      set x = the Element of (A \ ( Int A));



       A2: ( Int A) c= A by TOPS_1: 16;

      assume not A is open;

      then not A c= ( Int A) by A2, XBOOLE_0:def 10;

      then

       A3: (A \ ( Int A)) <> {} by XBOOLE_1: 37;

      then x in (A \ ( Int A));

      then

      reconsider x as Point of T;



       A4: x in A by A3, XBOOLE_0:def 5;

      x is_a_convergence_point_of (( NeighborhoodSystem x),T) by Th3;

      then A in ( NeighborhoodSystem x) by A1, A4;

      then A is a_neighborhood of x by Th2;

      then x in ( Int A) by CONNSP_2:def 1;

      hence thesis by A3, XBOOLE_0:def 5;

    end;

    definition

      let S be non empty 1-sorted;

      let N be non empty NetStr over S;

      :: YELLOW19:def2

      mode Subset of S,N -> Subset of S means

      : Def2: ex i be Element of N st it = ( rng the mapping of (N | i));

      existence

      proof

        set i = the Element of N;

        reconsider A = ( rng the mapping of (N | i)) as Subset of S;

        take A, i;

        thus thesis;

      end;

    end

    theorem :: YELLOW19:6

    for S be non empty 1-sorted holds for N be non empty NetStr over S holds for i be Element of N holds ( rng the mapping of (N | i)) is Subset of S, N by Def2;

    registration

      let S be non empty 1-sorted;

      let N be reflexive non empty NetStr over S;

      cluster -> non empty for Subset of S, N;

      coherence

      proof

        let A be Subset of S, N;

        ex i be Element of N st A = ( rng the mapping of (N | i)) by Def2;

        hence thesis;

      end;

    end

    theorem :: YELLOW19:7



     Th7: for S be non empty 1-sorted, N be net of S holds for i be Element of N, x be set holds x in ( rng the mapping of (N | i)) iff ex j be Element of N st i <= j & x = (N . j)

    proof

      let S be non empty 1-sorted, N be net of S;

      let i be Element of N, x be set;



       A1: ( dom the mapping of (N | i)) = the carrier of (N | i) by FUNCT_2:def 1;

      hereby

        assume x in ( rng the mapping of (N | i));

        then

        consider y be object such that

         A2: y in the carrier of (N | i) and

         A3: x = (the mapping of (N | i) . y) by A1, FUNCT_1:def 3;

        reconsider y as Element of (N | i) by A2;

        consider j be Element of N such that

         A4: j = y and

         A5: i <= j by WAYBEL_9:def 7;

        take j;

        thus i <= j by A5;



        thus x = ((N | i) . y) by A3

        .= (N . j) by A4, WAYBEL_9: 16;

      end;

      given j be Element of N such that

       A6: i <= j and

       A7: x = (N . j);

      reconsider k = j as Element of (N | i) by A6, WAYBEL_9:def 7;



       A8: x = ((N | i) . k) by A7, WAYBEL_9: 16

      .= (the mapping of (N | i) . j);

      j in the carrier of (N | i) by A6, WAYBEL_9:def 7;

      hence thesis by A1, A8, FUNCT_1:def 3;

    end;

    theorem :: YELLOW19:8



     Th8: for S be non empty 1-sorted, N be net of S holds for A be Subset of S, N holds N is_eventually_in A

    proof

      let S be non empty 1-sorted, N be net of S;

      let A be Subset of S, N;

      consider i be Element of N such that

       A1: A = ( rng the mapping of (N | i)) by Def2;

      take i;

      let j be Element of N;

      assume i <= j;

      then

      reconsider j9 = j as Element of (N | i) by WAYBEL_9:def 7;

      (N . j) = ((N | i) . j9) by WAYBEL_9: 16

      .= (the mapping of (N | i) . j9);

      hence thesis by A1, FUNCT_2: 4;

    end;

    theorem :: YELLOW19:9

    for S be non empty 1-sorted, N be net of S holds for F be finite non empty set st for A be Element of F holds A is Subset of S, N holds ex B be Subset of S, N st B c= ( meet F)

    proof

      let S be non empty 1-sorted, N be net of S;

      defpred P[ object, object] means ex i be Element of N st $2 = i & $1 = ( rng the mapping of (N | i));

      let F be finite non empty set such that

       A1: for A be Element of F holds A is Subset of S, N;

       A2:

      now

        let x be object;

        assume x in F;

        then

        reconsider A = x as Subset of S, N by A1;

        consider i be Element of N such that

         A3: A = ( rng the mapping of (N | i)) by Def2;

        reconsider y = i as object;

        take y;

        thus y in the carrier of N;

        thus P[x, y] by A3;

      end;

      consider f be Function such that

       A4: ( dom f) = F & ( rng f) c= the carrier of N and

       A5: for x be object st x in F holds P[x, (f . x)] from FUNCT_1:sch 6( A2);

      reconsider B = ( rng f) as finite Subset of N by A4, FINSET_1: 8;

      ( [#] N) is directed by WAYBEL_0:def 6;

      then

      consider j be Element of N such that j in ( [#] N) and

       A6: j is_>=_than B by WAYBEL_0: 1;

      reconsider C = ( rng the mapping of (N | j)) as Subset of S, N by Def2;

      take C;

      let x be object;



       A7: the carrier of (N | j) = { k where k be Element of N : j <= k } by WAYBEL_9: 12;

      assume x in C;

      then

      consider y be object such that

       A8: y in ( dom the mapping of (N | j)) and

       A9: x = (the mapping of (N | j) . y) by FUNCT_1:def 3;



       A10: y in the carrier of (N | j) by A8;

      reconsider y as Element of (N | j) by A8;

      consider k be Element of N such that

       A11: y = k and

       A12: j <= k by A10, A7;

      now

        let X;

        assume

         A13: X in F;

        then

        consider i be Element of N such that

         A14: (f . X) = i and

         A15: X = ( rng the mapping of (N | i)) by A5;

        i in B by A4, A13, A14, FUNCT_1:def 3;

        then i <= j by A6, LATTICE3:def 9;

        then i <= k by A12, ORDERS_2: 3;

        then y in { l where l be Element of N : i <= l } by A11;

        then

        reconsider z = y as Element of (N | i) by WAYBEL_9: 12;

        x = ((N | j) . y) by A9

        .= (N . k) by A11, WAYBEL_9: 16

        .= ((N | i) . z) by A11, WAYBEL_9: 16

        .= (the mapping of (N | i) . z);

        hence x in X by A15, FUNCT_2: 4;

      end;

      hence thesis by SETFAM_1:def 1;

    end;

    definition

      let T be non empty 1-sorted;

      let N be non empty NetStr over T;

      :: YELLOW19:def3

      func a_filter N -> Subset of ( BoolePoset ( [#] T)) equals { A where A be Subset of T : N is_eventually_in A };

      coherence

      proof

        set X = the carrier of T;

        set F = { A where A be Subset of T : N is_eventually_in A };



         A1: F c= ( bool X)

        proof

          let x be object;

          assume x in F;

          then ex A be Subset of T st x = A & N is_eventually_in A;

          hence thesis;

        end;

        ( BoolePoset X) = ( InclPoset ( bool X)) by YELLOW_1: 4

        .= RelStr (# ( bool X), ( RelIncl ( bool X)) #) by YELLOW_1:def 1;

        hence thesis by A1;

      end;

    end

    theorem :: YELLOW19:10



     Th10: for T be non empty 1-sorted holds for N be non empty NetStr over T holds for A be set holds A in ( a_filter N) iff N is_eventually_in A & A is Subset of T

    proof

      let T be non empty 1-sorted;

      let N be non empty NetStr over T;

      let B be set;

      B in ( a_filter N) iff ex A be Subset of T st B = A & N is_eventually_in A;

      hence thesis;

    end;

    registration

      let T be non empty 1-sorted;

      let N be non empty NetStr over T;

      cluster ( a_filter N) -> non empty upper;

      coherence

      proof

        set X = the carrier of T, L = ( BoolePoset ( [#] T));

        set F = ( a_filter N);

        N is_eventually_in ( [#] T)

        proof

          set i = the Element of N;

          take i;

          thus thesis;

        end;

        hence F is non empty by Th10;

        let a,b be Element of L;

        assume a in F;

        then

         A1: N is_eventually_in a by Th10;

        assume a <= b;

        then a c= b by YELLOW_1: 2;

        then

         A2: N is_eventually_in b by A1, WAYBEL_0: 8;

        ( BoolePoset X) = ( InclPoset ( bool X)) by YELLOW_1: 4

        .= RelStr (# ( bool X), ( RelIncl ( bool X)) #) by YELLOW_1:def 1;

        hence thesis by A2;

      end;

    end

    registration

      let T be non empty 1-sorted;

      let N be net of T;

      cluster ( a_filter N) -> proper filtered;

      coherence

      proof

        set X = the carrier of T, L = ( BoolePoset ( [#] T));

        set F = ( a_filter N);



         A1: ( BoolePoset X) = ( InclPoset ( bool X)) by YELLOW_1: 4

        .= RelStr (# ( bool X), ( RelIncl ( bool X)) #) by YELLOW_1:def 1;

        now

          thus {} c= X;

          assume {} in F;

          then N is_eventually_in {} by Th10;

          then

          consider i be Element of N such that

           A2: for j be Element of N st i <= j holds (N . j) in {} ;

          ex j be Element of N st i <= j & i <= j by YELLOW_6:def 3;

          hence contradiction by A2;

        end;

        then F <> ( bool X);

        hence F is proper by A1;

        let a,b be Element of L;

        assume that

         A3: a in F and

         A4: b in F;

        N is_eventually_in a by A3, Th10;

        then

        consider i1 be Element of N such that

         A5: for j be Element of N st i1 <= j holds (N . j) in a;

        N is_eventually_in b by A4, Th10;

        then

        consider i2 be Element of N such that

         A6: for j be Element of N st i2 <= j holds (N . j) in b;

        take z = (a "/\" b);



         A7: z = (a /\ b) by YELLOW_1: 17;

        then

         A8: z c= b by XBOOLE_1: 17;

        consider i be Element of N such that

         A9: i1 <= i and

         A10: i2 <= i by YELLOW_6:def 3;

        now

          let j be Element of N;

          assume

           A11: i <= j;

          then

           A12: (N . j) in b by A6, A10, ORDERS_2: 3;

          (N . j) in a by A5, A9, A11, ORDERS_2: 3;

          hence (N . j) in (a /\ b) by A12, XBOOLE_0:def 4;

        end;

        then N is_eventually_in z by A7;

        hence z in F by A1;

        z c= a by A7, XBOOLE_1: 17;

        hence thesis by A8, YELLOW_1: 2;

      end;

    end

    theorem :: YELLOW19:11



     Th11: for T be non empty TopSpace holds for N be net of T holds for x be Point of T holds x is_a_cluster_point_of N iff x is_a_cluster_point_of (( a_filter N),T)

    proof

      let T be non empty TopSpace;

      let N be net of T;

      set F = ( a_filter N);

      let x be Point of T;

      thus x is_a_cluster_point_of N implies x is_a_cluster_point_of (F,T)

      proof

        assume

         A1: for O be a_neighborhood of x holds N is_often_in O;

        let A be Subset of T;

        assume that

         A2: A is open and

         A3: x in A;

        let B be set;

        assume B in F;

        then N is_eventually_in B by Th10;

        then

        consider i be Element of N such that

         A4: for j be Element of N st i <= j holds (N . j) in B;

        A is a_neighborhood of x by A2, A3, CONNSP_2: 3;

        then N is_often_in A by A1;

        then ex j be Element of N st i <= j & (N . j) in A;

        then ex a be Point of T st a in B & a in A by A4;

        hence thesis by XBOOLE_0: 3;

      end;

      assume

       A5: for A be Subset of T st A is open & x in A holds for B be set st B in F holds A meets B;

      let O be a_neighborhood of x;

      let i be Element of N;

      reconsider B = ( rng the mapping of (N | i)) as Subset of T, N by Def2;

      N is_eventually_in B by Th8;

      then

       A6: B in F;

      x in ( Int O) by CONNSP_2:def 1;

      then ( Int O) meets B by A5, A6;

      then

      consider x be object such that

       A7: x in ( Int O) and

       A8: x in B by XBOOLE_0: 3;

      consider j be Element of N such that

       A9: i <= j and

       A10: x = (N . j) by A8, Th7;

      take j;

      ( Int O) c= O by TOPS_1: 16;

      hence thesis by A7, A9, A10;

    end;

    theorem :: YELLOW19:12



     Th12: for T be non empty TopSpace holds for N be net of T holds for x be Point of T holds x in ( Lim N) iff x is_a_convergence_point_of (( a_filter N),T)

    proof

      let T be non empty TopSpace;

      let N be net of T;

      set F = ( a_filter N);

      let x be Point of T;

      thus x in ( Lim N) implies x is_a_convergence_point_of (F,T)

      proof

        assume

         A1: x in ( Lim N);

        let A be Subset of T;

        assume that

         A2: A is open and

         A3: x in A;

        A is a_neighborhood of x by A2, A3, CONNSP_2: 3;

        then N is_eventually_in A by A1, YELLOW_6:def 15;

        hence thesis;

      end;

      assume

       A4: for A be Subset of T st A is open & x in A holds A in F;

      now

        let O be a_neighborhood of x;

        x in ( Int O) by CONNSP_2:def 1;

        then ( Int O) in F by A4;

        then

         A5: N is_eventually_in ( Int O) by Th10;

        ( Int O) c= O by TOPS_1: 16;

        hence N is_eventually_in O by A5, WAYBEL_0: 8;

      end;

      hence thesis by YELLOW_6:def 15;

    end;

    definition

      let L be non empty 1-sorted;

      let O be non empty Subset of L;

      let F be Filter of ( BoolePoset O);

      :: YELLOW19:def4

      func a_net F -> strict non empty NetStr over L means

      : Def4: the carrier of it = { [a, f] where a be Element of L, f be Element of F : a in f } & (for i,j be Element of it holds i <= j iff (j `2 ) c= (i `2 )) & for i be Element of it holds (it . i) = (i `1 );

      existence

      proof

        deffunc F( object) = ($1 `1 );

        set S = { [a, f] where a be Element of L, f be Element of F : a in f };

        ( Top ( BoolePoset O)) = O by YELLOW_1: 19;

        then

        reconsider f = O as Element of F by WAYBEL12: 8;

        reconsider f as Subset of L;

        consider a be Element of L such that

         A1: a in f by SUBSET_1: 4;

        reconsider a as Element of L;

         [a, f] in S by A1;

        then

        reconsider S as non empty set;

        defpred P[ object, object] means ($2 `2 ) c= ($1 `2 );

        consider R be Relation of S, S such that

         A2: for x,y be Element of S holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;



         A3: for x be object st x in S holds F(x) in the carrier of L

        proof

          let x be object;

          assume x in S;

          then

          consider a be Element of L, f be Element of F such that

           A4: x = [a, f] and a in f;

          thus thesis by A4;

        end;

        consider h be Function of S, the carrier of L such that

         A5: for x be object st x in S holds (h . x) = F(x) from FUNCT_2:sch 2( A3);

        take N = NetStr (# S, R, h #);

        for i,j be Element of N holds i <= j iff (j `2 ) c= (i `2 )

        proof

          let i,j be Element of N;

          reconsider x = i, y = j as Element of S;

           [x, y] in the InternalRel of N iff (y `2 ) c= (x `2 ) by A2;

          hence thesis by ORDERS_2:def 5;

        end;

        hence thesis by A5;

      end;

      uniqueness

      proof

        set S = { [a, f] where a be Element of L, f be Element of F : a in f };

        let it1,it2 be strict non empty NetStr over L such that

         A6: the carrier of it1 = { [a, f] where a be Element of L, f be Element of F : a in f } and

         A7: for i,j be Element of it1 holds i <= j iff (j `2 ) c= (i `2 ) and

         A8: for i be Element of it1 holds (it1 . i) = (i `1 ) and

         A9: the carrier of it2 = { [a, f] where a be Element of L, f be Element of F : a in f } and

         A10: for i,j be Element of it2 holds i <= j iff (j `2 ) c= (i `2 ) and

         A11: for i be Element of it2 holds (it2 . i) = (i `1 );



         A12: for x,y be object holds [x, y] in the InternalRel of it1 iff [x, y] in the InternalRel of it2

        proof

          let x,y be object;

          hereby

            assume

             A13: [x, y] in the InternalRel of it1;

            then

            reconsider i = x, j = y as Element of it1 by ZFMISC_1: 87;

            reconsider i9 = x, j9 = y as Element of it2 by A6, A9, A13, ZFMISC_1: 87;

            i <= j by A13, ORDERS_2:def 5;

            then (j9 `2 ) c= (i9 `2 ) by A7;

            then i9 <= j9 by A10;

            hence [x, y] in the InternalRel of it2 by ORDERS_2:def 5;

          end;

          assume

           A14: [x, y] in the InternalRel of it2;

          then

          reconsider i = x, j = y as Element of it2 by ZFMISC_1: 87;

          reconsider i9 = x, j9 = y as Element of it1 by A6, A9, A14, ZFMISC_1: 87;

          i <= j by A14, ORDERS_2:def 5;

          then (j9 `2 ) c= (i9 `2 ) by A10;

          then i9 <= j9 by A7;

          hence thesis by ORDERS_2:def 5;

        end;

        the mapping of it1 = the mapping of it2

        proof

          reconsider f2 = the mapping of it2 as Function of S, the carrier of L by A9;

          reconsider f1 = the mapping of it1 as Function of S, the carrier of L by A6;

          for x be object st x in S holds (f1 . x) = (f2 . x)

          proof

            let x be object;

            assume

             A15: x in S;

            then

            reconsider x1 = x as Element of it1 by A6;

            reconsider x2 = x as Element of it2 by A9, A15;

            reconsider x as Element of S by A15;

            (f1 . x) = (it1 . x1)

            .= (x1 `1 ) by A8

            .= (it2 . x2) by A11;

            hence thesis;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        hence thesis by A6, A9, A12, RELAT_1:def 2;

      end;

    end

    registration

      let L be non empty 1-sorted;

      let O be non empty Subset of L;

      let F be Filter of ( BoolePoset O);

      cluster ( a_net F) -> reflexive transitive;

      coherence

      proof

        for x,y,z be object st x in the carrier of ( a_net F) & y in the carrier of ( a_net F) & z in the carrier of ( a_net F) & [x, y] in the InternalRel of ( a_net F) & [y, z] in the InternalRel of ( a_net F) holds [x, z] in the InternalRel of ( a_net F)

        proof

          let x,y,z be object;

          assume that

           A1: x in the carrier of ( a_net F) and

           A2: y in the carrier of ( a_net F) and

           A3: z in the carrier of ( a_net F) and

           A4: [x, y] in the InternalRel of ( a_net F) and

           A5: [y, z] in the InternalRel of ( a_net F);

          reconsider k = z as Element of ( a_net F) by A3;

          reconsider j = y as Element of ( a_net F) by A2;

          j <= k by A5, ORDERS_2:def 5;

          then

           A6: (k `2 ) c= (j `2 ) by Def4;

          reconsider i = x as Element of ( a_net F) by A1;

          i <= j by A4, ORDERS_2:def 5;

          then (j `2 ) c= (i `2 ) by Def4;

          then (k `2 ) c= (i `2 ) by A6;

          then i <= k by Def4;

          hence thesis by ORDERS_2:def 5;

        end;

        then

         A7: the InternalRel of ( a_net F) is_transitive_in the carrier of ( a_net F) by RELAT_2:def 8;

        for x be object st x in the carrier of ( a_net F) holds [x, x] in the InternalRel of ( a_net F)

        proof

          let x be object;

          assume x in the carrier of ( a_net F);

          then

          reconsider i = x as Element of ( a_net F);

          (i `2 ) c= (i `2 );

          then i <= i by Def4;

          hence thesis by ORDERS_2:def 5;

        end;

        then the InternalRel of ( a_net F) is_reflexive_in the carrier of ( a_net F) by RELAT_2:def 1;

        hence thesis by A7, ORDERS_2:def 2, ORDERS_2:def 3;

      end;

    end

    registration

      let L be non empty 1-sorted;

      let O be non empty Subset of L;

      let F be proper Filter of ( BoolePoset O);

      cluster ( a_net F) -> directed;

      coherence

      proof

        set S = { [a, f] where a be Element of L, f be Element of F : a in f };

        for x,y be Element of ( a_net F) st x in ( [#] ( a_net F)) & y in ( [#] ( a_net F)) holds ex z be Element of ( a_net F) st z in ( [#] ( a_net F)) & x <= z & y <= z

        proof

          let x,y be Element of ( a_net F);

          assume that x in ( [#] ( a_net F)) and y in ( [#] ( a_net F));

          x in the carrier of ( a_net F);

          then x in S by Def4;

          then

          consider a be Element of L, f be Element of F such that

           A1: x = [a, f] and a in f;

          reconsider f as Element of ( BoolePoset O);

          y in the carrier of ( a_net F);

          then y in S by Def4;

          then

          consider b be Element of L, g be Element of F such that

           A2: y = [b, g] and b in g;

          reconsider g as Element of ( BoolePoset O);

          reconsider h = (f "/\" g) as Element of F by WAYBEL_0: 41;

          set s = the Element of h;



           A3: h c= O by WAYBEL_8: 26;

           not ( Bottom ( BoolePoset O)) in F by WAYBEL_7: 4;

          then not {} in F by YELLOW_1: 18;

          then

           A4: h <> {} ;

          then s in h;

          then s in O by A3;

          then

          reconsider s as Element of L;

           [s, h] in S by A4;

          then

          reconsider z = [s, h] as Element of ( a_net F) by Def4;

          reconsider i = x, j = y, k = z as Element of ( a_net F);



           A5: ( [b, g] `2 ) = g;

          take z;



           A6: ( [s, h] `2 ) = h;

          (f /\ g) c= g by XBOOLE_1: 17;

          then

           A7: h c= g by YELLOW_1: 17;

          (f /\ g) c= f by XBOOLE_1: 17;

          then

           A8: h c= f by YELLOW_1: 17;

          ( [a, f] `2 ) = f;

          hence thesis by A5, A6, A8, A7, Def4, A1, A2;

        end;

        then ( [#] ( a_net F)) is directed;

        hence thesis;

      end;

    end

    theorem :: YELLOW19:13



     Th13: for T be non empty 1-sorted holds for F be Filter of ( BoolePoset ( [#] T)) holds (F \ { {} }) = ( a_filter ( a_net F))

    proof

      let T be non empty 1-sorted;

      let F be Filter of ( BoolePoset ( [#] T));

      set X = ( a_filter ( a_net F));



       A1: the carrier of ( a_net F) = { [a, f] where a be Element of T, f be Element of F : a in f } by Def4;



       A2: ( BoolePoset ( [#] T)) = ( InclPoset ( bool ( [#] T))) by YELLOW_1: 4;

      thus (F \ { {} }) c= X

      proof

        let x be object;

        assume

         A3: x in (F \ { {} });

        then

        reconsider A = x as Subset of T by A2, YELLOW_1: 1;

        set a = the Element of A;

         not x in { {} } by A3, XBOOLE_0:def 5;

        then

         A4: A <> {} by TARSKI:def 1;

        then a in A;

        then

        reconsider a as Element of T;

        x in F by A3, XBOOLE_0:def 5;

        then [a, A] in the carrier of ( a_net F) by A1, A4;

        then

        reconsider i = [a, A] as Element of ( a_net F);

        ( a_net F) is_eventually_in A

        proof

          take i;

          let j be Element of ( a_net F);



           A5: (( a_net F) . j) = (j `1 ) by Def4;

          assume i <= j;

          then

           A6: (j `2 ) c= (i `2 ) by Def4;

          j in the carrier of ( a_net F);

          then

          consider a be Element of T, f be Element of F such that

           A7: j = [a, f] and

           A8: a in f by A1;



           A9: (j `1 ) = a by A7;

          (j `2 ) = f by A7;

          hence thesis by A8, A6, A5, A9;

        end;

        hence thesis;

      end;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume

       A10: x in X;

      then ( a_net F) is_eventually_in xx by Th10;

      then

      consider i be Element of ( a_net F) such that

       A11: for j be Element of ( a_net F) st i <= j holds (( a_net F) . j) in xx;

      i in the carrier of ( a_net F);

      then

      consider a be Element of T, f be Element of F such that

       A12: i = [a, f] and

       A13: a in f by A1;



       A14: the carrier of ( BoolePoset ( [#] T)) = ( bool ( [#] T)) by A2, YELLOW_1: 1;



       A15: f c= xx

      proof

        let x be object;

        assume

         A16: x in f;

        then

        reconsider b = x as Element of T by A14;

         [b, f] in the carrier of ( a_net F) by A1, A16;

        then

        reconsider j = [b, f] as Element of ( a_net F);



         A17: (j `2 ) = f;

        (j `1 ) = b;

        then

         A18: (( a_net F) . j) = b by Def4;

        (i `2 ) = f by A12;

        then i <= j by A17, Def4;

        hence thesis by A11, A18;

      end;

      x is Subset of T by A10, Th10;

      then

       A19: x in F by A15, WAYBEL_7: 7;

       not x in { {} } by A13, A15, TARSKI:def 1;

      hence thesis by A19, XBOOLE_0:def 5;

    end;

    theorem :: YELLOW19:14



     Th14: for T be non empty 1-sorted holds for F be proper Filter of ( BoolePoset ( [#] T)) holds F = ( a_filter ( a_net F))

    proof

      let T be non empty 1-sorted;

      let F be proper Filter of ( BoolePoset ( [#] T));

       not {} in F by Th1;

      then (F \ { {} }) = F by ZFMISC_1: 57;

      hence thesis by Th13;

    end;

    theorem :: YELLOW19:15



     Th15: for T be non empty 1-sorted holds for F be Filter of ( BoolePoset ( [#] T)) holds for A be non empty Subset of T holds A in F iff ( a_net F) is_eventually_in A

    proof

      let T be non empty 1-sorted;

      let F be Filter of ( BoolePoset ( [#] T));

      let B be non empty Subset of T;



       A1: B in F iff B in (F \ { {} }) by ZFMISC_1: 56;

      (F \ { {} }) = ( a_filter ( a_net F)) by Th13;

      hence thesis by A1, Th10;

    end;

    theorem :: YELLOW19:16



     Th16: for T be non empty TopSpace holds for F be proper Filter of ( BoolePoset ( [#] T)) holds for x be Point of T holds x is_a_cluster_point_of ( a_net F) iff x is_a_cluster_point_of (F,T)

    proof

      let T be non empty TopSpace;

      let F be proper Filter of ( BoolePoset ( [#] T));

      F = ( a_filter ( a_net F)) by Th14;

      hence thesis by Th11;

    end;

    theorem :: YELLOW19:17



     Th17: for T be non empty TopSpace holds for F be proper Filter of ( BoolePoset ( [#] T)) holds for x be Point of T holds x in ( Lim ( a_net F)) iff x is_a_convergence_point_of (F,T)

    proof

      let T be non empty TopSpace;

      let F be proper Filter of ( BoolePoset ( [#] T));

      F = ( a_filter ( a_net F)) by Th14;

      hence thesis by Th12;

    end;

    theorem :: YELLOW19:18



     Th18: for T be non empty TopSpace, x be Point of T, A be Subset of T st x in ( Cl A) holds for F be proper Filter of ( BoolePoset ( [#] T)) st F = ( NeighborhoodSystem x) holds ( a_net F) is_often_in A

    proof

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

      assume

       A1: x in ( Cl A);

      let F be proper Filter of ( BoolePoset ( [#] T)) such that

       A2: F = ( NeighborhoodSystem x);

      set N = ( a_net F);

      let i be Element of N;



       A3: the carrier of N = { [a, f] where a be Element of T, f be Element of F : a in f } by Def4;

      i in the carrier of N;

      then

      consider a be Element of T, f be Element of F such that

       A4: i = [a, f] and a in f by A3;

      reconsider f as a_neighborhood of x by A2, Th2;



       A5: (i `2 ) = f by A4;

      f meets A by A1, CONNSP_2: 27;

      then

      consider b be object such that

       A6: b in f and

       A7: b in A by XBOOLE_0: 3;

      reconsider b as Element of T by A6;

       [b, f] in the carrier of N by A3, A6;

      then

      reconsider j = [b, f] as Element of N;

      take j;



       A8: (j `1 ) = b;

      (j `2 ) = f;

      hence i <= j & (N . j) in A by A7, A5, A8, Def4;

    end;

    theorem :: YELLOW19:19



     Th19: for T be non empty 1-sorted, A be set holds for N be net of T st N is_eventually_in A holds for S be subnet of N holds S is_eventually_in A

    proof

      let T be non empty 1-sorted, A be set;

      let N be net of T;

      given i be Element of N such that

       A1: for j be Element of N st i <= j holds (N . j) in A;

      let S be subnet of N;

      consider f be Function of S, N such that

       A2: the mapping of S = (the mapping of N * f) and

       A3: for m be Element of N holds ex n be Element of S st for p be Element of S st n <= p holds m <= (f . p) by YELLOW_6:def 9;

      consider n be Element of S such that

       A4: for p be Element of S st n <= p holds i <= (f . p) by A3;

      take n;

      let p be Element of S;

      assume n <= p;

      then (N . (f . p)) in A by A1, A4;

      hence thesis by A2, FUNCT_2: 15;

    end;

    theorem :: YELLOW19:20

    for T be non empty TopSpace, F,G,x be set st F c= G & x is_a_convergence_point_of (F,T) holds x is_a_convergence_point_of (G,T);

    theorem :: YELLOW19:21



     Th21: for T be non empty TopSpace, A be Subset of T holds for x be Point of T holds x in ( Cl A) iff ex N be net of T st N is_eventually_in A & x is_a_cluster_point_of N

    proof

      let T be non empty TopSpace, A be Subset of T;

      let x be Point of T;

      reconsider F = ( NeighborhoodSystem x) as proper Filter of ( BoolePoset ( [#] T));

      hereby

        assume x in ( Cl A);

        then

        reconsider N = (( a_net F) " A) as subnet of ( a_net F) by Th18, YELLOW_6: 22;

        reconsider N9 = N as net of T;

        take N9;

        thus N9 is_eventually_in A by YELLOW_6: 23;

        x is_a_convergence_point_of (F,T) by Th3;

        then

         A1: x in ( Lim ( a_net F)) by Th17;

        ( Lim ( a_net F)) c= ( Lim N) by YELLOW_6: 32;

        hence x is_a_cluster_point_of N9 by A1, WAYBEL_9: 29;

      end;

      given N be net of T such that

       A2: N is_eventually_in A and

       A3: x is_a_cluster_point_of N;

      consider i be Element of N such that

       A4: for j be Element of N st i <= j holds (N . j) in A by A2;

      now

        let G be Subset of T;

        assume that

         A5: G is open and

         A6: x in G;

        ( Int G) = G by A5, TOPS_1: 23;

        then G is a_neighborhood of x by A6, CONNSP_2:def 1;

        then N is_often_in G by A3;

        then

        consider j be Element of N such that

         A7: i <= j and

         A8: (N . j) in G;

        (N . j) in A by A4, A7;

        hence A meets G by A8, XBOOLE_0: 3;

      end;

      hence thesis by PRE_TOPC:def 7;

    end;

    theorem :: YELLOW19:22



     Th22: for T be non empty TopSpace, A be Subset of T holds for x be Point of T holds x in ( Cl A) iff ex N be convergent net of T st N is_eventually_in A & x in ( Lim N)

    proof

      let T be non empty TopSpace, A be Subset of T;

      let x be Point of T;

      hereby

        assume x in ( Cl A);

        then

        consider N be net of T such that

         A1: N is_eventually_in A and

         A2: x is_a_cluster_point_of N by Th21;

        consider S be subnet of N such that

         A3: x in ( Lim S) by A2, WAYBEL_9: 32;

        reconsider S as convergent net of T by A3, YELLOW_6:def 16;

        take S;

        thus S is_eventually_in A by A1, Th19;

        thus x in ( Lim S) by A3;

      end;

      given N be convergent net of T such that

       A4: N is_eventually_in A and

       A5: x in ( Lim N);

      x is_a_cluster_point_of N by A5, WAYBEL_9: 29;

      hence thesis by A4, Th21;

    end;

    theorem :: YELLOW19:23

    for T be non empty TopSpace, A be Subset of T holds A is closed iff for N be net of T st N is_eventually_in A holds for x be Point of T st x is_a_cluster_point_of N holds x in A

    proof

      let T be non empty TopSpace, A be Subset of T;

      A is closed iff ( Cl A) = A by PRE_TOPC: 22;

      hence A is closed implies for N be net of T st N is_eventually_in A holds for x be Point of T st x is_a_cluster_point_of N holds x in A by Th21;

      assume

       A1: for N be net of T st N is_eventually_in A holds for x be Point of T st x is_a_cluster_point_of N holds x in A;

      A = ( Cl A)

      proof

        thus A c= ( Cl A) by PRE_TOPC: 18;

        let x be object;

        assume

         A2: x in ( Cl A);

        then

        reconsider y = x as Element of T;

        ex N be net of T st N is_eventually_in A & y is_a_cluster_point_of N by A2, Th21;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: YELLOW19:24

    for T be non empty TopSpace, A be Subset of T holds A is closed iff for N be convergent net of T st N is_eventually_in A holds for x be Point of T st x in ( Lim N) holds x in A

    proof

      let T be non empty TopSpace, A be Subset of T;

      A is closed iff ( Cl A) = A by PRE_TOPC: 22;

      hence A is closed implies for N be convergent net of T st N is_eventually_in A holds for x be Point of T st x in ( Lim N) holds x in A by Th22;

      assume

       A1: for N be convergent net of T st N is_eventually_in A holds for x be Point of T st x in ( Lim N) holds x in A;

      A = ( Cl A)

      proof

        thus A c= ( Cl A) by PRE_TOPC: 18;

        let x be object;

        assume

         A2: x in ( Cl A);

        then

        reconsider y = x as Element of T;

        ex N be convergent net of T st N is_eventually_in A & y in ( Lim N) by A2, Th22;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: YELLOW19:25



     Th25: for T be non empty TopSpace, A be Subset of T holds for x be Point of T holds x in ( Cl A) iff ex F be proper Filter of ( BoolePoset ( [#] T)) st A in F & x is_a_cluster_point_of (F,T)

    proof

      let T be non empty TopSpace, A be Subset of T;

      let x be Point of T;

      hereby

        assume x in ( Cl A);

        then

        consider N be net of T such that

         A1: N is_eventually_in A and

         A2: x is_a_cluster_point_of N by Th21;

        set F = ( a_filter N);

        take F;

        thus A in F by A1;

        thus x is_a_cluster_point_of (F,T) by A2, Th11;

      end;

      given F be proper Filter of ( BoolePoset ( [#] T)) such that

       A3: A in F and

       A4: x is_a_cluster_point_of (F,T);

      reconsider F9 = F as proper Filter of ( BoolePoset ( [#] T));



       A5: ( a_filter ( a_net F9)) = F by Th14;

      then

       A6: x is_a_cluster_point_of ( a_net F9) by A4, Th11;

      ( a_net F9) is_eventually_in A by A3, A5, Th10;

      hence thesis by A6, Th21;

    end;

    theorem :: YELLOW19:26



     Th26: for T be non empty TopSpace, A be Subset of T holds for x be Point of T holds x in ( Cl A) iff ex F be ultra Filter of ( BoolePoset ( [#] T)) st A in F & x is_a_convergence_point_of (F,T)

    proof

      let T be non empty TopSpace, A be Subset of T;

      let x be Point of T;

      hereby

        assume x in ( Cl A);

        then

        consider N be net of T such that

         A1: N is_eventually_in A and

         A2: x is_a_cluster_point_of N by Th21;

        consider S be subnet of N such that

         A3: x in ( Lim S) by A2, WAYBEL_9: 32;

        set F = ( a_filter S);

        consider G be Filter of ( BoolePoset ( [#] T)) such that

         A4: F c= G and

         A5: G is ultra by WAYBEL_7: 26;

        reconsider G as ultra Filter of ( BoolePoset ( [#] T)) by A5;

        take G;

        S is_eventually_in A by A1, Th19;

        then A in F;

        hence A in G by A4;

        x is_a_convergence_point_of (F,T) by A3, Th12;

        hence x is_a_convergence_point_of (G,T) by A4;

      end;

      given F be ultra Filter of ( BoolePoset ( [#] T)) such that

       A6: A in F and

       A7: x is_a_convergence_point_of (F,T);

      x is_a_cluster_point_of (F,T) by A7, WAYBEL_7: 27;

      hence thesis by A6, Th25;

    end;

    theorem :: YELLOW19:27

    for T be non empty TopSpace, A be Subset of T holds A is closed iff for F be proper Filter of ( BoolePoset ( [#] T)) st A in F holds for x be Point of T st x is_a_cluster_point_of (F,T) holds x in A

    proof

      let T be non empty TopSpace, A be Subset of T;

      A is closed iff ( Cl A) = A by PRE_TOPC: 22;

      hence A is closed implies for F be proper Filter of ( BoolePoset ( [#] T)) st A in F holds for x be Point of T st x is_a_cluster_point_of (F,T) holds x in A by Th25;

      assume

       A1: for F be proper Filter of ( BoolePoset ( [#] T)) st A in F holds for x be Point of T st x is_a_cluster_point_of (F,T) holds x in A;

      A = ( Cl A)

      proof

        thus A c= ( Cl A) by PRE_TOPC: 18;

        let x be object;

        assume

         A2: x in ( Cl A);

        then

        reconsider y = x as Element of T;

        ex F be proper Filter of ( BoolePoset ( [#] T)) st A in F & y is_a_cluster_point_of (F,T) by A2, Th25;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: YELLOW19:28

    for T be non empty TopSpace, A be Subset of T holds A is closed iff for F be ultra Filter of ( BoolePoset ( [#] T)) st A in F holds for x be Point of T st x is_a_convergence_point_of (F,T) holds x in A

    proof

      let T be non empty TopSpace, A be Subset of T;

      A is closed iff ( Cl A) = A by PRE_TOPC: 22;

      hence A is closed implies for F be ultra Filter of ( BoolePoset ( [#] T)) st A in F holds for x be Point of T st x is_a_convergence_point_of (F,T) holds x in A by Th26;

      assume

       A1: for F be ultra Filter of ( BoolePoset ( [#] T)) st A in F holds for x be Point of T st x is_a_convergence_point_of (F,T) holds x in A;

      A = ( Cl A)

      proof

        thus A c= ( Cl A) by PRE_TOPC: 18;

        let x be object;

        assume

         A2: x in ( Cl A);

        then

        reconsider y = x as Element of T;

        ex F be ultra Filter of ( BoolePoset ( [#] T)) st A in F & y is_a_convergence_point_of (F,T) by A2, Th26;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: YELLOW19:29



     Th29: for T be non empty TopSpace, N be net of T holds for s be Point of T holds s is_a_cluster_point_of N iff for A be Subset of T, N holds s in ( Cl A)

    proof

      let T be non empty TopSpace, N be net of T;

      let s be Point of T;

      thus s is_a_cluster_point_of N implies for A be Subset of T, N holds s in ( Cl A) by Th8, Th21;

      assume

       A1: for A be Subset of T, N holds s in ( Cl A);

      let V be a_neighborhood of s;

      let i be Element of N;

      reconsider A = ( rng the mapping of (N | i)) as Subset of T, N by Def2;

      set x = the Element of (A /\ ( Int V));



       A2: s in ( Int V) by CONNSP_2:def 1;

      s in ( Cl A) by A1;

      then A meets ( Int V) by A2, PRE_TOPC:def 7;

      then

       A3: (A /\ ( Int V)) <> ( {} T);

      then

       A4: x in ( Int V) by XBOOLE_0:def 4;



       A5: ( Int V) c= V by TOPS_1: 16;

      x in A by A3, XBOOLE_0:def 4;

      then

      consider j be object such that

       A6: j in ( dom the mapping of (N | i)) and

       A7: x = (the mapping of (N | i) . j) by FUNCT_1:def 3;



       A8: the carrier of (N | i) = { l where l be Element of N : i <= l } by WAYBEL_9: 12;

      reconsider j as Element of (N | i) by A6;

      ( dom the mapping of (N | i)) = the carrier of (N | i) by FUNCT_2:def 1;

      then

      consider l be Element of N such that

       A9: j = l and

       A10: i <= l by A6, A8;

      take l;

      thus i <= l by A10;

      x = ((N | i) . j) by A7

      .= (N . l) by A9, WAYBEL_9: 16;

      hence thesis by A4, A5;

    end;

    theorem :: YELLOW19:30

    for T be non empty TopSpace holds for F be Subset-Family of T st F is closed holds ( FinMeetCl F) is closed

    proof

      let T be non empty TopSpace;

      let F be Subset-Family of T such that

       A1: F is closed;

      now

        let P be Subset of T;

        assume P in ( FinMeetCl F);

        then

        consider Y be Subset-Family of T such that

         A2: Y c= F and Y is finite and

         A3: P = ( Intersect Y) by CANTOR_1:def 3;



         A4: P = the carrier of T & the carrier of T = ( [#] T) or P = ( meet Y) by A3, SETFAM_1:def 9;

        for A be Subset of T st A in Y holds A is closed by A1, A2;

        hence P is closed by A4, PRE_TOPC: 14;

      end;

      hence thesis;

    end;



     Lm1: for T be non empty TopSpace st T is compact holds for N be net of T holds ex x be Point of T st x is_a_cluster_point_of N

    proof

      let T be non empty TopSpace such that

       A1: T is compact;

      let N be net of T;

      set F = the set of all ( Cl A) where A be Subset of T, N;

      F c= ( bool the carrier of T)

      proof

        let x be object;

        assume x in F;

        then ex A be Subset of T, N st x = ( Cl A);

        hence thesis;

      end;

      then

      reconsider F as Subset-Family of T;

      set x = the Element of ( meet F);



       A2: F is centered

      proof

        defpred P[ object, object] means ex A be Subset of T, N, i be Element of N st $1 = ( Cl A) & $2 = i & A = ( rng the mapping of (N | i));

        set A0 = the Subset of T, N;

        ( Cl A0) in F;

        hence F <> {} ;

        let G be set such that

         A3: G <> {} and

         A4: G c= F and

         A5: G is finite;

         A6:

        now

          let x be object;

          assume x in G;

          then x in F by A4;

          then

          consider A be Subset of T, N such that

           A7: x = ( Cl A);

          consider i be Element of N such that

           A8: A = ( rng the mapping of (N | i)) by Def2;

          reconsider y = i as object;

          take y;

          thus y in the carrier of N;

          thus P[x, y] by A7, A8;

        end;

        consider f be Function such that

         A9: ( dom f) = G & ( rng f) c= the carrier of N and

         A10: for x be object st x in G holds P[x, (f . x)] from FUNCT_1:sch 6( A6);

        reconsider B = ( rng f) as finite Subset of N by A5, A9, FINSET_1: 8;

        ( [#] N) is directed by WAYBEL_0:def 6;

        then

        consider j be Element of N such that j in ( [#] N) and

         A11: j is_>=_than B by WAYBEL_0: 1;

        now

          let X;

          assume

           A12: X in G;

          then

          consider A be Subset of T, N, i be Element of N such that

           A13: X = ( Cl A) and

           A14: (f . X) = i and

           A15: A = ( rng the mapping of (N | i)) by A10;



           A16: A c= X by A13, PRE_TOPC: 18;



           A17: the mapping of (N | i) = (the mapping of N | the carrier of (N | i)) by WAYBEL_9:def 7;

          i in B by A9, A12, A14, FUNCT_1:def 3;

          then i <= j by A11, LATTICE3:def 9;

          then j in the carrier of (N | i) by WAYBEL_9:def 7;

          then

           A18: j in ( dom the mapping of (N | i)) by FUNCT_2:def 1;

          then (the mapping of (N | i) . j) in A by A15, FUNCT_1:def 3;

          then (N . j) in A by A18, A17, FUNCT_1: 47;

          hence (N . j) in X by A16;

        end;

        hence thesis by A3, SETFAM_1:def 1;

      end;

      F is closed

      proof

        let S be Subset of T;

        assume S in F;

        then ex A be Subset of T, N st S = ( Cl A);

        hence thesis;

      end;

      then

       A19: ( meet F) <> {} by A1, A2, COMPTS_1: 4;

      then x in ( meet F);

      then

      reconsider x as Point of T;

      take x;

      now

        let A be Subset of T, N;

        ( Cl A) in F;

        hence x in ( Cl A) by A19, SETFAM_1:def 1;

      end;

      hence thesis by Th29;

    end;



     Lm2: for T be non empty TopSpace st for N be net of T st N in ( NetUniv T) holds ex x be Point of T st x is_a_cluster_point_of N holds T is compact

    proof

      let T be non empty TopSpace;

      assume

       A1: for N be net of T st N in ( NetUniv T) holds ex x be Point of T st x is_a_cluster_point_of N;

      now

        set X = the carrier of T;

        defpred P[ object, object] means ex A be set st A = $1 & $2 in A;

        let F be Subset-Family of T such that

         A2: F is centered and

         A3: F is closed;

        set G = ( FinMeetCl F);

         A4:

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          set y = the Element of xx;

          assume x in G;

          then

          consider Y be Subset-Family of T such that

           A5: Y c= F and

           A6: Y is finite and

           A7: x = ( Intersect Y) by CANTOR_1:def 3;

          x = the carrier of T or x = ( meet Y) & ( meet Y) <> {} by A2, A5, A6, A7, SETFAM_1:def 9;

          then y in xx;

          hence ex y be object st y in the carrier of T & P[x, y] by A7;

        end;

        consider f be Function such that

         A8: ( dom f) = G & ( rng f) c= the carrier of T and

         A9: for a be object st a in G holds P[a, (f . a)] from FUNCT_1:sch 6( A4);



         A10: F c= G by CANTOR_1: 4;



         A11: F <> {} by A2;

        then

        reconsider G as non empty Subset-Family of T by A10;

        set R = (( InclPoset G) opp );



         A12: ( InclPoset G) = RelStr (# G, ( RelIncl G) #) by YELLOW_1:def 1;

        then

         A13: the carrier of R = G by YELLOW_6: 3;

        R is directed

        proof

          let x,y be Element of R such that x in ( [#] R) and y in ( [#] R);



           A14: ( ~ x) = x by LATTICE3:def 7;

          y in G by A13;

          then

          consider Y be Subset-Family of T such that

           A15: Y c= F and

           A16: Y is finite and

           A17: y = ( Intersect Y) by CANTOR_1:def 3;

          x in G by A13;

          then

          consider X be Subset-Family of T such that

           A18: X c= F and

           A19: X is finite and

           A20: x = ( Intersect X) by CANTOR_1:def 3;

          set z = ( Intersect (X \/ Y));

          (X \/ Y) c= F by A18, A15, XBOOLE_1: 8;

          then

          reconsider z as Element of R by A13, A19, A16, CANTOR_1:def 3;



           A21: ( ~ z) = z by LATTICE3:def 7;

          take z;

          thus z in ( [#] R);



           A22: ( ~ y) = y by LATTICE3:def 7;

          z c= y by A17, SETFAM_1: 44, XBOOLE_1: 7;

          then

           A23: ( ~ z) <= ( ~ y) by A22, A21, YELLOW_1: 3;

          z c= x by A20, SETFAM_1: 44, XBOOLE_1: 7;

          then ( ~ z) <= ( ~ x) by A14, A21, YELLOW_1: 3;

          hence x <= z & y <= z by A23, YELLOW_7: 1;

        end;

        then

        reconsider R as directed non empty transitive RelStr;

        reconsider f as Function of the carrier of R, the carrier of T by A8, A13, FUNCT_2: 2;

        set N = (R *' f);



         A24: the RelStr of N = the RelStr of R by WAYBEL32:def 3;



         A25: ( the_universe_of X) = ( Tarski-Class ( the_transitive-closure_of X)) by YELLOW_6:def 1;

        X c= ( the_transitive-closure_of X) by CLASSES1: 52;

        then X in ( Tarski-Class ( the_transitive-closure_of X)) by CLASSES1: 2, CLASSES1: 3;

        then ( bool X) in ( Tarski-Class ( the_transitive-closure_of X)) by CLASSES1: 4;

        then G in ( Tarski-Class ( the_transitive-closure_of X)) by CLASSES1: 3;

        then N in ( NetUniv T) by A13, A24, A25, YELLOW_6:def 11;

        then

        consider x be Point of T such that

         A26: x is_a_cluster_point_of N by A1;



         A27: the mapping of N = f by WAYBEL32:def 3;

        now

          let X;

          assume

           A28: X in F;

          then

          reconsider A = X as Subset of T;

          reconsider a = X as Element of N by A10, A12, A24, A28, YELLOW_6: 3;

           A29:

          now

            let V be Subset of T;

            assume that

             A30: V is open and

             A31: x in V;

            ( Int V) = V by A30, TOPS_1: 23;

            then V is a_neighborhood of x by A31, CONNSP_2:def 1;

            then N is_often_in V by A26;

            then

            consider b be Element of N such that

             A32: a <= b and

             A33: (N . b) in V;

            reconsider a9 = a, b9 = b as Element of (( InclPoset G) opp ) by A24;

            a9 <= b9 by A24, A32, YELLOW_0: 1;

            then

             A34: ( ~ a9) >= ( ~ b9) by YELLOW_7: 1;



             A35: ( ~ b9) = b by LATTICE3:def 7;

            ( ~ a9) = A by LATTICE3:def 7;

            then

             A36: b c= A by A34, A35, YELLOW_1: 3;

             P[b, (f . b)] by A9, A12, A35;

            then (N . b) in b by A27;

            hence A meets V by A33, A36, XBOOLE_0: 3;

          end;

          A is closed by A3, A28;

          then ( Cl A) = A by PRE_TOPC: 22;

          hence x in X by A29, PRE_TOPC:def 7;

        end;

        hence ( meet F) <> {} by A11, SETFAM_1:def 1;

      end;

      hence thesis by COMPTS_1: 4;

    end;

    theorem :: YELLOW19:31



     Th31: for T be non empty TopSpace holds T is compact iff for F be ultra Filter of ( BoolePoset ( [#] T)) holds ex x be Point of T st x is_a_convergence_point_of (F,T)

    proof

      let T be non empty TopSpace;

      set X = the carrier of T;

      hereby

        assume

         A1: T is compact;

        let F be ultra Filter of ( BoolePoset ( [#] T));

        set G = { ( Cl A) where A be Subset of T : A in F };

        G c= ( bool the carrier of T)

        proof

          let x be object;

          assume x in G;

          then ex A be Subset of T st x = ( Cl A) & A in F;

          hence thesis;

        end;

        then

        reconsider G as Subset-Family of T;



         A2: G is centered

        proof

          set A0 = the Element of F;

          reconsider A0 as Subset of T by WAYBEL_7: 2;

          ( Cl A0) in G;

          hence G <> {} ;

          let H be set;

          assume that

           A3: H <> {} and

           A4: H c= G and

           A5: H is finite;

          reconsider H1 = H as finite Subset-Family of X by A4, A5, XBOOLE_1: 1;

          H1 c= F

          proof

            let x be object;

            assume x in H1;

            then x in G by A4;

            then

            consider A be Subset of T such that

             A6: x = ( Cl A) and

             A7: A in F;

            A c= ( Cl A) by PRE_TOPC: 18;

            hence thesis by A6, A7, WAYBEL_7: 7;

          end;

          then ( Intersect H1) in F by WAYBEL_7: 11;

          then ( Intersect H1) <> {} by Th1;

          hence thesis by A3, SETFAM_1:def 9;

        end;

        set x = the Element of ( meet G);

        G is closed

        proof

          let A be Subset of T;

          assume A in G;

          then ex B be Subset of T st A = ( Cl B) & B in F;

          hence thesis;

        end;

        then

         A8: ( meet G) <> {} by A1, A2, COMPTS_1: 4;

        then x in ( meet G);

        then

        reconsider x as Point of T;

        take x;

        thus x is_a_convergence_point_of (F,T)

        proof

          let A be Subset of T such that

           A9: A is open and

           A10: x in A;

          set B = (A ` );

           A11:

          now

            assume B in F;

            then ( Cl B) in G;

            then

             A12: B in G by A9, PRE_TOPC: 22;

             not x in B by A10, XBOOLE_0:def 5;

            hence contradiction by A8, A12, SETFAM_1:def 1;

          end;

          F is prime by WAYBEL_7: 22;

          hence thesis by A11, WAYBEL_7: 21;

        end;

      end;

      assume

       A13: for F be ultra Filter of ( BoolePoset ( [#] T)) holds ex x be Point of T st x is_a_convergence_point_of (F,T);

      now

        set L = ( BoolePoset X);

        let F be Subset-Family of T such that

         A14: F is centered closed;

        reconsider Y = F as Subset of ( BoolePoset X) by WAYBEL_7: 2;

        set G = ( uparrow ( fininfs Y));

        now

          assume ( Bottom L) in G;

          then

          consider x be Element of ( BoolePoset X) such that

           A15: x <= ( Bottom L) and

           A16: x in ( fininfs Y) by WAYBEL_0:def 16;



           A17: ( Bottom L) = {} by YELLOW_1: 18;

          consider Z be finite Subset of Y such that

           A18: x = ( "/\" (Z,L)) and ex_inf_of (Z,L) by A16;

          reconsider Z as Subset of L by XBOOLE_1: 1;



           A19: x = ( Bottom L) by A15, YELLOW_5: 19;

          then x <> ( Top L) by WAYBEL_7: 3;

          then

           A20: Z <> {} by A18, YELLOW_0:def 12;

          then ( meet Z) <> {} by A14;

          hence contradiction by A17, A18, A19, A20, YELLOW_1: 20;

        end;

        then G is proper;

        then

        consider UF be Filter of L such that

         A21: G c= UF and

         A22: UF is ultra by WAYBEL_7: 26;

        consider x be Point of T such that

         A23: x is_a_convergence_point_of (UF,T) by A13, A22;

        F c= G by WAYBEL_0: 62;

        then

         A24: F c= UF by A21;

         A25:

        now

          let A be set;

          assume

           A26: A in F;

          then

          reconsider B = A as Subset of T;

           A27:

          now

            let C be Subset of T;

            assume that

             A28: C is open and

             A29: x in C;



             A30: C in UF by A23, A28, A29;

            A in UF by A24, A26;

            then

            reconsider c = C, a = A as Element of L by A30;

            (a "/\" c) in UF by A24, A26, A30, WAYBEL_0: 41;

            then (a "/\" c) <> {} by A22, Th1;

            then (A /\ C) <> {} by YELLOW_1: 17;

            hence A meets C;

          end;

          B is closed by A14, A26;

          then ( Cl B) = B by PRE_TOPC: 22;

          hence x in A by A27, PRE_TOPC: 24;

        end;

        F <> {} by A14;

        hence ( meet F) <> {} by A25, SETFAM_1:def 1;

      end;

      hence thesis by COMPTS_1: 4;

    end;

    theorem :: YELLOW19:32

    for T be non empty TopSpace holds T is compact iff for F be proper Filter of ( BoolePoset ( [#] T)) holds ex x be Point of T st x is_a_cluster_point_of (F,T)

    proof

      let T be non empty TopSpace;

      hereby

        assume

         A1: T is compact;

        let F be proper Filter of ( BoolePoset ( [#] T));

        reconsider G = F as proper Filter of ( BoolePoset ( [#] T));

        consider x be Point of T such that

         A2: x is_a_cluster_point_of ( a_net G) by A1, Lm1;

        take x;

        thus x is_a_cluster_point_of (F,T) by A2, Th16;

      end;

      assume

       A3: for F be proper Filter of ( BoolePoset ( [#] T)) holds ex x be Point of T st x is_a_cluster_point_of (F,T);

      now

        let N be net of T such that N in ( NetUniv T);

        reconsider F = ( a_filter N) as proper Filter of ( BoolePoset the carrier of T);

        consider x be Point of T such that

         A4: x is_a_cluster_point_of (F,T) by A3;

        take x;

        thus x is_a_cluster_point_of N by A4, Th11;

      end;

      hence thesis by Lm2;

    end;

    theorem :: YELLOW19:33



     Th33: for T be non empty TopSpace holds T is compact iff for N be net of T holds ex x be Point of T st x is_a_cluster_point_of N

    proof

      let T be non empty TopSpace;

      thus T is compact implies for N be net of T holds ex x be Point of T st x is_a_cluster_point_of N by Lm1;

      assume for N be net of T holds ex x be Point of T st x is_a_cluster_point_of N;

      then for N be net of T st N in ( NetUniv T) holds ex x be Point of T st x is_a_cluster_point_of N;

      hence thesis by Lm2;

    end;

    theorem :: YELLOW19:34

    for T be non empty TopSpace holds T is compact iff for N be net of T st N in ( NetUniv T) holds ex x be Point of T st x is_a_cluster_point_of N by Lm1, Lm2;

    registration

      let L be non empty 1-sorted;

      let N be transitive NetStr over L;

      cluster -> transitive for full SubNetStr of N;

      coherence

      proof

        let S be full SubNetStr of N;

        S is full SubRelStr of N by YELLOW_6:def 7;

        hence thesis;

      end;

    end

    registration

      let L be non empty 1-sorted;

      let N be non empty directed NetStr over L;

      cluster strict non empty directed full for SubNetStr of N;

      existence

      proof

        set S = the NetStr of N;



         A1: the RelStr of N = the RelStr of N;

        N is full SubRelStr of N by YELLOW_6: 6;

        then

         A2: S is full SubRelStr of N by A1, WAYBEL21: 12;

        the mapping of S = (the mapping of N | the carrier of S);

        then

        reconsider S as strict non empty full SubNetStr of N by A2, YELLOW_6:def 6, YELLOW_6:def 7;

        ( [#] N) is directed by WAYBEL_0:def 6;

        then ( [#] S) is directed by A1, WAYBEL_0: 3;

        then S is directed;

        hence thesis;

      end;

    end

    theorem :: YELLOW19:35

    for T be non empty TopSpace holds T is compact iff for N be net of T holds ex S be subnet of N st S is convergent

    proof

      let T be non empty TopSpace;

      hereby

        assume

         A1: T is compact;

        let N be net of T;

        consider x be Point of T such that

         A2: x is_a_cluster_point_of N by A1, Th33;

        consider S be subnet of N such that

         A3: x in ( Lim S) by A2, WAYBEL_9: 32;

        take S;

        thus S is convergent by A3, YELLOW_6:def 16;

      end;

      assume

       A4: for N be net of T holds ex S be subnet of N st S is convergent;

      now

        let N be net of T;

        consider S be subnet of N such that

         A5: S is convergent by A4;

        set x = the Element of ( Lim S);



         A6: ( Lim S) <> {} by A5, YELLOW_6:def 16;

        then x in ( Lim S);

        then

        reconsider x as Point of T;

        take x;

        thus x is_a_cluster_point_of N by A6, WAYBEL_9: 29, WAYBEL_9: 31;

      end;

      hence thesis by Th33;

    end;

    definition

      let S be non empty 1-sorted;

      let N be non empty NetStr over S;

      :: YELLOW19:def5

      attr N is Cauchy means for A be Subset of S holds N is_eventually_in A or N is_eventually_in (A ` );

    end

    registration

      let S be non empty 1-sorted;

      let F be ultra Filter of ( BoolePoset ( [#] S));

      cluster ( a_net F) -> Cauchy;

      coherence

      proof

        let A be Subset of S;

        F is prime by WAYBEL_7: 22;

        then

         A1: (A is empty or A is non empty) & ((A ` ) is empty or (A ` ) is non empty) & A in F or (A ` ) in F by WAYBEL_7: 21;

        (( {} S) ` ) = ( [#] S);

        then (A ` ) = ( {} S) implies A = ( [#] S);

        hence thesis by A1, Th15, YELLOW_6: 20;

      end;

    end

    theorem :: YELLOW19:36

    for T be non empty TopSpace holds T is compact iff for N be net of T st N is Cauchy holds N is convergent

    proof

      let T be non empty TopSpace;

      thus T is compact implies for N be net of T st N is Cauchy holds N is convergent

      proof

        assume

         A1: T is compact;

        let N be net of T such that

         A2: for A be Subset of T holds N is_eventually_in A or N is_eventually_in (A ` );

        consider x be Point of T such that

         A3: x is_a_cluster_point_of N by A1, Lm1;

        now

          let V be a_neighborhood of x;

          assume not N is_eventually_in V;

          then N is_eventually_in (V ` ) by A2;

          then

          consider i be Element of N such that

           A4: for j be Element of N st i <= j holds (N . j) in (V ` );

          N is_often_in V by A3;

          then

          consider j be Element of N such that

           A5: i <= j and

           A6: (N . j) in V;

          (N . j) in (V ` ) by A4, A5;

          hence contradiction by A6, XBOOLE_0:def 5;

        end;

        then x in ( Lim N) by YELLOW_6:def 15;

        hence thesis by YELLOW_6:def 16;

      end;

      assume

       A7: for N be net of T st N is Cauchy holds N is convergent;

      now

        let F be ultra Filter of ( BoolePoset ( [#] T));

        set x = the Element of ( Lim ( a_net F));

        ( a_net F) is convergent by A7;

        then

         A8: ( Lim ( a_net F)) <> {} by YELLOW_6:def 16;

        then x in ( Lim ( a_net F));

        then

        reconsider x as Point of T;

        take x;

        thus x is_a_convergence_point_of (F,T) by A8, Th17;

      end;

      hence thesis by Th31;

    end;