waybel_9.miz



    begin

    registration

      let L be non empty RelStr;

      cluster ( id L) -> monotone;

      coherence by YELLOW_2: 11;

    end

    definition

      let S,T be non empty RelStr, f be Function of S, T;

      :: original: antitone

      redefine

      :: WAYBEL_9:def1

      attr f is antitone means for x,y be Element of S st x <= y holds (f . x) >= (f . y);

      compatibility ;

    end

    theorem :: WAYBEL_9:1

    

     Th1: for S,T be RelStr, K,L be non empty RelStr holds for f be Function of S, T, g be Function of K, L st the RelStr of S = the RelStr of K & the RelStr of T = the RelStr of L & f = g & f is monotone holds g is monotone

    proof

      let S,T be RelStr, K,L be non empty RelStr, f be Function of S, T, g be Function of K, L such that

       A1: the RelStr of S = the RelStr of K and

       A2: the RelStr of T = the RelStr of L and

       A3: f = g and

       A4: f is monotone;

      reconsider S1 = S, T1 = T as non empty RelStr by A1, A2;

      let x,y be Element of K such that

       A5: x <= y;

      reconsider x1 = x, y1 = y as Element of S1 by A1;

      reconsider f1 = f as Function of S1, T1;

      x1 <= y1 by A1, A5;

      then (f1 . x1) <= (f1 . y1) by A4, WAYBEL_1:def 2;

      hence (g . x) <= (g . y) by A2, A3;

    end;

    theorem :: WAYBEL_9:2

    

     Th2: for S,T be RelStr, K,L be non empty RelStr holds for f be Function of S, T, g be Function of K, L st the RelStr of S = the RelStr of K & the RelStr of T = the RelStr of L & f = g & f is antitone holds g is antitone

    proof

      let S,T be RelStr, K,L be non empty RelStr, f be Function of S, T, g be Function of K, L such that

       A1: the RelStr of S = the RelStr of K and

       A2: the RelStr of T = the RelStr of L and

       A3: f = g and

       A4: f is antitone;

      reconsider S1 = S, T1 = T as non empty RelStr by A1, A2;

      let x,y be Element of K such that

       A5: x <= y;

      reconsider x1 = x, y1 = y as Element of S1 by A1;

      reconsider f1 = f as Function of S1, T1;

      x1 <= y1 by A1, A5;

      then (f1 . x1) >= (f1 . y1) by A4;

      hence thesis by A2, A3;

    end;

    theorem :: WAYBEL_9:3

    for A,B be 1-sorted holds for F be Subset-Family of A, G be Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds G is Cover of B;

    

     Lm1: for L be antisymmetric reflexive with_infima RelStr, x be Element of L holds ( uparrow x) = { z where z be Element of L : (z "/\" x) = x }

    proof

      let L be antisymmetric reflexive with_infima RelStr, x be Element of L;

      thus ( uparrow x) c= { z where z be Element of L : (z "/\" x) = x }

      proof

        let q be object;

        assume

         A1: q in ( uparrow x);

        then

        reconsider q1 = q as Element of L;

        x <= q1 by A1, WAYBEL_0: 18;

        then (q1 "/\" x) = x by YELLOW_0: 25;

        hence thesis;

      end;

      let q be object;

      assume q in { z where z be Element of L : (z "/\" x) = x };

      then

      consider z be Element of L such that

       A2: q = z and

       A3: (z "/\" x) = x;

      x <= z by A3, YELLOW_0: 25;

      hence thesis by A2, WAYBEL_0: 18;

    end;

    theorem :: WAYBEL_9:4

    

     Th4: for L be antisymmetric reflexive with_suprema RelStr, x be Element of L holds ( uparrow x) = ( {x} "\/" ( [#] L))

    proof

      let L be antisymmetric reflexive with_suprema RelStr, x be Element of L;

      

       A1: ( {x} "\/" ( [#] L)) = { (x "\/" s) where s be Element of L : s in ( [#] L) } by YELLOW_4: 15;

      thus ( uparrow x) c= ( {x} "\/" ( [#] L))

      proof

        let q be object;

        assume

         A2: q in ( uparrow x);

        then

        reconsider q1 = q as Element of L;

        x <= q1 by A2, WAYBEL_0: 18;

        then (x "\/" q1) = q1 by YELLOW_0: 24;

        hence thesis by A1;

      end;

      let q be object;

      assume q in ( {x} "\/" ( [#] L));

      then

      consider z be Element of L such that

       A3: q = (x "\/" z) and z in ( [#] L) by A1;

      x <= (x "\/" z) by YELLOW_0: 22;

      hence thesis by A3, WAYBEL_0: 18;

    end;

    

     Lm2: for L be antisymmetric reflexive with_suprema RelStr, x be Element of L holds ( downarrow x) = { z where z be Element of L : (z "\/" x) = x }

    proof

      let L be antisymmetric reflexive with_suprema RelStr, x be Element of L;

      thus ( downarrow x) c= { z where z be Element of L : (z "\/" x) = x }

      proof

        let q be object;

        assume

         A1: q in ( downarrow x);

        then

        reconsider q1 = q as Element of L;

        x >= q1 by A1, WAYBEL_0: 17;

        then (q1 "\/" x) = x by YELLOW_0: 24;

        hence thesis;

      end;

      let q be object;

      assume q in { z where z be Element of L : (z "\/" x) = x };

      then

      consider z be Element of L such that

       A2: q = z and

       A3: (z "\/" x) = x;

      x >= z by A3, YELLOW_0: 24;

      hence thesis by A2, WAYBEL_0: 17;

    end;

    theorem :: WAYBEL_9:5

    

     Th5: for L be antisymmetric reflexive with_infima RelStr, x be Element of L holds ( downarrow x) = ( {x} "/\" ( [#] L))

    proof

      let L be antisymmetric reflexive with_infima RelStr, x be Element of L;

      

       A1: ( {x} "/\" ( [#] L)) = { (x "/\" s) where s be Element of L : s in ( [#] L) } by YELLOW_4: 42;

      thus ( downarrow x) c= ( {x} "/\" ( [#] L))

      proof

        let q be object;

        assume

         A2: q in ( downarrow x);

        then

        reconsider q1 = q as Element of L;

        x >= q1 by A2, WAYBEL_0: 17;

        then (x "/\" q1) = q1 by YELLOW_0: 25;

        hence thesis by A1;

      end;

      let q be object;

      assume q in ( {x} "/\" ( [#] L));

      then

      consider z be Element of L such that

       A3: q = (x "/\" z) and z in ( [#] L) by A1;

      (x "/\" z) <= x by YELLOW_0: 23;

      hence thesis by A3, WAYBEL_0: 17;

    end;

    theorem :: WAYBEL_9:6

    for L be antisymmetric reflexive with_infima RelStr, y be Element of L holds ((y "/\" ) .: ( uparrow y)) = {y}

    proof

      let L be antisymmetric reflexive with_infima RelStr, y be Element of L;

      thus ((y "/\" ) .: ( uparrow y)) c= {y}

      proof

        let q be object;

        assume q in ((y "/\" ) .: ( uparrow y));

        then

        consider a be object such that a in ( dom (y "/\" )) and

         A1: a in ( uparrow y) and

         A2: q = ((y "/\" ) . a) by FUNCT_1:def 6;

        reconsider a as Element of L by A1;

        

         A3: y <= a by A1, WAYBEL_0: 18;

        q = (y "/\" a) by A2, WAYBEL_1:def 18

        .= y by A3, YELLOW_0: 25;

        hence thesis by TARSKI:def 1;

      end;

      let q be object;

      assume q in {y};

      then

       A4: q = y by TARSKI:def 1;

      y <= y;

      then

       A5: ( dom (y "/\" )) = the carrier of L & y in ( uparrow y) by FUNCT_2:def 1, WAYBEL_0: 18;

      y = (y "/\" y) by YELLOW_0: 25

      .= ((y "/\" ) . y) by WAYBEL_1:def 18;

      hence thesis by A4, A5, FUNCT_1:def 6;

    end;

    theorem :: WAYBEL_9:7

    

     Th7: for L be antisymmetric reflexive with_infima RelStr, x be Element of L holds ((x "/\" ) " {x}) = ( uparrow x)

    proof

      let L be antisymmetric reflexive with_infima RelStr, x be Element of L;

      thus ((x "/\" ) " {x}) c= ( uparrow x)

      proof

        let q be object;

        assume

         A1: q in ((x "/\" ) " {x});

        then

        reconsider q1 = q as Element of L;

        

         A2: ((x "/\" ) . q1) in {x} by A1, FUNCT_1:def 7;

        (x "/\" q1) = ((x "/\" ) . q1) by WAYBEL_1:def 18

        .= x by A2, TARSKI:def 1;

        then x <= q1 by YELLOW_0: 25;

        hence thesis by WAYBEL_0: 18;

      end;

      let q be object;

      assume

       A3: q in ( uparrow x);

      then

      reconsider q1 = q as Element of L;

      

       A4: x <= q1 by A3, WAYBEL_0: 18;

      ((x "/\" ) . q1) = (x "/\" q1) by WAYBEL_1:def 18

      .= x by A4, YELLOW_0: 25;

      then ( dom (x "/\" )) = the carrier of L & ((x "/\" ) . q1) in {x} by FUNCT_2:def 1, TARSKI:def 1;

      hence thesis by FUNCT_1:def 7;

    end;

    theorem :: WAYBEL_9:8

    

     Th8: for T be non empty 1-sorted, N be non empty NetStr over T holds N is_eventually_in ( rng the mapping of N)

    proof

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

      set i = the Element of N;

      take i;

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

      thus thesis by FUNCT_2: 4;

    end;

    

     Lm3: for L be non empty reflexive transitive RelStr holds for D be non empty directed Subset of L holds for n be Function of D, the carrier of L holds NetStr (# D, (the InternalRel of L |_2 D), n #) is net of L

    proof

      let L be non empty reflexive transitive RelStr, D be non empty directed Subset of L, n be Function of D, the carrier of L;

      set N = NetStr (# D, (the InternalRel of L |_2 D), n #);

      the InternalRel of N c= the InternalRel of L by XBOOLE_1: 17;

      then

      reconsider N as SubRelStr of L by YELLOW_0:def 13;

      reconsider N as full SubRelStr of L by YELLOW_0:def 14;

      N is directed

      proof

        let x,y be Element of N;

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

        reconsider x1 = x, y1 = y as Element of D;

        consider z1 be Element of L such that

         A1: z1 in D and

         A2: x1 <= z1 & y1 <= z1 by WAYBEL_0:def 1;

        reconsider z = z1 as Element of N by A1;

        take z;

        thus z in ( [#] N);

        thus thesis by A2, YELLOW_0: 60;

      end;

      then

      reconsider N as prenet of L;

      N is transitive;

      hence thesis;

    end;

    registration

      let L be non empty reflexive RelStr, D be non empty directed Subset of L, n be Function of D, the carrier of L;

      cluster NetStr (# D, (the InternalRel of L |_2 D), n #) -> directed;

      coherence by WAYBEL_2: 19;

    end

    registration

      let L be non empty reflexive transitive RelStr, D be non empty directed Subset of L, n be Function of D, the carrier of L;

      cluster NetStr (# D, (the InternalRel of L |_2 D), n #) -> transitive;

      coherence by Lm3;

    end

    theorem :: WAYBEL_9:9

    

     Th9: for L be non empty reflexive transitive RelStr st for x be Element of L, N be net of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L))))) holds L is satisfying_MC

    proof

      let L be non empty reflexive transitive RelStr such that

       A1: for x be Element of L, N be net of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L)))));

      let x be Element of L, D be non empty directed Subset of L;

      reconsider n = ( id D) as Function of D, the carrier of L by FUNCT_2: 7;

      set N = NetStr (# D, (the InternalRel of L |_2 D), n #);

      

       A2: N is eventually-directed & ( Sup ( netmap (N,L))) = ( sup N) by WAYBEL_2: 20;

      D c= D;

      

      then

       A3: D = (n .: D) by FUNCT_1: 92

      .= ( rng ( netmap (N,L))) by RELSET_1: 22;

      

      hence (x "/\" ( sup D)) = (x "/\" ( Sup ( netmap (N,L)))) by YELLOW_2:def 5

      .= ( sup ( {x} "/\" D)) by A1, A3, A2;

    end;

    theorem :: WAYBEL_9:10

    

     Th10: for L be non empty RelStr, a be Element of L, N be net of L holds (a "/\" N) is net of L

    proof

      let L be non empty RelStr, a be Element of L, N be net of L;

      set aN = (a "/\" N);

      aN is transitive

      proof

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

         A1: x <= y & y <= z;

        reconsider x1 = x, y1 = y, z1 = z as Element of N by WAYBEL_2: 22;

        

         A2: the RelStr of N = the RelStr of aN by WAYBEL_2:def 3;

        then x1 <= y1 & y1 <= z1 by A1;

        then x1 <= z1 by YELLOW_0:def 2;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    registration

      let L be non empty RelStr, x be Element of L, N be net of L;

      cluster (x "/\" N) -> transitive;

      coherence by Th10;

    end

    registration

      let L be non empty RelStr, x be Element of L, N be non empty reflexive NetStr over L;

      cluster (x "/\" N) -> reflexive;

      coherence

      proof

         the RelStr of N = the RelStr of (x "/\" N) by WAYBEL_2:def 3;

        then the InternalRel of (x "/\" N) is_reflexive_in the carrier of (x "/\" N) by ORDERS_2:def 2;

        hence thesis;

      end;

    end

    registration

      let L be non empty RelStr, x be Element of L, N be non empty antisymmetric NetStr over L;

      cluster (x "/\" N) -> antisymmetric;

      coherence

      proof

         the RelStr of N = the RelStr of (x "/\" N) by WAYBEL_2:def 3;

        then the InternalRel of (x "/\" N) is_antisymmetric_in the carrier of (x "/\" N) by ORDERS_2:def 4;

        hence thesis;

      end;

    end

    registration

      let L be non empty RelStr, x be Element of L, N be non empty transitive NetStr over L;

      cluster (x "/\" N) -> transitive;

      coherence

      proof

         the RelStr of N = the RelStr of (x "/\" N) by WAYBEL_2:def 3;

        then the InternalRel of (x "/\" N) is_transitive_in the carrier of (x "/\" N) by ORDERS_2:def 3;

        hence thesis;

      end;

    end

    registration

      let L be non empty RelStr, J be set, f be Function of J, the carrier of L;

      cluster ( FinSups f) -> transitive;

      coherence

      proof

        let x,y,z be Element of ( FinSups f) such that

         A1: x <= y and

         A2: y <= z;

        

         A3: (ex g be Function of ( Fin J), the carrier of L st for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & ( FinSups f) = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #)) & ( InclPoset ( Fin J)) = RelStr (# ( Fin J), ( RelIncl ( Fin J)) #) by WAYBEL_2:def 2, YELLOW_1:def 1;

        then

        reconsider x1 = x, y1 = y, z1 = z as Element of ( InclPoset ( Fin J));

        y1 <= z1 by A2, A3;

        then

         A4: y1 c= z1 by YELLOW_1: 3;

        x1 <= y1 by A1, A3;

        then x1 c= y1 by YELLOW_1: 3;

        then x1 c= z1 by A4;

        then x1 <= z1 by YELLOW_1: 3;

        hence thesis by A3;

      end;

    end

    begin

    definition

      let L be non empty RelStr, N be NetStr over L;

      :: WAYBEL_9:def2

      func inf N -> Element of L equals ( Inf the mapping of N);

      coherence ;

    end

    definition

      let L be RelStr, N be NetStr over L;

      :: WAYBEL_9:def3

      pred ex_sup_of N means ex_sup_of (( rng the mapping of N),L);

      :: WAYBEL_9:def4

      pred ex_inf_of N means ex_inf_of (( rng the mapping of N),L);

    end

    definition

      let L be RelStr;

      :: WAYBEL_9:def5

      func L +id -> strict NetStr over L means

      : Def5: the RelStr of it = the RelStr of L & the mapping of it = ( id L);

      existence

      proof

        take NetStr (# the carrier of L, the InternalRel of L, ( id L) #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let L be non empty RelStr;

      cluster (L +id ) -> non empty;

      coherence

      proof

         the RelStr of L = the RelStr of (L +id ) by Def5;

        hence thesis;

      end;

    end

    registration

      let L be reflexive RelStr;

      cluster (L +id ) -> reflexive;

      coherence

      proof

         the RelStr of L = the RelStr of (L +id ) by Def5;

        then the InternalRel of (L +id ) is_reflexive_in the carrier of (L +id ) by ORDERS_2:def 2;

        hence thesis;

      end;

    end

    registration

      let L be antisymmetric RelStr;

      cluster (L +id ) -> antisymmetric;

      coherence

      proof

         the RelStr of L = the RelStr of (L +id ) by Def5;

        then the InternalRel of (L +id ) is_antisymmetric_in the carrier of (L +id ) by ORDERS_2:def 4;

        hence thesis;

      end;

    end

    registration

      let L be transitive RelStr;

      cluster (L +id ) -> transitive;

      coherence

      proof

         the RelStr of L = the RelStr of (L +id ) by Def5;

        then the InternalRel of (L +id ) is_transitive_in the carrier of (L +id ) by ORDERS_2:def 3;

        hence thesis;

      end;

    end

    registration

      let L be with_suprema RelStr;

      cluster (L +id ) -> directed;

      coherence

      proof

        

         A1: the RelStr of L = the RelStr of (L +id ) by Def5;

        then ( [#] L) = ( [#] (L +id ));

        hence ( [#] (L +id )) is directed by A1, WAYBEL_0: 3;

      end;

    end

    registration

      let L be directed RelStr;

      cluster (L +id ) -> directed;

      coherence

      proof

        ( [#] L) is directed & the RelStr of L = the RelStr of (L +id ) by Def5, WAYBEL_0:def 6;

        hence ( [#] (L +id )) is directed by WAYBEL_0: 3;

      end;

    end

    registration

      let L be non empty RelStr;

      cluster (L +id ) -> monotone eventually-directed;

      coherence

      proof

        set N = (L +id );

        ( netmap (N,L)) = ( id L) & the RelStr of N = the RelStr of L by Def5;

        then ( netmap ((L +id ),L)) is monotone by Th1;

        hence N is monotone;

        for i be Element of N holds ex j be Element of N st for k be Element of N st j <= k holds (N . i) <= (N . k)

        proof

          let i be Element of N;

          take j = i;

          let k be Element of N such that

           A1: j <= k;

          

           A2: the RelStr of N = the RelStr of L by Def5;

          the mapping of N = ( id L) by Def5;

          then (the mapping of N . i) = i & (the mapping of N . k) = k by A2;

          hence thesis by A1, A2;

        end;

        hence thesis by WAYBEL_0: 11;

      end;

    end

    definition

      let L be RelStr;

      :: WAYBEL_9:def6

      func L opp+id -> strict NetStr over L means

      : Def6: the carrier of it = the carrier of L & the InternalRel of it = (the InternalRel of L ~ ) & the mapping of it = ( id L);

      existence

      proof

        take NetStr (# the carrier of L, (the InternalRel of L ~ ), ( id L) #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: WAYBEL_9:11

    

     Th11: for L be RelStr holds the RelStr of (L ~ ) = the RelStr of (L opp+id )

    proof

      let L be RelStr;

      the InternalRel of (L ~ ) = the InternalRel of (L opp+id ) by Def6;

      hence thesis by Def6;

    end;

    registration

      let L be non empty RelStr;

      cluster (L opp+id ) -> non empty;

      coherence

      proof

         the RelStr of (L ~ ) = the RelStr of (L opp+id ) by Th11;

        hence thesis;

      end;

    end

    registration

      let L be reflexive RelStr;

      cluster (L opp+id ) -> reflexive;

      coherence

      proof

        the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;

        then

         A1: (the InternalRel of L ~ ) is_reflexive_in the carrier of L by ORDERS_1: 79;

        the InternalRel of (L opp+id ) = (the InternalRel of L ~ ) by Def6;

        hence the InternalRel of (L opp+id ) is_reflexive_in the carrier of (L opp+id ) by A1, Def6;

      end;

    end

    registration

      let L be antisymmetric RelStr;

      cluster (L opp+id ) -> antisymmetric;

      coherence

      proof

        the InternalRel of L is_antisymmetric_in the carrier of L by ORDERS_2:def 4;

        then

         A1: (the InternalRel of L ~ ) is_antisymmetric_in the carrier of L by ORDERS_1: 81;

        the InternalRel of (L opp+id ) = (the InternalRel of L ~ ) by Def6;

        then the InternalRel of (L opp+id ) is_antisymmetric_in the carrier of (L opp+id ) by A1, Def6;

        hence thesis;

      end;

    end

    registration

      let L be transitive RelStr;

      cluster (L opp+id ) -> transitive;

      coherence

      proof

        the InternalRel of L is_transitive_in the carrier of L by ORDERS_2:def 3;

        then

         A1: (the InternalRel of L ~ ) is_transitive_in the carrier of L by ORDERS_1: 80;

        the InternalRel of (L opp+id ) = (the InternalRel of L ~ ) by Def6;

        then the InternalRel of (L opp+id ) is_transitive_in the carrier of (L opp+id ) by A1, Def6;

        hence thesis;

      end;

    end

    registration

      let L be with_infima RelStr;

      cluster (L opp+id ) -> directed;

      coherence

      proof

        reconsider A = (L ~ ) as with_suprema RelStr by YELLOW_7: 16;

         the RelStr of (L ~ ) = the RelStr of (L opp+id ) & ( [#] A) = ( [#] (L opp+id )) by Def6, Th11;

        hence ( [#] (L opp+id )) is directed by WAYBEL_0: 3;

      end;

    end

    registration

      let L be non empty RelStr;

      cluster (L opp+id ) -> antitone eventually-filtered;

      coherence

      proof

        set N = (L opp+id );

        thus N is antitone

        proof

          reconsider f = ( id L) as Function of (L ~ ), L;

          reconsider g = f as Function of L, (L ~ );

          g is antitone by YELLOW_7: 40;

          then

           A1: the RelStr of L = the RelStr of L & f is antitone by YELLOW_7: 41;

          ( netmap (N,L)) = ( id L) & the RelStr of (L opp+id ) = the RelStr of (L ~ ) by Def6, Th11;

          hence ( netmap (N,L)) is antitone by A1, Th2;

        end;

        for i be Element of N holds ex j be Element of N st for k be Element of N st j <= k holds (N . i) >= (N . k)

        proof

          let i be Element of N;

          take j = i;

          

           A2: the mapping of N = ( id L) & the InternalRel of N = (the InternalRel of L ~ ) by Def6;

          let k be Element of N;

          assume j <= k;

          then [i, k] in the InternalRel of N;

          then

           A3: [k, i] in (the InternalRel of N ~ ) by RELAT_1:def 7;

          reconsider i1 = i, k1 = k as Element of L by Def6;

          (( id L) . i1) = i1 & (( id L) . k1) = k1;

          hence thesis by A2, A3;

        end;

        hence thesis by WAYBEL_0: 12;

      end;

    end

    definition

      let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;

      :: WAYBEL_9:def7

      func N | i -> strict NetStr over L means

      : Def7: (for x be object holds x in the carrier of it iff ex y be Element of N st y = x & i <= y) & the InternalRel of it = (the InternalRel of N |_2 the carrier of it ) & the mapping of it = (the mapping of N | the carrier of it );

      existence

      proof

        defpred P[ object] means ex y be Element of N st y = $1 & i <= y;

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of N & P[x] from XBOOLE_0:sch 1;

        X c= the carrier of N by A1;

        then

        reconsider f = (the mapping of N | X) as Function of X, the carrier of L by FUNCT_2: 32;

        set IT = NetStr (# X, (the InternalRel of N |_2 X), f #);

        take IT;

        thus for x be object holds x in the carrier of IT iff ex y be Element of N st y = x & i <= y by A1;

        thus thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means ex y be Element of N st y = $1 & i <= y;

        let A,B be strict NetStr over L such that

         A2: for x be object holds x in the carrier of A iff P[x] and

         A3: the InternalRel of A = (the InternalRel of N |_2 the carrier of A) & the mapping of A = (the mapping of N | the carrier of A) and

         A4: for x be object holds x in the carrier of B iff P[x] and

         A5: the InternalRel of B = (the InternalRel of N |_2 the carrier of B) & the mapping of B = (the mapping of N | the carrier of B);

        the carrier of A = the carrier of B from XBOOLE_0:sch 2( A2, A4);

        hence thesis by A3, A5;

      end;

    end

    theorem :: WAYBEL_9:12

    for L be non empty 1-sorted, N be non empty NetStr over L holds for i be Element of N holds the carrier of (N | i) = { y where y be Element of N : i <= y }

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;

      thus the carrier of (N | i) c= { y where y be Element of N : i <= y }

      proof

        let q be object;

        assume q in the carrier of (N | i);

        then ex y be Element of N st y = q & i <= y by Def7;

        hence thesis;

      end;

      let q be object;

      assume q in { y where y be Element of N : i <= y };

      then ex y be Element of N st q = y & i <= y;

      hence thesis by Def7;

    end;

    theorem :: WAYBEL_9:13

    

     Th13: for L be non empty 1-sorted, N be non empty NetStr over L holds for i be Element of N holds the carrier of (N | i) c= the carrier of N

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;

      let x be object;

      assume x in the carrier of (N | i);

      then ex y be Element of N st y = x & i <= y by Def7;

      hence thesis;

    end;

    theorem :: WAYBEL_9:14

    

     Th14: for L be non empty 1-sorted, N be non empty NetStr over L holds for i be Element of N holds (N | i) is full SubNetStr of N

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N;

      

       A1: the mapping of (N | i) = (the mapping of N | the carrier of (N | i)) by Def7;

      the InternalRel of (N | i) = (the InternalRel of N |_2 the carrier of (N | i)) by Def7;

      then

       A2: the InternalRel of (N | i) c= the InternalRel of N by XBOOLE_1: 17;

      the carrier of (N | i) c= the carrier of N by Th13;

      then (N | i) is SubRelStr of N by A2, YELLOW_0:def 13;

      then

      reconsider K = (N | i) as SubNetStr of N by A1, YELLOW_6:def 6;

      the InternalRel of K = (the InternalRel of N |_2 the carrier of K) by Def7;

      then K is full SubRelStr of N by YELLOW_0:def 14, YELLOW_6:def 6;

      hence thesis by YELLOW_6:def 7;

    end;

    registration

      let L be non empty 1-sorted, N be non empty reflexive NetStr over L, i be Element of N;

      cluster (N | i) -> non empty reflexive;

      coherence

      proof

        

         A1: i <= i;

        hence (N | i) is non empty by Def7;

        reconsider A = (N | i) as strict non empty NetStr over L by A1, Def7;

        A is reflexive

        proof

          let x be Element of A;

          consider y be Element of N such that

           A2: y = x and i <= y by Def7;

          (N | i) is full SubNetStr of N & y <= y by Th14;

          hence thesis by A2, YELLOW_6: 12;

        end;

        hence thesis;

      end;

    end

    registration

      let L be non empty 1-sorted, N be non empty directed NetStr over L, i be Element of N;

      cluster (N | i) -> non empty;

      coherence

      proof

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

        hence thesis by Def7;

      end;

    end

    registration

      let L be non empty 1-sorted, N be non empty reflexive antisymmetric NetStr over L, i be Element of N;

      cluster (N | i) -> antisymmetric;

      coherence

      proof

        let x,y be Element of (N | i) such that

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

        consider y1 be Element of N such that

         A2: y1 = y and i <= y1 by Def7;

        consider x1 be Element of N such that

         A3: x1 = x and i <= x1 by Def7;

        (N | i) is SubNetStr of N by Th14;

        then x1 <= y1 & y1 <= x1 by A1, A3, A2, YELLOW_6: 11;

        hence thesis by A3, A2, YELLOW_0:def 3;

      end;

    end

    registration

      let L be non empty 1-sorted, N be non empty directed antisymmetric NetStr over L, i be Element of N;

      cluster (N | i) -> antisymmetric;

      coherence

      proof

        let x,y be Element of (N | i) such that

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

        consider y1 be Element of N such that

         A2: y1 = y and i <= y1 by Def7;

        consider x1 be Element of N such that

         A3: x1 = x and i <= x1 by Def7;

        (N | i) is SubNetStr of N by Th14;

        then x1 <= y1 & y1 <= x1 by A1, A3, A2, YELLOW_6: 11;

        hence thesis by A3, A2, YELLOW_0:def 3;

      end;

    end

    registration

      let L be non empty 1-sorted, N be non empty reflexive transitive NetStr over L, i be Element of N;

      cluster (N | i) -> transitive;

      coherence

      proof

        let x,y,z be Element of (N | i) such that

         A1: x <= y and

         A2: y <= z;

        consider z1 be Element of N such that

         A3: z1 = z and i <= z1 by Def7;

        consider x1 be Element of N such that

         A4: x1 = x and i <= x1 by Def7;

        consider y1 be Element of N such that

         A5: y1 = y and i <= y1 by Def7;

        

         A6: (N | i) is full SubNetStr of N by Th14;

        then

         A7: y1 <= z1 by A2, A5, A3, YELLOW_6: 11;

        x1 <= y1 by A1, A6, A4, A5, YELLOW_6: 11;

        then x1 <= z1 by A7, YELLOW_0:def 2;

        hence x <= z by A6, A4, A3, YELLOW_6: 12;

      end;

    end

    registration

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

      cluster (N | i) -> transitive directed;

      coherence

      proof

        thus (N | i) is transitive

        proof

          let x,y,z be Element of (N | i) such that

           A1: x <= y and

           A2: y <= z;

          consider z1 be Element of N such that

           A3: z1 = z and i <= z1 by Def7;

          consider x1 be Element of N such that

           A4: x1 = x and i <= x1 by Def7;

          consider y1 be Element of N such that

           A5: y1 = y and i <= y1 by Def7;

          

           A6: (N | i) is full SubNetStr of N by Th14;

          then

           A7: y1 <= z1 by A2, A5, A3, YELLOW_6: 11;

          x1 <= y1 by A1, A6, A4, A5, YELLOW_6: 11;

          then x1 <= z1 by A7, YELLOW_0:def 2;

          hence thesis by A6, A4, A3, YELLOW_6: 12;

        end;

        for x,y be Element of (N | i) holds ex z be Element of (N | i) st x <= z & y <= z

        proof

          let x,y be Element of (N | i);

          consider x1 be Element of N such that

           A8: x1 = x and

           A9: i <= x1 by Def7;

          consider y1 be Element of N such that

           A10: y1 = y and i <= y1 by Def7;

          consider z1 be Element of N such that

           A11: x1 <= z1 and

           A12: y1 <= z1 by YELLOW_6:def 3;

          i <= z1 by A9, A11, YELLOW_0:def 2;

          then

          reconsider z = z1 as Element of (N | i) by Def7;

          take z;

          (N | i) is full SubNetStr of N by Th14;

          hence thesis by A8, A10, A11, A12, YELLOW_6: 12;

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL_9:15

    for L be non empty 1-sorted, N be non empty reflexive NetStr over L holds for i,x be Element of N, x1 be Element of (N | i) st x = x1 holds (N . x) = ((N | i) . x1)

    proof

      let L be non empty 1-sorted, N be non empty reflexive NetStr over L, i,x be Element of N, x1 be Element of (N | i);

      assume x = x1;

      

      hence (N . x) = ((the mapping of N | the carrier of (N | i)) . x1) by FUNCT_1: 49

      .= ((N | i) . x1) by Def7;

    end;

    theorem :: WAYBEL_9:16

    

     Th16: for L be non empty 1-sorted, N be non empty directed NetStr over L holds for i,x be Element of N, x1 be Element of (N | i) st x = x1 holds (N . x) = ((N | i) . x1)

    proof

      let L be non empty 1-sorted, N be non empty directed NetStr over L, i,x be Element of N, x1 be Element of (N | i);

      assume x = x1;

      

      hence (N . x) = ((the mapping of N | the carrier of (N | i)) . x1) by FUNCT_1: 49

      .= ((N | i) . x1) by Def7;

    end;

    theorem :: WAYBEL_9:17

    

     Th17: for L be non empty 1-sorted, N be net of L, i be Element of N holds (N | i) is subnet of N

    proof

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

      reconsider A = (N | i) as net of L;

      

       A1: the carrier of A c= the carrier of N by Th13;

      A is subnet of N

      proof

        reconsider f = ( id the carrier of A) as Function of A, N by A1, FUNCT_2: 7;

        take f;

        for x be object st x in the carrier of A holds (the mapping of A . x) = ((the mapping of N * f) . x)

        proof

          let x be object such that

           A2: x in the carrier of A;

          

          thus (the mapping of A . x) = ((the mapping of N | the carrier of A) . x) by Def7

          .= (the mapping of N . x) by A2, FUNCT_1: 49

          .= (the mapping of N . (f . x)) by A2, FUNCT_1: 18

          .= ((the mapping of N * f) . x) by A2, FUNCT_2: 15;

        end;

        hence the mapping of A = (the mapping of N * f) by FUNCT_2: 12;

        let m be Element of N;

        consider z be Element of N such that

         A3: i <= z and

         A4: m <= z by YELLOW_6:def 3;

        reconsider n = z as Element of A by A3, Def7;

        take n;

        let p be Element of A such that

         A5: n <= p;

        reconsider p1 = p as Element of N by A1;

        A is SubNetStr of N by Th14;

        then z <= p1 by A5, YELLOW_6: 11;

        then m <= p1 by A4, YELLOW_0:def 2;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

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

      cluster strict for subnet of N;

      existence

      proof

        set A = NetStr (# the carrier of N, the InternalRel of N, the mapping of N #);

        

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

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

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

        then

        reconsider A as net of T by A1, WAYBEL_0:def 6, WAYBEL_8: 13;

        A is subnet of N

        proof

          reconsider f = ( id N) as Function of A, N;

          take f;

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

          let m be Element of N;

          reconsider n = m as Element of A;

          take n;

          let p be Element of A such that

           A2: n <= p;

          thus thesis by A2;

        end;

        then

        reconsider A as subnet of N;

        take A;

        thus thesis;

      end;

    end

    definition

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

      :: original: |

      redefine

      func N | i -> strict subnet of N ;

      coherence by Th17;

    end

    definition

      let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be NetStr over S;

      :: WAYBEL_9:def8

      func f * N -> strict NetStr over T means

      : Def8: the RelStr of it = the RelStr of N & the mapping of it = (f * the mapping of N);

      existence

      proof

        take NetStr (# the carrier of N, the InternalRel of N, (f * the mapping of N) #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be non empty NetStr over S;

      cluster (f * N) -> non empty;

      coherence

      proof

         the RelStr of N = the RelStr of (f * N) by Def8;

        hence thesis;

      end;

    end

    registration

      let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be reflexive NetStr over S;

      cluster (f * N) -> reflexive;

      coherence

      proof

         the RelStr of N = the RelStr of (f * N) by Def8;

        hence the InternalRel of (f * N) is_reflexive_in the carrier of (f * N) by ORDERS_2:def 2;

      end;

    end

    registration

      let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be antisymmetric NetStr over S;

      cluster (f * N) -> antisymmetric;

      coherence

      proof

         the RelStr of N = the RelStr of (f * N) by Def8;

        then the InternalRel of (f * N) is_antisymmetric_in the carrier of (f * N) by ORDERS_2:def 4;

        hence thesis;

      end;

    end

    registration

      let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be transitive NetStr over S;

      cluster (f * N) -> transitive;

      coherence

      proof

         the RelStr of N = the RelStr of (f * N) by Def8;

        then the InternalRel of (f * N) is_transitive_in the carrier of (f * N) by ORDERS_2:def 3;

        hence thesis;

      end;

    end

    registration

      let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be directed NetStr over S;

      cluster (f * N) -> directed;

      coherence

      proof

         the RelStr of N = the RelStr of (f * N) & ( [#] N) is directed by Def8, WAYBEL_0:def 6;

        hence ( [#] (f * N)) is directed by WAYBEL_0: 3;

      end;

    end

    theorem :: WAYBEL_9:18

    

     Th18: for L be non empty RelStr, N be non empty NetStr over L holds for x be Element of L holds ((x "/\" ) * N) = (x "/\" N)

    proof

      let L be non empty RelStr, N be non empty NetStr over L, x be Element of L;

      set n = the mapping of N;

      

       A1: the RelStr of ((x "/\" ) * N) = the RelStr of N by Def8

      .= the RelStr of (x "/\" N) by WAYBEL_2:def 3;

      

       A2: the RelStr of N = the RelStr of (x "/\" N) by WAYBEL_2:def 3;

      then

      reconsider f2 = the mapping of (x "/\" N) as Function of the carrier of N, the carrier of L;

      

       A3: for c be Element of N holds (((x "/\" ) * n) . c) = (f2 . c)

      proof

        let c be Element of N;

        consider y be Element of L such that

         A4: y = (n . c) and

         A5: (f2 . c) = (x "/\" y) by A2, WAYBEL_2:def 3;

        

        thus (((x "/\" ) * n) . c) = ((x "/\" ) . y) by A4, FUNCT_2: 15

        .= (f2 . c) by A5, WAYBEL_1:def 18;

      end;

      the mapping of ((x "/\" ) * N) = ((x "/\" ) * n) by Def8

      .= the mapping of (x "/\" N) by A3, FUNCT_2: 63;

      hence thesis by A1;

    end;

    begin

    theorem :: WAYBEL_9:19

    for S,T be TopStruct holds for F be Subset-Family of S, G be Subset-Family of T st the TopStruct of S = the TopStruct of T & F = G & F is open holds G is open

    proof

      let S,T be TopStruct, F be Subset-Family of S, G be Subset-Family of T such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: F = G & F is open;

      let P be Subset of T such that

       A3: P in G;

      reconsider R = P as Subset of S by A1;

      R is open by A2, A3;

      hence P in the topology of T by A1;

    end;

    theorem :: WAYBEL_9:20

    for S,T be TopStruct holds for F be Subset-Family of S, G be Subset-Family of T st the TopStruct of S = the TopStruct of T & F = G & F is closed holds G is closed

    proof

      let S,T be TopStruct, F be Subset-Family of S, G be Subset-Family of T such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: F = G & F is closed;

      let P be Subset of T such that

       A3: P in G;

      reconsider R = P as Subset of S by A1;

      R is closed by A2, A3;

      then (( [#] S) \ R) is open;

      hence (( [#] T) \ P) in the topology of T by A1;

    end;

    definition

      struct ( TopStruct, RelStr) TopRelStr (# the carrier -> set,

the InternalRel -> Relation of the carrier,

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

       attr strict strict;

    end

    registration

      let A be non empty set, R be Relation of A, A, T be Subset-Family of A;

      cluster TopRelStr (# A, R, T #) -> non empty;

      coherence ;

    end

    registration

      let x be set, R be Relation of {x};

      let T be Subset-Family of {x};

      cluster TopRelStr (# {x}, R, T #) -> 1 -element;

      coherence ;

    end

    registration

      let X be set, O be Order of X, T be Subset-Family of X;

      cluster TopRelStr (# X, O, T #) -> reflexive transitive antisymmetric;

      coherence

      proof

        set A = TopRelStr (# X, O, T #);

        

         A1: ( field the InternalRel of A) = the carrier of A by ORDERS_1: 12;

        then

         A2: the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 12;

        the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A by A1, RELAT_2:def 9, RELAT_2:def 16;

        hence thesis by A2;

      end;

    end

    

     Lm4: for tau be Subset-Family of { 0 }, r be Relation of { 0 } st tau = { {} , { 0 }} & r = { [ 0 , 0 ]} holds TopRelStr (# { 0 }, r, tau #) is reflexive discrete finite1 -element

    proof

      let tau be Subset-Family of { 0 }, r be Relation of { 0 } such that

       A1: tau = { {} , { 0 }} and

       A2: r = { [ 0 , 0 ]};

      set T = TopRelStr (# { 0 }, r, tau #);

      thus T is reflexive

      proof

        let x be Element of T;

        x = 0 by TARSKI:def 1;

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

        hence thesis by A2;

      end;

      the topology of T = ( bool the carrier of T) by A1, ZFMISC_1: 24;

      hence T is discrete by TDLAT_3:def 1;

      thus thesis;

    end;

    registration

      cluster reflexive discrete strict finite1 -element for TopRelStr;

      existence

      proof

         0 in { 0 } by TARSKI:def 1;

        then

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

         { {} , { 0 }} = ( bool { 0 }) by ZFMISC_1: 24;

        then

        reconsider tau = { {} , { 0 }} as Subset-Family of { 0 };

        take TopRelStr (# { 0 }, r, tau #);

        thus thesis by Lm4;

      end;

    end

    definition

      mode TopLattice is with_infima with_suprema reflexive transitive antisymmetric TopSpace-like TopRelStr;

    end

    registration

      cluster strict discrete finite compact Hausdorff1 -element for TopLattice;

      existence

      proof

        reconsider C = ( bool { 0 }) as Subset-Family of { 0 };

         0 in { 0 } by TARSKI:def 1;

        then

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

         { {} , { 0 }} = ( bool { 0 }) by ZFMISC_1: 24;

        then

        reconsider A = TopRelStr (# { 0 }, r, C #) as reflexive discrete finite1 -element TopRelStr by Lm4;

        reconsider A as TopLattice;

        take A;

        thus A is strict discrete finite;

        thus A is compact;

        thus A is Hausdorff

        proof

          let p,q be Point of A such that

           A1: not p = q;

          p = 0 by TARSKI:def 1;

          hence thesis by A1, TARSKI:def 1;

        end;

        thus thesis;

      end;

    end

    registration

      let T be Hausdorff non empty TopSpace;

      cluster -> Hausdorff for non empty SubSpace of T;

      coherence ;

    end

    theorem :: WAYBEL_9:21

    

     Th21: for T be non empty TopSpace, p be Point of T holds for A be Element of ( OpenNeighborhoods p) holds A is a_neighborhood of p

    proof

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

      ex W be Subset of T st W = A & p in W & W is open by YELLOW_6: 29;

      hence thesis by CONNSP_2: 3;

    end;

    theorem :: WAYBEL_9:22

    

     Th22: for T be non empty TopSpace, p be Point of T holds for A,B be Element of ( OpenNeighborhoods p) holds (A /\ B) is Element of ( OpenNeighborhoods p)

    proof

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

      consider W be Subset of T such that

       A1: W = A and

       A2: p in W & W is open by YELLOW_6: 29;

      consider X be Subset of T such that

       A3: X = B and

       A4: p in X & X is open by YELLOW_6: 29;

      p in (A /\ B) & (W /\ X) is open by A1, A2, A3, A4, XBOOLE_0:def 4;

      hence thesis by A1, A3, YELLOW_6: 30;

    end;

    theorem :: WAYBEL_9:23

    for T be non empty TopSpace, p be Point of T holds for A,B be Element of ( OpenNeighborhoods p) holds (A \/ B) is Element of ( OpenNeighborhoods p)

    proof

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

      consider W be Subset of T such that

       A1: W = A and

       A2: p in W and

       A3: W is open by YELLOW_6: 29;

      

       A4: p in (A \/ B) by A1, A2, XBOOLE_0:def 3;

      consider X be Subset of T such that

       A5: X = B and p in X and

       A6: X is open by YELLOW_6: 29;

      (W \/ X) is open by A3, A6;

      hence thesis by A1, A5, A4, YELLOW_6: 30;

    end;

    theorem :: WAYBEL_9:24

    

     Th24: for T be non empty TopSpace, p be Element of T holds for N be net of T st p in ( Lim N) holds for S be Subset of T st S = ( rng the mapping of N) holds p in ( Cl S)

    proof

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

       A1: p in ( Lim N);

      let S be Subset of T;

      assume S = ( rng the mapping of N);

      then

       A2: N is_eventually_in S by Th8;

      for G be Subset of T st G is open holds p in G implies S meets G

      proof

        let G be Subset of T such that

         A3: G is open and

         A4: p in G;

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

        then

        reconsider V = G as a_neighborhood of p by A4, CONNSP_2:def 1;

        N is_eventually_in V by A1, YELLOW_6:def 15;

        hence thesis by A2, YELLOW_6: 17;

      end;

      hence thesis by PRE_TOPC:def 7;

    end;

    theorem :: WAYBEL_9:25

    

     Th25: for T be Hausdorff TopLattice, N be convergent net of T holds for f be Function of T, T st f is continuous holds (f . ( lim N)) in ( Lim (f * N))

    proof

      let T be Hausdorff TopLattice, N be convergent net of T, f be Function of T, T such that

       A1: f is continuous;

      for V be a_neighborhood of (f . ( lim N)) holds (f * N) is_eventually_in V

      proof

        let V be a_neighborhood of (f . ( lim N));

        

         A2: ( dom f) = the carrier of T by FUNCT_2:def 1;

        consider O be a_neighborhood of ( lim N) such that

         A3: (f .: O) c= V by A1, BORSUK_1:def 1;

        ( lim N) in ( Lim N) by YELLOW_6:def 17;

        then N is_eventually_in O by YELLOW_6:def 15;

        then

        consider s0 be Element of N such that

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

        

         A5: the RelStr of (f * N) = the RelStr of N by Def8;

        then

        reconsider s1 = s0 as Element of (f * N);

        take s1;

        let j1 be Element of (f * N) such that

         A6: s1 <= j1;

        reconsider j = j1 as Element of N by A5;

        (N . j) in O by A4, A5, A6, YELLOW_0: 1;

        then

         A7: (f . (N . j)) in (f .: O) by A2, FUNCT_1:def 6;

        

         A8: the carrier of (f * N) = ( dom the mapping of N) by A5, FUNCT_2:def 1;

        ((f * N) . j1) = ((f * the mapping of N) . j1) by Def8

        .= (f . (N . j)) by A8, FUNCT_1: 13;

        hence thesis by A3, A7;

      end;

      hence thesis by YELLOW_6:def 15;

    end;

    theorem :: WAYBEL_9:26

    

     Th26: for T be Hausdorff TopLattice, N be convergent net of T holds for x be Element of T st (x "/\" ) is continuous holds (x "/\" ( lim N)) in ( Lim (x "/\" N))

    proof

      let T be Hausdorff TopLattice, N be convergent net of T, x be Element of T such that

       A1: (x "/\" ) is continuous;

      (x "/\" ( lim N)) = ((x "/\" ) . ( lim N)) by WAYBEL_1:def 18;

      then (x "/\" ( lim N)) in ( Lim ((x "/\" ) * N)) by A1, Th25;

      hence thesis by Th18;

    end;

    theorem :: WAYBEL_9:27

    

     Th27: for S be Hausdorff TopLattice, x be Element of S st for a be Element of S holds (a "/\" ) is continuous holds ( uparrow x) is closed

    proof

      let S be Hausdorff TopLattice, x be Element of S;

      assume for a be Element of S holds (a "/\" ) is continuous;

      then

       A1: (x "/\" ) is continuous;

      ((x "/\" ) " {x}) = ( uparrow x) & {x} is closed by Th7, PCOMPS_1: 7;

      hence thesis by A1;

    end;

    theorem :: WAYBEL_9:28

    

     Th28: for S be compact Hausdorff TopLattice, x be Element of S st for b be Element of S holds (b "/\" ) is continuous holds ( downarrow x) is closed

    proof

      let S be compact Hausdorff TopLattice, b be Element of S;

      assume for a be Element of S holds (a "/\" ) is continuous;

      then

       A1: (b "/\" ) is continuous;

      set g1 = (( rng (b "/\" )) |` (b "/\" ));

      

       A2: g1 = (b "/\" ) by RELAT_1: 94;

      

       A3: ( dom (b "/\" )) = the carrier of S by FUNCT_2:def 1;

      

       A4: ( {b} "/\" ( [#] S)) = { (b "/\" y) where y be Element of S : y in ( [#] S) } by YELLOW_4: 42;

      

       A5: ( rng (b "/\" )) = ( {b} "/\" ( [#] S))

      proof

        thus ( rng (b "/\" )) c= ( {b} "/\" ( [#] S))

        proof

          let q be object;

          assume q in ( rng (b "/\" ));

          then

          consider x be object such that

           A6: x in ( dom (b "/\" )) and

           A7: ((b "/\" ) . x) = q by FUNCT_1:def 3;

          reconsider x1 = x as Element of S by A6;

          q = (b "/\" x1) by A7, WAYBEL_1:def 18;

          hence thesis by A4;

        end;

        let q be object;

        assume q in ( {b} "/\" ( [#] S));

        then

        consider y be Element of S such that

         A8: q = (b "/\" y) and y in ( [#] S) by A4;

        q = ((b "/\" ) . y) by A8, WAYBEL_1:def 18;

        hence thesis by A3, FUNCT_1:def 3;

      end;

      

      then ( rng g1) = ( {b} "/\" ( [#] S)) by RELAT_1: 94

      .= ( [#] (S | ( rng (b "/\" )))) by A5, PRE_TOPC:def 5

      .= the carrier of (S | ( rng (b "/\" )));

      then

      reconsider g1 as Function of S, (S | ( rng (b "/\" ))) by A2, A3, FUNCT_2: 1;

      ( rng g1) = ( {b} "/\" ( [#] S)) by A5, RELAT_1: 94

      .= ( [#] (S | ( {b} "/\" ( [#] S)))) by PRE_TOPC:def 5;

      then (S | ( {b} "/\" ( [#] S))) is compact by A1, A2, A5, COMPTS_1: 14, PRE_TOPC: 27;

      then ( {b} "/\" ( [#] S)) is compact by COMPTS_1: 3;

      hence thesis by Th5;

    end;

    begin

    definition

      let T be non empty TopSpace, N be non empty NetStr over T, p be Point of T;

      :: WAYBEL_9:def9

      pred p is_a_cluster_point_of N means for O be a_neighborhood of p holds N is_often_in O;

    end

    theorem :: WAYBEL_9:29

    for L be non empty TopSpace, N be net of L holds for c be Point of L st c in ( Lim N) holds c is_a_cluster_point_of N

    proof

      let L be non empty TopSpace, N be net of L, c be Point of L such that

       A1: c in ( Lim N);

      let O be a_neighborhood of c;

      N is_eventually_in O by A1, YELLOW_6:def 15;

      hence thesis by YELLOW_6: 19;

    end;

    theorem :: WAYBEL_9:30

    

     Th30: for T be compact Hausdorff non empty TopSpace, N be net of T holds ex c be Point of T st c is_a_cluster_point_of N

    proof

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

      defpred P[ set, set] means ex X be Subset of T, a be Element of N st a = $1 & X = { (N . j) where j be Element of N : a <= j } & $2 = ( Cl X);

      

       A1: for e be Element of N holds ex u be Subset of T st P[e, u]

      proof

        let e be Element of N;

        reconsider a = e as Element of N;

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

        proof

          let q be object;

          assume q in { (N . j) where j be Element of N : a <= j };

          then ex j be Element of N st q = (N . j) & a <= j;

          hence thesis;

        end;

        then

        reconsider X = { (N . j) where j be Element of N : a <= j } as Subset of the carrier of T;

        take ( Cl X), X, a;

        thus thesis;

      end;

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

       A2: for e be Element of N holds P[e, (F . e)] from FUNCT_2:sch 3( A1);

      reconsider RF = ( rng F) as Subset-Family of T;

      

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

      

       A4: RF is centered

      proof

        thus RF <> {} by A3, RELAT_1: 42;

        defpred P[ set, set] means ex i be Element of N, h,Ch be Subset of T st i = $2 & Ch = $1 & h = { (N . j) where j be Element of N : i <= j } & Ch = ( Cl h);

        set J = { i where i be Element of N : ex h,Ch be Subset of T st h = { (N . j) where j be Element of N : i <= j } & Ch = ( Cl h) };

        let H be set such that

         A5: H <> {} and

         A6: H c= RF and

         A7: H is finite;

        reconsider H1 = H as non empty set by A5;

        set e = the Element of H1;

        e in RF by A6;

        then

        consider x be object such that

         A8: x in ( dom F) and e = (F . x) by FUNCT_1:def 3;

        reconsider x as Element of N by A8;

        consider X be Subset of T, a be Element of N such that a = x and

         A9: X = { (N . j) where j be Element of N : a <= j } & (F . x) = ( Cl X) by A2;

        a in J by A9;

        then

        reconsider J as non empty set;

        

         A10: for e be Element of H1 holds ex u be Element of J st P[e, u]

        proof

          let e be Element of H1;

          e in RF by A6;

          then

          consider x be object such that

           A11: x in ( dom F) and

           A12: e = (F . x) by FUNCT_1:def 3;

          reconsider x as Element of N by A11;

          consider X be Subset of T, a be Element of N such that

           A13: a = x and

           A14: X = { (N . j) where j be Element of N : a <= j } and

           A15: (F . x) = ( Cl X) by A2;

          a in J by A14, A15;

          then

          reconsider a as Element of J;

          take u = a, i = x, h = X, Ch = ( Cl X);

          thus i = u by A13;

          thus Ch = e by A12, A15;

          thus h = { (N . j) where j be Element of N : i <= j } by A13, A14;

          thus thesis;

        end;

        consider Q be Function of H1, J such that

         A16: for e be Element of H1 holds P[e, (Q . e)] from FUNCT_2:sch 3( A10);

        ( rng Q) c= ( [#] N)

        proof

          let q be object;

          assume q in ( rng Q);

          then

          consider x be object such that

           A17: x in ( dom Q) and

           A18: (Q . x) = q by FUNCT_1:def 3;

          reconsider x as Element of H1 by A17;

          ex i be Element of N, h,Ch be Subset of T st i = (Q . x) & Ch = x & h = { (N . j) where j be Element of N : i <= j } & Ch = ( Cl h) by A16;

          hence thesis by A18;

        end;

        then

        reconsider RQ = ( rng Q) as Subset of ( [#] N);

        

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

        ( dom Q) = H by FUNCT_2:def 1;

        then ( rng Q) is finite by A7, FINSET_1: 8;

        then

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

         A20: i0 is_>=_than RQ by A19, WAYBEL_0: 1;

        for Y be set holds Y in H implies (N . i0) in Y

        proof

          let Y be set;

          assume

           A21: Y in H;

          then

          consider i be Element of N, h,Ch be Subset of T such that

           A22: i = (Q . Y) and

           A23: Ch = Y and

           A24: h = { (N . j) where j be Element of N : i <= j } and

           A25: Ch = ( Cl h) by A16;

          Y in ( dom Q) by A21, FUNCT_2:def 1;

          then i in ( rng Q) by A22, FUNCT_1:def 3;

          then i <= i0 by A20;

          then

           A26: (N . i0) in h by A24;

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

          hence thesis by A23, A25, A26;

        end;

        hence thesis by A5, SETFAM_1:def 1;

      end;

      RF is closed

      proof

        let P be Subset of T;

        assume P in RF;

        then

        consider x be object such that

         A27: x in ( dom F) and

         A28: (F . x) = P by FUNCT_1:def 3;

        reconsider x as Element of N by A27;

        ex X be Subset of T, a be Element of N st a = x & X = { (N . j) where j be Element of N : a <= j } & (F . x) = ( Cl X) by A2;

        then P = ( Cl P) by A28;

        hence thesis;

      end;

      then ( meet RF) <> {} by A4, COMPTS_1: 4;

      then

      consider c be object such that

       A29: c in ( meet RF) by XBOOLE_0:def 1;

      reconsider c as Point of T by A29;

      take c;

      assume not c is_a_cluster_point_of N;

      then

      consider O be a_neighborhood of c such that

       A30: not N is_often_in O;

      N is_eventually_in (the carrier of T \ O) by A30, WAYBEL_0: 10;

      then

      consider s0 be Element of N such that

       A31: for j be Element of N st s0 <= j holds (N . j) in (the carrier of T \ O);

      consider Y be Subset of T, a be Element of N such that

       A32: a = s0 & Y = { (N . j) where j be Element of N : a <= j } and

       A33: (F . s0) = ( Cl Y) by A2;

      ( Cl Y) in RF by A3, A33, FUNCT_1:def 3;

      then

       A34: c in ( Cl Y) by A29, SETFAM_1:def 1;

       {} = (O /\ Y)

      proof

        thus {} c= (O /\ Y);

        let q be object such that

         A35: q in (O /\ Y);

        q in Y by A35, XBOOLE_0:def 4;

        then

        consider j be Element of N such that

         A36: q = (N . j) and

         A37: s0 <= j by A32;

        assume not q in {} ;

        (N . j) in (the carrier of T \ O) by A31, A37;

        then not (N . j) in O by XBOOLE_0:def 5;

        hence contradiction by A35, A36, XBOOLE_0:def 4;

      end;

      then O misses Y;

      then

       A38: ( Int O) misses Y by TOPS_1: 16, XBOOLE_1: 63;

      ( Int O) is open & c in ( Int O) by CONNSP_2:def 1;

      hence contradiction by A34, A38, PRE_TOPC:def 7;

    end;

    theorem :: WAYBEL_9:31

    

     Th31: for L be non empty TopSpace, N be net of L, M be subnet of N holds for c be Point of L st c is_a_cluster_point_of M holds c is_a_cluster_point_of N by YELLOW_6: 18;

    theorem :: WAYBEL_9:32

    

     Th32: for T be non empty TopSpace, N be net of T holds for x be Point of T st x is_a_cluster_point_of N holds ex M be subnet of N st x in ( Lim M)

    proof

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

       A1: x is_a_cluster_point_of N;

      set q = the Element of N;

      set S9 = { [s, O] where s be Element of N, O be Element of ( OpenNeighborhoods x) : (N . s) in O };

      reconsider O = ( [#] T) as Element of ( OpenNeighborhoods x) by YELLOW_6: 30;

      (N . q) in ( [#] T);

      then [q, O] in S9;

      then

      reconsider S9 as non empty set;

      set n = the mapping of N;

      defpred P[ set, set] means ex s1,s2 be Element of N st s1 = ($1 `1 ) & s2 = ($2 `1 ) & s1 <= s2 & ($2 `2 ) c= ($1 `2 );

      consider L be non empty strict RelStr such that

       A2: the carrier of L = S9 and

       A3: for a,b be Element of L holds a <= b iff P[a, b] from YELLOW_0:sch 1;

      deffunc F( Element of L) = (n . ($1 `1 ));

      

       A4: for a be Element of L holds F(a) in the carrier of T

      proof

        let a be Element of L;

        a in S9 by A2;

        then

        consider s be Element of N, O be Element of ( OpenNeighborhoods x) such that

         A5: a = [s, O] and (N . s) in O;

        (n . (a `1 )) = (n . s) by A5;

        hence thesis;

      end;

      consider g be Function of the carrier of L, the carrier of T such that

       A6: for x be Element of L holds (g . x) = F(x) from FUNCT_2:sch 8( A4);

      set M = NetStr (# the carrier of L, the InternalRel of L, g #);

      for a,b be Element of M holds ex z be Element of M st a <= z & b <= z

      proof

        let a,b be Element of M;

        a in S9 by A2;

        then

        consider aa be Element of N, Oa be Element of ( OpenNeighborhoods x) such that

         A7: a = [aa, Oa] and (N . aa) in Oa;

        b in S9 by A2;

        then

        consider bb be Element of N, Ob be Element of ( OpenNeighborhoods x) such that

         A8: b = [bb, Ob] and (N . bb) in Ob;

        consider z1 be Element of N such that

         A9: aa <= z1 and

         A10: bb <= z1 by YELLOW_6:def 3;

        Oa is a_neighborhood of x & Ob is a_neighborhood of x by Th21;

        then (Oa /\ Ob) is a_neighborhood of x by CONNSP_2: 2;

        then N is_often_in (Oa /\ Ob) by A1;

        then

        consider d be Element of N such that

         A11: z1 <= d and

         A12: (N . d) in (Oa /\ Ob);

        (Oa /\ Ob) is Element of ( OpenNeighborhoods x) by Th22;

        then [d, (Oa /\ Ob)] in S9 by A12;

        then

        reconsider z = [d, (Oa /\ Ob)] as Element of M by A2;

        reconsider A1 = a, C7 = b, z2 = z as Element of L;

        

         A13: (C7 `1 ) = bb & (C7 `2 ) = Ob by A8;

        take z;

        

         A14: (A1 `1 ) = aa & (A1 `2 ) = Oa by A7;

        

         A15: (z2 `1 ) = d & (z2 `2 ) = (Oa /\ Ob);

        (Oa /\ Ob) c= Ob & bb <= d by A10, A11, XBOOLE_1: 17, YELLOW_0:def 2;

        then

         A16: C7 <= z2 by A3, A13, A15;

        (Oa /\ Ob) c= Oa & aa <= d by A9, A11, XBOOLE_1: 17, YELLOW_0:def 2;

        then A1 <= z2 by A3, A14, A15;

        hence thesis by A16;

      end;

      then

      reconsider M as prenet of T by YELLOW_6:def 3;

      M is transitive

      proof

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

         A17: x <= y and

         A18: y <= z;

        reconsider x1 = x, y1 = y, z1 = z as Element of L;

        x1 <= y1 by A17;

        then

        consider sx,sy be Element of N such that

         A19: sx = (x1 `1 ) and

         A20: sy = (y1 `1 ) & sx <= sy & (y1 `2 ) c= (x1 `2 ) by A3;

        y1 <= z1 by A18;

        then

        consider s1,s2 be Element of N such that

         A21: s1 = (y1 `1 ) and

         A22: s2 = (z1 `1 ) and

         A23: s1 <= s2 & (z1 `2 ) c= (y1 `2 ) by A3;

        sx <= s2 & (z1 `2 ) c= (x1 `2 ) by A20, A21, A23, YELLOW_0:def 2;

        then x1 <= z1 by A3, A19, A22;

        hence thesis;

      end;

      then

      reconsider M as net of T;

      M is subnet of N

      proof

        deffunc F( Element of L) = ($1 `1 );

        

         A24: for a be Element of L holds F(a) in the carrier of N

        proof

          let a be Element of L;

          a in S9 by A2;

          then

          consider s be Element of N, O be Element of ( OpenNeighborhoods x) such that

           A25: a = [s, O] and (N . s) in O;

          (a `1 ) = s by A25;

          hence thesis;

        end;

        consider f be Function of the carrier of L, the carrier of N such that

         A26: for x be Element of L holds (f . x) = F(x) from FUNCT_2:sch 8( A24);

        reconsider f as Function of M, N;

        take f;

        for x be object st x in the carrier of M holds (g . x) = ((n * f) . x)

        proof

          let x be object;

          assume

           A27: x in the carrier of M;

          

          hence (g . x) = (n . (x `1 )) by A6

          .= (n . (f . x)) by A26, A27

          .= ((n * f) . x) by A27, FUNCT_2: 15;

        end;

        hence the mapping of M = (the mapping of N * f) by FUNCT_2: 12;

        let m be Element of N;

        (N . m) in ( [#] T);

        then [m, O] in S9;

        then

        reconsider n = [m, O] as Element of M by A2;

        take n;

        let p be Element of M such that

         A28: n <= p;

        reconsider n1 = n, p1 = p as Element of L;

        n1 <= p1 by A28;

        then

         A29: ex s1,s2 be Element of N st s1 = (n1 `1 ) & s2 = (p1 `1 ) & s1 <= s2 & (p1 `2 ) c= (n1 `2 ) by A3;

        (f . p) = (p `1 ) by A26;

        hence thesis by A29;

      end;

      then

      reconsider M as subnet of N;

      take M;

      for V be a_neighborhood of x holds M is_eventually_in V

      proof

        set i = the Element of N;

        let V be a_neighborhood of x;

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

        then

         A30: ( Int V) in the carrier of ( OpenNeighborhoods x) by YELLOW_6: 30;

        then ( Int V) is a_neighborhood of x by Th21;

        then N is_often_in ( Int V) by A1;

        then

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

         A31: (N . s) in ( Int V);

        

         A32: M is_eventually_in ( Int V)

        proof

           [s, ( Int V)] in S9 by A30, A31;

          then

          reconsider j = [s, ( Int V)] as Element of M by A2;

          take j;

          let s9 be Element of M such that

           A33: j <= s9;

          reconsider j1 = j, s1 = s9 as Element of L;

          j1 <= s1 by A33;

          then

           A34: ex s1,s2 be Element of N st s1 = (j `1 ) & s2 = (s9 `1 ) & s1 <= s2 & (s9 `2 ) c= (j `2 ) by A3;

          s9 in S9 by A2;

          then

          consider ss be Element of N, OO be Element of ( OpenNeighborhoods x) such that

           A35: s9 = [ss, OO] and

           A36: (N . ss) in OO;

          

           A37: (j `2 ) = ( Int V) & (s9 `2 ) = OO by A35;

          (M . s9) = (n . (s9 `1 )) by A6

          .= (N . ss) by A35;

          hence thesis by A36, A34, A37;

        end;

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

        hence thesis by A32, WAYBEL_0: 8;

      end;

      hence thesis by YELLOW_6:def 15;

    end;

    theorem :: WAYBEL_9:33

    

     Th33: for L be compact Hausdorff non empty TopSpace, N be net of L st for c,d be Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d holds for s be Point of L st s is_a_cluster_point_of N holds s in ( Lim N)

    proof

      let L be compact Hausdorff non empty TopSpace, N be net of L such that

       A1: for c,d be Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d;

      let c be Point of L such that

       A2: c is_a_cluster_point_of N;

      assume not c in ( Lim N);

      then

      consider M be subnet of N such that

       A3: not ex P be subnet of M st c in ( Lim P) by YELLOW_6: 37;

      consider d be Point of L such that

       A4: d is_a_cluster_point_of M by Th30;

      

       A5: d is_a_cluster_point_of N by A4, Th31;

      c <> d by A3, A4, Th32;

      hence contradiction by A1, A2, A5;

    end;

    theorem :: WAYBEL_9:34

    

     Th34: for S be non empty TopSpace, c be Point of S holds for N be net of S, A be Subset of S st c is_a_cluster_point_of N & A is closed & ( rng the mapping of N) c= A holds c in A

    proof

      let S be non empty TopSpace, c be Point of S, N be net of S, A be Subset of S such that

       A1: c is_a_cluster_point_of N and

       A2: A is closed and

       A3: ( rng the mapping of N) c= A;

      consider M be subnet of N such that

       A4: c in ( Lim M) by A1, Th32;

      reconsider R = ( rng the mapping of M) as Subset of S;

      ex f be Function of M, N st the mapping of M = (the mapping of N * f) & 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 YELLOW_6:def 9;

      then R c= ( rng the mapping of N) by RELAT_1: 26;

      then R c= A by A3;

      then

       A5: ( Cl R) c= ( Cl A) by PRE_TOPC: 19;

      c in ( Cl R) by A4, Th24;

      then c in ( Cl A) by A5;

      hence thesis by A2, PRE_TOPC: 22;

    end;

    

     Lm5: for S be compact Hausdorff TopLattice, N be net of S holds for c be Point of S, d be Element of S st c = d & (for x be Element of S holds (x "/\" ) is continuous) & N is eventually-directed & c is_a_cluster_point_of N holds d is_>=_than ( rng the mapping of N)

    proof

      let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be Element of S such that

       A1: c = d and

       A2: for x be Element of S holds (x "/\" ) is continuous and

       A3: N is eventually-directed and

       A4: c is_a_cluster_point_of N;

      let i be Element of S;

      assume i in ( rng the mapping of N);

      then

      consider iJ be object such that

       A5: iJ in ( dom the mapping of N) and

       A6: (the mapping of N . iJ) = i by FUNCT_1:def 3;

      reconsider i1 = iJ as Element of N by A5;

      ( uparrow (N . i1)) is closed by A2, Th27;

      then

       A7: ( Cl ( uparrow (N . i1))) = ( uparrow (N . i1)) by PRE_TOPC: 22;

      N is_eventually_in ( uparrow (N . i1))

      proof

        consider j be Element of N such that

         A8: for k be Element of N st j <= k holds (N . i1) <= (N . k) by A3, WAYBEL_0: 11;

        take j;

        let k be Element of N;

        assume j <= k;

        then (N . i1) <= (N . k) by A8;

        hence thesis by WAYBEL_0: 18;

      end;

      then

      consider t be Element of N such that

       A9: for j be Element of N st t <= j holds (N . j) in ( uparrow (N . i1));

      reconsider A = (N | t) as subnet of N;

      

       A10: ( rng the mapping of A) c= ( uparrow (N . i1))

      proof

        let q be object;

        assume q in ( rng the mapping of A);

        then

        consider x be object such that

         A11: x in ( dom the mapping of A) and

         A12: q = (the mapping of A . x) by FUNCT_1:def 3;

        reconsider x as Element of A by A11;

        consider y be Element of N such that

         A13: y = x and

         A14: t <= y by Def7;

        (A . x) = (N . y) by A13, Th16;

        hence thesis by A9, A12, A14;

      end;

      c is_a_cluster_point_of A

      proof

        let O be a_neighborhood of c;

        let i be Element of A;

        consider i2 be Element of N such that

         A15: i2 = i and

         A16: t <= i2 by Def7;

        N is_often_in O by A4;

        then

        consider j2 be Element of N such that

         A17: i2 <= j2 and

         A18: (N . j2) in O;

        t <= j2 by A16, A17, YELLOW_0:def 2;

        then

        reconsider j = j2 as Element of A by Def7;

        take j;

        A is full SubNetStr of N by Th14;

        hence i <= j by A15, A17, YELLOW_6: 12;

        thus thesis by A18, Th16;

      end;

      then

      consider M be subnet of A such that

       A19: c in ( Lim M) by Th32;

      reconsider R = ( rng the mapping of M) as Subset of S;

      

       A20: ( uparrow (N . i1)) = { z where z be Element of S : (z "/\" (N . i1)) = (N . i1) } by Lm1;

      ex f be Function of M, A st the mapping of M = (the mapping of A * f) & for m be Element of A holds ex n be Element of M st for p be Element of M st n <= p holds m <= (f . p) by YELLOW_6:def 9;

      then R c= ( rng the mapping of A) by RELAT_1: 26;

      then R c= ( uparrow (N . i1)) by A10;

      then

       A21: ( Cl R) c= ( Cl ( uparrow (N . i1))) by PRE_TOPC: 19;

      c in ( Cl R) by A19, Th24;

      then c in ( uparrow (N . i1)) by A7, A21;

      then ex z be Element of S st c = z & (z "/\" (N . i1)) = (N . i1) by A20;

      hence thesis by A1, A6, YELLOW_0: 25;

    end;

    

     Lm6: for S be compact Hausdorff TopLattice, N be net of S holds for c be Point of S, d be Element of S st c = d & (for x be Element of S holds (x "/\" ) is continuous) & c is_a_cluster_point_of N holds for b be Element of S st ( rng the mapping of N) is_<=_than b holds d <= b

    proof

      let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be Element of S such that

       A1: c = d and

       A2: for x be Element of S holds (x "/\" ) is continuous and

       A3: c is_a_cluster_point_of N;

      let b be Element of S such that

       A4: ( rng the mapping of N) is_<=_than b;

       A5:

      now

        let i be Element of N;

        

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

        (N . i) in ( rng the mapping of N) by A6, FUNCT_1:def 3;

        then (N . i) <= b by A4;

        then

         A7: (b "/\" (N . i)) = (N . i) by YELLOW_0: 25;

        b in {b} by TARSKI:def 1;

        hence (N . i) in ( {b} "/\" ( [#] S)) by A7, YELLOW_4: 37;

      end;

      

       A8: ( rng the mapping of N) c= ( {b} "/\" ( [#] S))

      proof

        let y be object;

        assume y in ( rng the mapping of N);

        then

        consider x be object such that

         A9: x in ( dom the mapping of N) and

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

        reconsider x as Element of N by A9;

        y = (N . x) by A10;

        hence thesis by A5;

      end;

      ( downarrow b) is closed by A2, Th28;

      then ( {b} "/\" ( [#] S)) is closed by Th5;

      then ( {b} "/\" ( [#] S)) = { (b "/\" y) where y be Element of S : y in ( [#] S) } & c in ( {b} "/\" ( [#] S)) by A3, A8, Th34, YELLOW_4: 42;

      then ex y be Element of S st c = (b "/\" y) & y in ( [#] S);

      hence thesis by A1, YELLOW_0: 23;

    end;

    theorem :: WAYBEL_9:35

    

     Th35: for S be compact Hausdorff TopLattice, c be Point of S holds for N be net of S st (for x be Element of S holds (x "/\" ) is continuous) & N is eventually-directed & c is_a_cluster_point_of N holds c = ( sup N)

    proof

      let S be compact Hausdorff TopLattice, c be Point of S, N be net of S such that

       A1: (for x be Element of S holds (x "/\" ) is continuous) & N is eventually-directed & c is_a_cluster_point_of N;

      reconsider c9 = c as Element of S;

      c9 is_>=_than ( rng the mapping of N) & for b be Element of S st ( rng the mapping of N) is_<=_than b holds c9 <= b by A1, Lm5, Lm6;

      

      hence c = ( sup ( rng the mapping of N)) by YELLOW_0: 30

      .= ( sup N) by YELLOW_2:def 5;

    end;

    

     Lm7: for S be compact Hausdorff TopLattice, N be net of S holds for c be Point of S, d be Element of S st c = d & (for x be Element of S holds (x "/\" ) is continuous) & N is eventually-filtered & c is_a_cluster_point_of N holds d is_<=_than ( rng the mapping of N)

    proof

      let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be Element of S such that

       A1: c = d and

       A2: for x be Element of S holds (x "/\" ) is continuous and

       A3: N is eventually-filtered and

       A4: c is_a_cluster_point_of N;

      let i be Element of S;

      assume i in ( rng the mapping of N);

      then

      consider iJ be object such that

       A5: iJ in ( dom the mapping of N) and

       A6: (the mapping of N . iJ) = i by FUNCT_1:def 3;

      reconsider i1 = iJ as Element of N by A5;

      ( downarrow (N . i1)) is closed by A2, Th28;

      then

       A7: ( Cl ( downarrow (N . i1))) = ( downarrow (N . i1)) by PRE_TOPC: 22;

      N is_eventually_in ( downarrow (N . i1))

      proof

        consider j be Element of N such that

         A8: for k be Element of N st j <= k holds (N . i1) >= (N . k) by A3, WAYBEL_0: 12;

        take j;

        let k be Element of N;

        assume j <= k;

        then (N . i1) >= (N . k) by A8;

        hence thesis by WAYBEL_0: 17;

      end;

      then

      consider t be Element of N such that

       A9: for j be Element of N st t <= j holds (N . j) in ( downarrow (N . i1));

      reconsider A = (N | t) as subnet of N;

      

       A10: ( rng the mapping of A) c= ( downarrow (N . i1))

      proof

        let q be object;

        assume q in ( rng the mapping of A);

        then

        consider x be object such that

         A11: x in ( dom the mapping of A) and

         A12: q = (the mapping of A . x) by FUNCT_1:def 3;

        reconsider x as Element of A by A11;

        consider y be Element of N such that

         A13: y = x and

         A14: t <= y by Def7;

        (A . x) = (N . y) by A13, Th16;

        hence thesis by A9, A12, A14;

      end;

      c is_a_cluster_point_of A

      proof

        let O be a_neighborhood of c;

        let i be Element of A;

        consider i2 be Element of N such that

         A15: i2 = i and

         A16: t <= i2 by Def7;

        N is_often_in O by A4;

        then

        consider j2 be Element of N such that

         A17: i2 <= j2 and

         A18: (N . j2) in O;

        t <= j2 by A16, A17, YELLOW_0:def 2;

        then

        reconsider j = j2 as Element of A by Def7;

        take j;

        A is full SubNetStr of N by Th14;

        hence i <= j by A15, A17, YELLOW_6: 12;

        thus thesis by A18, Th16;

      end;

      then

      consider M be subnet of A such that

       A19: c in ( Lim M) by Th32;

      reconsider R = ( rng the mapping of M) as Subset of S;

      

       A20: ( downarrow (N . i1)) = { z where z be Element of S : (z "\/" (N . i1)) = (N . i1) } by Lm2;

      ex f be Function of M, A st the mapping of M = (the mapping of A * f) & for m be Element of A holds ex n be Element of M st for p be Element of M st n <= p holds m <= (f . p) by YELLOW_6:def 9;

      then R c= ( rng the mapping of A) by RELAT_1: 26;

      then R c= ( downarrow (N . i1)) by A10;

      then

       A21: ( Cl R) c= ( Cl ( downarrow (N . i1))) by PRE_TOPC: 19;

      c in ( Cl R) by A19, Th24;

      then c in ( downarrow (N . i1)) by A7, A21;

      then ex z be Element of S st c = z & (z "\/" (N . i1)) = (N . i1) by A20;

      hence d <= i by A1, A6, YELLOW_0: 24;

    end;

    

     Lm8: for S be compact Hausdorff TopLattice, N be net of S holds for c be Point of S, d be Element of S st c = d & (for x be Element of S holds (x "/\" ) is continuous) & c is_a_cluster_point_of N holds for b be Element of S st ( rng the mapping of N) is_>=_than b holds d >= b

    proof

      let S be compact Hausdorff TopLattice, N be net of S, c be Point of S, d be Element of S such that

       A1: c = d and

       A2: for x be Element of S holds (x "/\" ) is continuous and

       A3: c is_a_cluster_point_of N;

      let b be Element of S such that

       A4: ( rng the mapping of N) is_>=_than b;

       A5:

      now

        let i be Element of N;

        

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

        (N . i) in ( rng the mapping of N) by A6, FUNCT_1:def 3;

        then (N . i) >= b by A4;

        then

         A7: (b "\/" (N . i)) = (N . i) by YELLOW_0: 24;

        b in {b} by TARSKI:def 1;

        hence (N . i) in ( {b} "\/" ( [#] S)) by A7, YELLOW_4: 10;

      end;

      

       A8: ( rng the mapping of N) c= ( {b} "\/" ( [#] S))

      proof

        let y be object;

        assume y in ( rng the mapping of N);

        then

        consider x be object such that

         A9: x in ( dom the mapping of N) and

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

        reconsider x as Element of N by A9;

        y = (N . x) by A10;

        hence thesis by A5;

      end;

      ( uparrow b) is closed by A2, Th27;

      then ( {b} "\/" ( [#] S)) is closed by Th4;

      then ( {b} "\/" ( [#] S)) = { (b "\/" y) where y be Element of S : y in ( [#] S) } & c in ( {b} "\/" ( [#] S)) by A3, A8, Th34, YELLOW_4: 15;

      then ex y be Element of S st c = (b "\/" y) & y in ( [#] S);

      hence thesis by A1, YELLOW_0: 22;

    end;

    theorem :: WAYBEL_9:36

    

     Th36: for S be compact Hausdorff TopLattice, c be Point of S holds for N be net of S st (for x be Element of S holds (x "/\" ) is continuous) & N is eventually-filtered & c is_a_cluster_point_of N holds c = ( inf N)

    proof

      let S be compact Hausdorff TopLattice, c be Point of S, N be net of S such that

       A1: (for x be Element of S holds (x "/\" ) is continuous) & N is eventually-filtered & c is_a_cluster_point_of N;

      reconsider c9 = c as Element of S;

      c9 is_<=_than ( rng the mapping of N) & for b be Element of S st ( rng the mapping of N) is_>=_than b holds c9 >= b by A1, Lm7, Lm8;

      

      hence c = ( inf ( rng the mapping of N)) by YELLOW_0: 31

      .= ( inf N) by YELLOW_2:def 6;

    end;

    begin

    theorem :: WAYBEL_9:37

    

     Th37: for S be Hausdorff TopLattice st (for N be net of S st N is eventually-directed holds ex_sup_of N & ( sup N) in ( Lim N)) & (for x be Element of S holds (x "/\" ) is continuous) holds S is meet-continuous

    proof

      let S be Hausdorff TopLattice such that

       A1: for N be net of S st N is eventually-directed holds ex_sup_of N & ( sup N) in ( Lim N) and

       A2: for x be Element of S holds (x "/\" ) is continuous;

      for X be non empty directed Subset of S holds ex_sup_of (X,S)

      proof

        let X be non empty directed Subset of S;

        reconsider n = ( id X) as Function of X, the carrier of S by FUNCT_2: 7;

        set N = NetStr (# X, (the InternalRel of S |_2 X), n #);

        N is eventually-directed by WAYBEL_2: 20;

        then

         A3: ex_sup_of N by A1;

        ( rng the mapping of N) = X by RELAT_1: 45;

        hence thesis by A3;

      end;

      hence S is up-complete by WAYBEL_0: 75;

      for x be Element of S, M be net of S st M is eventually-directed holds (x "/\" ( sup M)) = ( sup ( {x} "/\" ( rng ( netmap (M,S)))))

      proof

        let x be Element of S, M be net of S such that

         A4: M is eventually-directed;

        

         A5: ( sup M) in ( Lim M) by A1, A4;

        then

        reconsider M1 = M as convergent net of S by YELLOW_6:def 16;

        set xM = (x "/\" M);

        (x "/\" M) is eventually-directed by A4, WAYBEL_2: 27;

        then

         A6: ( sup xM) in ( Lim xM) by A1;

        (x "/\" ) is continuous by A2;

        then

         A7: (x "/\" ( lim M1)) in ( Lim (x "/\" M1)) by Th26;

        reconsider xM as convergent net of S by A6, YELLOW_6:def 16;

        

        thus (x "/\" ( sup M)) = (x "/\" ( lim M1)) by A5, YELLOW_6:def 17

        .= ( lim xM) by A7, YELLOW_6:def 17

        .= ( Sup the mapping of xM) by A6, YELLOW_6:def 17

        .= ( sup ( rng the mapping of xM)) by YELLOW_2:def 5

        .= ( sup ( {x} "/\" ( rng ( netmap (M,S))))) by WAYBEL_2: 23;

      end;

      hence thesis by Th9;

    end;

    theorem :: WAYBEL_9:38

    

     Th38: for S be compact Hausdorff TopLattice st for x be Element of S holds (x "/\" ) is continuous holds for N be net of S st N is eventually-directed holds ex_sup_of N & ( sup N) in ( Lim N)

    proof

      let S be compact Hausdorff TopLattice such that

       A1: for x be Element of S holds (x "/\" ) is continuous;

      let N be net of S such that

       A2: N is eventually-directed;

      

       A3: for c,d be Point of S st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d

      proof

        let c,d be Point of S such that

         A4: c is_a_cluster_point_of N and

         A5: d is_a_cluster_point_of N;

        

        thus c = ( sup N) by A1, A2, A4, Th35

        .= d by A1, A2, A5, Th35;

      end;

      consider c be Point of S such that

       A6: c is_a_cluster_point_of N by Th30;

      thus ex_sup_of N

      proof

        reconsider d = c as Element of S;

        set X = ( rng the mapping of N);

        X is_<=_than d & for b be Element of S st X is_<=_than b holds d <= b by A1, A2, A6, Lm5, Lm6;

        hence ex_sup_of (( rng the mapping of N),S) by YELLOW_0: 15;

      end;

      c = ( sup N) by A1, A2, A6, Th35;

      hence thesis by A6, A3, Th33;

    end;

    theorem :: WAYBEL_9:39

    

     Th39: for S be compact Hausdorff TopLattice st for x be Element of S holds (x "/\" ) is continuous holds for N be net of S st N is eventually-filtered holds ex_inf_of N & ( inf N) in ( Lim N)

    proof

      let S be compact Hausdorff TopLattice such that

       A1: for x be Element of S holds (x "/\" ) is continuous;

      let N be net of S such that

       A2: N is eventually-filtered;

      

       A3: for c,d be Point of S st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d

      proof

        let c,d be Point of S such that

         A4: c is_a_cluster_point_of N and

         A5: d is_a_cluster_point_of N;

        

        thus c = ( inf N) by A1, A2, A4, Th36

        .= d by A1, A2, A5, Th36;

      end;

      consider c be Point of S such that

       A6: c is_a_cluster_point_of N by Th30;

      thus ex_inf_of N

      proof

        reconsider d = c as Element of S;

        set X = ( rng the mapping of N);

        X is_>=_than d & for b be Element of S st X is_>=_than b holds d >= b by A1, A2, A6, Lm7, Lm8;

        hence ex_inf_of (( rng the mapping of N),S) by YELLOW_0: 16;

      end;

      c = ( inf N) by A1, A2, A6, Th36;

      hence thesis by A6, A3, Th33;

    end;

    theorem :: WAYBEL_9:40

    for S be compact Hausdorff TopLattice st for x be Element of S holds (x "/\" ) is continuous holds S is bounded

    proof

      let S be compact Hausdorff TopLattice such that

       A1: for x be Element of S holds (x "/\" ) is continuous;

      thus S is lower-bounded

      proof

        reconsider x = ( inf (S opp+id )) as Element of S;

        take x;

        

         A2: ( rng the mapping of (S opp+id )) = ( rng ( id S)) by Def6

        .= the carrier of S by RELAT_1: 45;

        then

         A3: x = ( "/\" (the carrier of S,S)) by YELLOW_2:def 6;

         ex_inf_of (S opp+id ) by A1, Th39;

        then ex_inf_of (the carrier of S,S) by A2;

        hence thesis by A3, YELLOW_0: 31;

      end;

      reconsider x = ( sup (S +id )) as Element of S;

      take x;

      

       A4: ( rng the mapping of (S +id )) = ( rng ( id S)) by Def5

      .= the carrier of S by RELAT_1: 45;

      then

       A5: x = ( "\/" (the carrier of S,S)) by YELLOW_2:def 5;

       ex_sup_of (S +id ) by A1, Th38;

      then ex_sup_of (the carrier of S,S) by A4;

      hence thesis by A5, YELLOW_0: 30;

    end;

    theorem :: WAYBEL_9:41

    for S be compact Hausdorff TopLattice st for x be Element of S holds (x "/\" ) is continuous holds S is meet-continuous

    proof

      let S be compact Hausdorff TopLattice;

      assume

       A1: for x be Element of S holds (x "/\" ) is continuous;

      then for N be net of S st N is eventually-directed holds ex_sup_of N & ( sup N) in ( Lim N) by Th38;

      hence thesis by A1, Th37;

    end;