waybel33.miz



    begin

    reserve x for set;

    definition

      let L be non empty Poset;

      let X be non empty Subset of L;

      let F be Filter of ( BoolePoset X);

      :: WAYBEL33:def1

      func lim_inf F -> Element of L equals ( "\/" ({ ( inf B) where B be Subset of L : B in F },L));

      correctness ;

    end

    theorem :: WAYBEL33:1

    for L1,L2 be complete LATTICE st the RelStr of L1 = the RelStr of L2 holds for X1 be non empty Subset of L1 holds for X2 be non empty Subset of L2 holds for F1 be Filter of ( BoolePoset X1), F2 be Filter of ( BoolePoset X2) st F1 = F2 holds ( lim_inf F1) = ( lim_inf F2)

    proof

      let L1,L2 be complete LATTICE such that

       A1: the RelStr of L1 = the RelStr of L2;

      let X1 be non empty Subset of L1;

      let X2 be non empty Subset of L2;

      let F1 be Filter of ( BoolePoset X1), F2 be Filter of ( BoolePoset X2) such that

       A2: F1 = F2;

      set Y2 = { ( inf B2) where B2 be Subset of L2 : B2 in F2 };

      set Y1 = { ( inf B1) where B1 be Subset of L1 : B1 in F1 };

      

       A3: Y2 c= Y1

      proof

        let x be object;

        assume x in Y2;

        then

        consider B2 be Subset of L2 such that

         A4: x = ( inf B2) and

         A5: B2 in F2;

        F1 c= the carrier of ( BoolePoset X1);

        then F1 c= ( bool X1) by WAYBEL_7: 2;

        then

        reconsider B1 = B2 as Subset of L1 by A2, A5, XBOOLE_1: 1;

        ( inf B1) = ( inf B2) by A1, YELLOW_0: 17, YELLOW_0: 27;

        hence thesis by A2, A4, A5;

      end;

      Y1 c= Y2

      proof

        let x be object;

        assume x in Y1;

        then

        consider B1 be Subset of L1 such that

         A6: x = ( inf B1) and

         A7: B1 in F1;

        F2 c= the carrier of ( BoolePoset X2);

        then F2 c= ( bool X2) by WAYBEL_7: 2;

        then

        reconsider B2 = B1 as Subset of L2 by A2, A7, XBOOLE_1: 1;

        ( inf B1) = ( inf B2) by A1, YELLOW_0: 17, YELLOW_0: 27;

        hence thesis by A2, A6, A7;

      end;

      then Y1 = Y2 by A3;

      hence thesis by A1, YELLOW_0: 17, YELLOW_0: 26;

    end;

    definition

      let L be non empty TopRelStr;

      :: WAYBEL33:def2

      attr L is lim-inf means

      : Def2: the topology of L = ( xi L);

    end

    registration

      cluster lim-inf -> TopSpace-like for non empty TopRelStr;

      coherence

      proof

        let L be non empty TopRelStr;

        set T = ( ConvergenceSpace ( lim_inf-Convergence L));

        assume L is lim-inf;

        

        then

         A1: the topology of L = ( xi L)

        .= the topology of T by WAYBEL28:def 4;

        

         A2: for a be Subset-Family of L st a c= the topology of L holds ( union a) in the topology of L

        proof

          let a be Subset-Family of L;

          reconsider b = a as Subset-Family of T by YELLOW_6:def 24;

          assume a c= the topology of L;

          then ( union b) in the topology of T by A1, PRE_TOPC:def 1;

          hence thesis by A1;

        end;

        the carrier of L = the carrier of T by YELLOW_6:def 24;

        then

         A3: the carrier of L in the topology of L by A1, PRE_TOPC:def 1;

        for a,b be Subset of L st a in the topology of L & b in the topology of L holds (a /\ b) in the topology of L by A1, PRE_TOPC:def 1;

        hence thesis by A3, A2;

      end;

    end

    registration

      cluster trivial -> lim-inf for TopLattice;

      coherence

      proof

        let L be TopLattice;

        assume L is trivial;

        then the carrier of L is 1 -element;

        then

        reconsider L9 = L as 1 -element TopLattice by STRUCT_0:def 19;

        the carrier of ( ConvergenceSpace ( lim_inf-Convergence L)) = the carrier of L9 by YELLOW_6:def 24;

        then

        reconsider S = ( ConvergenceSpace ( lim_inf-Convergence L)) as 1 -element TopSpace by STRUCT_0:def 19;

        set x = the Point of L9;

        reconsider y = x as Point of S by YELLOW_6:def 24;

        

        thus the topology of L = { {} , {y}} by YELLOW_9: 9

        .= the topology of S by YELLOW_9: 9

        .= ( xi L) by WAYBEL28:def 4;

      end;

    end

    registration

      cluster lim-inf continuous complete for TopLattice;

      existence

      proof

        take the 1 -element TopLattice;

        thus thesis;

      end;

    end

    theorem :: WAYBEL33:2

    

     Th2: for L1,L2 be non empty 1-sorted st the carrier of L1 = the carrier of L2 holds for N1 be NetStr over L1 holds ex N2 be strict NetStr over L2 st the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2

    proof

      let L1,L2 be non empty 1-sorted such that

       A1: the carrier of L1 = the carrier of L2;

      let N1 be NetStr over L1;

      reconsider f = the mapping of N1 as Function of the carrier of N1, the carrier of L2 by A1;

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

      thus thesis;

    end;

    theorem :: WAYBEL33:3

    

     Th3: for L1,L2 be non empty 1-sorted st the carrier of L1 = the carrier of L2 holds for N1 be NetStr over L1 st N1 in ( NetUniv L1) holds ex N2 be strict net of L2 st N2 in ( NetUniv L2) & the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2

    proof

      let L1,L2 be non empty 1-sorted such that

       A1: the carrier of L1 = the carrier of L2;

      let N1 be NetStr over L1;

      assume N1 in ( NetUniv L1);

      then

      consider N be strict net of L1 such that

       A2: N = N1 & the carrier of N in ( the_universe_of the carrier of L1) by YELLOW_6:def 11;

      reconsider f = the mapping of N as Function of the carrier of N, the carrier of L2 by A1;

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

      thus thesis by A1, A2, YELLOW_6:def 11;

    end;

     Lm1:

    now

      let L1,L2 be non empty RelStr;

      let N1 be net of L1, N2 be net of L2 such that

       A1: the RelStr of N1 = the RelStr of N2 and

       A2: the mapping of N1 = the mapping of N2;

      let j1 be Element of N1;

      deffunc I2( Element of N2) = { (N2 . i) where i be Element of N2 : i >= $1 };

      deffunc I1( Element of N1) = { (N1 . i) where i be Element of N1 : i >= $1 };

      let j2 be Element of N2 such that

       A3: j1 = j2;

      thus I1(j1) c= I2(j2)

      proof

        let y be object;

        assume y in I1(j1);

        then

        consider i1 be Element of N1 such that

         A4: y = (N1 . i1) and

         A5: i1 >= j1;

        reconsider i1 as Element of N1;

        reconsider i2 = i1, j2 as Element of N2 by A1;

        

         A6: (N1 . i1) = (N2 . i2) by A2;

        i2 >= j2 by A1, A3, A5, YELLOW_0: 1;

        hence thesis by A4, A6;

      end;

    end;

     Lm2:

    now

      let L1,L2 be /\-complete Semilattice such that

       A1: the RelStr of L1 = the RelStr of L2;

      let N1 be net of L1, N2 be net of L2 such that

       A2: the RelStr of N1 = the RelStr of N2 and

       A3: the mapping of N1 = the mapping of N2;

      deffunc I2( Element of N2) = { (N2 . i) where i be Element of N2 : i >= $1 };

      deffunc I1( Element of N1) = { (N1 . i) where i be Element of N1 : i >= $1 };

      set U1 = the set of all ( "/\" ( I1(j),L1)) where j be Element of N1;

      set U2 = the set of all ( "/\" ( I2(j),L2)) where j be Element of N2;

      thus U1 c= U2

      proof

        let x be object;

        assume x in U1;

        then

        consider j1 be Element of N1 such that

         A4: x = ( "/\" ( I1(j1),L1));

        reconsider j2 = j1 as Element of N2 by A2;

         I1(j1) c= I2(j2) & I2(j2) c= I1(j1) by A2, A3, Lm1;

        then

         A5: I1(j1) = I2(j2);

        reconsider j1 as Element of N1;

        

         A6: I1(j1) c= the carrier of L1

        proof

          let x be object;

          assume x in I1(j1);

          then ex i be Element of N1 st x = (N1 . i) & i >= j1;

          hence thesis;

        end;

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

        then

        consider j0 be Element of N1 such that j0 in the carrier of N1 and

         A7: j1 <= j0 and j1 <= j0;

        (N1 . j0) in I1(j1) by A7;

        then

        reconsider S = I1(j1) as non empty Subset of L1 by A6;

         ex_inf_of (S,L1) by WAYBEL_0: 76;

        then x = ( "/\" ( I2(j2),L2)) by A1, A4, A5, YELLOW_0: 27;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL33:4

    

     Th4: for L1,L2 be /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 holds for N1 be net of L1, N2 be net of L2 st the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2 holds ( lim_inf N1) = ( lim_inf N2)

    proof

      let L1,L2 be /\-complete up-complete Semilattice such that

       A1: the RelStr of L1 = the RelStr of L2;

      let N1 be net of L1, N2 be net of L2 such that

       A2: the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2;

      deffunc I2( Element of N2) = { (N2 . i) where i be Element of N2 : i >= $1 };

      deffunc I1( Element of N1) = { (N1 . i) where i be Element of N1 : i >= $1 };

      set U1 = the set of all ( "/\" ( I1(j),L1)) where j be Element of N1;

      set U2 = the set of all ( "/\" ( I2(j),L2)) where j be Element of N2;

      

       A3: ( lim_inf N1) = ( "\/" (U1,L1)) & ( lim_inf N2) = ( "\/" (U2,L2)) by WAYBEL11:def 6;

      U1 c= the carrier of L1

      proof

        let x be object;

        assume x in U1;

        then ex j be Element of N1 st x = ( "/\" ( I1(j),L1));

        hence thesis;

      end;

      then

      reconsider U1 as Subset of L1;

      U1 is non empty directed by WAYBEL32: 7;

      then

       A4: ex_sup_of (U1,L1) by WAYBEL_0: 75;

      U1 c= U2 & U2 c= U1 by A1, A2, Lm2;

      then U1 = U2;

      hence thesis by A1, A3, A4, YELLOW_0: 26;

    end;

    theorem :: WAYBEL33:5

    

     Th5: for L1,L2 be non empty 1-sorted st the carrier of L1 = the carrier of L2 holds for N1 be net of L1, N2 be net of L2 st the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2 holds for S1 be subnet of N1 holds ex S2 be strict subnet of N2 st the RelStr of S1 = the RelStr of S2 & the mapping of S1 = the mapping of S2

    proof

      let L1,L2 be non empty 1-sorted such that

       A1: the carrier of L1 = the carrier of L2;

      let N1 be net of L1, N2 be net of L2 such that

       A2: the RelStr of N1 = the RelStr of N2 and

       A3: the mapping of N1 = the mapping of N2;

      let S1 be subnet of N1;

      consider S2 be strict NetStr over L2 such that

       A4: the RelStr of S1 = the RelStr of S2 and

       A5: the mapping of S1 = the mapping of S2 by A1, Th2;

      reconsider S2 as strict net of L2 by A4;

      consider f be Function of S1, N1 such that

       A6: the mapping of S1 = (the mapping of N1 * f) and

       A7: for B5 be Element of N1 holds ex B6 be Element of S1 st for B7 be Element of S1 st B6 <= B7 holds B5 <= (f . B7) by YELLOW_6:def 9;

      reconsider g = f as Function of S2, N2 by A2, A4;

      S2 is subnet of N2

      proof

        take g;

        thus the mapping of S2 = (the mapping of N2 * g) by A3, A5, A6;

        let B2 be Element of N2;

        reconsider b2 = B2 as Element of N1 by A2;

        consider b6 be Element of S1 such that

         A8: for b7 be Element of S1 st b6 <= b7 holds b2 <= (f . b7) by A7;

        reconsider B3 = b6 as Element of S2 by A4;

        take B3;

        let B4 be Element of S2;

        reconsider b4 = B4 as Element of S1 by A4;

        assume B3 <= B4;

        then b6 <= b4 by A4, YELLOW_0: 1;

        then b2 <= (f . b4) by A8;

        hence thesis by A2, YELLOW_0: 1;

      end;

      hence thesis by A4, A5;

    end;

    theorem :: WAYBEL33:6

    

     Th6: for L1,L2 be /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 holds for N1 be NetStr over L1, a be set st [N1, a] in ( lim_inf-Convergence L1) holds ex N2 be strict net of L2 st [N2, a] in ( lim_inf-Convergence L2) & the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2

    proof

      let L1,L2 be /\-complete up-complete Semilattice such that

       A1: the RelStr of L1 = the RelStr of L2;

      let N1 be NetStr over L1, a be set;

      assume

       A2: [N1, a] in ( lim_inf-Convergence L1);

      ( lim_inf-Convergence L1) c= [:( NetUniv L1), the carrier of L1:] by YELLOW_6:def 18;

      then

      consider N,x be object such that

       A3: N in ( NetUniv L1) and

       A4: x in the carrier of L1 and

       A5: [N1, a] = [N, x] by A2, ZFMISC_1:def 2;

      reconsider x as Element of L1 by A4;

      

       A6: N = N1 by A5, XTUPLE_0: 1;

      then

      consider N2 be strict net of L2 such that

       A7: N2 in ( NetUniv L2) and

       A8: the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2 by A1, A3, Th3;

      ex N be strict net of L1 st N = N1 & the carrier of N in ( the_universe_of the carrier of L1) by A3, A6, YELLOW_6:def 11;

      then

      reconsider N1 as strict net of L1;

       A9:

      now

        let M be subnet of N2;

        consider M1 be strict subnet of N1 such that

         A10: the RelStr of M = the RelStr of M1 & the mapping of M = the mapping of M1 by A1, A8, Th5;

        

        thus x = ( lim_inf M1) by A2, A3, A5, A6, WAYBEL28:def 3

        .= ( lim_inf M) by A1, A10, Th4;

      end;

      take N2;

      x = a by A5, XTUPLE_0: 1;

      hence thesis by A1, A7, A8, A9, WAYBEL28:def 3;

    end;

    theorem :: WAYBEL33:7

    

     Th7: for L1,L2 be non empty 1-sorted holds for N1 be non empty NetStr over L1 holds for N2 be non empty NetStr over L2 st the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2 holds for X be set st N1 is_eventually_in X holds N2 is_eventually_in X

    proof

      let L1,L2 be non empty 1-sorted;

      let N1 be non empty NetStr over L1;

      let N2 be non empty NetStr over L2 such that

       A1: the RelStr of N1 = the RelStr of N2 and

       A2: the mapping of N1 = the mapping of N2;

      let X be set;

      given i1 be Element of N1 such that

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

      reconsider i2 = i1 as Element of N2 by A1;

      take i2;

      let j2 be Element of N2;

      reconsider j1 = j2 as Element of N1 by A1;

      assume i2 <= j2;

      then (N1 . j1) in X by A1, A3, YELLOW_0: 1;

      hence thesis by A2;

    end;

    

     Lm3: for L1,L2 be /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 holds the topology of ( ConvergenceSpace ( lim_inf-Convergence L1)) c= the topology of ( ConvergenceSpace ( lim_inf-Convergence L2))

    proof

      let L1,L2 be /\-complete up-complete Semilattice such that

       A1: the RelStr of L1 = the RelStr of L2;

      let x be object;

      

       A2: the topology of ( ConvergenceSpace ( lim_inf-Convergence L2)) = { V where V be Subset of L2 : for p be Element of L2 st p in V holds for N be net of L2 st [N, p] in ( lim_inf-Convergence L2) holds N is_eventually_in V } by YELLOW_6:def 24;

      

       A3: the topology of ( ConvergenceSpace ( lim_inf-Convergence L1)) = { V where V be Subset of L1 : for p be Element of L1 st p in V holds for N be net of L1 st [N, p] in ( lim_inf-Convergence L1) holds N is_eventually_in V } by YELLOW_6:def 24;

      assume x in the topology of ( ConvergenceSpace ( lim_inf-Convergence L1));

      then

      consider V be Subset of L1 such that

       A4: x = V and

       A5: for p be Element of L1 st p in V holds for N be net of L1 st [N, p] in ( lim_inf-Convergence L1) holds N is_eventually_in V by A3;

      reconsider V2 = V as Subset of L2 by A1;

      now

        let p be Element of L2 such that

         A6: p in V2;

        let N be net of L2;

        assume [N, p] in ( lim_inf-Convergence L2);

        then ex N1 be strict net of L1 st [N1, p] in ( lim_inf-Convergence L1) & the RelStr of N = the RelStr of N1 & the mapping of N = the mapping of N1 by A1, Th6;

        hence N is_eventually_in V2 by A5, A6, Th7;

      end;

      hence thesis by A2, A4;

    end;

    theorem :: WAYBEL33:8

    for L1,L2 be /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 holds ( ConvergenceSpace ( lim_inf-Convergence L1)) = ( ConvergenceSpace ( lim_inf-Convergence L2))

    proof

      let L1,L2 be /\-complete up-complete Semilattice such that

       A1: the RelStr of L1 = the RelStr of L2;

      set C2 = ( lim_inf-Convergence L2);

      set C1 = ( lim_inf-Convergence L1);

      set T1 = ( ConvergenceSpace C1);

      set T2 = ( ConvergenceSpace C2);

      the topology of T1 c= the topology of T2 & the topology of T2 c= the topology of T1 by A1, Lm3;

      then the carrier of T2 = the carrier of L2 & the topology of T1 = the topology of T2 by YELLOW_6:def 24;

      hence thesis by A1, YELLOW_6:def 24;

    end;

    theorem :: WAYBEL33:9

    

     Th9: for L1,L2 be /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 holds ( xi L1) = ( xi L2)

    proof

      let L1,L2 be /\-complete up-complete Semilattice;

      assume

       A1: the RelStr of L1 = the RelStr of L2;

      ( xi L1) = the topology of ( ConvergenceSpace ( lim_inf-Convergence L1)) & ( xi L2) = the topology of ( ConvergenceSpace ( lim_inf-Convergence L2)) by WAYBEL28:def 4;

      hence ( xi L1) c= ( xi L2) & ( xi L2) c= ( xi L1) by A1, Lm3;

    end;

    registration

      let R be /\-complete non empty reflexive RelStr;

      cluster -> /\-complete for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

        let X be non empty Subset of T;

        

         A1: the RelStr of T = the RelStr of R by YELLOW_9:def 4;

        then

        reconsider Y = X as non empty Subset of R;

        consider x be Element of R such that

         A2: x is_<=_than Y and

         A3: for y be Element of R st y is_<=_than Y holds x >= y by WAYBEL_0:def 40;

        reconsider y = x as Element of T by A1;

        take y;

        thus y is_<=_than X by A1, A2, YELLOW_0: 2;

        let z be Element of T;

        reconsider v = z as Element of R by A1;

        assume z is_<=_than X;

        then x >= v by A1, A3, YELLOW_0: 2;

        hence thesis by A1, YELLOW_0: 1;

      end;

    end

    registration

      let R be Semilattice;

      cluster -> with_infima for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

        let x,y be Element of T;

        

         A1: the RelStr of T = the RelStr of R by YELLOW_9:def 4;

        then

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

        consider z9 be Element of R such that

         A2: z9 <= x9 & z9 <= y9 and

         A3: for v9 be Element of R st v9 <= x9 & v9 <= y9 holds v9 <= z9 by LATTICE3:def 11;

        reconsider z = z9 as Element of T by A1;

        take z;

        thus z <= x & z <= y by A1, A2, YELLOW_0: 1;

        let v be Element of T;

        reconsider v9 = v as Element of R by A1;

        assume v <= x & v <= y;

        then v9 <= x9 & v9 <= y9 by A1, YELLOW_0: 1;

        then v9 <= z9 by A3;

        hence v <= z by A1, YELLOW_0: 1;

      end;

    end

    registration

      let L be /\-complete up-complete Semilattice;

      cluster strict lim-inf for TopAugmentation of L;

      existence

      proof

        set T = TopRelStr (# the carrier of L, the InternalRel of L, ( xi L) #);

        

         A1: the RelStr of T = the RelStr of L;

        then

        reconsider T as TopAugmentation of L by YELLOW_9:def 4;

        take T;

        thus T is strict;

        thus the topology of T = ( xi T) by A1, Th9;

      end;

    end

    theorem :: WAYBEL33:10

    

     Th10: for L be /\-complete up-complete Semilattice holds for X be lim-inf TopAugmentation of L holds ( xi L) = the topology of X

    proof

      let L be /\-complete up-complete Semilattice;

      let X be lim-inf TopAugmentation of L;

      the topology of X = ( xi X) & the RelStr of X = the RelStr of L by Def2, YELLOW_9:def 4;

      hence thesis by Th9;

    end;

    definition

      let L be /\-complete up-complete Semilattice;

      :: WAYBEL33:def3

      func Xi L -> strict TopAugmentation of L means

      : Def3: it is lim-inf;

      uniqueness

      proof

        let T1,T2 be strict TopAugmentation of L such that

         A1: the topology of T1 = ( xi T1) & the topology of T2 = ( xi T2);

         the RelStr of T1 = the RelStr of L & the RelStr of T2 = the RelStr of L by YELLOW_9:def 4;

        hence thesis by A1, Th9;

      end;

      existence

      proof

        set T = TopRelStr (# the carrier of L, the InternalRel of L, ( xi L) #);

        

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

        then

        reconsider T as strict TopAugmentation of L by YELLOW_9:def 4;

        take T;

        thus the topology of T = ( xi T) by A2, Th9;

      end;

    end

    registration

      let L be /\-complete up-complete Semilattice;

      cluster ( Xi L) -> lim-inf;

      coherence by Def3;

    end

    theorem :: WAYBEL33:11

    

     Th11: for L be complete LATTICE, N be net of L holds ( lim_inf N) = ( "\/" ( the set of all ( inf (N | i)) where i be Element of N,L))

    proof

      let L be complete LATTICE, N be net of L;

      set X = the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },L)) where j be Element of N;

      set Y = the set of all ( inf (N | i)) where i be Element of N;

      for x be object st x in X holds x in Y

      proof

        let x be object;

        assume x in X;

        then

        consider j be Element of N such that

         A1: x = ( "/\" ({ (N . i) where i be Element of N : i >= j },L));

        reconsider x as Element of L by A1;

        set S = { (N . i) where i be Element of N : i >= j };

        reconsider i = j as Element of N;

        for b be object st b in ( rng the mapping of (N | i)) holds b in S

        proof

          let b be object;

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

          then b in the set of all ((N | i) . k) where k be Element of (N | i) by WAYBEL11: 19;

          then

          consider k be Element of (N | i) such that

           A2: b = ((N | i) . k);

          the carrier of (N | i) c= the carrier of N by WAYBEL_9: 13;

          then

          reconsider l = k as Element of N;

          k in the carrier of (N | i);

          then k in { y where y be Element of N : i <= y } by WAYBEL_9: 12;

          then

           A3: ex y be Element of N st k = y & i <= y;

          reconsider k as Element of (N | i);

          (N . l) = ((N | i) . k) by WAYBEL_9: 16;

          hence thesis by A2, A3;

        end;

        then

         A4: ( rng the mapping of (N | i)) c= S;

        

         A5: ex_inf_of (S,L) by YELLOW_0: 17;

        then

         A6: S is_>=_than x by A1, YELLOW_0:def 10;

        

         A7: ( rng the mapping of (N | i)) is_>=_than x by A6, A4;

        for b be object st b in S holds b in ( rng the mapping of (N | i))

        proof

          let b be object;

          assume b in S;

          then

          consider k be Element of N such that

           A8: b = (N . k) and

           A9: k >= j;

          reconsider l = k as Element of N;

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

          then

          reconsider k as Element of (N | i) by WAYBEL_9: 12;

          reconsider k as Element of (N | i);

          (N . l) = ((N | i) . k) by WAYBEL_9: 16;

          then b in the set of all ((N | i) . m) where m be Element of (N | i) by A8;

          hence thesis by WAYBEL11: 19;

        end;

        then S c= ( rng the mapping of (N | i));

        then S = ( rng the mapping of (N | i)) by A4;

        then for a be Element of L st ( rng the mapping of (N | i)) is_>=_than a holds a <= x by A1, A5, YELLOW_0:def 10;

        then

        consider i be Element of N such that

         A10: ex_inf_of (( rng the mapping of (N | i)),L) & ( rng the mapping of (N | i)) is_>=_than x & for a be Element of L st ( rng the mapping of (N | i)) is_>=_than a holds a <= x by A7, YELLOW_0: 17;

        

         A11: ( inf (N | i)) = ( Inf the mapping of (N | i)) by WAYBEL_9:def 2

        .= ( "/\" (( rng the mapping of (N | i)),L)) by YELLOW_2:def 6;

        x = ( "/\" (( rng the mapping of (N | i)),L)) by A10, YELLOW_0:def 10;

        hence thesis by A11;

      end;

      then

       A12: ( lim_inf N) = ( "\/" (X,L)) & X c= Y by WAYBEL11:def 6;

      for x be object st x in Y holds x in X

      proof

        let x be object;

        assume x in Y;

        then

        consider i be Element of N such that

         A13: x = ( inf (N | i));

        set S = { (N . j) where j be Element of N : j >= i };

        for b be object st b in ( rng the mapping of (N | i)) holds b in S

        proof

          let b be object;

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

          then b in the set of all ((N | i) . k) where k be Element of (N | i) by WAYBEL11: 19;

          then

          consider k be Element of (N | i) such that

           A14: b = ((N | i) . k);

          the carrier of (N | i) c= the carrier of N by WAYBEL_9: 13;

          then

          reconsider l = k as Element of N;

          k in the carrier of (N | i);

          then k in { y where y be Element of N : i <= y } by WAYBEL_9: 12;

          then

           A15: ex y be Element of N st k = y & i <= y;

          reconsider k as Element of (N | i);

          (N . l) = ((N | i) . k) by WAYBEL_9: 16;

          hence thesis by A14, A15;

        end;

        then

         A16: ( rng the mapping of (N | i)) c= S;

        reconsider x as Element of L by A13;

        

         A17: x = ( Inf the mapping of (N | i)) by A13, WAYBEL_9:def 2

        .= ( "/\" (( rng the mapping of (N | i)),L)) by YELLOW_2:def 6;

        for b be object st b in S holds b in ( rng the mapping of (N | i))

        proof

          let b be object;

          assume b in S;

          then

          consider k be Element of N such that

           A18: b = (N . k) and

           A19: k >= i;

          reconsider l = k as Element of N;

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

          then

          reconsider k as Element of (N | i) by WAYBEL_9: 12;

          reconsider k as Element of (N | i);

          (N . l) = ((N | i) . k) by WAYBEL_9: 16;

          then b in the set of all ((N | i) . m) where m be Element of (N | i) by A18;

          hence thesis by WAYBEL11: 19;

        end;

        then S c= ( rng the mapping of (N | i));

        then ( rng the mapping of (N | i)) = S by A16;

        hence thesis by A17;

      end;

      then Y c= X;

      hence thesis by A12, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL33:12

    

     Th12: for L be complete LATTICE, F be proper Filter of ( BoolePoset ( [#] L)), f be Subset of L st f in F holds for i be Element of ( a_net F) st (i `2 ) = f holds ( inf f) = ( inf (( a_net F) | i))

    proof

      let L be complete LATTICE;

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

      let f be Subset of L;

      assume

       A1: f in F;

      let i be Element of ( a_net F);

      assume

       A2: (i `2 ) = f;

      for b be object st b in f holds b in ( rng the mapping of (( a_net F) | i))

      proof

        let b be object;

        assume

         A3: b in f;

        then

        reconsider b as Element of L;

        reconsider f as Element of F by A1;

         [b, f] in { [a, g] where a be Element of L, g be Element of F : a in g } by A3;

        then

        reconsider k = [b, f] as Element of ( a_net F) by YELLOW19:def 4;

        reconsider l = k as Element of ( a_net F);

        ( [b, f] `1 ) = b;

        then

         A4: b = (( a_net F) . k) by YELLOW19:def 4;

        (k `2 ) c= (i `2 ) by A2;

        then i <= k by YELLOW19:def 4;

        then l in { y where y be Element of ( a_net F) : i <= y };

        then

        reconsider k as Element of (( a_net F) | i) by WAYBEL_9: 12;

        reconsider k as Element of (( a_net F) | i);

        (( a_net F) . l) = ((( a_net F) | i) . k) by WAYBEL_9: 16;

        then b in the set of all ((( a_net F) | i) . m) where m be Element of (( a_net F) | i) by A4;

        hence thesis by WAYBEL11: 19;

      end;

      then

       A5: f c= ( rng the mapping of (( a_net F) | i));

      for b be object st b in ( rng the mapping of (( a_net F) | i)) holds b in f

      proof

        let b be object;

        assume b in ( rng the mapping of (( a_net F) | i));

        then b in the set of all ((( a_net F) | i) . k) where k be Element of (( a_net F) | i) by WAYBEL11: 19;

        then

        consider k be Element of (( a_net F) | i) such that

         A6: b = ((( a_net F) | i) . k);

        

         A7: the carrier of (( a_net F) | i) c= the carrier of ( a_net F) by WAYBEL_9: 13;

        then

        reconsider l = k as Element of ( a_net F);

        k in the carrier of ( a_net F) by A7;

        then

         A8: k in { [c, g] where c be Element of L, g be Element of F : c in g } by YELLOW19:def 4;

        k in the carrier of (( a_net F) | i);

        then k in { y where y be Element of ( a_net F) : i <= y } by WAYBEL_9: 12;

        then ex y be Element of ( a_net F) st k = y & i <= y;

        then

         A9: (l `2 ) c= f by A2, YELLOW19:def 4;

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

         A10: k = [c, g] and

         A11: c in g by A8;

        reconsider k as Element of (( a_net F) | i);

        (( a_net F) . l) = ((( a_net F) | i) . k) by WAYBEL_9: 16;

        then b = (l `1 ) by A6, YELLOW19:def 4;

        hence thesis by A11, A9, A10;

      end;

      then

       A12: ( rng the mapping of (( a_net F) | i)) c= f;

      ( inf (( a_net F) | i)) = ( Inf the mapping of (( a_net F) | i)) by WAYBEL_9:def 2

      .= ( "/\" (( rng the mapping of (( a_net F) | i)),L)) by YELLOW_2:def 6;

      hence thesis by A12, A5, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL33:13

    

     Th13: for L be complete LATTICE, F be proper Filter of ( BoolePoset ( [#] L)) holds ( lim_inf F) = ( lim_inf ( a_net F))

    proof

      let L be complete LATTICE;

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

      set X = the set of all ( inf (( a_net F) | i)) where i be Element of ( a_net F);

      set Y = { ( inf B) where B be Subset of L : B in F };

      for x be object st x in X holds x in Y

      proof

        let x be object;

        assume x in X;

        then

        consider i be Element of ( a_net F) such that

         A1: x = ( inf (( a_net F) | i));

        reconsider i as Element of ( a_net F);

        i in the carrier of ( a_net F);

        then i in { [b, g] where b be Element of L, g be Element of F : b in g } by YELLOW19:def 4;

        then

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

         A2: i = [a, f] and a in f;

        reconsider i as Element of ( a_net F);

        reconsider f as Element of ( BoolePoset ( [#] L));

        reconsider f as Subset of L by WAYBEL_7: 2;

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

        then ( inf f) = ( inf (( a_net F) | i)) by Th12, A2;

        hence thesis by A1;

      end;

      then

       A3: X c= Y;

      for x be object st x in Y holds x in X

      proof

        let x be object;

        assume x in Y;

        then

        consider B be Subset of L such that

         A4: x = ( inf B) and

         A5: B in F;

         not ( Bottom ( BoolePoset ( [#] L))) in F by WAYBEL_7: 4;

        then B <> {} by A5, YELLOW_1: 18;

        then

        consider a be Element of L such that

         A6: a in B by SUBSET_1: 4;

        reconsider B as Element of F by A5;

         [a, B] in { [b, f] where b be Element of L, f be Element of F : b in f } by A6;

        then

        reconsider i = [a, B] as Element of ( a_net F) by YELLOW19:def 4;

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

        then x = ( inf (( a_net F) | i)) by A4, Th12;

        hence thesis;

      end;

      then

       A7: Y c= X;

      ( lim_inf ( a_net F)) = ( "\/" (X,L)) by Th11;

      hence thesis by A3, A7, XBOOLE_0:def 10;

    end;

    

     Lm4: for L be LATTICE, F be non empty Subset of ( BoolePoset ( [#] L)) holds { [a, f] where a be Element of L, f be Element of F : a in f } c= [:the carrier of L, ( bool the carrier of L):]

    proof

      let L be LATTICE;

      let F be non empty Subset of ( BoolePoset ( [#] L));

      let x be object;

      assume x in { [a, f] where a be Element of L, f be Element of F : a in f };

      then

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

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

      f is Subset of ( [#] L) by WAYBEL_7: 2;

      hence thesis by A1, ZFMISC_1:def 2;

    end;

    theorem :: WAYBEL33:14

    

     Th14: for L be complete LATTICE, F be proper Filter of ( BoolePoset ( [#] L)) holds ( a_net F) in ( NetUniv L)

    proof

      let L be complete LATTICE;

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

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

      set UN = ( the_universe_of the carrier of L);

      reconsider UN as universal set;

      ( the_transitive-closure_of the carrier of L) in UN by CLASSES1: 2;

      then

       A1: the carrier of L in UN by CLASSES1: 3, CLASSES1: 52;

      then ( bool the carrier of L) in UN by CLASSES2: 59;

      then

       A2: [:the carrier of L, ( bool the carrier of L):] in UN by A1, CLASSES2: 61;

      S c= [:the carrier of L, ( bool the carrier of L):] by Lm4;

      then S = the carrier of ( a_net F) & S in UN by A2, CLASSES1:def 1, YELLOW19:def 4;

      hence thesis by YELLOW_6:def 11;

    end;

    theorem :: WAYBEL33:15

    

     Th15: for L be complete LATTICE, F be ultra Filter of ( BoolePoset ( [#] L)) holds for p be greater_or_equal_to_id Function of ( a_net F), ( a_net F) holds ( lim_inf F) >= ( inf (( a_net F) * p))

    proof

      let L be complete LATTICE, F be ultra Filter of ( BoolePoset ( [#] L)), p be greater_or_equal_to_id Function of ( a_net F), ( a_net F);

      set M = (( a_net F) * p);

      set rM = ( rng the mapping of M);

      set C = the Element of F;

      

       A1: ( inf M) = ( Inf the mapping of M) by WAYBEL_9:def 2

      .= ( "/\" (rM,L)) by YELLOW_2:def 6;

      F c= the carrier of ( BoolePoset ( [#] L));

      then F c= ( bool ( [#] L)) by WAYBEL_7: 2;

      then C in ( bool ( [#] L));

      then

       A2: (C \ rM) c= ( [#] L) by XBOOLE_1: 1;

      then

      reconsider D = (C \ rM), A = (C /\ rM) as Element of ( BoolePoset ( [#] L)) by WAYBEL_7: 2;

      

       A3: the carrier of M = the carrier of ( a_net F) by WAYBEL28: 6;

      then

      reconsider g = p as Function of M, ( a_net F);

       A4:

      now

        set d = the Element of D;

        assume

         A5: D in F;

         not ( Bottom ( BoolePoset ( [#] L))) in F by WAYBEL_7: 4;

        then

         A6: D <> {} by A5, YELLOW_1: 18;

        then

         A7: d in D;

        reconsider D as Element of F by A5;

        reconsider d as Element of L by A2, A7;

         [d, D] in { [a, f] where a be Element of L, f be Element of F : a in f } by A6;

        then

        reconsider dD = [d, D] as Element of ( a_net F) by YELLOW19:def 4;

        reconsider dD9 = dD as Element of M by WAYBEL28: 6;

        

         A8: ( dom p) = the carrier of ( a_net F) by FUNCT_2: 52;

        ex i be Element of M st for j be Element of M st j >= i holds (g . j) >= dD

        proof

          consider i be Element of M such that

           A9: i = dD9;

          take i;

          for j be Element of M st j >= i holds (g . j) >= dD

          proof

            reconsider i9 = i as Element of ( a_net F) by WAYBEL28: 6;

            let j be Element of M;

            reconsider j9 = j as Element of ( a_net F) by WAYBEL28: 6;

            

             A10: j9 <= (g . j) by WAYBEL28:def 1;

            reconsider i9 as Element of ( a_net F);

            reconsider j9 as Element of ( a_net F);

            

             A11: the RelStr of M = the RelStr of ( a_net F) by WAYBEL28:def 2;

            assume j >= i;

            then i9 <= j9 by A11, YELLOW_0: 1;

            hence thesis by A9, A10, YELLOW_0:def 2;

          end;

          hence thesis;

        end;

        then

        consider i be Element of M such that

         A12: for j be Element of M st j >= i holds (g . j) >= dD;

         the RelStr of M = the RelStr of ( a_net F) by WAYBEL28:def 2;

        then M is reflexive by WAYBEL_8: 12;

        then i >= i by YELLOW_0:def 1;

        then

         A13: (g . i) >= dD by A12;

        ( [d, D] `2 ) = D;

        then

         A14: ((p . i) `2 ) c= D by A13, YELLOW19:def 4;

        reconsider G = (g . i) as Element of ( a_net F);

        (g . i) in the carrier of ( a_net F);

        then (g . i) in { [a, f] where a be Element of L, f be Element of F : a in f } by YELLOW19:def 4;

        then

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

         A15: (g . i) = [a, f] and

         A16: a in f;

        

         A17: ((p . i) `1 ) in ((p . i) `2 ) by A15, A16;

        (M . i) = ((the mapping of ( a_net F) * p) . i) by WAYBEL28:def 2

        .= (( a_net F) . G) by A3, A8, FUNCT_1: 13

        .= ((p . i) `1 ) by YELLOW19:def 4;

        then not (M . i) in rM by A14, A17, XBOOLE_0:def 5;

        hence contradiction by FUNCT_2: 4;

      end;

      set Y = { ( inf B) where B be Subset of L : B in F };

      reconsider A9 = A as Subset of L;

      

       A18: (D "\/" A) = (D \/ A) by YELLOW_1: 17

      .= C by XBOOLE_1: 51;

      F is prime by WAYBEL_7: 22;

      then A in F by A18, A4;

      then ( inf A9) in Y;

      then

       A19: ( inf A9) <= ( lim_inf F) by YELLOW_0: 17, YELLOW_4: 1;

      A c= rM by XBOOLE_1: 17;

      then ( inf M) <= ( inf A9) by A1, WAYBEL_7: 1;

      hence thesis by A19, YELLOW_0:def 2;

    end;

    theorem :: WAYBEL33:16

    

     Th16: for L be complete LATTICE, F be ultra Filter of ( BoolePoset ( [#] L)) holds for M be subnet of ( a_net F) holds ( lim_inf F) = ( lim_inf M)

    proof

      let L be complete LATTICE, F be ultra Filter of ( BoolePoset ( [#] L)), M be subnet of ( a_net F);

      ( lim_inf F) = ( lim_inf ( a_net F)) & for p be greater_or_equal_to_id Function of ( a_net F), ( a_net F) holds ( lim_inf F) >= ( inf (( a_net F) * p)) by Th13, Th15;

      hence thesis by WAYBEL28: 14;

    end;

    theorem :: WAYBEL33:17

    

     Th17: for L be non empty 1-sorted holds for N be net of L holds for A be set st N is_often_in A holds ex N9 be strict subnet of N st ( rng the mapping of N9) c= A & N9 is SubNetStr of N

    proof

      let L be non empty 1-sorted;

      let N be net of L;

      let A be set;

      assume N is_often_in A;

      then

      reconsider N9 = (N " A) as strict subnet of N by YELLOW_6: 22;

      take N9;

      ( rng the mapping of N9) c= A

      proof

        let y be object;

        assume y in ( rng the mapping of N9);

        then

        consider x be object such that

         A1: x in ( dom the mapping of N9) and

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

        

         A3: x in ( dom (the mapping of N | the carrier of N9)) by A1, YELLOW_6:def 6;

        then x in (( dom the mapping of N) /\ the carrier of N9) by RELAT_1: 61;

        then x in the carrier of N9 by XBOOLE_0:def 4;

        then

         A4: x in (the mapping of N " A) by YELLOW_6:def 10;

        y = ((the mapping of N | the carrier of N9) . x) by A2, YELLOW_6:def 6;

        then y = (the mapping of N . x) by A3, FUNCT_1: 47;

        hence thesis by A4, FUNCT_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL33:18

    

     Th18: for L be complete lim-inf TopLattice, A be non empty Subset of L holds A is closed iff for F be ultra Filter of ( BoolePoset ( [#] L)) st A in F holds ( lim_inf F) in A

    proof

      let L be complete lim-inf TopLattice;

      let A be non empty Subset of L;

      ( xi L) = the topology of ( ConvergenceSpace ( lim_inf-Convergence L)) by WAYBEL28:def 4;

      then

       A1: ( xi L) = { V where V be Subset of L : for p be Element of L st p in V holds for N be net of L st [N, p] in ( lim_inf-Convergence L) holds N is_eventually_in V } by YELLOW_6:def 24;

      set V = (A ` );

      

       A2: the topology of L = ( xi L) by Def2;

      hereby

        assume A is closed;

        then (A ` ) in ( xi L) by A2, PRE_TOPC:def 2;

        then

         A3: ex V be Subset of L st V = (A ` ) & for p be Element of L st p in V holds for N be net of L st [N, p] in ( lim_inf-Convergence L) holds N is_eventually_in V by A1;

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

        assume

         A4: A in F;

        (for M be subnet of ( a_net F) holds ( lim_inf F) = ( lim_inf M)) & ( a_net F) in ( NetUniv L) by Th14, Th16;

        then

         A5: [( a_net F), ( lim_inf F)] in ( lim_inf-Convergence L) by WAYBEL28:def 3;

        assume not ( lim_inf F) in A;

        then ( lim_inf F) in (A ` ) by XBOOLE_0:def 5;

        then ( a_net F) is_eventually_in (A ` ) by A3, A5;

        then

        consider i be Element of ( a_net F) such that

         A6: for j be Element of ( a_net F) st i <= j holds (( a_net F) . j) in (A ` );

        

         A7: the carrier of ( a_net F) = { [a, f] where a be Element of L, f be Element of F : a in f } by YELLOW19:def 4;

        i in the carrier of ( a_net F);

        then

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

         A8: i = [a, f] and a in f by A7;

        reconsider A9 = A, f9 = f as Element of ( BoolePoset ( [#] L)) by A4;

        consider B be Element of ( BoolePoset ( [#] L)) such that

         A9: B in F and

         A10: A9 >= B and

         A11: f9 >= B by A4, WAYBEL_0:def 2;

        set b = the Element of B;

         not ( Bottom ( BoolePoset ( [#] L))) in F by WAYBEL_7: 4;

        then B is non empty by A9, YELLOW_1: 18;

        then

         A12: b in B;

        the carrier of ( BoolePoset ( [#] L)) = ( bool the carrier of L) by WAYBEL_7: 2;

        then [b, B] in the carrier of ( a_net F) by A7, A9, A12;

        then

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

        B c= f by A11, YELLOW_1: 2;

        then (j `2 ) c= f;

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

        then j >= i by YELLOW19:def 4;

        then (( a_net F) . j) in (A ` ) by A6;

        then (j `1 ) in (A ` ) by YELLOW19:def 4;

        then

         A13: b in (A ` );

        B c= A by A10, YELLOW_1: 2;

        hence contradiction by A12, A13, XBOOLE_0:def 5;

      end;

      assume

       A14: for F be ultra Filter of ( BoolePoset ( [#] L)) st A in F holds ( lim_inf F) in A;

      now

        let p be Element of L;

        assume p in V;

        then

         A15: not p in (V ` ) by XBOOLE_0:def 5;

        reconsider x = p as Element of L;

        let N be net of L such that

         A16: [N, p] in ( lim_inf-Convergence L);

        assume not N is_eventually_in V;

        then N is_often_in A by WAYBEL_0: 10;

        then

        consider N9 be strict subnet of N such that

         A17: ( rng the mapping of N9) c= A and

         A18: N9 is SubNetStr of N by Th17;

        ( lim_inf-Convergence L) c= [:( NetUniv L), the carrier of L:] by YELLOW_6:def 18;

        then

         A19: N in ( NetUniv L) by A16, ZFMISC_1: 87;

        then

         A20: ex N1 be strict net of L st N1 = N & the carrier of N1 in ( the_universe_of the carrier of L) by YELLOW_6:def 11;

        set j0 = the Element of N9;

        reconsider rj = ( rng the mapping of (N9 | j0)), a = A as Element of ( BoolePoset ( [#] L)) by WAYBEL_7: 2;

        set j2 = the Element of N9;

        set G = the set of all ( rng the mapping of (N9 | j)) where j be Element of N9;

        set g = ( rng the mapping of (N9 | j2));

        

         A21: g in G;

        for g be object st g in G holds g in the carrier of ( BoolePoset ( [#] L))

        proof

          let g be object;

          assume g in G;

          then ex j3 be Element of N9 st g = ( rng the mapping of (N9 | j3));

          then g in ( bool ( [#] L));

          hence thesis by WAYBEL_7: 2;

        end;

        then

        reconsider G as non empty Subset of ( BoolePoset ( [#] L)) by A21, TARSKI:def 3;

        

         A22: G c= ( fininfs G) by WAYBEL_0: 50;

        now

          let p be object;

          assume p in rj;

          then p in ( rng (the mapping of N9 | the carrier of (N9 | j0))) by WAYBEL_9:def 7;

          then

          consider q be object such that

           A23: q in ( dom (the mapping of N9 | the carrier of (N9 | j0))) and

           A24: p = ((the mapping of N9 | the carrier of (N9 | j0)) . q) by FUNCT_1:def 3;

          q in (( dom the mapping of N9) /\ the carrier of (N9 | j0)) by A23, RELAT_1: 61;

          then

           A25: q in ( dom the mapping of N9) by XBOOLE_0:def 4;

          p = (the mapping of N9 . q) by A23, A24, FUNCT_1: 47;

          hence p in ( rng the mapping of N9) by A25, FUNCT_1: 3;

        end;

        then rj c= ( rng the mapping of N9);

        then rj c= a by A17;

        then ( rng the mapping of (N9 | j0)) in G & rj <= a by YELLOW_1: 2;

        then

         A26: a in ( uparrow ( fininfs G)) by A22, WAYBEL_0:def 16;

        

         A27: x = ( lim_inf N9) by A16, A19, WAYBEL28:def 3;

        then

         A28: x = ( "\/" ( the set of all ( inf (N9 | j)) where j be Element of N9,L)) by Th11;

        the carrier of N9 c= the carrier of N by A18, YELLOW_6: 10;

        then the carrier of N9 in ( the_universe_of the carrier of L) by A20, CLASSES1:def 1;

        then

         A29: N9 in ( NetUniv L) by YELLOW_6:def 11;

        

         A30: not {} in ( fininfs G)

        proof

          assume {} in ( fininfs G);

          then

          consider Y be finite Subset of G such that

           A31: {} = ( "/\" (Y,( BoolePoset ( [#] L)))) and ex_inf_of (Y,( BoolePoset ( [#] L)));

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

          

           A32: ( "/\" ( {} ,( BoolePoset ( [#] L)))) = ( Top ( BoolePoset ( [#] L))) by YELLOW_0:def 12

          .= ( [#] L) by YELLOW_1: 19;

          reconsider Y as finite Subset of ( BoolePoset ( [#] L)) by XBOOLE_1: 1;

          

           A33: for x be object st x in Y holds ex y be object st y in the carrier of N9 & P[x, y]

          proof

            let x be object;

            assume x in Y;

            then x in G;

            then

             A34: ex j be Element of N9 st x = ( rng the mapping of (N9 | j));

            assume for y be object st y in the carrier of N9 holds not P[x, y];

            hence contradiction by A34;

          end;

          consider f be Function such that

           A35: ( dom f) = Y & ( rng f) c= the carrier of N9 and

           A36: for x be object st x in Y holds P[x, (f . x)] from FUNCT_1:sch 6( A33);

          reconsider C = ( rng f) as finite Subset of ( [#] N9) by A35, FINSET_1: 8;

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

          then

          consider j0 be Element of N9 such that j0 in ( [#] N9) and

           A37: j0 is_>=_than C by WAYBEL_0: 1;

          for y be set st y in Y holds ( rng the mapping of (N9 | j0)) c= y

          proof

            let y be set such that

             A38: y in Y;

            consider j1 be Element of N9 such that

             A39: j1 = (f . y) and

             A40: y = ( rng the mapping of (N9 | j1)) by A36, A38;

            

             A41: (f . y) in ( rng f) by A35, A38, FUNCT_1: 3;

            then

            reconsider f1 = (f . y) as Element of N9 by A35;

            

             A42: f1 <= j0 by A37, A41;

            for p be object st p in ( rng the mapping of (N9 | j0)) holds p in y

            proof

              let p be object;

              assume p in ( rng the mapping of (N9 | j0));

              then p in ( rng (the mapping of N9 | the carrier of (N9 | j0))) by WAYBEL_9:def 7;

              then

              consider q be object such that

               A43: q in ( dom (the mapping of N9 | the carrier of (N9 | j0))) and

               A44: p = ((the mapping of N9 | the carrier of (N9 | j0)) . q) by FUNCT_1:def 3;

              

               A45: q in (( dom the mapping of N9) /\ the carrier of (N9 | j0)) by A43, RELAT_1: 61;

              then q in the carrier of (N9 | j0) by XBOOLE_0:def 4;

              then q in { n9 where n9 be Element of N9 : j0 <= n9 } by WAYBEL_9: 12;

              then

              consider n9 be Element of N9 such that

               A46: q = n9 and

               A47: j0 <= n9;

              f1 <= n9 by A42, A47, YELLOW_0:def 2;

              then q in { m9 where m9 be Element of N9 : j1 <= m9 } by A39, A46;

              then

               A48: q in the carrier of (N9 | j1) by WAYBEL_9: 12;

              q in ( dom the mapping of N9) by A45, XBOOLE_0:def 4;

              then q in (( dom the mapping of N9) /\ the carrier of (N9 | j1)) by A48, XBOOLE_0:def 4;

              then

               A49: q in ( dom (the mapping of N9 | the carrier of (N9 | j1))) by RELAT_1: 61;

              p = (the mapping of N9 . q) by A43, A44, FUNCT_1: 47;

              then p = ((the mapping of N9 | the carrier of (N9 | j1)) . q) by A49, FUNCT_1: 47;

              then p in ( rng (the mapping of N9 | the carrier of (N9 | j1))) by A49, FUNCT_1: 3;

              hence thesis by A40, WAYBEL_9:def 7;

            end;

            hence thesis;

          end;

          then ( rng the mapping of (N9 | j0)) c= ( meet Y) by A31, A32, SETFAM_1: 5;

          then ( rng the mapping of (N9 | j0)) c= {} by A31, A32, YELLOW_1: 20;

          hence contradiction;

        end;

        for y be Element of ( BoolePoset ( [#] L)) st ( Bottom ( BoolePoset ( [#] L))) >= y holds not y in ( fininfs G)

        proof

          let y be Element of ( BoolePoset ( [#] L));

          assume ( Bottom ( BoolePoset ( [#] L))) >= y;

          then {} = ( Bottom ( BoolePoset ( [#] L))) & y c= ( Bottom ( BoolePoset ( [#] L))) by YELLOW_1: 2, YELLOW_1: 18;

          hence thesis by A30;

        end;

        then not ( Bottom ( BoolePoset ( [#] L))) in ( uparrow ( fininfs G)) by WAYBEL_0:def 16;

        then ( uparrow ( fininfs G)) is proper;

        then

        consider F be Filter of ( BoolePoset ( [#] L)) such that

         A50: ( uparrow ( fininfs G)) c= F and

         A51: F is ultra by WAYBEL_7: 26;

        

         A52: ( fininfs G) c= ( uparrow ( fininfs G)) by WAYBEL_0: 16;

        

         A53: the set of all ( inf (N9 | j)) where j be Element of N9 c= { ( inf f) where f be Subset of L : f in F }

        proof

          let x be object;

          assume x in the set of all ( inf (N9 | j)) where j be Element of N9;

          then

          consider j3 be Element of N9 such that

           A54: x = ( inf (N9 | j3));

          reconsider f1 = ( rng the mapping of (N9 | j3)) as Subset of L;

          ( fininfs G) c= F by A50, A52;

          then

           A55: f1 in G & G c= F by A22;

          x = ( Inf the mapping of (N9 | j3)) by A54, WAYBEL_9:def 2

          .= ( "/\" (( rng the mapping of (N9 | j3)),L)) by YELLOW_2:def 6;

          hence thesis by A55;

        end;

        now

          let M be subnet of N9;

          M is subnet of N by YELLOW_6: 15;

          hence x = ( lim_inf M) by A16, A19, WAYBEL28:def 3;

        end;

        then

         A56: for M be subnet of N9 st M in ( NetUniv L) holds x = ( lim_inf M);

        { ( inf f) where f be Subset of L : f in F } is_<=_than x

        proof

          let y be Element of L;

          assume y in { ( inf f) where f be Subset of L : f in F };

          then

          consider f0 be Subset of L such that

           A57: y = ( inf f0) and

           A58: f0 in F;

          defpred P[ Element of N9, Element of N9] means $1 <= $2 & (N9 . $2) in f0;

           A59:

          now

            let j be Element of N9;

             not ( Bottom ( BoolePoset ( [#] L))) in F by A51, WAYBEL_7: 4;

            then

             A60: not {} in F by YELLOW_1: 18;

            G c= ( uparrow ( fininfs G)) by A22, A52;

            then

             A61: G c= F by A50;

            ( rng the mapping of (N9 | j)) in G;

            then (f0 /\ ( rng the mapping of (N9 | j))) in F by A58, A61, WAYBEL_7: 9;

            then

            consider nj be Element of L such that

             A62: nj in (f0 /\ ( rng the mapping of (N9 | j))) by A60, SUBSET_1: 4;

            nj in ( rng the mapping of (N9 | j)) by A62, XBOOLE_0:def 4;

            then

            consider pj9 be object such that

             A63: pj9 in ( dom the mapping of (N9 | j)) and

             A64: nj = (the mapping of (N9 | j) . pj9) by FUNCT_1:def 3;

            pj9 in the carrier of (N9 | j) by A63;

            then pj9 in { y9 where y9 be Element of N9 : j <= y9 } by WAYBEL_9: 12;

            then

            consider pj be Element of N9 such that

             A65: pj = pj9 and

             A66: j <= pj;

            reconsider pj9 as Element of (N9 | j) by A63;

            take pj;

            (N9 . pj) = ((N9 | j) . pj9) by A65, WAYBEL_9: 16

            .= (the mapping of (N9 | j) . pj9);

            hence P[j, pj] by A62, A64, A66, XBOOLE_0:def 4;

          end;

          consider p be Function of N9, N9 such that

           A67: for j be Element of N9 holds P[j, (p . j)] from FUNCT_2:sch 3( A59);

          for b be object st b in ( rng the mapping of (N9 * p)) holds b in f0

          proof

            let b be object;

            assume b in ( rng the mapping of (N9 * p));

            then b in the set of all ((N9 * p) . k) where k be Element of (N9 * p) by WAYBEL11: 19;

            then

            consider k be Element of (N9 * p) such that

             A68: b = ((N9 * p) . k);

            reconsider l = k as Element of N9 by WAYBEL28: 6;

            the carrier of (N9 * p) = the carrier of N9 by WAYBEL28: 6;

            then k in the carrier of N9;

            then

             A69: k in ( dom p) by FUNCT_2: 52;

            ((N9 * p) . k) = ((the mapping of N9 * p) . k) by WAYBEL28:def 2

            .= (N9 . (p . l)) by A69, FUNCT_1: 13;

            hence thesis by A67, A68;

          end;

          then ( rng the mapping of (N9 * p)) c= f0;

          then

           A70: ( "/\" (f0,L)) <= ( "/\" (( rng the mapping of (N9 * p)),L)) by WAYBEL_7: 1;

          

           A71: for M be subnet of N9 st M in ( NetUniv L) holds x >= ( inf M) by A29, A56, WAYBEL28: 3;

          p is greater_or_equal_to_id by A67, WAYBEL28:def 1;

          then

           A72: ( inf (N9 * p)) <= x by A29, A27, A71, WAYBEL28: 13;

          ( inf (N9 * p)) = ( Inf the mapping of (N9 * p)) by WAYBEL_9:def 2

          .= ( "/\" (( rng the mapping of (N9 * p)),L)) by YELLOW_2:def 6;

          hence thesis by A57, A72, A70, YELLOW_0:def 2;

        end;

        then

         A73: ( lim_inf F) <= x by YELLOW_0: 32;

         ex_sup_of ({ ( inf f) where f be Subset of L : f in F },L) & ex_sup_of ( the set of all ( inf (N9 | j)) where j be Element of N9,L) by YELLOW_0: 17;

        then x <= ( lim_inf F) by A28, A53, YELLOW_0: 34;

        then x = ( lim_inf F) by A73, YELLOW_0:def 3;

        hence contradiction by A14, A50, A51, A26, A15;

      end;

      then (A ` ) in ( xi L) by A1;

      then (A ` ) is open by A2;

      hence thesis;

    end;

    theorem :: WAYBEL33:19

    

     Th19: for L be non empty reflexive RelStr holds ( sigma L) c= ( xi L) by WAYBEL28: 28;

    theorem :: WAYBEL33:20

    

     Th20: for T1,T2 be non empty TopSpace, B be prebasis of T1 st B c= the topology of T2 & the carrier of T1 in the topology of T2 holds the topology of T1 c= the topology of T2

    proof

      let T1,T2 be non empty TopSpace;

      let B be prebasis of T1 such that

       A1: B c= the topology of T2 and

       A2: the carrier of T1 in the topology of T2;

      let x be object;

      ( FinMeetCl B) is Basis of T1 by YELLOW_9: 23;

      then

       A3: the topology of T1 = ( UniCl ( FinMeetCl B)) by YELLOW_9: 22;

      assume x in the topology of T1;

      then

      consider Y be Subset-Family of T1 such that

       A4: Y c= ( FinMeetCl B) and

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

      

       A6: Y c= the topology of T2

      proof

        let y be object;

        assume y in Y;

        then

        consider Z be Subset-Family of T1 such that

         A7: Z c= B and

         A8: Z is finite and

         A9: y = ( Intersect Z) by A4, CANTOR_1:def 3;

        Z c= the topology of T2 by A1, A7;

        then

        reconsider Z9 = Z as Subset-Family of T2 by XBOOLE_1: 1;

        y = the carrier of T1 or Z9 c= the topology of T2 & y = ( meet Z9) & ( meet Z9) = ( Intersect Z9) by A1, A7, A9, SETFAM_1:def 9;

        then y = the carrier of T1 or y in ( FinMeetCl the topology of T2) by A8, CANTOR_1:def 3;

        hence thesis by A2, CANTOR_1: 5;

      end;

      then

      reconsider Y as Subset-Family of T2 by XBOOLE_1: 1;

      ( union Y) in ( UniCl the topology of T2) by A6, CANTOR_1:def 1;

      hence thesis by A5, CANTOR_1: 6;

    end;

    theorem :: WAYBEL33:21

    

     Th21: for L be complete LATTICE holds ( omega L) c= ( xi L)

    proof

      let L be complete LATTICE;

      set S = the lower correct TopAugmentation of L;

      set X = the lim-inf TopAugmentation of L;

      reconsider B = the set of all (( uparrow x) ` ) where x be Element of S as prebasis of S by WAYBEL19:def 1;

      

       A1: the RelStr of S = the RelStr of L & the RelStr of X = the RelStr of L by YELLOW_9:def 4;

      

       A2: B c= the topology of X

      proof

        let b be object;

        assume b in B;

        then

        consider x be Element of S such that

         A3: b = (( uparrow x) ` );

        reconsider y = x as Element of X by A1;

        set A = ( uparrow y);

        X is SubRelStr of X by YELLOW_6: 6;

        then S is SubRelStr of X by A1, WAYBEL21: 12;

        then

         A4: ( uparrow x) c= ( uparrow y) by WAYBEL23: 14;

        

         A5: ( inf A) = y by WAYBEL_0: 39;

        now

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

          assume A in F;

          then ( inf A) in { ( inf C) where C be Subset of X : C in F };

          then ( inf A) <= ( "\/" ({ ( inf C) where C be Subset of X : C in F },X)) by YELLOW_2: 22;

          hence ( lim_inf F) in A by A5, WAYBEL_0: 18;

        end;

        then

         A6: A is closed by Th18;

        S is SubRelStr of S by YELLOW_6: 6;

        then X is SubRelStr of S by A1, WAYBEL21: 12;

        then ( uparrow y) c= ( uparrow x) by WAYBEL23: 14;

        then ( uparrow y) = ( uparrow x) by A4;

        hence thesis by A1, A3, A6, PRE_TOPC:def 2;

      end;

      the carrier of S in the topology of X by A1, PRE_TOPC:def 1;

      then the topology of S c= the topology of X by A2, Th20;

      then ( omega L) c= the topology of X by WAYBEL19:def 2;

      hence thesis by Th10;

    end;

    theorem :: WAYBEL33:22

    

     Th22: for T1,T2 be TopSpace, T be non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds for R be Refinement of T1, T2 holds T is TopExtension of R

    proof

      let T1,T2 be TopSpace, T be non empty TopSpace such that

       A1: the carrier of T1 = the carrier of T and

       A2: the topology of T1 c= the topology of T and

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

       A4: the topology of T2 c= the topology of T;

      let R be Refinement of T1, T2;

      

       A5: the carrier of R = (the carrier of T \/ the carrier of T) by A1, A3, YELLOW_9:def 6;

      hence the carrier of R = the carrier of T;

      reconsider S = (the topology of T1 \/ the topology of T2) as prebasis of R by YELLOW_9:def 6;

      ( FinMeetCl S) is Basis of R by YELLOW_9: 23;

      then

       A6: ( UniCl ( FinMeetCl S)) = the topology of R by YELLOW_9: 22;

      S c= the topology of T by A2, A4, XBOOLE_1: 8;

      then ( FinMeetCl S) c= ( FinMeetCl the topology of T) by A5, CANTOR_1: 14;

      then the topology of R c= ( UniCl ( FinMeetCl the topology of T)) by A5, A6, CANTOR_1: 9;

      hence thesis by CANTOR_1: 7;

    end;

    theorem :: WAYBEL33:23

    

     Th23: for T1 be TopSpace, T2 be TopExtension of T1 holds for A be Subset of T1 holds (A is open implies A is open Subset of T2) & (A is closed implies A is closed Subset of T2)

    proof

      let T1 be TopSpace, T2 be TopExtension of T1;

      let A be Subset of T1;

      

       A1: the carrier of T1 = the carrier of T2 by YELLOW_9:def 5;

      reconsider B = A as Subset of T2 by YELLOW_9:def 5;

      reconsider C = (( [#] T2) \ B) as Subset of T2;

      

       A2: the topology of T1 c= the topology of T2 by YELLOW_9:def 5;

      thus A is open implies A is open Subset of T2

      proof

        assume A in the topology of T1;

        then A in the topology of T2 by A2;

        hence thesis by PRE_TOPC:def 2;

      end;

      assume (( [#] T1) \ A) in the topology of T1;

      then C is open by A2, A1;

      hence thesis by PRE_TOPC:def 3;

    end;

    theorem :: WAYBEL33:24

    

     Th24: for L be complete LATTICE holds ( lambda L) c= ( xi L)

    proof

      let L be complete LATTICE;

      set T = the Lawson correct TopAugmentation of L;

      set S = the Scott TopAugmentation of L;

      set LL = the lower correct TopAugmentation of L;

      set LI = the lim-inf TopAugmentation of L;

      

       A1: the RelStr of LI = the RelStr of L by YELLOW_9:def 4;

      

       A2: ( xi L) = the topology of LI by Th10;

      ( omega L) = the topology of LL by WAYBEL19:def 2;

      then the RelStr of LL = the RelStr of L & the topology of LL c= ( xi L) by Th21, YELLOW_9:def 4;

      then

       A3: LI is TopExtension of LL by A2, A1, YELLOW_9:def 5;

      ( sigma L) = the topology of S by YELLOW_9: 51;

      then the RelStr of S = the RelStr of L & the topology of S c= ( xi L) by Th19, YELLOW_9:def 4;

      then T is Refinement of S, LL & LI is TopExtension of S by A2, A1, WAYBEL19: 29, YELLOW_9:def 5;

      then ( lambda L) = the topology of T & LI is TopExtension of T by A3, Th22, WAYBEL19:def 4;

      hence thesis by A2, YELLOW_9:def 5;

    end;

    theorem :: WAYBEL33:25

    

     Th25: for L be complete LATTICE holds for T be lim-inf TopAugmentation of L holds for S be Lawson correct TopAugmentation of L holds T is TopExtension of S

    proof

      let L be complete LATTICE;

      let T be lim-inf TopAugmentation of L;

      let S be Lawson correct TopAugmentation of L;

      ( lambda L) = the topology of S & ( xi L) = the topology of T by Th10, WAYBEL19:def 4;

      then

       A1: the topology of S c= the topology of T by Th24;

       the RelStr of T = the RelStr of L & the RelStr of S = the RelStr of L by YELLOW_9:def 4;

      hence thesis by A1, YELLOW_9:def 5;

    end;

    theorem :: WAYBEL33:26

    

     Th26: for L be complete lim-inf TopLattice holds for F be ultra Filter of ( BoolePoset ( [#] L)) holds ( lim_inf F) is_a_convergence_point_of (F,L)

    proof

      let L be complete lim-inf TopLattice;

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

      set x = ( lim_inf F);

      let A be Subset of L;

      assume that

       A1: A is open and

       A2: x in A and

       A3: not A in F;

      F is prime by WAYBEL_7: 22;

      then

       A4: (( [#] L) \ A) in F by A3, WAYBEL_7: 21;

      then (A ` ) <> {} by YELLOW19: 1;

      then x in (A ` ) by A1, A4, Th18;

      hence contradiction by A2, XBOOLE_0:def 5;

    end;

    ::$Notion-Name

    theorem :: WAYBEL33:27

    for L be complete lim-inf TopLattice holds L is compact T_1

    proof

      let L be complete lim-inf TopLattice;

      set T = the Lawson correct TopAugmentation of L;

      now

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

        reconsider x = ( lim_inf F) as Point of L;

        take x;

        thus x is_a_convergence_point_of (F,L) by Th26;

      end;

      hence L is compact by YELLOW19: 31;

      now

        let x be Point of L;

        reconsider y = x as Element of L;

         the RelStr of L = the RelStr of T by YELLOW_9:def 4;

        then

        reconsider z = y as Element of T;

        L is TopAugmentation of L by YELLOW_9: 44;

        then

         A1: L is TopExtension of T by Th25;

         {z} is closed;

        then {y} is closed by A1, Th23;

        hence ( Cl {x}) = {x} by PRE_TOPC: 22;

      end;

      hence thesis by FRECHET2: 43;

    end;