yellow_6.miz



    begin

    reserve x,y,z,X for set,

T for Universe;

    definition

      let X;

      :: YELLOW_6:def1

      func the_universe_of X -> set equals ( Tarski-Class ( the_transitive-closure_of X));

      correctness ;

    end

    registration

      let X;

      cluster ( the_universe_of X) -> epsilon-transitive Tarski;

      coherence ;

    end

    registration

      let X;

      cluster ( the_universe_of X) -> universal non empty;

      coherence ;

    end

    theorem :: YELLOW_6:1

    

     Th1: for f be Function st ( dom f) in T & ( rng f) c= T holds ( product f) in T

    proof

      let f be Function such that

       A1: ( dom f) in T and

       A2: ( rng f) c= T;

      ( card ( dom f)) in ( card T) by A1, CLASSES2: 1;

      then ( card ( rng f)) in ( card T) by CARD_2: 61, ORDINAL1: 12;

      then ( rng f) in T by A2, CLASSES1: 1;

      then ( union ( rng f)) in T by CLASSES2: 59;

      then ( Union f) in T by CARD_3:def 4;

      then ( product f) c= ( Funcs (( dom f),( Union f))) & ( Funcs (( dom f),( Union f))) in T by A1, CLASSES2: 61, FUNCT_6: 1;

      hence thesis by CLASSES1:def 1;

    end;

    begin

    begin

    theorem :: YELLOW_6:2

    

     Th2: for Y be non empty set holds for J be 1-sorted-yielding ManySortedSet of Y, i be Element of Y holds (( Carrier J) . i) = the carrier of (J . i)

    proof

      let Y be non empty set;

      let J be 1-sorted-yielding ManySortedSet of Y, i be Element of Y;

      ex R be 1-sorted st R = (J . i) & (( Carrier J) . i) = the carrier of R by PRALG_1:def 15;

      hence thesis;

    end;

    registration

      cluster non empty constant 1-sorted-yielding for Function;

      existence

      proof

        set S = the 1-sorted;

        take f = ( { {} } --> S);

        thus f is non empty;

        thus f is constant;

        let x be object;

        assume x in ( dom f);

        hence thesis by FUNCOP_1: 7;

      end;

    end

    notation

      let J be 1-sorted-yielding Function;

      synonym J is yielding_non-empty_carriers for J is non-Empty;

    end

    definition

      let J be 1-sorted-yielding Function;

      :: original: yielding_non-empty_carriers

      redefine

      :: YELLOW_6:def2

      attr J is yielding_non-empty_carriers means

      : Def2: for i be set st i in ( rng J) holds i is non empty 1-sorted;

      compatibility

      proof

        hereby

          assume

           A1: J is non-Empty;

          let i be set;

          assume

           A2: i in ( rng J);

          then ex x be object st x in ( dom J) & i = (J . x) by FUNCT_1:def 3;

          hence i is non empty 1-sorted by A1, A2, PRALG_1:def 11;

        end;

        assume

         A3: for i be set st i in ( rng J) holds i is non empty 1-sorted;

        let S be 1-sorted;

        thus thesis by A3;

      end;

    end

    registration

      let X be set;

      let L be 1-sorted;

      cluster (X --> L) -> 1-sorted-yielding;

      coherence

      proof

        let x be object;

        set IT = (X --> L);

        assume x in ( dom IT);

        then (IT . x) in ( rng IT) by FUNCT_1:def 3;

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let I be set;

      cluster yielding_non-empty_carriers for 1-sorted-yielding ManySortedSet of I;

      existence

      proof

        set R = the non empty 1-sorted;

        take (I --> R);

        let i be set;

        assume i in ( rng (I --> R));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let I be non empty set;

      let J be RelStr-yielding ManySortedSet of I;

      cluster the carrier of ( product J) -> functional;

      coherence

      proof

        ( product ( Carrier J)) is functional;

        hence thesis by YELLOW_1:def 4;

      end;

    end

    registration

      let I be set;

      let J be yielding_non-empty_carriers 1-sorted-yielding ManySortedSet of I;

      cluster ( Carrier J) -> non-empty;

      coherence

      proof

        assume {} in ( rng ( Carrier J));

        then

        consider i be object such that

         A1: i in ( dom ( Carrier J)) and

         A2: (( Carrier J) . i) = {} by FUNCT_1:def 3;

        

         A3: i in I by A1;

        then

        consider R be 1-sorted such that

         A4: R = (J . i) and

         A5: (( Carrier J) . i) = the carrier of R by PRALG_1:def 15;

        

         A6: R is empty by A2, A5;

        i in ( dom J) by A3, PARTFUN1:def 2;

        then R in ( rng J) by A4, FUNCT_1:def 3;

        hence contradiction by A6, Def2;

      end;

    end

    begin

    registration

      let T be non empty RelStr, A be lower Subset of T;

      cluster (A ` ) -> upper;

      coherence

      proof

        let x,y be Element of T such that

         A1: x in (A ` ) and

         A2: x <= y;

         not x in A by A1, XBOOLE_0:def 5;

        then not y in A by A2, WAYBEL_0:def 19;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    registration

      let T be non empty RelStr, A be upper Subset of T;

      cluster (A ` ) -> lower;

      coherence

      proof

        let x,y be Element of T such that

         A1: x in (A ` ) and

         A2: y <= x;

         not x in A by A1, XBOOLE_0:def 5;

        then not y in A by A2, WAYBEL_0:def 20;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    definition

      let N be non empty RelStr;

      :: original: directed

      redefine

      :: YELLOW_6:def3

      attr N is directed means

      : Def3: for x,y be Element of N holds ex z be Element of N st x <= z & y <= z;

      compatibility

      proof

        hereby

          assume

           A1: N is directed;

          let x,y be Element of N;

          ( [#] N) is directed by A1;

          then ex z be Element of N st z in ( [#] N) & x <= z & y <= z;

          hence ex z be Element of N st x <= z & y <= z;

        end;

        assume

         A2: for x,y be Element of N holds ex z be Element of N st x <= z & y <= z;

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

        consider z be Element of N such that

         A3: x <= z & y <= z by A2;

        take z;

        thus z in ( [#] N);

        thus thesis by A3;

      end;

    end

    registration

      let X be set;

      cluster ( BoolePoset X) -> directed;

      coherence ;

    end

    registration

      cluster non empty directed transitive strict for RelStr;

      existence

      proof

        take ( BoolePoset {} );

        thus thesis;

      end;

    end

    

     Lm1: for N be non empty RelStr holds N is directed iff the RelStr of N is directed

    proof

      let N be non empty RelStr;

      thus N is directed implies the RelStr of N is directed

      proof

        assume

         A1: N is directed;

        let x,y be Element of the RelStr of N;

        reconsider x9 = x, y9 = y as Element of N;

        consider z9 be Element of N such that

         A2: x9 <= z9 & y9 <= z9 by A1;

        reconsider z = z9 as Element of the RelStr of N;

        take z;

         [x, z] in the InternalRel of N & [y, z] in the InternalRel of N by A2, ORDERS_2:def 5;

        hence thesis by ORDERS_2:def 5;

      end;

      assume

       A3: the RelStr of N is directed;

      let x,y be Element of N;

      reconsider x9 = x, y9 = y as Element of the RelStr of N;

      consider z9 be Element of the RelStr of N such that

       A4: x9 <= z9 & y9 <= z9 by A3;

      reconsider z = z9 as Element of N;

      take z;

       [x9, z9] in the InternalRel of the RelStr of N & [y9, z9] in the InternalRel of the RelStr of N by A4, ORDERS_2:def 5;

      hence thesis by ORDERS_2:def 5;

    end;

    

     Lm2: for N be non empty RelStr holds N is transitive iff the RelStr of N is transitive

    proof

      let N be non empty RelStr;

      thus N is transitive implies the RelStr of N is transitive

      proof

        assume

         A1: N is transitive;

        let x,y,z be Element of the RelStr of N such that

         A2: x <= y and

         A3: y <= z;

        reconsider x9 = x, y9 = y, z9 = z as Element of N;

         [y, z] in the InternalRel of the RelStr of N by A3, ORDERS_2:def 5;

        then

         A4: y9 <= z9 by ORDERS_2:def 5;

         [x, y] in the InternalRel of the RelStr of N by A2, ORDERS_2:def 5;

        then x9 <= y9 by ORDERS_2:def 5;

        then x9 <= z9 by A1, A4;

        then [x9, z9] in the InternalRel of N by ORDERS_2:def 5;

        hence thesis by ORDERS_2:def 5;

      end;

      assume

       A5: the RelStr of N is transitive;

      let x,y,z be Element of N such that

       A6: x <= y and

       A7: y <= z;

      reconsider x9 = x, y9 = y, z9 = z as Element of the RelStr of N;

       [y9, z9] in the InternalRel of the RelStr of N by A7, ORDERS_2:def 5;

      then

       A8: y9 <= z9 by ORDERS_2:def 5;

       [x9, y9] in the InternalRel of the RelStr of N by A6, ORDERS_2:def 5;

      then x9 <= y9 by ORDERS_2:def 5;

      then x9 <= z9 by A5, A8;

      then [x, z] in the InternalRel of N by ORDERS_2:def 5;

      hence thesis by ORDERS_2:def 5;

    end;

    registration

      let I be set;

      cluster yielding_non-empty_carriers for RelStr-yielding ManySortedSet of I;

      existence

      proof

        set R = the non empty RelStr;

        take (I --> R);

        let i be set;

        assume i in ( rng (I --> R));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let I be non empty set;

      let J be yielding_non-empty_carriers RelStr-yielding ManySortedSet of I;

      cluster ( product J) -> non empty;

      coherence ;

    end

    registration

      let Y1,Y2 be directed RelStr;

      cluster [:Y1, Y2:] -> directed;

      coherence

      proof

        reconsider S2 = ( [#] Y2) as directed Subset of Y2 by WAYBEL_0:def 6;

        reconsider S1 = ( [#] Y1) as directed Subset of Y1 by WAYBEL_0:def 6;

         [:S1, S2:] is directed;

        then ( [#] [:Y1, Y2:]) is directed by YELLOW_3:def 2;

        hence thesis;

      end;

    end

    theorem :: YELLOW_6:3

    

     Th3: for R be RelStr holds the carrier of R = the carrier of (R ~ )

    proof

      let R be RelStr;

      (R ~ ) = RelStr (# the carrier of R, (the InternalRel of R ~ ) #) by LATTICE3:def 5;

      hence thesis;

    end;

    

     Lm3: for R,S be RelStr, p,q be Element of R, p9,q9 be Element of S st p = p9 & q = q9 & the RelStr of R = the RelStr of S holds p <= q implies p9 <= q9

    proof

      let R,S be RelStr, p,q be Element of R, p9,q9 be Element of S such that

       A1: p = p9 & q = q9 & the RelStr of R = the RelStr of S;

      assume p <= q;

      then [p9, q9] in the InternalRel of S by A1, ORDERS_2:def 5;

      hence thesis by ORDERS_2:def 5;

    end;

    definition

      let S be 1-sorted, N be NetStr over S;

      :: YELLOW_6:def4

      attr N is constant means

      : Def4: the mapping of N is constant;

    end

    definition

      let R be RelStr, T be non empty 1-sorted, p be Element of T;

      :: YELLOW_6:def5

      func ConstantNet (R,p) -> strict NetStr over T means

      : Def5: the RelStr of it = the RelStr of R & the mapping of it = (the carrier of it --> p);

      existence

      proof

        reconsider f = (the carrier of R --> p) as Function of R, T;

        take NetStr (# the carrier of R, the InternalRel of R, f #);

        thus thesis;

      end;

      correctness ;

    end

    registration

      let R be RelStr, T be non empty 1-sorted, p be Element of T;

      cluster ( ConstantNet (R,p)) -> constant;

      coherence

      proof

        (the carrier of ( ConstantNet (R,p)) --> p) is constant;

        hence the mapping of ( ConstantNet (R,p)) is constant by Def5;

      end;

    end

    registration

      let R be non empty RelStr, T be non empty 1-sorted, p be Element of T;

      cluster ( ConstantNet (R,p)) -> non empty;

      coherence

      proof

         the RelStr of ( ConstantNet (R,p)) = the RelStr of R by Def5;

        hence the carrier of ( ConstantNet (R,p)) is non empty;

      end;

    end

    registration

      let R be non empty directed RelStr, T be non empty 1-sorted, p be Element of T;

      cluster ( ConstantNet (R,p)) -> directed;

      coherence

      proof

         the RelStr of ( ConstantNet (R,p)) = the RelStr of R & the RelStr of R is directed by Def5, Lm1;

        hence thesis by Lm1;

      end;

    end

    registration

      let R be non empty transitive RelStr, T be non empty 1-sorted, p be Element of T;

      cluster ( ConstantNet (R,p)) -> transitive;

      coherence

      proof

         the RelStr of ( ConstantNet (R,p)) = the RelStr of R & the RelStr of R is transitive by Def5, Lm2;

        hence thesis by Lm2;

      end;

    end

    theorem :: YELLOW_6:4

    

     Th4: for R be RelStr, T be non empty 1-sorted, p be Element of T holds the carrier of ( ConstantNet (R,p)) = the carrier of R

    proof

      let R be RelStr, T be non empty 1-sorted, p be Element of T;

       the RelStr of ( ConstantNet (R,p)) = the RelStr of R by Def5;

      hence thesis;

    end;

    theorem :: YELLOW_6:5

    

     Th5: for R be non empty RelStr, T be non empty 1-sorted, p be Element of T, q be Element of ( ConstantNet (R,p)) holds (( ConstantNet (R,p)) . q) = p

    proof

      let R be non empty RelStr, T be non empty 1-sorted, p be Element of T, q be Element of ( ConstantNet (R,p));

      

      thus (( ConstantNet (R,p)) . q) = ((the carrier of ( ConstantNet (R,p)) --> p) . q) by Def5

      .= p;

    end;

    registration

      let T be non empty 1-sorted, N be non empty NetStr over T;

      cluster the mapping of N -> non empty;

      coherence ;

    end

    begin

    theorem :: YELLOW_6:6

    

     Th6: for R be RelStr holds R is full SubRelStr of R

    proof

      let R be RelStr;

      the InternalRel of R c= the InternalRel of R;

      then

      reconsider R9 = R as SubRelStr of R by YELLOW_0:def 13;

      the InternalRel of R9 = (the InternalRel of R |_2 the carrier of R9) by XBOOLE_1: 28;

      hence thesis by YELLOW_0:def 14;

    end;

    theorem :: YELLOW_6:7

    

     Th7: for R be RelStr, S be SubRelStr of R, T be SubRelStr of S holds T is SubRelStr of R

    proof

      let R be RelStr, S be SubRelStr of R, T be SubRelStr of S;

      the InternalRel of S c= the InternalRel of R & the InternalRel of T c= the InternalRel of S by YELLOW_0:def 13;

      then

       A1: the InternalRel of T c= the InternalRel of R;

      the carrier of S c= the carrier of R & the carrier of T c= the carrier of S by YELLOW_0:def 13;

      then the carrier of T c= the carrier of R;

      hence thesis by A1, YELLOW_0:def 13;

    end;

    definition

      let S be 1-sorted, N be NetStr over S;

      :: YELLOW_6:def6

      mode SubNetStr of N -> NetStr over S means

      : Def6: it is SubRelStr of N & the mapping of it = (the mapping of N | the carrier of it );

      existence

      proof

        take N;

        thus N is SubRelStr of N by Th6;

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

      end;

    end

    theorem :: YELLOW_6:8

    for S be 1-sorted, N be NetStr over S holds N is SubNetStr of N

    proof

      let S be 1-sorted, N be NetStr over S;

      N is SubRelStr of N & the mapping of N = (the mapping of N | the carrier of N) by Th6;

      hence thesis by Def6;

    end;

    theorem :: YELLOW_6:9

    for Q be 1-sorted, R be NetStr over Q, S be SubNetStr of R, T be SubNetStr of S holds T is SubNetStr of R

    proof

      let Q be 1-sorted, R be NetStr over Q, S be SubNetStr of R, T be SubNetStr of S;

      

       A1: T is SubRelStr of S by Def6;

      then

       A2: the carrier of T c= the carrier of S by YELLOW_0:def 13;

      

       A3: the mapping of T = (the mapping of S | the carrier of T) by Def6

      .= ((the mapping of R | the carrier of S) | the carrier of T) by Def6

      .= (the mapping of R | (the carrier of S /\ the carrier of T)) by RELAT_1: 71

      .= (the mapping of R | the carrier of T) by A2, XBOOLE_1: 28;

      S is SubRelStr of R by Def6;

      then T is SubRelStr of R by A1, Th7;

      hence thesis by A3, Def6;

    end;

    

     Lm4: for S be 1-sorted, R be NetStr over S holds the NetStr of R is SubNetStr of R

    proof

      let S be 1-sorted, N be NetStr over S;

       the NetStr of N is SubRelStr of N & the mapping of the NetStr of N = (the mapping of N | the carrier of the NetStr of N) by YELLOW_0:def 13;

      hence thesis by Def6;

    end;

    definition

      let S be 1-sorted, N be NetStr over S, M be SubNetStr of N;

      :: YELLOW_6:def7

      attr M is full means

      : Def7: M is full SubRelStr of N;

    end

    

     Lm5: for S be 1-sorted, R be NetStr over S holds the NetStr of R is full SubRelStr of R

    proof

      let S be 1-sorted, R be NetStr over S;

      reconsider R9 = the NetStr of R as SubRelStr of R by YELLOW_0:def 13;

      the InternalRel of R9 = (the InternalRel of R |_2 the carrier of R9) by XBOOLE_1: 28;

      hence thesis by YELLOW_0:def 14;

    end;

    registration

      let S be 1-sorted, N be NetStr over S;

      cluster full strict for SubNetStr of N;

      existence

      proof

        reconsider M = the NetStr of N as SubNetStr of N by Lm4;

        take M;

        thus M is full SubRelStr of N by Lm5;

        thus thesis;

      end;

    end

    registration

      let S be 1-sorted, N be non empty NetStr over S;

      cluster full non empty strict for SubNetStr of N;

      existence

      proof

        reconsider M = the NetStr of N as SubNetStr of N by Lm4;

        take M;

        thus M is full SubRelStr of N by Lm5;

        thus thesis;

      end;

    end

    theorem :: YELLOW_6:10

    

     Th10: for S be 1-sorted, N be NetStr over S, M be SubNetStr of N holds the carrier of M c= the carrier of N

    proof

      let S be 1-sorted, N be NetStr over S, M be SubNetStr of N;

      M is SubRelStr of N by Def6;

      hence thesis by YELLOW_0:def 13;

    end;

    theorem :: YELLOW_6:11

    

     Th11: for S be 1-sorted, N be NetStr over S, M be SubNetStr of N, x,y be Element of N, i,j be Element of M st x = i & y = j & i <= j holds x <= y

    proof

      let S be 1-sorted, N be NetStr over S, M be SubNetStr of N, x,y be Element of N, i,j be Element of M such that

       A1: x = i & y = j and

       A2: i <= j;

      reconsider M as SubRelStr of N by Def6;

      reconsider i9 = i, j9 = j as Element of M;

      i9 <= j9 by A2;

      hence thesis by A1, YELLOW_0: 59;

    end;

    theorem :: YELLOW_6:12

    

     Th12: for S be 1-sorted, N be non empty NetStr over S, M be non empty full SubNetStr of N, x,y be Element of N, i,j be Element of M st x = i & y = j & x <= y holds i <= j

    proof

      let S be 1-sorted, N be non empty NetStr over S, M be non empty full SubNetStr of N, x,y be Element of N, i,j be Element of M such that

       A1: x = i & y = j & x <= y;

      reconsider M as full non empty SubRelStr of N by Def7;

      reconsider i9 = i, j9 = j as Element of M;

      i9 <= j9 by A1, YELLOW_0: 60;

      hence thesis;

    end;

    begin

    registration

      let T be non empty 1-sorted;

      cluster constant strict for net of T;

      existence

      proof

        set R = the non empty directed transitive RelStr, p = the Element of T;

        take ( ConstantNet (R,p));

        thus thesis;

      end;

    end

    registration

      let T be non empty 1-sorted, N be constant NetStr over T;

      cluster the mapping of N -> constant;

      coherence by Def4;

    end

    definition

      let T be non empty 1-sorted, N be NetStr over T;

      assume

       A1: N is constant non empty;

      :: YELLOW_6:def8

      func the_value_of N -> Element of T equals

      : Def8: ( the_value_of the mapping of N);

      coherence

      proof

        reconsider M = N as constant non empty NetStr over T by A1;

        set f = the mapping of M;

        ex x be set st x in ( dom f) & ( the_value_of f) = (f . x) by FUNCT_1:def 12;

        then ( the_value_of f) in ( rng f) by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    theorem :: YELLOW_6:13

    

     Th13: for R be non empty RelStr, T be non empty 1-sorted, p be Element of T holds ( the_value_of ( ConstantNet (R,p))) = p

    proof

      let R be non empty RelStr, T be non empty 1-sorted, p be Element of T;

      

      thus ( the_value_of ( ConstantNet (R,p))) = ( the_value_of the mapping of ( ConstantNet (R,p))) by Def8

      .= ( the_value_of (the carrier of ( ConstantNet (R,p)) --> p)) by Def5

      .= p by FUNCOP_1: 79;

    end;

    definition

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

      :: YELLOW_6:def9

      mode subnet of N -> net of T means

      : Def9: ex f be Function of it , N st the mapping of it = (the mapping of N * f) & for m be Element of N holds ex n be Element of it st for p be Element of it st n <= p holds m <= (f . p);

      existence

      proof

        take N, ( id N);

        thus the mapping of N = (the mapping of N * ( id N)) by FUNCT_2: 17;

        let m be Element of N;

        take n = m;

        let p be Element of N;

        assume n <= p;

        hence thesis;

      end;

    end

    theorem :: YELLOW_6:14

    for T be non empty 1-sorted, N be net of T holds N is subnet of N

    proof

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

      take ( id N);

      thus the mapping of N = (the mapping of N * ( id N)) by FUNCT_2: 17;

      let m be Element of N;

      take n = m;

      let p be Element of N;

      assume n <= p;

      hence thesis;

    end;

    theorem :: YELLOW_6:15

    for T be non empty 1-sorted, N1,N2,N3 be net of T st N1 is subnet of N2 & N2 is subnet of N3 holds N1 is subnet of N3

    proof

      let T be non empty 1-sorted, N1,N2,N3 be net of T;

      given f be Function of N1, N2 such that

       A1: the mapping of N1 = (the mapping of N2 * f) and

       A2: for m be Element of N2 holds ex n be Element of N1 st for p be Element of N1 st n <= p holds m <= (f . p);

      given g be Function of N2, N3 such that

       A3: the mapping of N2 = (the mapping of N3 * g) and

       A4: for m be Element of N3 holds ex n be Element of N2 st for p be Element of N2 st n <= p holds m <= (g . p);

      take (g * f);

      thus the mapping of N1 = (the mapping of N3 * (g * f)) by A1, A3, RELAT_1: 36;

      let m be Element of N3;

      consider m1 be Element of N2 such that

       A5: for p be Element of N2 st m1 <= p holds m <= (g . p) by A4;

      consider n be Element of N1 such that

       A6: for p be Element of N1 st n <= p holds m1 <= (f . p) by A2;

      take n;

      let p be Element of N1;

      assume n <= p;

      then m <= (g . (f . p)) by A5, A6;

      hence thesis by FUNCT_2: 15;

    end;

    theorem :: YELLOW_6:16

    

     Th16: for T be non empty 1-sorted, N be constant net of T, i be Element of N holds (N . i) = ( the_value_of N)

    proof

      let T be non empty 1-sorted, N be constant net of T, i be Element of N;

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

      

      hence (N . i) = ( the_value_of the mapping of N) by FUNCT_1:def 12

      .= ( the_value_of N) by Def8;

    end;

    theorem :: YELLOW_6:17

    

     Th17: for L be non empty 1-sorted, N be net of L, X,Y be set st N is_eventually_in X & N is_eventually_in Y holds X meets Y

    proof

      let L be non empty 1-sorted, N be net of L, X,Y be set;

      assume N is_eventually_in X;

      then

      consider i1 be Element of N such that

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

      assume N is_eventually_in Y;

      then

      consider i2 be Element of N such that

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

      consider i be Element of N such that

       A3: i1 <= i and

       A4: i2 <= i by Def3;

      

       A5: (N . i) in Y by A2, A4;

      (N . i) in X by A1, A3;

      hence thesis by A5, XBOOLE_0: 3;

    end;

    theorem :: YELLOW_6:18

    

     Th18: for S be non empty 1-sorted, N be net of S, M be subnet of N, X st M is_often_in X holds N is_often_in X

    proof

      let S be non empty 1-sorted, N be net of S, M be subnet of N, X such that

       A1: M is_often_in X;

      let i be Element of N;

      consider f be Function of M, N such that

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

       A3: for m be Element of N holds ex n be Element of M st for p be Element of M st n <= p holds m <= (f . p) by Def9;

      consider n be Element of M such that

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

      consider m be Element of M such that

       A5: n <= m and

       A6: (M . m) in X by A1;

      take (f . m);

      thus i <= (f . m) by A4, A5;

      thus thesis by A2, A6, FUNCT_2: 15;

    end;

    theorem :: YELLOW_6:19

    

     Th19: for S be non empty 1-sorted, N be net of S, X st N is_eventually_in X holds N is_often_in X

    proof

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

      given i be Element of N such that

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

      let j be Element of N;

      consider z be Element of N such that

       A2: i <= z & j <= z by Def3;

      take z;

      thus thesis by A1, A2;

    end;

    theorem :: YELLOW_6:20

    

     Th20: for S be non empty 1-sorted, N be net of S holds N is_eventually_in the carrier of S

    proof

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

      set i = the Element of N;

      take i;

      let j be Element of N;

      assume i <= j;

      thus thesis;

    end;

    begin

    definition

      let S be 1-sorted, N be NetStr over S, X;

      :: YELLOW_6:def10

      func N " X -> strict SubNetStr of N means

      : Def10: it is full SubRelStr of N & the carrier of it = (the mapping of N " X);

      existence

      proof

        set c = (the mapping of N " X);

        reconsider i = (the InternalRel of N |_2 c) as Relation of c, c;

        per cases ;

          suppose S is non empty;

          then

          reconsider S as non empty 1-sorted;

          set c = (the mapping of N " X);

          reconsider m = (the mapping of N | c) as Function of c, S by FUNCT_2: 32;

          set S = NetStr (# c, i, m #);

          

           A1: i c= the InternalRel of N by XBOOLE_1: 17;

          then S is SubRelStr of N by YELLOW_0:def 13;

          then

          reconsider S as strict SubNetStr of N by Def6;

          take S;

          thus thesis by A1, YELLOW_0:def 13, YELLOW_0:def 14;

        end;

          suppose

           A2: S is empty;

          then the mapping of N = {} ;

          then c = {} ;

          then

          reconsider m = {} as Function of c, S by RELSET_1: 12;

          set S = NetStr (# c, i, m #);

          

           A3: the mapping of S = (the mapping of N | the carrier of S) by A2;

          

           A4: i c= the InternalRel of N by XBOOLE_1: 17;

          then S is SubRelStr of N by YELLOW_0:def 13;

          then

          reconsider S as strict SubNetStr of N by A3, Def6;

          take S;

          thus thesis by A4, YELLOW_0:def 13, YELLOW_0:def 14;

        end;

      end;

      uniqueness

      proof

        let it1,it2 be strict SubNetStr of N such that

         A5: it1 is full SubRelStr of N and

         A6: the carrier of it1 = (the mapping of N " X) and

         A7: it2 is full SubRelStr of N and

         A8: the carrier of it2 = (the mapping of N " X);

        

         A9: the mapping of it1 = (the mapping of N | the carrier of it2) by A6, A8, Def6

        .= the mapping of it2 by Def6;

         the RelStr of it1 = the RelStr of it2 by A5, A6, A7, A8, YELLOW_0: 57;

        hence thesis by A9;

      end;

    end

    registration

      let S be 1-sorted, N be transitive NetStr over S, X;

      cluster (N " X) -> transitive full;

      coherence

      proof

        reconsider M = (N " X) as full SubRelStr of N by Def10;

        M is transitive;

        hence thesis;

      end;

    end

    theorem :: YELLOW_6:21

    

     Th21: for S be non empty 1-sorted, N be net of S, X st N is_often_in X holds (N " X) is non empty directed

    proof

      let S be non empty 1-sorted, N be net of S, X such that

       A1: N is_often_in X;

      set i = the Element of N;

      consider j be Element of N such that i <= j and

       A2: (N . j) in X by A1;

      

       A3: j in (the mapping of N " X) by A2, FUNCT_2: 38;

      hence the carrier of (N " X) is non empty by Def10;

      reconsider M = (N " X) as non empty full SubNetStr of N by A3, Def10;

      M is directed

      proof

        let i,j be Element of M;

        the carrier of M c= the carrier of N by Th10;

        then

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

        consider z be Element of N such that

         A4: x <= z & y <= z by Def3;

        consider e be Element of N such that

         A5: z <= e and

         A6: (N . e) in X by A1;

        e in (the mapping of N " X) by A6, FUNCT_2: 38;

        then

        reconsider k = e as Element of M by Def10;

        take k;

        x <= e & y <= e by A4, A5, YELLOW_0:def 2;

        hence thesis by Th12;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_6:22

    

     Th22: for S be non empty 1-sorted, N be net of S, X st N is_often_in X holds (N " X) is subnet of N

    proof

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

      assume

       A1: N is_often_in X;

      then

      reconsider M = (N " X) as net of S by Th21;

      M is subnet of N

      proof

        set f = ( id M);

        the carrier of M c= the carrier of N by Th10;

        then

        reconsider f as Function of M, N by FUNCT_2: 7;

        take f;

        the mapping of M = (the mapping of N | the carrier of M) by Def6;

        hence the mapping of M = (the mapping of N * f) by RELAT_1: 65;

        let m be Element of N;

        consider j be Element of N such that

         A2: m <= j and

         A3: (N . j) in X by A1;

        j in (the mapping of N " X) by A3, FUNCT_2: 38;

        then

        reconsider n = j as Element of M by Def10;

        take n;

        let p be Element of M such that

         A4: n <= p;

        j <= (f . p) by A4, Th11;

        hence thesis by A2, YELLOW_0:def 2;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_6:23

    

     Th23: for S be non empty 1-sorted, N be net of S, X holds for M be subnet of N st M = (N " X) holds M is_eventually_in X

    proof

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

      let M be subnet of N such that

       A1: M = (N " X);

      set i = the Element of M;

      take i;

      let j be Element of M such that i <= j;

      j in the carrier of M;

      then j in (the mapping of N " X) by A1, Def10;

      then

       A2: (the mapping of N . j) in X by FUNCT_1:def 7;

      the mapping of M = (the mapping of N | the carrier of M) by A1, Def6;

      hence thesis by A2, FUNCT_1: 49;

    end;

    begin

    definition

      let X be non empty 1-sorted;

      :: YELLOW_6:def11

      func NetUniv X -> set means

      : Def11: for x be object holds x in it iff ex N be strict net of X st N = x & the carrier of N in ( the_universe_of the carrier of X);

      existence

      proof

        deffunc f( set) = { NetStr (# $1, r, f #) where r be Relation of $1, $1, f be Element of ( Funcs ($1,the carrier of X)) : NetStr (# $1, r, f #) is net of X };

        set I = ( the_universe_of the carrier of X);

        consider M be ManySortedSet of I such that

         A1: for i be set st i in I holds (M . i) = f(i) from PBOOLE:sch 7;

        take IT = ( Union M);

        let x be object;

        

         A2: ( Union M) = ( union ( rng M)) by CARD_3:def 4;

        hereby

          assume x in IT;

          then

          consider y such that

           A3: x in y and

           A4: y in ( rng M) by A2, TARSKI:def 4;

          consider z be object such that

           A5: z in ( dom M) and

           A6: (M . z) = y by A4, FUNCT_1:def 3;

          reconsider z as set by TARSKI: 1;

          z in I by A5;

          then y = { NetStr (# z, r, f #) where r be Relation of z, z, f be Element of ( Funcs (z,the carrier of X)) : NetStr (# z, r, f #) is net of X } by A1, A6;

          then

          consider r be Relation of z, z, f be Element of ( Funcs (z,the carrier of X)) such that

           A7: x = NetStr (# z, r, f #) and

           A8: NetStr (# z, r, f #) is net of X by A3;

          reconsider N = NetStr (# z, r, f #) as strict net of X by A8;

          take N;

          thus N = x by A7;

          thus the carrier of N in ( the_universe_of the carrier of X) by A5;

        end;

        given N be strict net of X such that

         A9: N = x and

         A10: the carrier of N in ( the_universe_of the carrier of X);

        set i = the carrier of N;

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

        then

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

        

         A12: the mapping of N in ( Funcs (i,the carrier of X)) by FUNCT_2: 8;

        (M . i) = { NetStr (# i, r, f #) where r be Relation of i, i, f be Element of ( Funcs (i,the carrier of X)) : NetStr (# i, r, f #) is net of X } by A1, A10;

        then N in (M . i) by A12;

        hence thesis by A2, A9, A11, TARSKI:def 4;

      end;

      uniqueness

      proof

        defpred P[ object] means ex N be strict net of X st N = $1 & the carrier of N in ( the_universe_of the carrier of X);

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    registration

      let X be non empty 1-sorted;

      cluster ( NetUniv X) -> non empty;

      coherence

      proof

         {} in { {} } by TARSKI:def 1;

        then

        reconsider r = { [ {} , {} ]} as Relation of { {} } by RELSET_1: 3;

        set R = RelStr (# { {} }, r #);

         A1:

        now

          let x,y be Element of R;

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

          then [x, y] in { [ {} , {} ]} by TARSKI:def 1;

          hence x <= y by ORDERS_2:def 5;

        end;

        

         A2: R is transitive by A1;

        R is directed

        proof

          let x,y be Element of R;

          take x;

          thus thesis by A1;

        end;

        then

        reconsider R as transitive directed non empty RelStr by A2;

        set V = ( the_universe_of the carrier of X);

        set q = the Element of X;

        set N = ( ConstantNet (R,q));

         the RelStr of N = the RelStr of R & {} in V by Def5, CLASSES2: 56;

        then the carrier of N in V by CLASSES2: 2;

        hence thesis by Def11;

      end;

    end

    

     Lm6: for S1,S2 be non empty 1-sorted st the carrier of S1 = the carrier of S2 holds for N be constant net of S1 holds N is constant net of S2

    proof

      let S1,S2 be non empty 1-sorted such that

       A1: the carrier of S1 = the carrier of S2;

      let N be constant net of S1;

      reconsider M = N as net of S2 by A1;

      the mapping of N is constant;

      then the mapping of M is constant;

      hence thesis by Def4;

    end;

    

     Lm7: for S1,S2 be non empty 1-sorted st the carrier of S1 = the carrier of S2 holds ( NetUniv S1) = ( NetUniv S2)

    proof

      let S1,S2 be non empty 1-sorted;

      defpred P[ object] means ex N be strict net of S2 st N = $1 & the carrier of N in ( the_universe_of the carrier of S2);

      assume

       A1: the carrier of S1 = the carrier of S2;

       A2:

      now

        let x be object;

        hereby

          assume x in ( NetUniv S1);

          then

          consider N be strict net of S1 such that

           A3: N = x & the carrier of N in ( the_universe_of the carrier of S1) by Def11;

          reconsider N as strict net of S2 by A1;

          thus P[x]

          proof

            take N;

            thus thesis by A1, A3;

          end;

        end;

        assume P[x];

        then

        consider N be strict net of S2 such that

         A4: N = x & the carrier of N in ( the_universe_of the carrier of S2);

        reconsider N as strict net of S1 by A1;

        now

          take N;

          thus N = x & the carrier of N in ( the_universe_of the carrier of S1) by A1, A4;

        end;

        hence x in ( NetUniv S1) by Def11;

      end;

      

       A5: for x be object holds x in ( NetUniv S2) iff P[x] by Def11;

      thus ( NetUniv S1) = ( NetUniv S2) from XBOOLE_0:sch 2( A2, A5);

    end;

    begin

    definition

      let X be set, T be 1-sorted;

      :: YELLOW_6:def12

      mode net_set of X,T -> ManySortedSet of X means

      : Def12: for i be set st i in ( rng it ) holds i is net of T;

      existence

      proof

        set N = the net of T;

        take (X --> N);

        let i be set;

        assume i in ( rng (X --> N));

        hence thesis by TARSKI:def 1;

      end;

    end

    theorem :: YELLOW_6:24

    

     Th24: for X be set, T be 1-sorted, F be ManySortedSet of X holds F is net_set of X, T iff for i be set st i in X holds (F . i) is net of T

    proof

      let X be set, T be 1-sorted, F be ManySortedSet of X;

      hereby

        assume

         A1: F is net_set of X, T;

        let i be set;

        assume i in X;

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

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

        hence (F . i) is net of T by A1, Def12;

      end;

      assume

       A2: for i be set st i in X holds (F . i) is net of T;

      let x be set;

      assume x in ( rng F);

      then ex i be object st i in ( dom F) & x = (F . i) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    definition

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

      let J be net_set of X, T, i be Element of X;

      :: original: .

      redefine

      func J . i -> net of T ;

      coherence by Th24;

    end

    registration

      let X be set, T be 1-sorted;

      cluster -> RelStr-yielding for net_set of X, T;

      coherence

      proof

        let F be net_set of X, T;

        let v be set;

        assume v in ( rng F);

        hence thesis by Def12;

      end;

    end

    registration

      let T be 1-sorted, Y be net of T;

      cluster -> yielding_non-empty_carriers for net_set of the carrier of Y, T;

      coherence by Def12;

    end

    registration

      let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y, T;

      cluster ( product J) -> directed transitive;

      coherence

      proof

        

         A1: the carrier of ( product J) = ( product ( Carrier J)) by YELLOW_1:def 4;

        thus ( product J) is directed

        proof

          let x,y be Element of ( product J);

          defpred P[ Element of Y, object] means [(x . $1), $2] in the InternalRel of (J . $1) & [(y . $1), $2] in the InternalRel of (J . $1);

           A2:

          now

            let i be Element of Y;

            consider zi be Element of (J . i) such that

             A3: (x . i) <= zi & (y . i) <= zi by Def3;

            reconsider z = zi as object;

            take z;

            thus P[i, z] by A3, ORDERS_2:def 5;

          end;

          consider z be ManySortedSet of the carrier of Y such that

           A4: for i be Element of Y holds P[i, (z . i)] from PBOOLE:sch 6( A2);

           A5:

          now

            let i be object;

            assume i in ( dom ( Carrier J));

            then

            reconsider j = i as Element of Y;

             [(x . j), (z . j)] in the InternalRel of (J . j) by A4;

            then (z . j) in the carrier of (J . j) by ZFMISC_1: 87;

            hence (z . i) in (( Carrier J) . i) by Th2;

          end;

          ( dom z) = the carrier of Y by PARTFUN1:def 2

          .= ( dom ( Carrier J)) by PARTFUN1:def 2;

          then

          reconsider z as Element of ( product J) by A1, A5, CARD_3: 9;

          take z;

          for i be object st i in the carrier of Y holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (x . i) & yi = (z . i) & xi <= yi

          proof

            let i be object;

            assume i in the carrier of Y;

            then

            reconsider j = i as Element of Y;

            reconsider xi = (x . j), zi = (z . j) as Element of (J . j);

            take (J . j), xi, zi;

            thus (J . j) = (J . i) & xi = (x . i) & zi = (z . i);

             [xi, zi] in the InternalRel of (J . j) by A4;

            hence thesis by ORDERS_2:def 5;

          end;

          hence x <= z by A1, YELLOW_1:def 4;

          for i be object st i in the carrier of Y holds ex R be RelStr, yi,zi be Element of R st R = (J . i) & yi = (y . i) & zi = (z . i) & yi <= zi

          proof

            let i be object;

            assume i in the carrier of Y;

            then

            reconsider j = i as Element of Y;

            reconsider yi = (y . j), zi = (z . j) as Element of (J . j);

            take (J . j), yi, zi;

            thus (J . j) = (J . i) & yi = (y . i) & zi = (z . i);

             [yi, zi] in the InternalRel of (J . j) by A4;

            hence thesis by ORDERS_2:def 5;

          end;

          hence thesis by A1, YELLOW_1:def 4;

        end;

        let x,y,z be Element of ( product J) such that

         A6: x <= y and

         A7: y <= z;

        

         A8: ex fy,gz be Function st fy = y & gz = z & for i be object st i in the carrier of Y holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (fy . i) & yi = (gz . i) & xi <= yi by A1, A7, YELLOW_1:def 4;

        

         A9: ex fx,gy be Function st fx = x & gy = y & for i be object st i in the carrier of Y holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (fx . i) & yi = (gy . i) & xi <= yi by A1, A6, YELLOW_1:def 4;

        for i be object st i in the carrier of Y holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (x . i) & yi = (z . i) & xi <= yi

        proof

          let i be object;

          assume

           A10: i in the carrier of Y;

          then

          reconsider j = i as Element of Y;

          consider R1 be RelStr, xi,yi be Element of R1 such that

           A11: R1 = (J . i) and

           A12: xi = (x . i) and

           A13: yi = (y . i) & xi <= yi by A9, A10;

          consider R2 be RelStr, yi9,zi be Element of R2 such that

           A14: R2 = (J . i) and

           A15: yi9 = (y . i) and

           A16: zi = (z . i) and

           A17: yi9 <= zi by A8, A10;

          reconsider xi, zi as Element of (J . j) by A11, A14;

          take (J . j), xi, zi;

          thus (J . j) = (J . i) & xi = (x . i) & zi = (z . i) by A12, A16;

          thus thesis by A11, A13, A14, A15, A17, YELLOW_0:def 2;

        end;

        hence thesis by A1, YELLOW_1:def 4;

      end;

    end

    registration

      let X be set, T be 1-sorted;

      cluster -> yielding_non-empty_carriers for net_set of X, T;

      coherence by Def12;

    end

    registration

      let X be set, T be 1-sorted;

      cluster yielding_non-empty_carriers for net_set of X, T;

      existence

      proof

        set F = the net_set of X, T;

        take F;

        thus thesis;

      end;

    end

    definition

      let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y, T;

      :: YELLOW_6:def13

      func Iterated J -> strict net of T means

      : Def13: the RelStr of it = [:Y, ( product J):] & for i be Element of Y, f be Function st i in the carrier of Y & f in the carrier of ( product J) holds (the mapping of it . (i,f)) = (the mapping of (J . i) . (f . i));

      existence

      proof

        deffunc F( Element of Y, Element of ( product J)) = (the mapping of (J . $1) . ($2 . $1));

        set R = [:Y, ( product J):];

        

         A1: for i be Element of Y, f be Element of ( product J) holds F(i,f) in the carrier of T;

        consider F be Function of [:the carrier of Y, the carrier of ( product J):], T such that

         A2: for i be Element of Y, f be Element of ( product J) holds (F . (i,f)) = F(i,f) from FUNCT_7:sch 1( A1);

        the carrier of R = [:the carrier of Y, the carrier of ( product J):] by YELLOW_3:def 2;

        then

        reconsider F as Function of R, T;

        reconsider N = NetStr (# the carrier of R, the InternalRel of R, F #) as strict net of T by Lm1, Lm2;

        take N;

        thus the RelStr of N = [:Y, ( product J):];

        let i be Element of Y, f be Function such that i in the carrier of Y and

         A3: f in the carrier of ( product J);

        thus thesis by A2, A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be strict net of T such that

         A4: the RelStr of IT1 = [:Y, ( product J):] and

         A5: for i be Element of Y, f be Function st i in the carrier of Y & f in the carrier of ( product J) holds (the mapping of IT1 . (i,f)) = (the mapping of (J . i) . (f . i)) and

         A6: the RelStr of IT2 = [:Y, ( product J):] and

         A7: for i be Element of Y, f be Function st i in the carrier of Y & f in the carrier of ( product J) holds (the mapping of IT2 . (i,f)) = (the mapping of (J . i) . (f . i));

        the carrier of the RelStr of IT2 = [:the carrier of Y, the carrier of ( product J):] by A6, YELLOW_3:def 2;

        then

        reconsider m1 = the mapping of IT1, m2 = the mapping of IT2 as Function of [:the carrier of Y, the carrier of ( product J):], T by A4, A6;

        now

          let c be Element of [:the carrier of Y, the carrier of ( product J):];

          consider c1 be Element of Y, c2 be Element of ( product J) such that

           A8: c = [c1, c2] by DOMAIN_1: 1;

          reconsider d = c2 as Element of ( product ( Carrier J)) by YELLOW_1:def 4;

          

          thus (m1 . c) = (m1 . (c1,d)) by A8

          .= (the mapping of (J . c1) . (d . c1)) by A5

          .= (m2 . (c1,d)) by A7

          .= (m2 . c) by A8;

        end;

        hence thesis by A4, A6, FUNCT_2: 63;

      end;

    end

    theorem :: YELLOW_6:25

    

     Th25: for T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y, T st Y in ( NetUniv T) & for i be Element of Y holds (J . i) in ( NetUniv T) holds ( Iterated J) in ( NetUniv T)

    proof

      let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y, T such that

       A1: Y in ( NetUniv T) and

       A2: for i be Element of Y holds (J . i) in ( NetUniv T);

      

       A3: ( rng ( Carrier J)) c= ( the_universe_of the carrier of T)

      proof

        let x be object;

        assume x in ( rng ( Carrier J));

        then

        consider y be object such that

         A4: y in ( dom ( Carrier J)) and

         A5: (( Carrier J) . y) = x by FUNCT_1:def 3;

        reconsider i = y as Element of Y by A4;

        (J . i) in ( NetUniv T) by A2;

        then ex N be strict net of T st N = (J . i) & the carrier of N in ( the_universe_of the carrier of T) by Def11;

        hence thesis by A5, Th2;

      end;

       the RelStr of ( Iterated J) = [:Y, ( product J):] by Def13;

      then

       A6: the carrier of ( Iterated J) = [:the carrier of Y, the carrier of ( product J):] by YELLOW_3:def 2;

      

       A7: ex N be strict net of T st N = Y & the carrier of N in ( the_universe_of the carrier of T) by A1, Def11;

      then ( dom ( Carrier J)) in ( the_universe_of the carrier of T) by PARTFUN1:def 2;

      then ( product ( Carrier J)) in ( the_universe_of the carrier of T) by A3, Th1;

      then the carrier of ( product J) in ( the_universe_of the carrier of T) by YELLOW_1:def 4;

      then the carrier of ( Iterated J) in ( the_universe_of the carrier of T) by A6, A7, CLASSES2: 61;

      hence thesis by Def11;

    end;

    theorem :: YELLOW_6:26

    

     Th26: for T be non empty 1-sorted, N be net of T holds for J be net_set of the carrier of N, T holds the carrier of ( Iterated J) = [:the carrier of N, ( product ( Carrier J)):]

    proof

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

      let J be net_set of the carrier of N, T;

       the RelStr of ( Iterated J) = [:N, ( product J):] by Def13;

      

      hence the carrier of ( Iterated J) = [:the carrier of N, the carrier of ( product J):] by YELLOW_3:def 2

      .= [:the carrier of N, ( product ( Carrier J)):] by YELLOW_1:def 4;

    end;

    theorem :: YELLOW_6:27

    

     Th27: for T be non empty 1-sorted, N be net of T, J be net_set of the carrier of N, T, i be Element of N, f be Element of ( product J), x be Element of ( Iterated J) st x = [i, f] holds (( Iterated J) . x) = (the mapping of (J . i) . (f . i))

    proof

      let T be non empty 1-sorted, N be net of T, J be net_set of the carrier of N, T, i be Element of N, f be Element of ( product J), x be Element of ( Iterated J);

      assume x = [i, f];

      

      hence (( Iterated J) . x) = (the mapping of ( Iterated J) . (i,f))

      .= (the mapping of (J . i) . (f . i)) by Def13;

    end;

    theorem :: YELLOW_6:28

    

     Th28: for T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y, T holds ( rng the mapping of ( Iterated J)) c= ( union the set of all ( rng the mapping of (J . i)) where i be Element of Y)

    proof

      let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y, T;

      let x be object;

      set X = the set of all ( rng the mapping of (J . i)) where i be Element of Y;

      assume x in ( rng the mapping of ( Iterated J));

      then

      consider y be object such that

       A1: y in ( dom the mapping of ( Iterated J)) and

       A2: (the mapping of ( Iterated J) . y) = x by FUNCT_1:def 3;

      y in the carrier of ( Iterated J) by A1;

      then y in [:the carrier of Y, ( product ( Carrier J)):] by Th26;

      then

      consider y1 be Element of Y, y2 be Element of ( product ( Carrier J)) such that

       A3: y = [y1, y2] by DOMAIN_1: 1;

      y1 in the carrier of Y;

      then y1 in ( dom ( Carrier J)) by PARTFUN1:def 2;

      then (y2 . y1) in (( Carrier J) . y1) by CARD_3: 9;

      then (y2 . y1) in the carrier of (J . y1) by Th2;

      then

       A4: (y2 . y1) in ( dom the mapping of (J . y1)) by FUNCT_2:def 1;

      y2 in ( product ( Carrier J));

      then

       A5: y2 in the carrier of ( product J) by YELLOW_1:def 4;

      x = (the mapping of ( Iterated J) . (y1,y2)) by A2, A3

      .= (the mapping of (J . y1) . (y2 . y1)) by A5, Def13;

      then

       A6: x in ( rng the mapping of (J . y1)) by A4, FUNCT_1:def 3;

      reconsider y1 as Element of Y;

      ( rng the mapping of (J . y1)) in X;

      hence thesis by A6, TARSKI:def 4;

    end;

    begin

    definition

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

      :: YELLOW_6:def14

      func OpenNeighborhoods p -> RelStr equals (( InclPoset { V where V be Subset of T : p in V & V is open }) ~ );

      correctness ;

    end

    registration

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

      cluster ( OpenNeighborhoods p) -> non empty;

      coherence

      proof

        set Xp = { v where v be Subset of T : p in v & v is open };

        ( [#] T) in the carrier of ( InclPoset Xp);

        hence the carrier of ( OpenNeighborhoods p) is non empty;

      end;

    end

    theorem :: YELLOW_6:29

    

     Th29: for T be non empty TopSpace, p be Point of T, x be Element of ( OpenNeighborhoods p) holds ex W be Subset of T st W = x & p in W & W is open

    proof

      let T be non empty TopSpace, p be Point of T, x be Element of ( OpenNeighborhoods p);

      set X = { V where V be Subset of T : p in V & V is open };

      x in the carrier of (( InclPoset X) ~ );

      then x in the carrier of ( InclPoset X) by Th3;

      hence thesis;

    end;

    theorem :: YELLOW_6:30

    

     Th30: for T be non empty TopSpace, p be Point of T holds for x be Subset of T holds x in the carrier of ( OpenNeighborhoods p) iff p in x & x is open

    proof

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

      let x be Subset of T;

      set Xp = { v where v be Subset of T : p in v & v is open };

      reconsider i = x as Subset of T;

      thus x in the carrier of ( OpenNeighborhoods p) implies p in x & x is open

      proof

        assume x in the carrier of ( OpenNeighborhoods p);

        then ex v be Subset of T st i = v & p in v & v is open by Th29;

        hence thesis;

      end;

      assume p in x & x is open;

      then x in the carrier of ( InclPoset Xp);

      hence thesis by Th3;

    end;

    theorem :: YELLOW_6:31

    

     Th31: for T be non empty TopSpace, p be Point of T holds for x,y be Element of ( OpenNeighborhoods p) holds x <= y iff y c= x

    proof

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

      set X = { V where V be Subset of T : p in V & V is open };

      ( [#] T) in X;

      then

      reconsider X as non empty set;

      let x,y be Element of ( OpenNeighborhoods p);

      (( InclPoset X) ~ ) = RelStr (# the carrier of ( InclPoset X), (the InternalRel of ( InclPoset X) ~ ) #) by LATTICE3:def 5;

      then

      reconsider a = x, b = y as Element of ( InclPoset X);

      

       A1: b <= a iff y c= x by YELLOW_1: 3;

      x = (a ~ ) & y = (b ~ ) by LATTICE3:def 6;

      hence thesis by A1, LATTICE3: 9;

    end;

    registration

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

      cluster ( OpenNeighborhoods p) -> transitive directed;

      coherence

      proof

        thus ( OpenNeighborhoods p) is transitive;

        let x,y be Element of ( OpenNeighborhoods p);

        set X = { V where V be Subset of T : p in V & V is open };

        consider V be Subset of T such that

         A1: x = V and

         A2: p in V & V is open by Th29;

        consider W be Subset of T such that

         A3: y = W and

         A4: p in W & W is open by Th29;

        set z = (V /\ W);

        p in z & z is open by A2, A4, XBOOLE_0:def 4;

        then z in X;

        then

        reconsider z as Element of ( OpenNeighborhoods p) by Th3;

        

         A5: z c= y by A3, XBOOLE_1: 17;

        take z;

        z c= x by A1, XBOOLE_1: 17;

        hence thesis by A5, Th31;

      end;

    end

    begin

    definition

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

      defpred P[ Point of T] means for V be a_neighborhood of $1 holds N is_eventually_in V;

      :: YELLOW_6:def15

      func Lim N -> Subset of T means

      : Def15: for p be Point of T holds p in it iff for V be a_neighborhood of p holds N is_eventually_in V;

      existence

      proof

        consider IT be Subset of T such that

         A1: for p be Point of T holds p in IT iff P[p] from SUBSET_1:sch 3;

        take IT;

        let p be Point of T;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of T such that

         A2: for p be Point of T holds p in it1 iff P[p] and

         A3: for p be Point of T holds p in it2 iff P[p];

        thus thesis from SUBSET_1:sch 4( A2, A3);

      end;

    end

    theorem :: YELLOW_6:32

    

     Th32: for T be non empty TopSpace, N be net of T, Y be subnet of N holds ( Lim N) c= ( Lim Y)

    proof

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

      let x be object;

      consider f be Function of Y, N such that

       A1: the mapping of Y = (the mapping of N * f) and

       A2: for m be Element of N holds ex n be Element of Y st for p be Element of Y st n <= p holds m <= (f . p) by Def9;

      assume

       A3: x in ( Lim N);

      then

      reconsider p = x as Point of T;

      for V be a_neighborhood of p holds Y is_eventually_in V

      proof

        let V be a_neighborhood of p;

        N is_eventually_in V by A3, Def15;

        then

        consider ii be Element of N such that

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

        consider n be Element of Y such that

         A5: for p be Element of Y st n <= p holds ii <= (f . p) by A2;

        take n;

        let j be Element of Y;

        assume

         A6: n <= j;

        (N . (f . j)) = (Y . j) by A1, FUNCT_2: 15;

        hence thesis by A4, A5, A6;

      end;

      hence thesis by Def15;

    end;

    theorem :: YELLOW_6:33

    

     Th33: for T be non empty TopSpace, N be constant net of T holds ( the_value_of N) in ( Lim N)

    proof

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

      set p = ( the_value_of N);

      for S be a_neighborhood of p holds N is_eventually_in S

      proof

        set i = the Element of N;

        let S be a_neighborhood of p;

        take i;

        let j be Element of N such that i <= j;

        (N . j) = p by Th16;

        hence thesis by CONNSP_2: 4;

      end;

      hence thesis by Def15;

    end;

    theorem :: YELLOW_6:34

    

     Th34: for T be non empty TopSpace, N be net of T, p be Point of T st p in ( Lim N) holds for d be Element of N holds ex S be Subset of T st S = { (N . c) where c be Element of N : d <= c } & p in ( Cl S)

    proof

      let T be non empty TopSpace, N be net of T, p be Point of T such that

       A1: p in ( Lim N);

      let d be Element of N;

      { (N . c) where c be Element of N : d <= c } c= the carrier of T

      proof

        let x be object;

        assume x in { (N . c) where c be Element of N : d <= c };

        then ex c be Element of N st x = (N . c) & d <= c;

        hence thesis;

      end;

      then

      reconsider S = { (N . c) where c be Element of N : d <= c } as Subset of T;

      take S;

      thus S = { (N . c) where c be Element of N : d <= c };

      now

        let G be a_neighborhood of p;

        N is_eventually_in G by A1, Def15;

        then

        consider i be Element of N such that

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

        consider e be Element of N such that

         A3: d <= e and

         A4: i <= e by Def3;

        

         A5: (N . e) in S by A3;

        (N . e) in G by A2, A4;

        hence G meets S by A5, XBOOLE_0: 3;

      end;

      hence thesis by CONNSP_2: 27;

    end;

    theorem :: YELLOW_6:35

    

     Th35: for T be non empty TopSpace holds T is Hausdorff iff for N be net of T, p,q be Point of T st p in ( Lim N) & q in ( Lim N) holds p = q

    proof

      let T be non empty TopSpace;

      thus T is Hausdorff implies for N be net of T, p,q be Point of T st p in ( Lim N) & q in ( Lim N) holds p = q

      proof

        assume

         A1: T is Hausdorff;

        let N be net of T;

        given p1,p2 be Point of T such that

         A2: p1 in ( Lim N) and

         A3: p2 in ( Lim N) and

         A4: p1 <> p2;

        consider W,V be Subset of T such that

         A5: W is open and

         A6: V is open and

         A7: p1 in W and

         A8: p2 in V and

         A9: W misses V by A1, A4;

        V is a_neighborhood of p2 by A6, A8, CONNSP_2: 3;

        then

         A10: N is_eventually_in V by A3, Def15;

        W is a_neighborhood of p1 by A5, A7, CONNSP_2: 3;

        then N is_eventually_in W by A2, Def15;

        hence contradiction by A9, A10, Th17;

      end;

      assume

       A11: for N be net of T, p,q be Point of T st p in ( Lim N) & q in ( Lim N) holds p = q;

      given p,q be Point of T such that

       A12: p <> q and

       A13: for W,V be Subset of T st W is open & V is open & p in W & q in V holds W meets V;

      set pN = [:( OpenNeighborhoods p), ( OpenNeighborhoods q):];

      set cT = the carrier of T, cpN = the carrier of pN;

      deffunc F( Element of cpN) = (($1 `1 ) /\ ($1 `2 ));

      

       A14: for i be Element of cpN holds cT meets F(i)

      proof

        let i be Element of cpN;

        consider W be Subset of T such that

         A15: W = (i `1 ) and

         A16: p in W & W is open by Th29;

        consider V be Subset of T such that

         A17: V = (i `2 ) and

         A18: q in V & V is open by Th29;

        (i `1 ) meets (i `2 ) by A13, A15, A16, A17, A18;

        then (W /\ V) c= cT & ((i `1 ) /\ (i `2 )) <> {} by XBOOLE_0:def 7;

        then (cT /\ ((i `1 ) /\ (i `2 ))) <> {} by A15, A17, XBOOLE_1: 28;

        hence thesis by XBOOLE_0:def 7;

      end;

      consider f be Function of cpN, cT such that

       A19: for i be Element of cpN holds (f . i) in F(i) from FUNCT_2:sch 10( A14);

      reconsider N = NetStr (# the carrier of pN, the InternalRel of pN, f #) as net of T by Lm1, Lm2;

      

       A20: cpN = [:the carrier of ( OpenNeighborhoods p), the carrier of ( OpenNeighborhoods q):] by YELLOW_3:def 2;

      now

        let V be a_neighborhood of q;

        

         A21: N is_eventually_in ( Int V)

        proof

          

           A22: ( [#] T) in the carrier of ( OpenNeighborhoods p) by Th30;

          q in ( Int V) & ( Int V) is open by CONNSP_2:def 1;

          then ( Int V) in the carrier of ( OpenNeighborhoods q) by Th30;

          then

          reconsider i = [( [#] T), ( Int V)] as Element of N by A20, A22, ZFMISC_1: 87;

          take i;

          let j be Element of N;

          reconsider j9 = j, i9 = i as Element of pN;

          consider j1 be Element of ( OpenNeighborhoods p), j2 be Element of ( OpenNeighborhoods q) such that

           A23: j = [j1, j2] by A20, DOMAIN_1: 1;

          

           A24: (j `2 ) = j2 by A23;

          consider W1 be Subset of T such that

           A25: j1 = W1 and p in W1 and W1 is open by Th29;

          consider W2 be Subset of T such that

           A26: j2 = W2 and q in W2 and W2 is open by Th29;

          assume i <= j;

          then [i, j] in the InternalRel of pN by ORDERS_2:def 5;

          then i9 <= j9 by ORDERS_2:def 5;

          then (i9 `2 ) = ( Int V) & (i9 `2 ) <= (j9 `2 ) by YELLOW_3: 12;

          then W2 c= ( Int V) by A24, A26, Th31;

          then

           A27: (W1 /\ W2) c= (( Int V) /\ ( [#] T)) by XBOOLE_1: 27;

          (j `1 ) = j1 by A23;

          then (f . j) in (W1 /\ W2) by A19, A24, A25, A26;

          then (f . j) in (( Int V) /\ ( [#] T)) by A27;

          hence thesis by XBOOLE_1: 28;

        end;

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

        hence N is_eventually_in V by A21, WAYBEL_0: 8;

      end;

      then

       A28: q in ( Lim N) by Def15;

      now

        let V be a_neighborhood of p;

        

         A29: N is_eventually_in ( Int V)

        proof

          

           A30: ( [#] T) in the carrier of ( OpenNeighborhoods q) by Th30;

          p in ( Int V) & ( Int V) is open by CONNSP_2:def 1;

          then ( Int V) in the carrier of ( OpenNeighborhoods p) by Th30;

          then

          reconsider i = [( Int V), ( [#] T)] as Element of N by A20, A30, ZFMISC_1: 87;

          take i;

          let j be Element of N;

          reconsider j9 = j, i9 = i as Element of pN;

          consider j1 be Element of ( OpenNeighborhoods p), j2 be Element of ( OpenNeighborhoods q) such that

           A31: j = [j1, j2] by A20, DOMAIN_1: 1;

          

           A32: (j `1 ) = j1 by A31;

          consider W2 be Subset of T such that

           A33: j2 = W2 and q in W2 and W2 is open by Th29;

          consider W1 be Subset of T such that

           A34: j1 = W1 and p in W1 and W1 is open by Th29;

          assume i <= j;

          then [i, j] in the InternalRel of pN by ORDERS_2:def 5;

          then i9 <= j9 by ORDERS_2:def 5;

          then (i9 `1 ) = ( Int V) & (i9 `1 ) <= (j9 `1 ) by YELLOW_3: 12;

          then W1 c= ( Int V) by A32, A34, Th31;

          then

           A35: (W1 /\ W2) c= (( Int V) /\ ( [#] T)) by XBOOLE_1: 27;

          (j `2 ) = j2 by A31;

          then (f . j) in (W1 /\ W2) by A19, A32, A34, A33;

          then (f . j) in (( Int V) /\ ( [#] T)) by A35;

          hence thesis by XBOOLE_1: 28;

        end;

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

        hence N is_eventually_in V by A29, WAYBEL_0: 8;

      end;

      then p in ( Lim N) by Def15;

      hence contradiction by A11, A12, A28;

    end;

    registration

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

      cluster ( Lim N) -> trivial;

      coherence

      proof

        for p,q be Point of T st p in ( Lim N) & q in ( Lim N) holds p = q by Th35;

        hence thesis by SUBSET_1: 45;

      end;

    end

    definition

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

      :: YELLOW_6:def16

      attr N is convergent means

      : Def16: ( Lim N) <> {} ;

    end

    registration

      let T be non empty TopSpace;

      cluster constant -> convergent for net of T;

      coherence by Th33;

    end

    registration

      let T be non empty TopSpace;

      cluster convergent strict for net of T;

      existence

      proof

        set R = the non empty transitive directed RelStr, p = the Point of T;

        take ( ConstantNet (R,p));

        thus thesis;

      end;

    end

    definition

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

      :: YELLOW_6:def17

      func lim N -> Element of T means

      : Def17: it in ( Lim N);

      existence by Def16, SUBSET_1: 4;

      correctness by ZFMISC_1:def 10;

    end

    theorem :: YELLOW_6:36

    for T be Hausdorff non empty TopSpace, N be constant net of T holds ( lim N) = ( the_value_of N)

    proof

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

      ( the_value_of N) in ( Lim N) by Th33;

      hence thesis by Def17;

    end;

    theorem :: YELLOW_6:37

    for T be non empty TopSpace, N be net of T holds for p be Point of T st not p in ( Lim N) holds ex Y be subnet of N st not ex Z be subnet of Y st p in ( Lim Z)

    proof

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

      let p be Point of T;

      assume not p in ( Lim N);

      then

      consider V be a_neighborhood of p such that

       A1: not N is_eventually_in V by Def15;

      N is_often_in (the carrier of T \ V) by A1, WAYBEL_0: 9;

      then

      reconsider Y = (N " (the carrier of T \ V)) as subnet of N by Th22;

      take Y;

      let Z be subnet of Y;

      assume p in ( Lim Z);

      then Z is_eventually_in V by Def15;

      then

       A2: Y is_often_in V by Th18, Th19;

      Y is_eventually_in (the carrier of T \ V) by Th23;

      hence contradiction by A2, WAYBEL_0: 10;

    end;

    theorem :: YELLOW_6:38

    

     Th38: for T be non empty TopSpace, N be net of T st N in ( NetUniv T) holds for p be Point of T st not p in ( Lim N) holds ex Y be subnet of N st Y in ( NetUniv T) & not ex Z be subnet of Y st p in ( Lim Z)

    proof

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

      assume N in ( NetUniv T);

      then

       A1: ex M be strict net of T st M = N & the carrier of M in ( the_universe_of the carrier of T) by Def11;

      let p be Point of T;

      assume not p in ( Lim N);

      then

      consider V be a_neighborhood of p such that

       A2: not N is_eventually_in V by Def15;

      N is_often_in (the carrier of T \ V) by A2, WAYBEL_0: 9;

      then

      reconsider Y = (N " (the carrier of T \ V)) as subnet of N by Th22;

      take Y;

      the carrier of Y = (the mapping of N " (the carrier of T \ V)) by Def10;

      then the carrier of Y in ( the_universe_of the carrier of T) by A1, CLASSES1:def 1;

      hence Y in ( NetUniv T) by Def11;

      let Z be subnet of Y;

      assume p in ( Lim Z);

      then Z is_eventually_in V by Def15;

      then

       A3: Y is_often_in V by Th18, Th19;

      Y is_eventually_in (the carrier of T \ V) by Th23;

      hence contradiction by A3, WAYBEL_0: 10;

    end;

    theorem :: YELLOW_6:39

    

     Th39: for T be non empty TopSpace, N be net of T, p be Point of T st p in ( Lim N) holds for J be net_set of the carrier of N, T st for i be Element of N holds (N . i) in ( Lim (J . i)) holds p in ( Lim ( Iterated J))

    proof

      let T be non empty TopSpace, N be net of T, p be Point of T such that

       A1: p in ( Lim N);

      let J be net_set of the carrier of N, T such that

       A2: for i be Element of N holds (N . i) in ( Lim (J . i));

      for V be a_neighborhood of p holds ( Iterated J) is_eventually_in V

      proof

        let V be a_neighborhood of p;

        p in ( Int ( Int V)) by CONNSP_2:def 1;

        then

        reconsider W = ( Int V) as a_neighborhood of p by CONNSP_2:def 1;

        N is_eventually_in W by A1, Def15;

        then

        consider i be Element of N such that

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

        defpred P[ Element of N, object] means ex m be Element of (J . $1) st m = $2 & (i <= $1 implies for n be Element of (J . $1) st m <= n holds ((J . $1) . n) in W);

        

         A4: ( Int V) = ( Int ( Int V));

        

         A5: for j be Element of N holds ex e be object st P[j, e]

        proof

          let j be Element of N;

          reconsider j9 = j as Element of N;

          per cases ;

            suppose i <= j;

            then (N . j9) in W by A3;

            then

             A6: W is a_neighborhood of (N . j) by A4, CONNSP_2:def 1;

            (N . j) in ( Lim (J . j)) by A2;

            then (J . j) is_eventually_in W by A6, Def15;

            then

            consider e be Element of (J . j) such that

             A7: for u be Element of (J . j) st e <= u holds ((J . j) . u) in W;

            take e, e;

            thus e = e;

            assume i <= j;

            thus thesis by A7;

          end;

            suppose

             A8: not i <= j;

            set e = the Element of (J . j);

            take e, e;

            thus thesis by A8;

          end;

        end;

        consider f be ManySortedSet of the carrier of N such that

         A9: for j be Element of N holds P[j, (f . j)] from PBOOLE:sch 6( A5);

        

         A10: for x be object st x in ( dom ( Carrier J)) holds (f . x) in (( Carrier J) . x)

        proof

          let x be object;

          assume x in ( dom ( Carrier J));

          then

          reconsider j = x as Element of N;

          ex m be Element of (J . j) st m = (f . j) & (i <= j implies for n be Element of (J . j) st m <= n holds ((J . j) . n) in W) by A9;

          then (f . x) in the carrier of (J . j);

          hence thesis by Th2;

        end;

        ( dom ( Carrier J)) = the carrier of N by PARTFUN1:def 2;

        then ( dom f) = ( dom ( Carrier J)) by PARTFUN1:def 2;

        then

         A11: f in ( product ( Carrier J)) by A10, CARD_3: 9;

        

         A12: the carrier of ( Iterated J) = [:the carrier of N, ( product ( Carrier J)):] by Th26;

        then

        reconsider x = [i, f] as Element of ( Iterated J) by A11, ZFMISC_1: 87;

        take x;

        let j be Element of ( Iterated J) such that

         A13: x <= j;

        consider j1 be Element of N, j2 be Element of ( product ( Carrier J)) such that

         A14: j = [j1, j2] by A12, DOMAIN_1: 1;

        reconsider j2, i2 = f as Element of ( product J) by A11, YELLOW_1:def 4;

        reconsider i1 = i, j1 as Element of N;

        i2 in the carrier of ( product J);

        then

         A15: i2 in ( product ( Carrier J)) by YELLOW_1:def 4;

         the RelStr of ( Iterated J) = [:N, ( product J):] by Def13;

        then

         A16: [i1, i2] <= [j1, j2] by A13, A14, YELLOW_0: 1;

        then i2 <= j2 by YELLOW_3: 11;

        then ex f,g be Function st f = i2 & g = j2 & for i be object st i in the carrier of N holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A15, YELLOW_1:def 4;

        then

         A17: ex R be RelStr, xi,yi be Element of R st R = (J . j1) & xi = (i2 . j1) & yi = (j2 . j1) & xi <= yi;

        ex m be Element of (J . j1) st m = (f . j1) & (i <= j1 implies for n be Element of (J . j1) st m <= n holds ((J . j1) . n) in W) by A9;

        then ((J . j1) . (j2 . j1)) in W by A16, A17, YELLOW_3: 11;

        then

         A18: (( Iterated J) . j) in W by A14, Th27;

        W c= V by TOPS_1: 16;

        hence thesis by A18;

      end;

      hence thesis by Def15;

    end;

    begin

    definition

      let S be non empty 1-sorted;

      :: YELLOW_6:def18

      mode Convergence-Class of S -> set means

      : Def18: it c= [:( NetUniv S), the carrier of S:];

      existence ;

    end

    registration

      let S be non empty 1-sorted;

      cluster -> Relation-like for Convergence-Class of S;

      coherence

      proof

        let C be Convergence-Class of S;

        C is Subset of [:( NetUniv S), the carrier of S:] by Def18;

        hence thesis;

      end;

    end

    definition

      let T be non empty TopSpace;

      :: YELLOW_6:def19

      func Convergence T -> Convergence-Class of T means

      : Def19: for N be net of T, p be Point of T holds [N, p] in it iff N in ( NetUniv T) & p in ( Lim N);

      existence

      proof

        defpred P[ object, object] means ex N be net of T, p be Point of T st N = $1 & p = $2 & p in ( Lim N);

        consider R be Relation of ( NetUniv T), the carrier of T such that

         A1: for x,y be object holds [x, y] in R iff x in ( NetUniv T) & y in the carrier of T & P[x, y] from RELSET_1:sch 1;

        reconsider R as Convergence-Class of T by Def18;

        take R;

        let N be net of T, p be Point of T;

        hereby

          assume

           A2: [N, p] in R;

          hence N in ( NetUniv T) by A1;

          ex N9 be net of T, p9 be Point of T st N9 = N & p9 = p & p9 in ( Lim N9) by A1, A2;

          hence p in ( Lim N);

        end;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Convergence-Class of T such that

         A3: for N be net of T, p be Point of T holds [N, p] in it1 iff N in ( NetUniv T) & p in ( Lim N) and

         A4: for N be net of T, p be Point of T holds [N, p] in it2 iff N in ( NetUniv T) & p in ( Lim N);

        let x,y be object;

        

         A5: it1 c= [:( NetUniv T), the carrier of T:] by Def18;

        thus [x, y] in it1 implies [x, y] in it2

        proof

          assume

           A6: [x, y] in it1;

          then

          reconsider p = y as Point of T by A5, ZFMISC_1: 87;

          x in ( NetUniv T) by A5, A6, ZFMISC_1: 87;

          then

          consider N be strict net of T such that

           A7: N = x and the carrier of N in ( the_universe_of the carrier of T) by Def11;

           [N, p] in it1 by A6, A7;

          then

           A8: N in ( NetUniv T) by A3;

          p in ( Lim N) by A3, A6, A7;

          hence thesis by A4, A7, A8;

        end;

        assume

         A9: [x, y] in it2;

        

         A10: it2 c= [:( NetUniv T), the carrier of T:] by Def18;

        then

        reconsider p = y as Point of T by A9, ZFMISC_1: 87;

        x in ( NetUniv T) by A10, A9, ZFMISC_1: 87;

        then

        consider N be strict net of T such that

         A11: N = x and the carrier of N in ( the_universe_of the carrier of T) by Def11;

         [N, p] in it2 by A9, A11;

        then

         A12: N in ( NetUniv T) by A4;

        p in ( Lim N) by A4, A9, A11;

        hence thesis by A3, A11, A12;

      end;

    end

    definition

      let T be non empty 1-sorted, C be Convergence-Class of T;

      :: YELLOW_6:def20

      attr C is (CONSTANTS) means

      : Def20: for N be constant net of T st N in ( NetUniv T) holds [N, ( the_value_of N)] in C;

      :: YELLOW_6:def21

      attr C is (SUBNETS) means

      : Def21: for N be net of T, Y be subnet of N st Y in ( NetUniv T) holds for p be Element of T holds [N, p] in C implies [Y, p] in C;

      :: YELLOW_6:def22

      attr C is (DIVERGENCE) means

      : Def22: for X be net of T, p be Element of T st X in ( NetUniv T) & not [X, p] in C holds ex Y be subnet of X st Y in ( NetUniv T) & not ex Z be subnet of Y st [Z, p] in C;

      :: YELLOW_6:def23

      attr C is (ITERATED_LIMITS) means

      : Def23: for X be net of T, p be Element of T st [X, p] in C holds for J be net_set of the carrier of X, T st for i be Element of X holds [(J . i), (X . i)] in C holds [( Iterated J), p] in C;

    end

    registration

      let T be non empty TopSpace;

      cluster ( Convergence T) -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS);

      coherence

      proof

        set C = ( Convergence T);

        thus C is (CONSTANTS)

        proof

          let N be constant net of T such that

           A1: N in ( NetUniv T);

          ( the_value_of N) in ( Lim N) by Th33;

          hence thesis by A1, Def19;

        end;

        thus C is (SUBNETS)

        proof

          let N be net of T, Y be subnet of N such that

           A2: Y in ( NetUniv T);

          let p be Element of T;

          assume [N, p] in C;

          then

           A3: p in ( Lim N) by Def19;

          ( Lim N) c= ( Lim Y) by Th32;

          hence thesis by A2, A3, Def19;

        end;

        thus C is (DIVERGENCE)

        proof

          let X be net of T, p be Element of T such that

           A4: X in ( NetUniv T);

          assume not [X, p] in C;

          then not p in ( Lim X) by A4, Def19;

          then

          consider Y be subnet of X such that

           A5: Y in ( NetUniv T) and

           A6: not ex Z be subnet of Y st p in ( Lim Z) by A4, Th38;

          take Y;

          thus Y in ( NetUniv T) by A5;

          let Z be subnet of Y;

           not p in ( Lim Z) by A6;

          hence thesis by Def19;

        end;

        let X be net of T, p be Element of T;

        assume

         A7: [X, p] in C;

        let J be net_set of the carrier of X, T such that

         A8: for i be Element of X holds [(J . i), (X . i)] in C;

         A9:

        now

          let i be Element of X;

           [(J . i), (X . i)] in C by A8;

          hence (X . i) in ( Lim (J . i)) & (J . i) in ( NetUniv T) by Def19;

        end;

        X in ( NetUniv T) by A7, Def19;

        then

         A10: ( Iterated J) in ( NetUniv T) by A9, Th25;

        p in ( Lim X) by A7, Def19;

        then p in ( Lim ( Iterated J)) by A9, Th39;

        hence thesis by A10, Def19;

      end;

    end

    definition

      let S be non empty 1-sorted, C be Convergence-Class of S;

      :: YELLOW_6:def24

      func ConvergenceSpace C -> strict TopStruct means

      : Def24: the carrier of it = the carrier of S & the topology of it = { V where V be Subset of S : for p be Element of S st p in V holds for N be net of S st [N, p] in C holds N is_eventually_in V };

      existence

      proof

        defpred P[ set] means for p be Element of S st p in $1 holds for N be net of S st [N, p] in C holds N is_eventually_in $1;

        reconsider X = { V where V be Subset of S : P[V] } as Subset-Family of S from DOMAIN_1:sch 7;

        take TopStruct (# the carrier of S, X #);

        thus thesis;

      end;

      correctness ;

    end

    registration

      let S be non empty 1-sorted, C be Convergence-Class of S;

      cluster ( ConvergenceSpace C) -> non empty;

      coherence

      proof

        the carrier of ( ConvergenceSpace C) = the carrier of S by Def24;

        hence the carrier of ( ConvergenceSpace C) is non empty;

      end;

    end

    registration

      let S be non empty 1-sorted, C be Convergence-Class of S;

      cluster ( ConvergenceSpace C) -> TopSpace-like;

      coherence

      proof

        set IT = ( ConvergenceSpace C);

        

         A1: the topology of IT = { V where V be Subset of S : for p be Element of S st p in V holds for N be net of S st [N, p] in C holds N is_eventually_in V } by Def24;

        reconsider V = ( [#] IT) as Subset of S by Def24;

        V = the carrier of S by Def24;

        then for p be Element of S st p in V holds for N be net of S st [N, p] in C holds N is_eventually_in V by Th20;

        hence the carrier of IT in the topology of IT by A1;

        hereby

          let a be Subset-Family of IT such that

           A2: a c= the topology of IT;

          reconsider V = ( union a) as Subset of S by Def24;

          now

            let p be Element of S;

            assume p in V;

            then

            consider X such that

             A3: p in X and

             A4: X in a by TARSKI:def 4;

            

             A5: X c= V by A4, ZFMISC_1: 74;

            X in the topology of IT by A2, A4;

            then

             A6: ex W be Subset of S st X = W & for p be Element of S st p in W holds for N be net of S st [N, p] in C holds N is_eventually_in W by A1;

            let N be net of S;

            assume [N, p] in C;

            hence N is_eventually_in V by A3, A6, A5, WAYBEL_0: 8;

          end;

          hence ( union a) in the topology of IT by A1;

        end;

        let a,b be Subset of IT;

        assume a in the topology of IT;

        then

        consider Va be Subset of S such that

         A7: a = Va and

         A8: for p be Element of S st p in Va holds for N be net of S st [N, p] in C holds N is_eventually_in Va by A1;

        reconsider V = (a /\ b) as Subset of S by Def24;

        assume b in the topology of IT;

        then

        consider Vb be Subset of S such that

         A9: b = Vb and

         A10: for p be Element of S st p in Vb holds for N be net of S st [N, p] in C holds N is_eventually_in Vb by A1;

        now

          let p be Element of S such that

           A11: p in V;

          let N be net of S;

          assume

           A12: [N, p] in C;

          p in b by A11, XBOOLE_0:def 4;

          then N is_eventually_in Vb by A9, A10, A12;

          then

          consider i2 be Element of N such that

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

          p in a by A11, XBOOLE_0:def 4;

          then N is_eventually_in Va by A7, A8, A12;

          then

          consider i1 be Element of N such that

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

          consider i be Element of N such that

           A15: i1 <= i and

           A16: i2 <= i by Def3;

          thus N is_eventually_in V

          proof

            take i;

            let j be Element of N;

            assume

             A17: i <= j;

            then i2 <= j by A16, YELLOW_0:def 2;

            then

             A18: (N . j) in Vb by A13;

            i1 <= j by A15, A17, YELLOW_0:def 2;

            then (N . j) in Va by A14;

            hence thesis by A7, A9, A18, XBOOLE_0:def 4;

          end;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: YELLOW_6:40

    

     Th40: for S be non empty 1-sorted, C be Convergence-Class of S holds C c= ( Convergence ( ConvergenceSpace C))

    proof

      let S be non empty 1-sorted, C be Convergence-Class of S;

      set T = ( ConvergenceSpace C);

      let x,y be object;

      assume

       A1: [x, y] in C;

      C c= [:( NetUniv S), the carrier of S:] by Def18;

      then

      consider M be Element of ( NetUniv S), p be Element of S such that

       A2: [x, y] = [M, p] by A1, DOMAIN_1: 1;

      reconsider q = p as Point of T by Def24;

      

       A3: the carrier of S = the carrier of T & M in ( NetUniv S) by Def24;

      ex N be strict net of S st N = M & the carrier of N in ( the_universe_of the carrier of S) by Def11;

      then

      reconsider M as net of S;

      reconsider N = M as net of T by Def24;

      

       A4: the topology of T = { V where V be Subset of S : for p be Element of S st p in V holds for N be net of S st [N, p] in C holds N is_eventually_in V } by Def24;

      now

        let V be a_neighborhood of q;

        ( Int V) in the topology of T by PRE_TOPC:def 2;

        then p in ( Int V) & ex W be Subset of S st W = ( Int V) & for p be Element of S st p in W holds for N be net of S st [N, p] in C holds N is_eventually_in W by A4, CONNSP_2:def 1;

        then M is_eventually_in ( Int V) by A1, A2;

        then

        consider ii be Element of M such that

         A5: for j be Element of M st ii <= j holds (M . j) in ( Int V);

        reconsider i = ii as Element of N;

        now

          let j be Element of N such that

           A6: i <= j;

          reconsider jj = j as Element of M;

          (M . jj) = (N . j);

          hence (N . j) in ( Int V) by A5, A6;

        end;

        then ( Int V) c= V & N is_eventually_in ( Int V) by TOPS_1: 16;

        hence N is_eventually_in V by WAYBEL_0: 8;

      end;

      then

       A7: p in ( Lim N) by Def15;

      N in ( NetUniv T) by A3, Lm7;

      hence thesis by A2, A7, Def19;

    end;

    definition

      let T be non empty 1-sorted, C be Convergence-Class of T;

      :: YELLOW_6:def25

      attr C is topological means C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS);

    end

    registration

      let T be non empty 1-sorted;

      cluster non empty topological for Convergence-Class of T;

      existence

      proof

        reconsider C = [:( NetUniv T), the carrier of T:] as Convergence-Class of T by Def18;

        take C;

        thus C is non empty;

        thus C is topological

        proof

          thus C is (CONSTANTS) by ZFMISC_1: 87;

          thus C is (SUBNETS) by ZFMISC_1: 87;

          thus C is (DIVERGENCE) by ZFMISC_1: 87;

          let X be net of T, p be Element of T;

          assume [X, p] in C;

          then

           A1: X in ( NetUniv T) by ZFMISC_1: 87;

          let J be net_set of the carrier of X, T such that

           A2: for i be Element of X holds [(J . i), (X . i)] in C;

          now

            let i be Element of X;

             [(J . i), (X . i)] in C by A2;

            hence (J . i) in ( NetUniv T) by ZFMISC_1: 87;

          end;

          then ( Iterated J) in ( NetUniv T) by A1, Th25;

          hence thesis by ZFMISC_1: 87;

        end;

      end;

    end

    registration

      let T be non empty 1-sorted;

      cluster topological -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) for Convergence-Class of T;

      coherence ;

      cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) -> topological for Convergence-Class of T;

      coherence ;

    end

    theorem :: YELLOW_6:41

    

     Th41: for T be non empty 1-sorted, C be topological Convergence-Class of T, S be Subset of ( ConvergenceSpace C) qua non empty TopSpace holds S is open iff for p be Element of T st p in S holds for N be net of T st [N, p] in C holds N is_eventually_in S

    proof

      let T be non empty 1-sorted, C be topological Convergence-Class of T, S be Subset of ( ConvergenceSpace C);

      

       A1: the topology of ( ConvergenceSpace C) = { V where V be Subset of T : for p be Element of T st p in V holds for N be net of T st [N, p] in C holds N is_eventually_in V } by Def24;

      then

       A2: S in the topology of ( ConvergenceSpace C) implies ex V be Subset of T st S = V & for p be Element of T st p in V holds for N be net of T st [N, p] in C holds N is_eventually_in V;

      the carrier of ( ConvergenceSpace C) = the carrier of T by Def24;

      then (for p be Element of T st p in S holds for N be net of T st [N, p] in C holds N is_eventually_in S) implies S in the topology of ( ConvergenceSpace C) by A1;

      hence thesis by A2;

    end;

    theorem :: YELLOW_6:42

    

     Th42: for T be non empty 1-sorted, C be topological Convergence-Class of T, S be Subset of ( ConvergenceSpace C) qua non empty TopSpace holds S is closed iff for p be Element of T holds for N be net of T st [N, p] in C & N is_often_in S holds p in S

    proof

      let T be non empty 1-sorted, C be topological Convergence-Class of T, S be Subset of ( ConvergenceSpace C);

      set CC = ( ConvergenceSpace C);

      

       A1: the carrier of T = the carrier of CC by Def24;

      hereby

        assume S is closed;

        then

         A2: (S ` ) is open;

        let p be Element of T;

        let N be net of T such that

         A3: [N, p] in C;

        assume N is_often_in S;

        then not N is_eventually_in (( [#] CC) \ S) by A1, WAYBEL_0: 10;

        then not p in (S ` ) by A3, A2, Th41;

        hence p in S by A1, XBOOLE_0:def 5;

      end;

      assume

       A4: for p be Element of T holds for N be net of T st [N, p] in C & N is_often_in S holds p in S;

      now

        let p be Element of T;

        assume p in (S ` );

        then

         A5: not p in S by XBOOLE_0:def 5;

        let N be net of T;

        assume [N, p] in C;

        then not N is_often_in S by A4, A5;

        hence N is_eventually_in (S ` ) by A1, WAYBEL_0: 10;

      end;

      then (S ` ) is open by Th41;

      hence thesis;

    end;

    theorem :: YELLOW_6:43

    

     Th43: for T be non empty 1-sorted, C be topological Convergence-Class of T, S be Subset of ( ConvergenceSpace C), p be Point of ( ConvergenceSpace C) st p in ( Cl S) holds ex N be net of ( ConvergenceSpace C) st [N, p] in C & ( rng the mapping of N) c= S & p in ( Lim N)

    proof

      let T be non empty 1-sorted, C be topological Convergence-Class of T, S be Subset of ( ConvergenceSpace C) qua non empty TopSpace, p be Point of ( ConvergenceSpace C) such that

       A1: p in ( Cl S);

      set CC = ( ConvergenceSpace C);

      defpred P[ Point of CC] means ex N be net of ( ConvergenceSpace C) st [N, $1] in C & ( rng the mapping of N) c= S & $1 in ( Lim N);

      set F = { q where q be Point of CC : P[q] };

      F is Subset of CC from DOMAIN_1:sch 7;

      then

      reconsider F as Subset of CC;

      for p be Element of T holds for N be net of T st [N, p] in C & N is_often_in F holds p in F

      proof

        let p be Element of T;

        reconsider q = p as Point of CC by Def24;

        let N be net of T such that

         A2: [N, p] in C and

         A3: N is_often_in F;

        C c= [:( NetUniv T), the carrier of T:] by Def18;

        then N in ( NetUniv T) by A2, ZFMISC_1: 87;

        then

         A4: ex N0 be strict net of T st N0 = N & the carrier of N0 in ( the_universe_of the carrier of T) by Def11;

        reconsider M = (N " F) as subnet of N by A3, Th22;

        defpred P[ Element of M, object] means [$2, (M . $1)] in C & ex X be net of T st X = $2 & ( rng the mapping of X) c= S;

         A5:

        now

          let i be Element of M;

          i in the carrier of M;

          then i in (the mapping of N " F) by Def10;

          then

           A6: (the mapping of N . i) in F by FUNCT_2: 38;

          the mapping of M = (the mapping of N | the carrier of M) by Def6;

          then (the mapping of M . i) in F by A6, FUNCT_1: 49;

          then

          consider q be Point of CC such that

           A7: (M . i) = q and

           A8: ex N be net of ( ConvergenceSpace C) st [N, q] in C & ( rng the mapping of N) c= S & q in ( Lim N);

          consider N be net of CC such that

           A9: [N, q] in C and

           A10: ( rng the mapping of N) c= S and q in ( Lim N) by A8;

          reconsider x = N as object;

          take x;

          thus P[i, x]

          proof

            thus [x, (M . i)] in C by A7, A9;

            reconsider X = N as net of T by Def24;

            take X;

            thus X = x;

            thus thesis by A10;

          end;

        end;

        consider J be ManySortedSet of the carrier of M such that

         A11: for i be Element of M holds P[i, (J . i)] from PBOOLE:sch 6( A5);

        for i be set st i in the carrier of M holds (J . i) is net of T

        proof

          let i be set;

          assume i in the carrier of M;

          then ex X be net of T st X = (J . i) & ( rng the mapping of X) c= S by A11;

          hence thesis;

        end;

        then

        reconsider J as net_set of the carrier of M, T by Th24;

        set XX = the set of all ( rng the mapping of (J . i)) where i be Element of M;

        

         A12: for i be Element of M holds [(J . i), (M . i)] in C & ( rng the mapping of (J . i)) c= S

        proof

          let i be Element of M;

          thus [(J . i), (M . i)] in C by A11;

          ex X be net of T st X = (J . i) & ( rng the mapping of X) c= S by A11;

          hence thesis;

        end;

        for x st x in XX holds x c= S

        proof

          let x;

          assume x in XX;

          then ex i be Element of M st x = ( rng the mapping of (J . i));

          hence thesis by A12;

        end;

        then

         A13: ( union XX) c= S by ZFMISC_1: 76;

        reconsider I = ( Iterated J) as net of CC by Def24;

        ( rng the mapping of I) c= ( union XX) by Th28;

        then

         A14: ( rng the mapping of I) c= S by A13;

        the carrier of M = (the mapping of N " F) by Def10;

        then the carrier of M in ( the_universe_of the carrier of T) by A4, CLASSES1:def 1;

        then M in ( NetUniv T) by Def11;

        then [M, p] in C by A2, Def21;

        then

         A15: [I, p] in C by A12, Def23;

        C c= ( Convergence CC) by Th40;

        then q in ( Lim I) by A15, Def19;

        hence thesis by A15, A14;

      end;

      then

       A16: F is closed by Th42;

      S c= F

      proof

         {} in { {} } by TARSKI:def 1;

        then

        reconsider r = { [ {} , {} ]} as Relation of { {} } by RELSET_1: 3;

        set R = RelStr (# { {} }, r #);

         A17:

        now

          let x,y be Element of R;

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

          then [x, y] in { [ {} , {} ]} by TARSKI:def 1;

          hence x <= y by ORDERS_2:def 5;

        end;

        

         A18: R is transitive by A17;

        R is directed

        proof

          let x,y be Element of R;

          take x;

          thus thesis by A17;

        end;

        then

        reconsider R as transitive directed non empty RelStr by A18;

        let x be object;

        set V = ( the_universe_of the carrier of T);

        assume

         A19: x in S;

        then

        reconsider q = x as Point of CC;

        set N = ( ConstantNet (R,q));

        the mapping of N = (the carrier of N --> q) by Def5;

        then ( rng the mapping of N) = {q} by FUNCOP_1: 8;

        then

         A20: ( rng the mapping of N) c= S by A19, ZFMISC_1: 31;

         {} in V by CLASSES2: 56;

        then

         A21: the carrier of R in V by CLASSES2: 2;

        the carrier of CC = the carrier of T by Def24;

        then

        reconsider M = N as constant strict net of T by Lm6;

        

         A22: ( the_value_of N) = q by Th13;

        then ( the_value_of the mapping of M) = q by Def8;

        then

         A23: ( the_value_of M) = q by Def8;

         the RelStr of N = the RelStr of R by Def5;

        then M in ( NetUniv T) by A21, Def11;

        then

         A24: [M, q] in C by A23, Def20;

        q in ( Lim N) by A22, Th33;

        hence thesis by A24, A20;

      end;

      then ( Cl S) c= F by A16, TOPS_1: 5;

      then p in F by A1;

      then ex q be Point of CC st p = q & ex N be net of ( ConvergenceSpace C) st [N, q] in C & ( rng the mapping of N) c= S & q in ( Lim N);

      hence thesis;

    end;

    theorem :: YELLOW_6:44

    for T be non empty 1-sorted, C be Convergence-Class of T holds ( Convergence ( ConvergenceSpace C)) = C iff C is topological

    proof

      let T be non empty 1-sorted, C be Convergence-Class of T;

      set CC = ( ConvergenceSpace C), CCC = ( Convergence ( ConvergenceSpace C));

      

       A1: the carrier of ( ConvergenceSpace C) = the carrier of T by Def24;

      

       A2: for N be net of T, n be net of CC st N = n holds for x be subnet of n holds x is subnet of N

      proof

        let N be net of T, n be net of CC such that

         A3: N = n;

        let X be subnet of n;

        reconsider x = X as net of T by Def24;

        consider f be Function of X, n such that

         A4: the mapping of X = (the mapping of n * f) and

         A5: for m be Element of n holds ex n be Element of X st for p be Element of X st n <= p holds m <= (f . p) by Def9;

        reconsider f as Function of x, N by A3;

        the mapping of x = (the mapping of N * f) by A3, A4;

        hence thesis by A3, A5, Def9;

      end;

      

       A6: for N be net of T, n be net of CC st N = n holds for X be subnet of N holds X is subnet of n

      proof

        let N be net of T, n be net of CC such that

         A7: N = n;

        let X be subnet of N;

        reconsider x = X as net of CC by Def24;

        consider f be Function of X, N such that

         A8: the mapping of X = (the mapping of N * f) and

         A9: for m be Element of N holds ex n be Element of X st for p be Element of X st n <= p holds m <= (f . p) by Def9;

        reconsider f as Function of x, n by A7;

        the mapping of x = (the mapping of n * f) by A7, A8;

        hence thesis by A7, A9, Def9;

      end;

      

       A10: for N be net of T holds N is net of CC by Def24;

      hereby

        assume

         A11: CCC = C;

        

         A12: C is (SUBNETS)

        proof

          let N be net of T, Y be subnet of N;

          reconsider M = N as net of CC by Def24;

          reconsider X = Y as subnet of M by A6;

          assume Y in ( NetUniv T);

          then

           A13: X in ( NetUniv CC) by A1, Lm7;

          let p be Element of T;

          reconsider q = p as Element of CC by Def24;

          assume [N, p] in C;

          then [M, q] in CCC by A11;

          hence thesis by A11, A13, Def21;

        end;

        

         A14: C is (ITERATED_LIMITS)

        proof

          let X be net of T, p be Element of T;

          reconsider q = p as Element of CC by Def24;

          reconsider x = X as net of CC by Def24;

          assume

           A15: [X, p] in C;

          let J be net_set of the carrier of X, T;

          reconsider I = J as ManySortedSet of the carrier of x;

          I is net_set of the carrier of x, CC

          proof

            let i be set;

            assume i in ( rng I);

            then i is net of T by Def12;

            hence thesis by A10;

          end;

          then

          reconsider I = J as net_set of the carrier of x, CC;

          assume

           A16: for i be Element of X holds [(J . i), (X . i)] in C;

          now

            let i be Element of x;

            reconsider j = i as Element of X;

            (X . j) = (x . i);

            hence [(I . i), (x . i)] in CCC by A11, A16;

          end;

          then

           A17: [( Iterated I), q] in CCC by A11, A15, Def23;

          

           A18: the RelStr of ( Iterated I) = [:X, ( product J):] by Def13

          .= the RelStr of ( Iterated J) by Def13;

           A19:

          now

            let j be object;

            assume j in ( dom the mapping of ( Iterated I));

            then

            reconsider jj = j as Element of ( Iterated I);

            the carrier of ( Iterated I) = [:the carrier of x, ( product ( Carrier I)):] by Th26;

            then

            consider j1 be Element of x, j2 be Element of ( product ( Carrier I)) such that

             A20: jj = [j1, j2] by DOMAIN_1: 1;

            reconsider i1 = j1 as Element of X;

            reconsider j2 as Element of ( product I) by YELLOW_1:def 4;

            set i2 = j2;

            the carrier of ( Iterated J) = [:the carrier of X, ( product ( Carrier J)):] by Th26;

            then

            reconsider i = [i1, i2] as Element of ( Iterated J) by ZFMISC_1: 87;

            

            thus (the mapping of ( Iterated I) . j) = (( Iterated I) . jj)

            .= (the mapping of (I . j1) . (j2 . j1)) by A20, Th27

            .= (the mapping of (J . i1) . (i2 . i1))

            .= (( Iterated J) . i) by Th27

            .= (the mapping of ( Iterated J) . j) by A20;

          end;

          ( dom the mapping of ( Iterated I)) = the carrier of ( Iterated I) by FUNCT_2:def 1;

          then ( dom the mapping of ( Iterated I)) = ( dom the mapping of ( Iterated J)) by A18, FUNCT_2:def 1;

          then the mapping of ( Iterated I) = the mapping of ( Iterated J) by A19, FUNCT_1: 2;

          hence thesis by A11, A17, A18;

        end;

        

         A21: C is (DIVERGENCE)

        proof

          let X be net of T, p be Element of T;

          reconsider q = p as Element of CC by Def24;

          reconsider x = X as net of CC by Def24;

          assume X in ( NetUniv T);

          then

           A22: x in ( NetUniv CC) by A1, Lm7;

          assume not [X, p] in C;

          then

          consider y be subnet of x such that

           A23: y in ( NetUniv CC) and

           A24: not ex z be subnet of y st [z, q] in CCC by A11, A22, Def22;

          reconsider Y = y as subnet of X by A2;

          take Y;

          thus Y in ( NetUniv T) by A1, A23, Lm7;

          let Z be subnet of Y;

          reconsider z = Z as subnet of y by A6;

           not [z, q] in CCC by A24;

          hence thesis by A11;

        end;

        C is (CONSTANTS)

        proof

          let N be constant net of T;

          reconsider M = N as net of CC by Def24;

          the mapping of N is constant;

          then the mapping of M is constant;

          then

          reconsider M as constant net of CC by Def4;

          assume N in ( NetUniv T);

          then

           A25: M in ( NetUniv CC) by A1, Lm7;

          ( the_value_of M) = ( the_value_of the mapping of M) by Def8

          .= ( the_value_of the mapping of N)

          .= ( the_value_of N) by Def8;

          hence thesis by A11, A25, Def20;

        end;

        hence C is topological by A12, A21, A14;

      end;

      assume

       A26: C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS);

      then

      reconsider C9 = C as topological Convergence-Class of T;

      

       A27: ( Convergence ( ConvergenceSpace C)) c= C

      proof

        let x,y be object;

        assume

         A28: [x, y] in ( Convergence CC);

        ( Convergence CC) c= [:( NetUniv CC), the carrier of CC:] by Def18;

        then

        consider M be Element of ( NetUniv CC), p be Element of CC such that

         A29: [x, y] = [M, p] by A28, DOMAIN_1: 1;

        reconsider q = p as Point of T by Def24;

        

         A30: M in ( NetUniv CC);

        

         A31: ex N be strict net of CC st N = M & the carrier of N in ( the_universe_of the carrier of CC) by Def11;

        assume

         A32: not [x, y] in C;

        reconsider M as net of CC by A31;

        reconsider N = M as net of T by Def24;

        N in ( NetUniv T) by A1, A30, Lm7;

        then

        consider Y be subnet of N such that

         A33: Y in ( NetUniv T) and

         A34: not ex Z be subnet of Y st [Z, q] in C by A26, A29, A32;

        reconsider Y9 = Y as subnet of M by A6;

        reconsider YY = the RelStr of Y as transitive directed non empty RelStr by Lm1, Lm2;

        set X = ( ConstantNet (YY,q));

        defpred P[ object, object] means ex i be Element of Y, Ji be net of T st $1 = i & Ji = $2 & [Ji, p] in C & ( rng the mapping of Ji) c= { (Y . c) where c be Element of Y : i <= c };

        

         A35: the RelStr of X = YY by Def5;

        reconsider X as constant non empty strict net of T;

        

         A36: p in ( Lim M) by A28, A29, Def19;

        

         A37: for x be object st x in the carrier of X holds ex j be object st P[x, j]

        proof

          let x be object;

          assume x in the carrier of X;

          then

          reconsider i9 = x as Element of Y9 by Th4;

          reconsider i = i9 as Element of Y;

          ( Lim M) c= ( Lim Y9) by Th32;

          then

          consider S be Subset of CC such that

           A38: S = { (Y9 . c) where c be Element of Y9 : i9 <= c } and

           A39: p in ( Cl S) by A36, Th34;

          consider Go be net of ( ConvergenceSpace C9) such that

           A40: [Go, p] in C9 and

           A41: ( rng the mapping of Go) c= S and p in ( Lim Go) by A39, Th43;

          reconsider Ji = Go as net of T by Def24;

          take Ji, i, Ji;

          thus x = i & Ji = Ji & [Ji, p] in C by A40;

          let e be object;

          assume e in ( rng the mapping of Ji);

          then e in S by A41;

          then

          consider c9 be Element of Y9 such that

           A42: e = (Y9 . c9) and

           A43: i9 <= c9 by A38;

          reconsider cc = c9 as Element of Y;

          e = (Y . cc) by A42;

          hence thesis by A43;

        end;

        consider J be ManySortedSet of the carrier of X such that

         A44: for x be object st x in the carrier of X holds P[x, (J . x)] from PBOOLE:sch 3( A37);

        now

          let x be set;

          assume x in the carrier of X;

          then ex i be Element of Y, Ji be net of T st x = i & Ji = (J . x) & [Ji, p] in C & ( rng the mapping of Ji) c= { (Y . c) where c be Element of Y : i <= c } by A44;

          hence (J . x) is net of T;

        end;

        then

        reconsider J as yielding_non-empty_carriers net_set of the carrier of X, T by Th24;

        reconsider X9 = X as net of CC by Def24;

        

         A45: the mapping of X9 is constant;

        

         A46: for i be Element of X holds [(J . i), (X . i)] in C

        proof

          let i be Element of X;

          ex ii be Element of Y, Ji be net of T st i = ii & Ji = (J . i) & [Ji, p] in C & ( rng the mapping of Ji) c= { (Y . c) where c be Element of Y : ii <= c } by A44;

          hence thesis by Th5;

        end;

        

         A47: ( the_value_of X) = q by Th13;

        reconsider X9 as constant net of CC by A45, Def4;

        

         A48: the RelStr of ( Iterated J) = [:X, ( product J):] by Def13;

        then

         A49: the carrier of ( Iterated J) = [:the carrier of X, the carrier of ( product J):] by YELLOW_3:def 2;

        

         A50: ( Iterated J) is subnet of Y

        proof

          set F = the Element of ( product J);

          set h = the mapping of ( Iterated J), g = the mapping of Y9;

          defpred P[ object, object, object] means ex f be Function, x be Element of X st (f . $2) = $1 & x = $3 & (the mapping of (J . x) . $2) = (the mapping of Y . $1);

          deffunc F( Element of Y) = { c where c be Element of Y : $1 <= c };

          consider B be ManySortedSet of the carrier of Y such that

           A51: for i be Element of Y holds (B . i) = F(i) from PBOOLE:sch 5;

          now

            assume {} in ( rng B);

            then

            consider i be object such that

             A52: i in ( dom B) and

             A53: (B . i) = {} by FUNCT_1:def 3;

            reconsider i as Element of Y by A52;

            consider j be Element of Y such that

             A54: i <= j and i <= j by Def3;

            j in { c where c be Element of Y : i <= c } by A54;

            hence contradiction by A51, A53;

          end;

          then

          reconsider B as non-empty ManySortedSet of the carrier of Y by RELAT_1:def 9;

          deffunc F( Element of X) = the carrier of (J . $1);

          consider M be ManySortedSet of the carrier of X such that

           A55: for x be Element of X holds (M . x) = F(x) from PBOOLE:sch 5;

          reconsider B9 = B as non-empty ManySortedSet of the carrier of X by A35;

          

           A56: for i be object st i in the carrier of X holds for x be object st x in (M . i) holds ex y be object st y in (B9 . i) & P[y, x, i]

          proof

            let i be object such that

             A57: i in the carrier of X;

            consider e be Element of Y, Ji be net of T such that

             A58: i = e and

             A59: Ji = (J . i) and [Ji, p] in C and

             A60: ( rng the mapping of Ji) c= { (Y . c) where c be Element of Y : e <= c } by A44, A57;

            reconsider i9 = i as Element of X by A57;

            defpred P[ object, object] means (the mapping of Ji . $1) = (the mapping of Y . $2);

            

             A61: for ji be Element of Ji holds ex u be Element of (B9 . i9) st P[ji, u]

            proof

              let ji be Element of Ji;

              ji in the carrier of Ji;

              then ji in ( dom the mapping of Ji) by FUNCT_2:def 1;

              then (the mapping of Ji . ji) in ( rng the mapping of Ji) by FUNCT_1:def 3;

              then (the mapping of Ji . ji) in { (Y . c) where c be Element of Y : e <= c } by A60;

              then

              consider c be Element of Y such that

               A62: (the mapping of Ji . ji) = (Y . c) and

               A63: e <= c;

              c in { cc where cc be Element of Y : e <= cc } by A63;

              then

              reconsider c as Element of (B9 . i9) by A51, A58;

              take c;

              thus (the mapping of Ji . ji) = (the mapping of Y . c) by A62;

            end;

            consider f be Function of Ji, (B9 . i9) such that

             A64: for ji be Element of Ji holds P[ji, (f . ji)] from FUNCT_2:sch 3( A61);

            let x be object;

            assume x in (M . i);

            then

            reconsider ji = x as Element of Ji by A55, A57, A59;

            reconsider f as Function of Ji, (B . i);

            take (f . x);

            (f . ji) in (B . i);

            hence (f . x) in (B9 . i);

            take f, i9;

            thus (f . x) = (f . x) & i9 = i;

            

            thus (the mapping of (J . i9) . x) = (the mapping of Ji . ji) by A59

            .= (the mapping of Y . (f . x)) by A64;

          end;

          consider u be ManySortedFunction of M, B9 such that

           A65: for i be object st i in the carrier of X holds ex f be Function of (M . i), (B9 . i) st f = (u . i) & for x be object st x in (M . i) holds P[(f . x), x, i] from MSSUBFAM:sch 1( A56);

          deffunc F( Element of X, Element of ( product J)) = ((u . $1) . ($2 . $1));

          

           A66: for x be Element of X, y be Element of ( product J) holds F(x,y) in the carrier of Y

          proof

            let x be Element of X, y be Element of ( product J);

            reconsider x9 = x as Element of X9;

            reconsider k = x as Element of Y by A35;

            defpred P[ Element of Y] means k <= $1;

            set ZZ = { c where c be Element of Y : P[c] };

            

             A67: ZZ is Subset of Y from DOMAIN_1:sch 7;

            x9 in the carrier of X9;

            then

             A68: x9 in ( dom ( Carrier J)) by PARTFUN1:def 2;

            y in the carrier of ( product J);

            then y in ( product ( Carrier J)) by YELLOW_1:def 4;

            then (y . x9) in (( Carrier J) . x9) by A68, CARD_3: 9;

            then (y . x9) in the carrier of (J . x) by Th2;

            then (u . k) is Function of (M . k), (B . k) & (y . x) in (M . k) by A55, PBOOLE:def 15;

            then

             A69: ((u . k) . (y . x)) in (B . k) by FUNCT_2: 5;

            (B . k) = ZZ by A51;

            hence thesis by A67, A69;

          end;

          consider f be Function of [:the carrier of X, the carrier of ( product J):], Y such that

           A70: for x be Element of X, y be Element of ( product J) holds (f . (x,y)) = F(x,y) from FUNCT_7:sch 1( A66);

          reconsider f as Function of ( Iterated J), Y by A49;

          

           A71: for x be Element of X, j be Element of (M . x) holds (the mapping of (J . x) . j) = (the mapping of Y . ((u . x) . j))

          proof

            let i be Element of X, j be Element of (M . i);

            consider f be Function of (M . i), (B9 . i) such that

             A72: f = (u . i) and

             A73: for x be object st x in (M . i) holds P[(f . x), x, i] by A65;

            (M . i) = the carrier of (J . i) by A55;

            then P[(f . j), j, i] by A73;

            hence thesis by A72;

          end;

          

           A74: for x be object st x in ( dom h) holds (h . x) = (g . (f . x))

          proof

            let x be object;

            assume x in ( dom h);

            then x in the carrier of ( Iterated J);

            then x in [:the carrier of X9, ( product ( Carrier J)):] by Th26;

            then x in [:the carrier of X9, the carrier of ( product J):] by YELLOW_1:def 4;

            then

            consider x1 be Element of X9, x2 be Element of ( product J) such that

             A75: x = [x1, x2] by DOMAIN_1: 1;

            reconsider x9 = x1 as Element of X;

            x2 in the carrier of ( product J);

            then

             A76: x2 in ( product ( Carrier J)) by YELLOW_1:def 4;

            ( dom ( Carrier J)) = the carrier of X9 & the carrier of (J . x9) = (( Carrier J) . x1) by Th2, PARTFUN1:def 2;

            then (x2 . x1) in the carrier of (J . x9) by A76, CARD_3: 9;

            then

            reconsider j = (x2 . x1) as Element of (M . x9) by A55;

            

            thus (h . x) = (h . (x1,x2)) by A75

            .= (the mapping of (J . x9) . (x2 . x1)) by Def13

            .= (g . ((u . x9) . j)) by A71

            .= (g . (f . (x1,x2))) by A70

            .= (g . (f . x)) by A75;

          end;

          take f;

          for x be object holds x in ( dom h) iff x in ( dom f) & (f . x) in ( dom g)

          proof

            let x be object;

            hereby

              assume x in ( dom h);

              then x in the carrier of ( Iterated J);

              then x in [:the carrier of X9, ( product ( Carrier J)):] by Th26;

              then

               A77: x in [:the carrier of X9, the carrier of ( product J):] by YELLOW_1:def 4;

              hence x in ( dom f) by FUNCT_2:def 1;

              (f . x) in the carrier of Y by A77, FUNCT_2: 5;

              hence (f . x) in ( dom g) by FUNCT_2:def 1;

            end;

            assume that

             A78: x in ( dom f) and (f . x) in ( dom g);

            x in [:the carrier of X9, the carrier of ( product J):] by A78, FUNCT_2:def 1;

            then x in [:the carrier of X9, ( product ( Carrier J)):] by YELLOW_1:def 4;

            then x in the carrier of ( Iterated J) by Th26;

            hence thesis by FUNCT_2:def 1;

          end;

          hence the mapping of ( Iterated J) = (the mapping of Y * f) by A74, FUNCT_1: 10;

          let m be Element of Y;

          reconsider n = [m, F] as Element of ( Iterated J) by A35, A49, ZFMISC_1: 87;

          take n;

          let p be Element of ( Iterated J);

          consider k9 be Element of X, G be Element of ( product J) such that

           A79: p = [k9, G] by A49, DOMAIN_1: 1;

          reconsider m9 = m as Element of X by A35;

          reconsider F as Element of ( product J);

          G in the carrier of ( product J);

          then

           A80: ( dom ( Carrier J)) = the carrier of X9 & G in ( product ( Carrier J)) by PARTFUN1:def 2, YELLOW_1:def 4;

          reconsider k = k9 as Element of Y by A35;

          

           A81: (f . (k9,G)) = ((u . k) . (G . k)) by A70;

          reconsider k99 = k9 as Element of X9;

          

           A82: (u . k) is Function of (M . k), (B . k) by PBOOLE:def 15;

          then

           A83: ( rng (u . k)) c= (B . k) by RELAT_1:def 19;

          ( dom (u . k)) = (M . k) by A82, FUNCT_2:def 1

          .= the carrier of (J . k9) by A55

          .= (( Carrier J) . k99) by Th2;

          then

           A84: (G . k99) in ( dom (u . k)) by A80, CARD_3: 9;

          reconsider k9 = k as Element of X;

          reconsider G as Element of ( product J);

          assume n <= p;

          then [m9, F] <= [k9, G] by A48, A79, Lm3;

          then m9 <= k9 by YELLOW_3: 11;

          then

           A85: m <= k by A35, Lm3;

          (f . p) in ( rng (u . k)) by A79, A81, A84, FUNCT_1:def 3;

          then (f . p) in (B . k) by A83;

          then (f . p) in { c where c be Element of Y : k <= c } by A51;

          then ex c be Element of Y st c = (f . p) & k <= c;

          hence thesis by A85, YELLOW_0:def 2;

        end;

        

         A86: the RelStr of X = the RelStr of Y by Def5;

        ex N0 be strict net of T st N0 = Y & the carrier of N0 in ( the_universe_of the carrier of T) by A33, Def11;

        then X in ( NetUniv T) by A86, Def11;

        then [X, q] in C by A26, A47;

        then [( Iterated J), q] in C by A26, A46;

        hence contradiction by A34, A50;

      end;

      C c= ( Convergence ( ConvergenceSpace C)) by Th40;

      hence thesis by A27;

    end;