waybel22.miz



    begin

    

     Lm1: for L be complete LATTICE, X be set st X c= ( bool the carrier of L) holds ( "/\" (( union X),L)) = ( "/\" ({ ( inf Y) where Y be Subset of L : Y in X },L))

    proof

      let L be complete LATTICE, X be set such that

       A1: X c= ( bool the carrier of L);

      defpred P[ Subset of L] means $1 in X;

      set XX = { Z where Z be Subset of L : P[Z] };

       A2:

      now

        let x be object;

        hereby

          assume x in XX;

          then ex Z be Subset of L st x = Z & Z in X;

          hence x in X;

        end;

        assume

         A3: x in X;

        then

        reconsider x9 = x as Subset of L by A1;

        x9 in XX by A3;

        hence x in XX;

      end;

      ( "/\" ({ ( "/\" (Y,L)) where Y be Subset of L : P[Y] },L)) = ( "/\" (( union XX),L)) from YELLOW_3:sch 3;

      hence thesis by A2, TARSKI: 2;

    end;

    

     Lm2: for L be complete LATTICE, X be set st X c= ( bool the carrier of L) holds ( "\/" (( union X),L)) = ( "\/" ({ ( sup Y) where Y be Subset of L : Y in X },L))

    proof

      let L be complete LATTICE, X be set such that

       A1: X c= ( bool the carrier of L);

      defpred P[ set] means $1 in X;

      set XX = { Z where Z be Subset of L : P[Z] };

       A2:

      now

        let x be object;

        hereby

          assume x in XX;

          then ex Z be Subset of L st x = Z & Z in X;

          hence x in X;

        end;

        assume

         A3: x in X;

        then

        reconsider x9 = x as Subset of L by A1;

        x9 in XX by A3;

        hence x in XX;

      end;

      ( "\/" ({ ( "\/" (Y,L)) where Y be Subset of L : P[Y] },L)) = ( "\/" (( union XX),L)) from YELLOW_3:sch 5;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: WAYBEL22:1

    

     Th1: for L be upper-bounded Semilattice, F be non empty directed Subset of ( InclPoset ( Filt L)) holds ( sup F) = ( union F)

    proof

      let L be upper-bounded Semilattice, F be non empty directed Subset of ( InclPoset ( Filt L));

      ( Filt L) = ( Ids (L opp )) by WAYBEL16: 7;

      hence thesis by WAYBEL13: 9;

    end;

    theorem :: WAYBEL22:2

    

     Th2: for L,S,T be complete non empty Poset, f be CLHomomorphism of L, S, g be CLHomomorphism of S, T holds (g * f) is CLHomomorphism of L, T

    proof

      let L,S,T be complete non empty Poset, f be CLHomomorphism of L, S, g be CLHomomorphism of S, T;

      f is directed-sups-preserving & g is directed-sups-preserving by WAYBEL16:def 1;

      then

       A1: (g * f) is directed-sups-preserving by WAYBEL20: 28;

      f is infs-preserving & g is infs-preserving by WAYBEL16:def 1;

      then (g * f) is infs-preserving by WAYBEL20: 25;

      hence thesis by A1, WAYBEL16:def 1;

    end;

    theorem :: WAYBEL22:3

    

     Th3: for L be non empty RelStr holds ( id L) is infs-preserving

    proof

      let L be non empty RelStr;

      let X be Subset of L;

      set f = ( id L);

      assume ex_inf_of (X,L);

      hence ex_inf_of ((f .: X),L) by FUNCT_1: 92;

      (f .: X) = X by FUNCT_1: 92;

      hence thesis;

    end;

    theorem :: WAYBEL22:4

    

     Th4: for L be non empty RelStr holds ( id L) is directed-sups-preserving

    proof

      let L be non empty RelStr;

      let X be Subset of L such that X is non empty directed;

      set f = ( id L);

      assume ex_sup_of (X,L);

      hence ex_sup_of ((f .: X),L) by FUNCT_1: 92;

      (f .: X) = X by FUNCT_1: 92;

      hence thesis;

    end;

    theorem :: WAYBEL22:5

    

     Th5: for L be complete non empty Poset holds ( id L) is CLHomomorphism of L, L

    proof

      let L be complete non empty Poset;

      ( id L) is directed-sups-preserving & ( id L) is infs-preserving by Th3, Th4;

      hence thesis by WAYBEL16:def 1;

    end;

    theorem :: WAYBEL22:6

    

     Th6: for L be upper-bounded with_infima non empty Poset holds ( InclPoset ( Filt L)) is CLSubFrame of ( BoolePoset the carrier of L)

    proof

      let L be upper-bounded with_infima non empty Poset;

      set cL = the carrier of L;

      set BP = ( BoolePoset cL);

      set cBP = the carrier of BP;

      set rBP = the InternalRel of BP;

      set IP = ( InclPoset ( Filt L));

      set cIP = the carrier of IP;

      set rIP = the InternalRel of IP;

      

       A1: ( InclPoset ( bool cL)) = RelStr (# ( bool cL), ( RelIncl ( bool cL)) #) by YELLOW_1:def 1;

      

       A2: ( InclPoset ( Filt L)) = RelStr (# ( Filt L), ( RelIncl ( Filt L)) #) by YELLOW_1:def 1;

      

       A3: ( BoolePoset cL) = ( InclPoset ( bool cL)) by YELLOW_1: 4;

      

       A4: cIP c= cBP

      proof

        let x be object;

        assume x in cIP;

        then ex X be Filter of L st x = X by A2;

        hence thesis by A3, A1;

      end;

      

       A5: ( field rIP) = ( Filt L) by A2, WELLORD2:def 1;

      rIP c= rBP

      proof

        let p be object;

        assume

         A6: p in rIP;

        then

        consider x,y be object such that

         A7: p = [x, y] by RELAT_1:def 1;

        

         A8: y in ( field rIP) by A6, A7, RELAT_1: 15;

        then

        consider Y be Filter of L such that

         A9: y = Y by A5;

        

         A10: x in ( field rIP) by A6, A7, RELAT_1: 15;

        then

        consider X be Filter of L such that

         A11: x = X by A5;

        X c= Y by A2, A5, A6, A7, A10, A8, A11, A9, WELLORD2:def 1;

        hence thesis by A3, A1, A7, A11, A9, WELLORD2:def 1;

      end;

      then

      reconsider IP as SubRelStr of BP by A4, YELLOW_0:def 13;

      now

        let p be object;

        

         A12: (rBP |_2 cIP) = (rBP /\ [:cIP, cIP:]) by WELLORD1:def 6;

        hereby

          assume

           A13: p in rIP;

          then

          consider x,y be object such that

           A14: p = [x, y] by RELAT_1:def 1;

          

           A15: y in ( field rIP) by A13, A14, RELAT_1: 15;

          then

          consider Y be Filter of L such that

           A16: y = Y by A5;

          

           A17: x in ( field rIP) by A13, A14, RELAT_1: 15;

          then

          consider X be Filter of L such that

           A18: x = X by A5;

          X c= Y by A2, A5, A13, A14, A17, A15, A18, A16, WELLORD2:def 1;

          then p in rBP by A3, A1, A14, A18, A16, WELLORD2:def 1;

          hence p in (rBP |_2 cIP) by A12, A13, XBOOLE_0:def 4;

        end;

        assume

         A19: p in (rBP |_2 cIP);

        then

         A20: p in rBP by A12, XBOOLE_0:def 4;

        p in [:cIP, cIP:] by A12, A19, XBOOLE_0:def 4;

        then

        consider x,y be object such that

         A21: x in cIP & y in cIP and

         A22: p = [x, y] by ZFMISC_1:def 2;

        reconsider x, y as set by TARSKI: 1;

        (ex X be Filter of L st x = X) & ex Y be Filter of L st y = Y by A2, A21;

        then x c= y by A3, A1, A20, A22, WELLORD2:def 1;

        hence p in rIP by A2, A21, A22, WELLORD2:def 1;

      end;

      then rIP = (rBP |_2 cIP) by TARSKI: 2;

      then

      reconsider IP as full SubRelStr of BP by YELLOW_0:def 14;

      

       A23: ( Filt L) c= ( bool cL)

      proof

        let x be object;

        assume x in ( Filt L);

        then ex X be Filter of L st x = X;

        hence thesis;

      end;

      

       A24: IP is directed-sups-inheriting

      proof

        let X be directed Subset of IP such that

         A25: X <> {} and ex_sup_of (X,BP);

        consider Y be object such that

         A26: Y in X by A25, XBOOLE_0:def 1;

        reconsider F = X as Subset-Family of cL by A2, A23, XBOOLE_1: 1;

        

         A27: for P,R be Subset of L st P in F & R in F holds ex Z be Subset of L st Z in F & (P \/ R) c= Z

        proof

          let P,R be Subset of L;

          assume

           A28: P in F & R in F;

          then

          reconsider P9 = P, R9 = R as Element of IP;

          consider Z be Element of IP such that

           A29: Z in X and

           A30: P9 <= Z & R9 <= Z by A28, WAYBEL_0:def 1;

          Z in the carrier of IP by A29;

          then

          consider Z9 be Filter of L such that

           A31: Z9 = Z by A2;

          take Z9;

          thus Z9 in F by A29, A31;

          P9 c= Z & R9 c= Z by A30, YELLOW_1: 3;

          hence thesis by A31, XBOOLE_1: 8;

        end;

        reconsider X9 = X as Subset of BP by A3, A1, A2, A23, XBOOLE_1: 1;

        set sX = ( "\/" (X,BP));

        

         A32: ( sup X9) = ( union X) by YELLOW_1: 21;

        reconsider sX as Subset of L by A1, YELLOW_1: 4;

        

         A33: for X be Subset of L st X in F holds X is upper filtered

        proof

          let X be Subset of L;

          assume X in F;

          then X in ( Filt L) by A2;

          then ex Y be Filter of L st X = Y;

          hence thesis;

        end;

        then for X be Subset of L st X in F holds X is upper;

        then

         A34: sX is upper by A32, WAYBEL_0: 28;

        for X be Subset of L st X in F holds X is filtered by A33;

        then

         A35: sX is filtered by A32, A27, WAYBEL_0: 47;

        reconsider Y as set by TARSKI: 1;

        Y in ( Filt L) by A2, A26;

        then ex Z be Filter of L st Y = Z;

        then ( Top L) in Y by WAYBEL_4: 22;

        then sX is non empty by A32, A26, TARSKI:def 4;

        hence thesis by A2, A34, A35;

      end;

      IP is infs-inheriting

      proof

        let X be Subset of IP such that ex_inf_of (X,BP);

        set sX = ( "/\" (X,BP));

        per cases ;

          suppose

           A36: X is empty;

          

           A37: ( [#] L) = cL;

          ( "/\" (X,BP)) = ( Top BP) by A36

          .= cL by YELLOW_1: 19;

          hence thesis by A2, A37;

        end;

          suppose

           A38: X is non empty;

          reconsider F = X as Subset-Family of cL by A2, A23, XBOOLE_1: 1;

          reconsider sX as Subset of L by A1, YELLOW_1: 4;

          reconsider X9 = X as Subset of BP by A3, A1, A2, A23, XBOOLE_1: 1;

          

           A39: ( inf X9) = ( meet X) by A38, YELLOW_1: 20;

          

           A40: for X be Subset of L st X in F holds X is upper filtered

          proof

            let X be Subset of L;

            assume X in F;

            then X in ( Filt L) by A2;

            then ex Y be Filter of L st X = Y;

            hence thesis;

          end;

          then

           A41: sX is filtered by A39, YELLOW_2: 39;

          for X be Subset of L st X in F holds X is upper by A40;

          then

           A42: sX is upper by A39, YELLOW_2: 37;

          for Y be set st Y in X holds ( Top L) in Y

          proof

            let Y be set;

            assume Y in X;

            then Y in ( Filt L) by A2;

            then ex Z be Filter of L st Y = Z;

            hence thesis by WAYBEL_4: 22;

          end;

          then sX is non empty by A38, A39, SETFAM_1:def 1;

          hence thesis by A2, A42, A41;

        end;

      end;

      hence thesis by A24;

    end;

    registration

      let L be upper-bounded with_infima non empty Poset;

      cluster ( InclPoset ( Filt L)) -> continuous;

      coherence

      proof

        ( InclPoset ( Filt L)) is CLSubFrame of ( BoolePoset the carrier of L) by Th6;

        hence thesis by WAYBEL_5: 28;

      end;

    end

    registration

      let L be upper-bounded non empty Poset;

      cluster -> non empty for Element of ( InclPoset ( Filt L));

      coherence

      proof

        let x be Element of ( InclPoset ( Filt L));

        ( InclPoset ( Filt L)) = RelStr (# ( Filt L), ( RelIncl ( Filt L)) #) by YELLOW_1:def 1;

        then x in ( Filt L);

        then ex X be Filter of L st x = X;

        hence thesis;

      end;

    end

    begin

    definition

      let S be continuous complete non empty Poset;

      let A be set;

      :: WAYBEL22:def1

      pred A is_FreeGen_set_of S means for T be continuous complete non empty Poset holds for f be Function of A, the carrier of T holds ex h be CLHomomorphism of S, T st (h | A) = f & for h9 be CLHomomorphism of S, T st (h9 | A) = f holds h9 = h;

    end

    theorem :: WAYBEL22:7

    

     Th7: for S be continuous complete non empty Poset, A be set st A is_FreeGen_set_of S holds A is Subset of S

    proof

      set T = the continuous complete non empty Poset;

      let S be continuous complete non empty Poset, A be set such that

       A1: A is_FreeGen_set_of S;

      set f = the Function of A, the carrier of T;

      consider h be CLHomomorphism of S, T such that

       A2: (h | A) = f and for h9 be CLHomomorphism of S, T st (h9 | A) = f holds h9 = h by A1;

      ( dom (h | A)) = (( dom h) /\ A) by RELAT_1: 61;

      hence thesis by A2, FUNCT_2:def 1;

    end;

    theorem :: WAYBEL22:8

    

     Th8: for S be continuous complete non empty Poset, A be set st A is_FreeGen_set_of S holds for h9 be CLHomomorphism of S, S st (h9 | A) = ( id A) holds h9 = ( id S)

    proof

      let S be continuous complete non empty Poset, A be set such that

       A1: A is_FreeGen_set_of S;

      set L = S;

      

       A2: A is Subset of L by A1, Th7;

      then

       A3: (( id L) | A) = ( id A) by FUNCT_3: 1;

      ( dom ( id A)) = A & ( rng ( id A)) = A;

      then

      reconsider f = ( id A) as Function of A, the carrier of L by A2, RELSET_1: 4;

      consider h be CLHomomorphism of L, L such that (h | A) = f and

       A4: for h9 be CLHomomorphism of L, L st (h9 | A) = f holds h9 = h by A1;

      

       A5: ( id L) is CLHomomorphism of L, L by Th5;

      let h9 be CLHomomorphism of S, S;

      assume (h9 | A) = ( id A);

      

      hence h9 = h by A4

      .= ( id L) by A4, A5, A3;

    end;

    begin

    reserve X for set,

F for Filter of ( BoolePoset X),

x for Element of ( BoolePoset X),

z for Element of X;

    definition

      let X;

      :: WAYBEL22:def2

      func FixedUltraFilters X -> Subset-Family of ( BoolePoset X) equals { ( uparrow x) : ex z st x = {z} };

      coherence

      proof

        set FUF = { ( uparrow x) where x be Element of ( BoolePoset X) : ex y be Element of X st x = {y} };

        FUF c= ( bool the carrier of ( BoolePoset X))

        proof

          let z be object;

          assume z in FUF;

          then ex x be Element of ( BoolePoset X) st z = ( uparrow x) & ex y be Element of X st x = {y};

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL22:9

    

     Th9: ( FixedUltraFilters X) c= ( Filt ( BoolePoset X))

    proof

      let F be object;

      assume F in ( FixedUltraFilters X);

      then ex x be Element of ( BoolePoset X) st F = ( uparrow x) & ex y be Element of X st x = {y};

      hence thesis;

    end;

    theorem :: WAYBEL22:10

    

     Th10: ( card ( FixedUltraFilters X)) = ( card X)

    proof

      set FUF = { ( uparrow x) : ex z st x = {z} };

      

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

      

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

      then

       A3: the carrier of ( BoolePoset X) = ( bool X) by YELLOW_1: 4;

      (X,FUF) are_equipotent

      proof

        defpred P[ object, object] means ex y be Element of X, x be Element of ( BoolePoset X) st x = {y} & $1 = y & $2 = ( uparrow x);

        

         A4: for x be object st x in X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume

           A5: x in X;

          then

          reconsider x9 = x as Element of X;

          reconsider bx = {x} as Element of ( BoolePoset X) by A1, A2, A5, ZFMISC_1: 31;

          take ( uparrow bx);

          take x9;

          take bx;

          thus thesis;

        end;

        consider f be Function such that

         A6: ( dom f) = X & for x be object st x in X holds P[x, (f . x)] from CLASSES1:sch 1( A4);

        take f;

        thus f is one-to-one

        proof

          let x1,x2 be object such that

           A7: x1 in ( dom f) and

           A8: x2 in ( dom f) and

           A9: (f . x1) = (f . x2);

          consider x29 be Element of X, bx2 be Element of ( BoolePoset X) such that

           A10: bx2 = {x29} & x2 = x29 and

           A11: (f . x2) = ( uparrow bx2) by A6, A8;

          consider x19 be Element of X, bx1 be Element of ( BoolePoset X) such that

           A12: bx1 = {x19} & x1 = x19 and

           A13: (f . x1) = ( uparrow bx1) by A6, A7;

          bx1 = bx2 by A9, A13, A11, WAYBEL_0: 20;

          hence thesis by A12, A10, ZFMISC_1: 3;

        end;

        thus ( dom f) = X by A6;

        now

          let z be object;

          hereby

            assume z in ( rng f);

            then

            consider x1 be object such that

             A14: x1 in ( dom f) and

             A15: z = (f . x1) by FUNCT_1:def 3;

            ex x19 be Element of X, bx1 be Element of ( BoolePoset X) st bx1 = {x19} & x1 = x19 & (f . x1) = ( uparrow bx1) by A6, A14;

            hence z in FUF by A15;

          end;

          assume z in FUF;

          then

          consider bx be Element of ( BoolePoset X) such that

           A16: z = ( uparrow bx) and

           A17: ex y be Element of X st bx = {y};

          consider y be Element of X such that

           A18: bx = {y} by A17;

          

           A19: y in X by A3, A18, ZFMISC_1: 31;

          then ex x19 be Element of X, bx1 be Element of ( BoolePoset X) st bx1 = {x19} & y = x19 & (f . y) = ( uparrow bx1) by A6;

          hence z in ( rng f) by A6, A16, A18, A19, FUNCT_1:def 3;

        end;

        hence thesis by TARSKI: 2;

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: WAYBEL22:11

    

     Th11: F = ( "\/" ({ ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Y },( InclPoset ( Filt ( BoolePoset X))))) where Y be Subset of X : Y in F },( InclPoset ( Filt ( BoolePoset X)))))

    proof

      set BP = ( BoolePoset X);

      set IP = ( InclPoset ( Filt BP));

      set cIP = the carrier of IP;

      set Xs = { ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Y },IP)) where Y be Subset of X : Y in F };

      set RS = ( "\/" (Xs,IP));

      

       A1: ( InclPoset ( Filt BP)) = RelStr (# ( Filt BP), ( RelIncl ( Filt BP)) #) by YELLOW_1:def 1;

      F in ( Filt BP);

      then

      reconsider F9 = F as Element of IP by A1;

      

       A2: Xs c= cIP

      proof

        let p be object;

        assume p in Xs;

        then ex YY be Subset of X st p = ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in YY },IP)) & YY in F;

        hence thesis;

      end;

      

       A3: the carrier of BP = the carrier of ( LattPOSet ( BooleLatt X)) by YELLOW_1:def 2

      .= ( bool X) by LATTICE3:def 1;

      now

        consider YY be object such that

         A4: YY in F by XBOOLE_0:def 1;

        reconsider YY as set by TARSKI: 1;

        ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in YY },IP)) in Xs by A3, A4;

        hence Xs is non empty;

      end;

      then

      reconsider Xs9 = Xs as non empty Subset of IP by A2;

      

       A5: ex_sup_of (Xs9,IP) by YELLOW_0: 17;

      F c= RS

      proof

        let p be object;

        assume

         A6: p in F;

        then

        reconsider Y = p as Element of F;

        set Xsi = { ( uparrow x) where x be Element of BP : ex z be Element of X st x = {z} & z in Y };

        

         A7: ( "/\" (Xsi,IP)) in Xs by A3;

        per cases ;

          suppose

           A8: Xsi is empty;

          

           A9: p in the carrier of BP by A6;

          Xs9 is_<=_than RS by A5, YELLOW_0:def 9;

          then

           A10: ( "/\" (Xsi,IP)) <= RS by A7;

          ( "/\" (Xsi,IP)) = ( Top IP) by A8

          .= ( bool X) by WAYBEL16: 15;

          then ( bool X) c= RS by A10, YELLOW_1: 3;

          hence thesis by A3, A9;

        end;

          suppose

           A11: Xsi is non empty;

          Xsi c= cIP

          proof

            let r be object;

            assume r in Xsi;

            then ex xz be Element of BP st r = ( uparrow xz) & ex z be Element of X st xz = {z} & z in Y;

            hence thesis by A1;

          end;

          then

          reconsider Xsi as non empty Subset of IP by A11;

          for yy be set st yy in Xsi holds Y in yy

          proof

            reconsider Y9 = Y as Element of BP;

            let yy be set;

            assume yy in Xsi;

            then

            consider r be Element of BP such that

             A12: yy = ( uparrow r) and

             A13: ex z be Element of X st r = {z} & z in Y;

            r c= Y by A13, ZFMISC_1: 31;

            then r <= Y9 by YELLOW_1: 2;

            hence thesis by A12, WAYBEL_0: 18;

          end;

          then ( "/\" (Xsi,IP)) = ( meet Xsi) & Y in ( meet Xsi) by SETFAM_1:def 1, WAYBEL16: 10;

          then

           A14: p in ( union Xs) by A7, TARSKI:def 4;

          ( union Xs9) c= RS by WAYBEL16: 17, YELLOW_0: 17;

          hence thesis by A14;

        end;

      end;

      then

       A15: F9 <= RS by YELLOW_1: 3;

      Xs is_<=_than F9

      proof

        let b be Element of IP;

        assume b in Xs;

        then

        consider Y be Subset of X such that

         A16: b = ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Y },IP)) and

         A17: Y in F;

        reconsider Y9 = Y as Element of F by A17;

        set Xsi = { ( uparrow x) : ex z st x = {z} & z in Y };

        per cases ;

          suppose

           A18: Y is empty;

          now

            assume Xsi is non empty;

            then

            consider p be object such that

             A19: p in Xsi by XBOOLE_0:def 1;

            ex x be Element of BP st p = ( uparrow x) & ex z be Element of X st x = {z} & z in Y by A19;

            hence contradiction by A18;

          end;

          

          then

           A20: ( "/\" (Xsi,IP)) = ( Top IP)

          .= ( bool X) by WAYBEL16: 15;

          ( Bottom BP) = {} by YELLOW_1: 18;

          then ( uparrow ( Bottom BP)) c= F by A17, A18, WAYBEL11: 42;

          then ( bool X) c= F by A3, WAYBEL14: 10;

          hence b <= F9 by A3, A16, A20, XBOOLE_0:def 10;

        end;

          suppose

           A21: Y is non empty;

           A22:

          now

            consider z be object such that

             A23: z in Y by A21, XBOOLE_0:def 1;

            reconsider z as Element of X by A23;

            reconsider x = {z} as Element of BP by A3, A23, ZFMISC_1: 31;

            ( uparrow x) in Xsi by A23;

            hence Xsi is non empty;

          end;

          Xsi c= cIP

          proof

            let r be object;

            assume r in Xsi;

            then ex xz be Element of BP st r = ( uparrow xz) & ex z be Element of X st xz = {z} & z in Y;

            hence thesis by A1;

          end;

          then

          reconsider Xsi as non empty Subset of IP by A22;

          

           A24: ( "/\" (Xsi,IP)) = ( meet Xsi) by WAYBEL16: 10;

          b c= F9

          proof

            let yy be object;

            b in ( Filt BP) by A1;

            then

            consider bf be Filter of BP such that

             A25: b = bf;

            assume

             A26: yy in b;

            then

            reconsider yy9 = yy as Element of bf by A25;

            reconsider yy9 as Element of BP;

            Y c= yy9

            proof

              let zz be object;

              assume

               A27: zz in Y;

              then

              reconsider z = zz as Element of X;

              reconsider xz = {z} as Element of BP by A3, A27, ZFMISC_1: 31;

              ( uparrow xz) in Xsi by A27;

              then yy in ( uparrow xz) by A16, A24, A26, SETFAM_1:def 1;

              then xz <= yy9 by WAYBEL_0: 18;

              then {z} c= yy9 by YELLOW_1: 2;

              hence thesis by ZFMISC_1: 31;

            end;

            then Y9 <= yy9 by YELLOW_1: 2;

            then ( uparrow Y9) c= F9 & yy in ( uparrow Y9) by WAYBEL11: 42, WAYBEL_0: 18;

            hence thesis;

          end;

          hence b <= F9 by YELLOW_1: 3;

        end;

      end;

      then RS <= F9 by A5, YELLOW_0:def 9;

      hence thesis by A15, YELLOW_0:def 3;

    end;

    definition

      let X;

      let L be continuous complete non empty Poset;

      let f be Function of ( FixedUltraFilters X), the carrier of L;

      :: WAYBEL22:def3

      func f -extension_to_hom -> Function of ( InclPoset ( Filt ( BoolePoset X))), L means

      : Def3: for Fi be Element of ( InclPoset ( Filt ( BoolePoset X))) holds (it . Fi) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in Fi },L));

      existence

      proof

        set IP = ( InclPoset ( Filt ( BoolePoset X)));

        deffunc F( Element of IP) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in $1 },L));

        consider F be Function of the carrier of IP, the carrier of L such that

         A1: for Fi be Element of IP holds (F . Fi) = F(Fi) from FUNCT_2:sch 4;

        reconsider F as Function of IP, L;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set IP = ( InclPoset ( Filt ( BoolePoset X)));

        let it1,it2 be Function of IP, L such that

         A2: for Fi be Element of IP holds (it1 . Fi) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in Fi },L)) and

         A3: for Fi be Element of IP holds (it2 . Fi) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in Fi },L));

        reconsider it29 = it2 as Function of the carrier of IP, the carrier of L;

        reconsider it19 = it1 as Function of the carrier of IP, the carrier of L;

        now

          let Fi be Element of IP;

          

          thus (it19 . Fi) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in Fi },L)) by A2

          .= (it29 . Fi) by A3;

        end;

        hence it1 = it2 by FUNCT_2: 63;

      end;

    end

    theorem :: WAYBEL22:12

    for L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L holds (f -extension_to_hom ) is monotone

    proof

      let L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L;

      let F1,F2 be Element of ( InclPoset ( Filt ( BoolePoset X)));

      set F = (f -extension_to_hom );

      set F1s = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in F1 };

      set F2s = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in F2 };

      

       A1: ex_sup_of (F1s,L) & ex_sup_of (F2s,L) by YELLOW_0: 17;

      

       A2: (F . F1) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in F1 },L)) by Def3;

      assume F1 <= F2;

      then

       A3: F1 c= F2 by YELLOW_1: 3;

      

       A4: F1s c= F2s

      proof

        let s be object;

        assume s in F1s;

        then ex Y be Subset of X st s = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) & Y in F1;

        hence thesis by A3;

      end;

      

       A5: (F . F2) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in F2 },L)) by Def3;

      let FF1,FF2 be Element of L;

      assume FF1 = (F . F1) & FF2 = (F . F2);

      hence FF1 <= FF2 by A2, A5, A1, A4, YELLOW_0: 34;

    end;

    theorem :: WAYBEL22:13

    

     Th13: for L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L holds ((f -extension_to_hom ) . ( Top ( InclPoset ( Filt ( BoolePoset X))))) = ( Top L)

    proof

      let L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L;

      set IP = ( InclPoset ( Filt ( BoolePoset X)));

      set F = (f -extension_to_hom );

      reconsider T = ( Top IP) as Element of IP;

      reconsider E = {} as Subset of X by XBOOLE_1: 2;

      set Z = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in T };

      

       A1: { (f . ( uparrow x)) : ex z st x = {z} & z in E } = {}

      proof

        assume not thesis;

        then

        consider r be object such that

         A2: r in { (f . ( uparrow x)) : ex z st x = {z} & z in E } by XBOOLE_0:def 1;

        ex x st r = (f . ( uparrow x)) & ex z st x = {z} & z in E by A2;

        hence contradiction;

      end;

      

       A3: (F . T) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in T },L)) by Def3;

      T = ( bool X) by WAYBEL16: 15;

      then

       A4: ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in E },L)) in Z;

      Z is_<=_than ( "\/" (Z,L)) by YELLOW_0: 32;

      then ( Top L) <= ( "\/" (Z,L)) by A4, A1;

      hence thesis by A3, WAYBEL15: 3;

    end;

    registration

      let X;

      let L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L;

      cluster (f -extension_to_hom ) -> directed-sups-preserving;

      coherence

      proof

        set F = (f -extension_to_hom );

        set IP = ( InclPoset ( Filt ( BoolePoset X)));

        let Fs be Subset of IP such that

         A1: Fs is non empty directed;

        reconsider Fs9 = Fs as non empty Subset of IP by A1;

        set FFsU = the set of all { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in YY } where YY be Element of Fs9;

        reconsider sFs = ( sup Fs) as Element of IP;

        set FFs = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in sFs };

        

         A2: ( sup Fs) = ( union Fs) by A1, Th1;

        now

          let p be object;

          hereby

            assume p in FFs;

            then

            consider Y be Subset of X such that

             A3: p = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) and

             A4: Y in sFs;

            consider YY be set such that

             A5: Y in YY and

             A6: YY in Fs by A2, A4, TARSKI:def 4;

            

             A7: { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y1 },L)) where Y1 be Subset of X : Y1 in YY } in FFsU by A6;

            p in { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y1 },L)) where Y1 be Subset of X : Y1 in YY } by A3, A5;

            hence p in ( union FFsU) by A7, TARSKI:def 4;

          end;

          assume p in ( union FFsU);

          then

          consider r be set such that

           A8: p in r and

           A9: r in FFsU by TARSKI:def 4;

          consider YY be Element of Fs9 such that

           A10: r = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in YY } by A9;

          consider Y be Subset of X such that

           A11: p = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) and

           A12: Y in YY by A8, A10;

          Y in sFs by A2, A12, TARSKI:def 4;

          hence p in FFs by A11;

        end;

        then

         A13: FFs = ( union FFsU) by TARSKI: 2;

        set Zs = { ( sup Z) where Z be Subset of L : Z in FFsU };

        assume ex_sup_of (Fs,IP);

        thus ex_sup_of ((F .: Fs),L) by YELLOW_0: 17;

        FFsU c= ( bool the carrier of L)

        proof

          let r be object;

          reconsider rr = r as set by TARSKI: 1;

          assume r in FFsU;

          then

          consider YY be Element of Fs9 such that

           A14: r = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in YY };

          rr c= the carrier of L

          proof

            let s be object;

            assume s in rr;

            then ex Y be Subset of X st s = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) & Y in YY by A14;

            hence thesis;

          end;

          hence thesis;

        end;

        then

         A15: ( "\/" (( union FFsU),L)) = ( "\/" (Zs,L)) by Lm2;

         A16:

        now

          let r be object;

          hereby

            assume r in (F .: Fs);

            then

            consider YY be object such that

             A17: YY in the carrier of IP and

             A18: YY in Fs and

             A19: (F . YY) = r by FUNCT_2: 64;

            reconsider YY as Element of Fs by A18;

            reconsider YY9 = YY as Element of IP by A17;

            set Zi = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in YY9 };

            Zi c= the carrier of L

            proof

              let t be object;

              assume t in Zi;

              then ex Y be Subset of X st t = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) & Y in YY9;

              hence thesis;

            end;

            then

            reconsider Zi as Subset of L;

            

             A20: Zi in FFsU;

            (F . YY9) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in YY9 },L)) by Def3;

            hence r in Zs by A19, A20;

          end;

          assume r in Zs;

          then

          consider Z be Subset of L such that

           A21: r = ( sup Z) and

           A22: Z in FFsU;

          consider YY be Element of Fs such that

           A23: Z = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in YY } by A22;

          reconsider YY as Element of Fs9;

          reconsider YY9 = YY as Element of IP;

          (F . YY9) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in YY9 },L)) by Def3;

          hence r in (F .: Fs) by A21, A23, FUNCT_2: 35;

        end;

        (F . sFs) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in sFs },L)) by Def3;

        hence thesis by A15, A13, A16, TARSKI: 2;

      end;

    end

    registration

      let X;

      let L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L;

      cluster (f -extension_to_hom ) -> infs-preserving;

      coherence

      proof

        set FUF = ( FixedUltraFilters X);

        set cL = the carrier of L;

        set F = (f -extension_to_hom );

        set BP = ( BoolePoset X);

        set IP = ( InclPoset ( Filt BP));

        set cIP = the carrier of IP;

        

         A1: ( InclPoset ( Filt BP)) = RelStr (# ( Filt BP), ( RelIncl ( Filt BP)) #) by YELLOW_1:def 1;

        let Fs be Subset of IP;

        assume ex_inf_of (Fs,IP);

        thus ex_inf_of ((F .: Fs),L) by YELLOW_0: 17;

        

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

        

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

        then

         A4: the carrier of ( BoolePoset X) = ( bool X) by YELLOW_1: 4;

        per cases ;

          suppose Fs is empty;

          then ( "/\" ((F .: Fs),L)) = ( Top L) & ( "/\" (Fs,IP)) = ( Top IP);

          hence thesis by Th13;

        end;

          suppose Fs is non empty;

          then

          reconsider Fs9 = Fs as non empty Subset of IP;

          defpred P[ object, object, object] means ex D2 be set st D2 = $2 & $1 = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in D2 },L));

          deffunc FDi( Element of Fs9) = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in $1 };

           not {} in Fs9;

          then Fs9 is with_non-empty_elements by SETFAM_1:def 8;

          then

          reconsider K = ( id Fs9) as non-empty ManySortedSet of Fs9;

          

           A5: for i be object st i in Fs9 holds for s be object st s in (K . i) holds ex y be object st y in ((Fs9 --> cL) . i) & P[y, s, i]

          proof

            let i be object such that

             A6: i in Fs9;

            let s be object such that s in (K . i);

            reconsider D2 = s as set by TARSKI: 1;

            take y = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in D2 },L));

            y in cL;

            hence y in ((Fs9 --> cL) . i) by A6, FUNCOP_1: 7;

            take D2;

            thus D2 = s;

            thus y = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in D2 },L));

          end;

          consider FD be ManySortedFunction of K, (Fs9 --> cL) such that

           A7: for i be object st i in Fs9 holds ex g be Function of (K . i), ((Fs9 --> cL) . i) st g = (FD . i) & for s be object st s in (K . i) holds P[(g . s), s, i] from MSSUBFAM:sch 1( A5);

          defpred rFD[ Element of Fs9] means ( rng (FD . $1)) = FDi($1);

          

           A8: for s be Element of Fs9 holds rFD[s]

          proof

            let s be Element of Fs9;

            now

              let t be object;

              consider g be Function of (K . s), ((Fs9 --> cL) . s) such that

               A9: g = (FD . s) and

               A10: for u be object st u in (K . s) holds P[(g . u), u, s] by A7;

              hereby

                assume t in ( rng (FD . s));

                then

                consider u be object such that

                 A11: u in ( dom (FD . s)) and

                 A12: t = ((FD . s) . u) by FUNCT_1:def 3;

                consider g be Function of (K . s), ((Fs9 --> cL) . s) such that

                 A13: g = (FD . s) and

                 A14: for u be object st u in (K . s) holds P[(g . u), u, s] by A7;

                

                 A15: ( dom (FD . s)) = (K . s) by FUNCT_2:def 1;

                reconsider u as set by TARSKI: 1;

                 P[(g . u), u, s] by A11, A14;

                then

                 A16: (g . u) = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in u },L));

                s in cIP;

                then (K . s) = s & ex FF be Filter of BP st s = FF by A1;

                then

                reconsider u as Subset of X by A3, A11, A15, YELLOW_1: 4;

                u in s by A11;

                then t in { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in s } by A12, A13, A16;

                hence t in FDi(s);

              end;

              assume t in FDi(s);

              then

              consider Y be Subset of X such that

               A17: t = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) and

               A18: Y in s;

              ( dom (FD . s)) = (K . s) by FUNCT_2:def 1;

              then

               A19: Y in ( dom (FD . s)) by A18;

               P[(g . Y), Y, s] by A10, A18;

              then (g . Y) = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L));

              hence t in ( rng (FD . s)) by A17, A19, A9, FUNCT_1:def 3;

            end;

            hence thesis by TARSKI: 2;

          end;

          ( meet Fs9) is Filter of ( BoolePoset X) by WAYBEL16: 9;

          then ( meet Fs9) in ( Filt BP);

          then

          reconsider mFs = ( meet Fs9) as Element of cIP by A1;

          set smFs = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in mFs };

          

           A20: ( dom FD) = Fs9 by PARTFUN1:def 2;

          reconsider FD as DoubleIndexedSet of K, L;

          now

            let r be object;

            hereby

              assume r in (F .: Fs);

              then

              consider s be object such that

               A21: s in cIP and

               A22: s in Fs and

               A23: (F . s) = r by FUNCT_2: 64;

              reconsider s9 = s as Element of cIP by A21;

              reconsider s as Element of Fs9 by A22;

              

               A24: rFD[s] by A8;

              (F . s9) = ( "\/" ({ ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in s9 },L)) by Def3;

              then r = ( Sup (FD . s)) by A23, A24, YELLOW_2:def 5;

              hence r in ( rng ( Sups FD)) by WAYBEL_5: 14;

            end;

            assume r in ( rng ( Sups FD));

            then

            consider s be Element of Fs9 such that

             A25: r = ( Sup (FD . s)) by WAYBEL_5: 14;

             rFD[s] by A8;

            

            then (F . s) = ( "\/" (( rng (FD . s)),L)) by Def3

            .= ( Sup (FD . s)) by YELLOW_2:def 5;

            hence r in (F .: Fs) by A25, FUNCT_2: 35;

          end;

          then (F .: Fs) = ( rng ( Sups FD)) by TARSKI: 2;

          then

           A26: ( inf (F .: Fs)) = ( Inf ( Sups FD)) by YELLOW_2:def 6;

           A27:

          now

            reconsider pdFD = ( product ( doms FD)) as non empty functional set;

            let r be object;

            reconsider dFFD = (( product ( doms FD)) --> Fs9) as ManySortedSet of pdFD;

            reconsider FFD = ( Frege FD) as DoubleIndexedSet of dFFD, L;

            deffunc rFFDs( Element of pdFD) = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in ($1 . u) },L)) where u be Element of Fs9 : u in ( dom (FFD . $1)) };

            

             A28: ( dom FFD) = pdFD by PARTFUN1:def 2;

             A29:

            now

              let s be Element of pdFD;

              

               A30: ( dom FD) = ( dom (FFD . s)) by A28, WAYBEL_5: 8;

              now

                let t be object;

                hereby

                  assume t in ( rng (FFD . s));

                  then

                  consider u be object such that

                   A31: u in ( dom (FFD . s)) and

                   A32: t = ((FFD . s) . u) by FUNCT_1:def 3;

                  

                   A33: ((FFD . s) . u) = ((FD . u) . (s . u)) by A28, A30, A31, WAYBEL_5: 9;

                  reconsider u as Element of Fs9 by A31;

                  consider g be Function of (K . u), ((Fs9 --> cL) . u) such that

                   A34: g = (FD . u) and

                   A35: for v be object st v in (K . u) holds P[(g . v), v, u] by A7;

                  ( dom (FD . u)) = (K . u) by FUNCT_2:def 1;

                  then P[(g . (s . u)), (s . u), s] by A20, A28, A35, WAYBEL_5: 9;

                  then (g . (s . u)) = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) },L));

                  hence t in rFFDs(s) by A31, A32, A33, A34;

                end;

                assume t in rFFDs(s);

                then

                consider u be Element of Fs9 such that

                 A36: t = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) },L)) & u in ( dom (FFD . s));

                reconsider u as Element of Fs9;

                consider g be Function of (K . u), ((Fs9 --> cL) . u) such that

                 A37: g = (FD . u) and

                 A38: for v be object st v in (K . u) holds P[(g . v), v, u] by A7;

                ( dom (FD . u)) = (K . u) by FUNCT_2:def 1;

                then P[(g . (s . u)), (s . u), s] by A20, A28, A38, WAYBEL_5: 9;

                then (g . (s . u)) = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) },L));

                hence t in ( rng (FFD . s)) by A28, A30, A36, A37, WAYBEL_5: 9;

              end;

              hence ( rng (FFD . s)) = rFFDs(s) by TARSKI: 2;

            end;

            hereby

              assume r in ( rng ( Infs ( Frege FD)));

              then

              consider s be Element of pdFD such that

               A39: r = ( Inf (FFD . s)) by WAYBEL_5: 14;

              set idFFDs = { { (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) } where u be Element of Fs9 : u in ( dom (FFD . s)) };

              

               A40: idFFDs c= ( bool the carrier of L)

              proof

                let t be object;

                reconsider tt = t as set by TARSKI: 1;

                assume t in idFFDs;

                then

                consider u be Element of Fs9 such that

                 A41: t = { (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) } and u in ( dom (FFD . s));

                tt c= cL

                proof

                  let v be object;

                  assume v in tt;

                  then

                  consider x such that

                   A42: v = (f . ( uparrow x)) and

                   A43: ex z st x = {z} & z in (s . u) by A41;

                  ( uparrow x) in FUF by A43;

                  hence thesis by A42, FUNCT_2: 5;

                end;

                hence thesis;

              end;

              now

                let t be object;

                hereby

                  assume t in rFFDs(s);

                  then

                  consider u be Element of Fs9 such that

                   A44: t = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) },L)) and

                   A45: u in ( dom (FFD . s));

                  { (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) } c= cL

                  proof

                    let v be object;

                    assume v in { (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) };

                    then

                    consider x such that

                     A46: v = (f . ( uparrow x)) and

                     A47: ex z st x = {z} & z in (s . u);

                    ( uparrow x) in FUF by A47;

                    hence thesis by A46, FUNCT_2: 5;

                  end;

                  then

                  reconsider Y1 = { (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) } as Subset of L;

                  Y1 in idFFDs by A45;

                  hence t in { ( inf YY) where YY be Subset of L : YY in idFFDs } by A44;

                end;

                assume t in { ( inf YY) where YY be Subset of L : YY in idFFDs };

                then

                consider YY be Subset of L such that

                 A48: t = ( inf YY) and

                 A49: YY in idFFDs;

                ex u1 be Element of Fs9 st YY = { (f . ( uparrow x)) : ex z st x = {z} & z in (s . u1) } & u1 in ( dom (FFD . s)) by A49;

                hence t in rFFDs(s) by A48;

              end;

              then

               A50: rFFDs(s) = { ( inf YY) where YY be Subset of L : YY in idFFDs } by TARSKI: 2;

              

               A51: ( dom s) = ( dom FD) by A28, WAYBEL_5: 8;

              ( union ( rng s)) c= X

              proof

                let t be object;

                assume t in ( union ( rng s));

                then

                consider te be set such that

                 A52: t in te and

                 A53: te in ( rng s) by TARSKI:def 4;

                consider u be object such that

                 A54: u in ( dom s) and

                 A55: te = (s . u) by A53, FUNCT_1:def 3;

                reconsider u as set by TARSKI: 1;

                (FD . u) is Function of (K . u), cL by A51, A54, WAYBEL_5: 6;

                

                then ( dom (FD . u)) = (K . u) by FUNCT_2:def 1

                .= u by A51, A54, FUNCT_1: 17;

                then

                 A56: te in u by A28, A51, A54, A55, WAYBEL_5: 9;

                u in cIP by A20, A51, A54;

                then ex FF be Filter of BP st u = FF by A1;

                hence thesis by A4, A52, A56;

              end;

              then

              reconsider Y = ( union ( rng s)) as Subset of X;

              set Ys = { (f . ( uparrow x)) : ex z st x = {z} & z in Y };

              

               A57: ( dom FD) = ( dom (FFD . s)) by A28, WAYBEL_5: 8;

              now

                let t be object;

                hereby

                  assume t in ( union idFFDs);

                  then

                  consider te be set such that

                   A58: t in te and

                   A59: te in idFFDs by TARSKI:def 4;

                  consider u be Element of Fs9 such that

                   A60: te = { (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) } and

                   A61: u in ( dom (FFD . s)) by A59;

                  consider x such that

                   A62: t = (f . ( uparrow x)) and

                   A63: ex z st x = {z} & z in (s . u) by A58, A60;

                  consider z such that

                   A64: x = {z} and

                   A65: z in (s . u) by A63;

                  (s . u) in ( rng s) by A57, A51, A61, FUNCT_1:def 3;

                  then z in Y by A65, TARSKI:def 4;

                  hence t in Ys by A62, A64;

                end;

                assume t in Ys;

                then

                consider x such that

                 A66: t = (f . ( uparrow x)) and

                 A67: ex z st x = {z} & z in Y;

                consider z such that

                 A68: x = {z} and

                 A69: z in Y by A67;

                consider ze be set such that

                 A70: z in ze and

                 A71: ze in ( rng s) by A69, TARSKI:def 4;

                consider u be object such that

                 A72: u in ( dom s) and

                 A73: ze = (s . u) by A71, FUNCT_1:def 3;

                reconsider u as Element of Fs9 by A51, A72;

                

                 A74: { (f . ( uparrow x1)) where x1 be Element of BP : ex z st x1 = {z} & z in (s . u) } in idFFDs by A57, A51, A72;

                t in { (f . ( uparrow x1)) where x1 be Element of BP : ex z st x1 = {z} & z in (s . u) } by A66, A68, A70, A73;

                hence t in ( union idFFDs) by A74, TARSKI:def 4;

              end;

              then

               A75: ( union idFFDs) = Ys by TARSKI: 2;

              now

                reconsider Y9 = Y as Element of BP by A3, YELLOW_1: 4;

                let Z be set;

                assume

                 A76: Z in Fs9;

                then (FD . Z) is Function of (K . Z), cL by WAYBEL_5: 6;

                

                then

                 A77: ( dom (FD . Z)) = (K . Z) by FUNCT_2:def 1

                .= Z by A76, FUNCT_1: 17;

                (s . Z) in ( rng s) by A20, A51, A76, FUNCT_1:def 3;

                then

                 A78: (s . Z) c= Y by ZFMISC_1: 74;

                then

                reconsider sZ = (s . Z) as Element of BP by A2, A3, XBOOLE_1: 1;

                

                 A79: sZ <= Y9 by A78, YELLOW_1: 2;

                Z in cIP by A76;

                then

                 A80: ex FF be Filter of BP st Z = FF by A1;

                (s . Z) in ( dom (FD . Z)) by A20, A28, A76, WAYBEL_5: 9;

                hence Y in Z by A80, A77, A79, WAYBEL_0:def 20;

              end;

              then Y in mFs by SETFAM_1:def 1;

              then

               A81: ( "/\" (Ys,L)) in smFs;

              ( "/\" (( rng (FFD . s)),L)) = ( "/\" ( rFFDs(s),L)) by A29

              .= ( "/\" (( union idFFDs),L)) by A40, A50, Lm1;

              hence r in smFs by A39, A81, A75, YELLOW_2:def 6;

            end;

            assume r in smFs;

            then

            consider Y be Subset of X such that

             A82: r = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) and

             A83: Y in mFs;

            

             A84: ( "/\" ( {r},L)) = r by A82, YELLOW_0: 39;

            set s = (Fs9 --> Y);

            

             A85: ( dom ( doms FD)) = ( dom FD) by FUNCT_6: 59

            .= ( dom s) by A20;

             A86:

            now

              let w be object;

              assume

               A87: w in ( dom ( doms FD));

              then (FD . w) is Function of (K . w), ((Fs9 --> cL) . w) by A85, PBOOLE:def 15;

              

              then

               A88: ( dom (FD . w)) = (K . w) by A85, A87, FUNCT_2:def 1

              .= w by A85, A87, FUNCT_1: 18;

              (( doms FD) . w) = ( dom (FD . w)) & (s . w) = Y by A20, A85, A87, FUNCOP_1: 7, FUNCT_6: 22;

              hence (s . w) in (( doms FD) . w) by A83, A85, A87, A88, SETFAM_1:def 1;

            end;

            set s9 = s;

            reconsider s as Element of pdFD by A85, A86, CARD_3: 9;

            now

              set u = the Element of Fs9;

              let t be object;

              

               A89: ( dom s9) = Fs9 & (s . u) = Y;

              hereby

                assume t in rFFDs(s);

                then

                consider u be Element of Fs9 such that

                 A90: t = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) },L)) and u in ( dom (FFD . s));

                thus t in {r} by A82, A90, TARSKI:def 1;

              end;

              assume t in {r};

              then

               A91: t = r by TARSKI:def 1;

              ( dom FD) = ( dom (FFD . s)) & ( dom s) = ( dom FD) by A28, WAYBEL_5: 8;

              hence t in rFFDs(s) by A82, A91, A89;

            end;

            then

             A92: { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in (s . u) },L)) where u be Element of Fs9 : u in ( dom (FFD . s)) } = {r} by TARSKI: 2;

            ( Inf (FFD . s)) = ( "/\" (( rng (FFD . s)),L)) & ( rng (FFD . s)) = rFFDs(s) by A29, YELLOW_2:def 6;

            hence r in ( rng ( Infs ( Frege FD))) by A92, A84, WAYBEL_5: 14;

          end;

          for j be Element of Fs9 holds ( rng (FD . j)) is directed

          proof

            let j be Element of Fs9;

            let k,m be Element of L;

            assume that

             A93: k in ( rng (FD . j)) and

             A94: m in ( rng (FD . j));

            consider kd be object such that

             A95: kd in ( dom (FD . j)) and

             A96: ((FD . j) . kd) = k by A93, FUNCT_1:def 3;

            consider md be object such that

             A97: md in ( dom (FD . j)) and

             A98: ((FD . j) . md) = m by A94, FUNCT_1:def 3;

            j in cIP;

            then

            consider FF be Filter of BP such that

             A99: j = FF by A1;

            

             A100: ( dom (FD . j)) = (K . j) by FUNCT_2:def 1;

            then

            reconsider kd as Element of BP by A95, A99;

            reconsider md as Element of BP by A97, A100, A99;

            consider nd be Element of BP such that

             A101: nd in FF and

             A102: nd <= kd and

             A103: nd <= md by A95, A97, A99, WAYBEL_0:def 2;

            set n = ((FD . j) . nd);

            

             A104: n in ( rng (FD . j)) by A100, A99, A101, FUNCT_1:def 3;

            consider g be Function of (K . j), ((Fs9 --> cL) . j) such that

             A105: g = (FD . j) and

             A106: for u be object st u in (K . j) holds P[(g . u), u, j] by A7;

            set nds = { (f . ( uparrow x)) : ex z st x = {z} & z in nd };

             P[(g . nd), nd, j] by A99, A101, A106;

            then

             A107: (g . nd) = ( "/\" (nds,L));

            reconsider n as Element of L by A104;

            take n;

            thus n in ( rng (FD . j)) by A100, A99, A101, FUNCT_1:def 3;

            

             A108: ex_inf_of (nds,L) by YELLOW_0: 17;

            set mds = { (f . ( uparrow x)) : ex z st x = {z} & z in md };

            

             A109: nd c= md by A103, YELLOW_1: 2;

            

             A110: nds c= mds

            proof

              let w be object;

              assume w in nds;

              then ex x st w = (f . ( uparrow x)) & ex z st x = {z} & z in nd;

              hence thesis by A109;

            end;

            

             A111: ex_inf_of (mds,L) by YELLOW_0: 17;

            set kds = { (f . ( uparrow x)) : ex z st x = {z} & z in kd };

            

             A112: ex_inf_of (kds,L) by YELLOW_0: 17;

            

             A113: nd c= kd by A102, YELLOW_1: 2;

            

             A114: nds c= kds

            proof

              let w be object;

              assume w in nds;

              then ex x st w = (f . ( uparrow x)) & ex z st x = {z} & z in nd;

              hence thesis by A113;

            end;

             P[(g . kd), kd, j] by A95, A106;

            then (g . kd) = ( "/\" (kds,L));

            hence k <= n by A96, A105, A107, A112, A108, A114, YELLOW_0: 35;

             P[(g . md), md, j] by A97, A106;

            then (g . md) = ( "/\" (mds,L));

            hence m <= n by A98, A105, A107, A108, A111, A110, YELLOW_0: 35;

          end;

          

          then

           A115: ( Inf ( Sups FD)) = ( Sup ( Infs ( Frege FD))) by WAYBEL_5: 19

          .= ( "\/" (( rng ( Infs ( Frege FD))),L)) by YELLOW_2:def 5;

          ( inf Fs9) = ( meet Fs9) & (F . ( meet Fs9)) = ( "\/" (smFs,L)) by Def3, WAYBEL16: 10;

          hence thesis by A26, A115, A27, TARSKI: 2;

        end;

      end;

    end

    theorem :: WAYBEL22:14

    

     Th14: for L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L holds ((f -extension_to_hom ) | ( FixedUltraFilters X)) = f

    proof

      let L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L;

      set FUF = ( FixedUltraFilters X);

      set BP = ( BoolePoset X);

      set IP = ( InclPoset ( Filt BP));

      

       A1: ( InclPoset ( Filt BP)) = RelStr (# ( Filt BP), ( RelIncl ( Filt BP)) #) by YELLOW_1:def 1;

      set F = (f -extension_to_hom );

      

       A2: the carrier of BP = the carrier of ( LattPOSet ( BooleLatt X)) by YELLOW_1:def 2

      .= ( bool X) by LATTICE3:def 1;

      now

        

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

        hence FUF = ( dom (F | FUF)) by A1, Th9, RELAT_1: 62;

        thus FUF = ( dom f) by FUNCT_2:def 1;

        let xf be object;

        assume

         A4: xf in FUF;

        then

        reconsider FUF9 = FUF as non empty Subset-Family of ( BoolePoset X);

        

         A5: ((F | FUF) . xf) = (F . xf) by A4, FUNCT_1: 49;

        FUF c= ( dom F) by A1, A3, Th9;

        then

        reconsider x9 = xf as Element of IP by A4, FUNCT_2:def 1;

        reconsider xf9 = xf as Element of FUF9 by A4;

        set Xs = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in x9 };

        reconsider f9 = f as Function of FUF9, the carrier of L;

        (f9 . xf9) is Element of L;

        then

        reconsider fxf = (f . xf9) as Element of L;

        consider xx be Element of ( BoolePoset X) such that

         A6: xf = ( uparrow xx) and

         A7: ex y be Element of X st xx = {y} by A4;

        

         A8: Xs is_<=_than fxf

        proof

          let b be Element of L;

          assume b in Xs;

          then

          consider Y be Subset of X such that

           A9: b = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) and

           A10: Y in x9;

          set Xsi = { (f . ( uparrow x)) : ex z st x = {z} & z in Y };

           ex_inf_of (Xsi,L) by YELLOW_0: 17;

          then

           A11: Xsi is_>=_than b by A9, YELLOW_0:def 10;

          reconsider Y as Element of ( BoolePoset X) by A6, A10;

          consider y be Element of X such that

           A12: xx = {y} by A7;

          xx <= Y by A6, A10, WAYBEL_0: 18;

          then xx c= Y by YELLOW_1: 2;

          then y in Y by A12, ZFMISC_1: 31;

          then fxf in Xsi by A6, A12;

          hence b <= fxf by A11;

        end;

        

         A13: for a be Element of L st Xs is_<=_than a holds fxf <= a

        proof

          xx <= xx;

          then

          reconsider Y = xx as Element of x9 by A6, WAYBEL_0: 18;

          set Xsi = { (f . ( uparrow x)) : ex z st x = {z} & z in Y };

          consider y be Element of X such that

           A14: xx = {y} by A7;

          now

            let p be object;

            hereby

              assume p in Xsi;

              then

              consider r be Element of ( BoolePoset X) such that

               A15: p = (f . ( uparrow r)) and

               A16: ex z be Element of X st r = {z} & z in Y;

              xx = r by A14, A16, TARSKI:def 1;

              hence p in {fxf} by A6, A15, TARSKI:def 1;

            end;

            assume p in {fxf};

            then

             A17: p = fxf by TARSKI:def 1;

            y in Y by A14, TARSKI:def 1;

            hence p in Xsi by A6, A14, A17;

          end;

          then Xsi = {fxf} by TARSKI: 2;

          then fxf = ( "/\" (Xsi,L)) by YELLOW_0: 39;

          then

           A18: fxf in Xs by A2;

          let a be Element of L;

          assume Xs is_<=_than a;

          hence thesis by A18;

        end;

         ex_sup_of (Xs,L) by YELLOW_0: 17;

        then (f . xf) = ( "\/" (Xs,L)) by A8, A13, YELLOW_0:def 9;

        hence ((F | FUF) . xf) = (f . xf) by A5, Def3;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL22:15

    

     Th15: for L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L, h be CLHomomorphism of ( InclPoset ( Filt ( BoolePoset X))), L st (h | ( FixedUltraFilters X)) = f holds h = (f -extension_to_hom )

    proof

      let L be continuous complete non empty Poset, f be Function of ( FixedUltraFilters X), the carrier of L, h be CLHomomorphism of ( InclPoset ( Filt ( BoolePoset X))), L;

      assume

       A1: (h | ( FixedUltraFilters X)) = f;

      set F = (f -extension_to_hom );

      set cL = the carrier of L;

      set BP = ( BoolePoset X);

      set IP = ( InclPoset ( Filt BP));

      set cIP = the carrier of IP;

      

       A2: ( InclPoset ( Filt BP)) = RelStr (# ( Filt BP), ( RelIncl ( Filt BP)) #) by YELLOW_1:def 1;

      reconsider F9 = F as Function of cIP, cL;

      reconsider h9 = h as Function of cIP, cL;

      

       A3: the carrier of BP = the carrier of ( LattPOSet ( BooleLatt X)) by YELLOW_1:def 2

      .= ( bool X) by LATTICE3:def 1;

      now

        set FUF = ( FixedUltraFilters X);

        let Fi be Element of cIP;

        Fi in ( Filt BP) by A2;

        then

        consider FF be Filter of BP such that

         A4: Fi = FF;

        set Xsf = { ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) where Y be Subset of X : Y in FF };

        set Xs = { ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Y },IP)) where Y be Subset of X : Y in FF };

        

         A5: Xs c= cIP

        proof

          let p be object;

          assume p in Xs;

          then ex YY be Subset of X st p = ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in YY },IP)) & YY in FF;

          hence thesis;

        end;

        now

          consider YY be object such that

           A6: YY in FF by XBOOLE_0:def 1;

          reconsider YY as set by TARSKI: 1;

          ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in YY },IP)) in Xs by A3, A6;

          hence Xs is non empty;

        end;

        then

        reconsider Xs as non empty Subset of IP by A5;

        

         A7: ex_sup_of (Xs,IP) by YELLOW_0: 17;

        

         A8: Xs is directed

        proof

          let a,b be Element of IP;

          assume that

           A9: a in Xs and

           A10: b in Xs;

          consider Yb be Subset of X such that

           A11: b = ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Yb },IP)) and

           A12: Yb in FF by A10;

          reconsider Yb9 = Yb as Element of FF by A12;

          set Xsb = { ( uparrow x) : ex z st x = {z} & z in Yb };

          consider Ya be Subset of X such that

           A13: a = ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Ya },IP)) and

           A14: Ya in FF by A9;

          reconsider Ya9 = Ya as Element of FF by A14;

          set Xsa = { ( uparrow x) : ex z st x = {z} & z in Ya };

          per cases ;

            suppose

             A15: Xsa is empty;

            take a;

            thus a in Xs by A9;

            thus a <= a;

            ( "/\" (Xsa,IP)) = ( Top IP) by A15;

            hence b <= a by A13, YELLOW_0: 45;

          end;

            suppose

             A16: Xsb is empty;

            take b;

            thus b in Xs by A10;

            ( "/\" (Xsb,IP)) = ( Top IP) by A16;

            hence a <= b by A11, YELLOW_0: 45;

            thus b <= b;

          end;

            suppose

             A17: Xsa is non empty & Xsb is non empty;

            Xsb c= cIP

            proof

              let r be object;

              assume r in Xsb;

              then ex xz be Element of BP st r = ( uparrow xz) & ex z st xz = {z} & z in Yb;

              hence thesis by A2;

            end;

            then

            reconsider Xsb as non empty Subset of IP by A17;

            Xsa c= cIP

            proof

              let r be object;

              assume r in Xsa;

              then ex xz be Element of BP st r = ( uparrow xz) & ex z st xz = {z} & z in Ya;

              hence thesis by A2;

            end;

            then

            reconsider Xsa as non empty Subset of IP by A17;

            

             A18: ( "/\" (Xsb,IP)) = ( meet Xsb) by WAYBEL16: 10;

            consider Yab be Element of BP such that

             A19: Yab in FF and

             A20: Yab <= Ya9 and

             A21: Yab <= Yb9 by WAYBEL_0:def 2;

            reconsider Yab as Element of FF by A19;

            set c = ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Yab },IP));

            set Xsc = { ( uparrow x) : ex z st x = {z} & z in Yab };

            

             A22: ( "/\" (Xsa,IP)) = ( meet Xsa) by WAYBEL16: 10;

            thus thesis

            proof

              per cases ;

                suppose

                 A23: Xsc is empty;

                take c;

                thus c in Xs by A3;

                

                 A24: ( "/\" (Xsc,IP)) = ( Top IP) by A23;

                hence a <= c by YELLOW_0: 45;

                thus b <= c by A24, YELLOW_0: 45;

              end;

                suppose

                 A25: Xsc is non empty;

                Xsc c= cIP

                proof

                  let r be object;

                  assume r in Xsc;

                  then ex xz be Element of BP st r = ( uparrow xz) & ex z st xz = {z} & z in Yab;

                  hence thesis by A2;

                end;

                then

                reconsider Xsc as non empty Subset of IP by A25;

                take c;

                thus c in Xs by A3;

                

                 A26: ( "/\" (Xsc,IP)) = ( meet Xsc) by WAYBEL16: 10;

                a c= c

                proof

                  let d be object;

                  Xsc c= Xsa

                  proof

                    let r be object;

                    assume r in Xsc;

                    then

                     A27: ex xz be Element of BP st r = ( uparrow xz) & ex z st xz = {z} & z in Yab;

                    Yab c= Ya by A20, YELLOW_1: 2;

                    hence thesis by A27;

                  end;

                  then

                   A28: ( meet Xsa) c= ( meet Xsc) by SETFAM_1: 6;

                  assume d in a;

                  hence thesis by A13, A22, A26, A28;

                end;

                hence a <= c by YELLOW_1: 3;

                b c= c

                proof

                  let d be object;

                  Xsc c= Xsb

                  proof

                    let r be object;

                    assume r in Xsc;

                    then

                     A29: ex xz be Element of BP st r = ( uparrow xz) & ex z st xz = {z} & z in Yab;

                    Yab c= Yb by A21, YELLOW_1: 2;

                    hence thesis by A29;

                  end;

                  then

                   A30: ( meet Xsb) c= ( meet Xsc) by SETFAM_1: 6;

                  assume d in b;

                  hence thesis by A11, A18, A26, A30;

                end;

                hence b <= c by YELLOW_1: 3;

              end;

            end;

          end;

        end;

        

         A31: h is infs-preserving by WAYBEL16:def 1;

        now

          let s be object;

          hereby

            assume s in (h .: Xs);

            then

            consider t be object such that t in the carrier of IP and

             A32: t in Xs and

             A33: s = (h . t) by FUNCT_2: 64;

            consider Y be Subset of X such that

             A34: t = ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Y },IP)) & Y in FF by A32;

            set Xsi = { ( uparrow x) : ex z st x = {z} & z in Y };

            Xsi c= cIP

            proof

              let r be object;

              assume r in Xsi;

              then ex xz be Element of BP st r = ( uparrow xz) & ex z be Element of X st xz = {z} & z in Y;

              hence thesis by A2;

            end;

            then

            reconsider Xsi as Subset of IP;

            set Xsif = { (f . ( uparrow x)) : ex z st x = {z} & z in Y };

            now

              let u be object;

              hereby

                assume u in (h .: Xsi);

                then

                consider v be object such that v in the carrier of IP and

                 A35: v in Xsi and

                 A36: u = (h . v) by FUNCT_2: 64;

                

                 A37: ex x st v = ( uparrow x) & ex z st x = {z} & z in Y by A35;

                then v in FUF;

                then (h . v) = (f . v) by A1, FUNCT_1: 49;

                hence u in Xsif by A36, A37;

              end;

              assume u in Xsif;

              then

              consider x such that

               A38: u = (f . ( uparrow x)) and

               A39: ex z st x = {z} & z in Y;

              ( uparrow x) in FUF by A39;

              then

               A40: (h . ( uparrow x)) = (f . ( uparrow x)) by A1, FUNCT_1: 49;

              ( uparrow x) in Xsi by A39;

              hence u in (h .: Xsi) by A38, A40, FUNCT_2: 35;

            end;

            then

             A41: (h .: Xsi) = Xsif by TARSKI: 2;

            h preserves_inf_of Xsi & ex_inf_of (Xsi,IP) by A31, YELLOW_0: 17;

            then ( inf (h .: Xsi)) = (h . ( inf Xsi));

            hence s in Xsf by A33, A34, A41;

          end;

          assume s in Xsf;

          then

          consider Y be Subset of X such that

           A42: s = ( "/\" ({ (f . ( uparrow x)) : ex z st x = {z} & z in Y },L)) and

           A43: Y in FF;

          set Xsi = { ( uparrow x) : ex z st x = {z} & z in Y };

          Xsi c= cIP

          proof

            let r be object;

            assume r in Xsi;

            then ex xz be Element of BP st r = ( uparrow xz) & ex z be Element of X st xz = {z} & z in Y;

            hence thesis by A2;

          end;

          then

          reconsider Xsi as Subset of IP;

          set Xsif = { (f . ( uparrow x)) : ex z st x = {z} & z in Y };

          h preserves_inf_of Xsi & ex_inf_of (Xsi,IP) by A31, YELLOW_0: 17;

          then

           A44: ( inf (h .: Xsi)) = (h . ( inf Xsi));

          now

            let u be object;

            hereby

              assume u in (h .: Xsi);

              then

              consider v be object such that v in the carrier of IP and

               A45: v in Xsi and

               A46: u = (h . v) by FUNCT_2: 64;

              

               A47: ex x st v = ( uparrow x) & ex z st x = {z} & z in Y by A45;

              then v in FUF;

              then (h . v) = (f . v) by A1, FUNCT_1: 49;

              hence u in Xsif by A46, A47;

            end;

            assume u in Xsif;

            then

            consider x such that

             A48: u = (f . ( uparrow x)) and

             A49: ex z st x = {z} & z in Y;

            ( uparrow x) in FUF by A49;

            then

             A50: (h . ( uparrow x)) = (f . ( uparrow x)) by A1, FUNCT_1: 49;

            ( uparrow x) in Xsi by A49;

            hence u in (h .: Xsi) by A48, A50, FUNCT_2: 35;

          end;

          then

           A51: (h .: Xsi) = Xsif by TARSKI: 2;

          ( inf Xsi) in Xs by A43;

          hence s in (h .: Xs) by A42, A44, A51, FUNCT_2: 35;

        end;

        then

         A52: (h .: Xs) = Xsf by TARSKI: 2;

        

         A53: FF = ( "\/" ({ ( "/\" ({ ( uparrow x) : ex z st x = {z} & z in Y },IP)) where Y be Subset of X : Y in FF },IP)) by Th11;

        h is directed-sups-preserving by WAYBEL16:def 1;

        then h preserves_sup_of Xs by A8;

        

        hence (h9 . Fi) = ( sup (h .: Xs)) by A4, A53, A7

        .= (F9 . Fi) by A4, A52, Def3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: WAYBEL22:16

    

     Th16: ( FixedUltraFilters X) is_FreeGen_set_of ( InclPoset ( Filt ( BoolePoset X)))

    proof

      set FUF = ( FixedUltraFilters X);

      set IP = ( InclPoset ( Filt ( BoolePoset X)));

      let L be continuous complete non empty Poset;

      let f be Function of FUF, the carrier of L;

      reconsider F = (f -extension_to_hom ) as CLHomomorphism of IP, L by WAYBEL16:def 1;

      take F;

      thus (F | FUF) = f by Th14;

      let h9 be CLHomomorphism of IP, L;

      assume (h9 | FUF) = f;

      hence thesis by Th15;

    end;

    theorem :: WAYBEL22:17

    

     Th17: for L,M be continuous complete LATTICE, F,G be set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & ( card F) = ( card G) holds (L,M) are_isomorphic

    proof

      let L,M be continuous complete LATTICE, Lg,Mg be set such that

       A1: Lg is_FreeGen_set_of L and

       A2: Mg is_FreeGen_set_of M and

       A3: ( card Lg) = ( card Mg);

      (Lg,Mg) are_equipotent by A3, CARD_1: 5;

      then

      consider f be Function such that

       A4: f is one-to-one and

       A5: ( dom f) = Lg and

       A6: ( rng f) = Mg;

      set g = (f " );

      

       A7: ( dom g) = Mg by A4, A6, FUNCT_1: 33;

      reconsider Mg as Subset of M by A2, Th7;

      

       A8: ( rng g) = Lg by A4, A5, FUNCT_1: 33;

      reconsider Lg as Subset of L by A1, Th7;

      Mg c= the carrier of M;

      then

      reconsider f as Function of Lg, the carrier of M by A5, A6, FUNCT_2:def 1, RELSET_1: 4;

      consider F be CLHomomorphism of L, M such that

       A9: (F | Lg) = f and for h9 be CLHomomorphism of L, M st (h9 | Lg) = f holds h9 = F by A1;

      Lg c= the carrier of L;

      then

      reconsider g as Function of Mg, the carrier of L by A7, A8, FUNCT_2:def 1, RELSET_1: 4;

      consider G be CLHomomorphism of M, L such that

       A10: (G | Mg) = g and for h9 be CLHomomorphism of M, L st (h9 | Mg) = g holds h9 = G by A2;

      reconsider GF = (G * F) as CLHomomorphism of L, L by Th2;

      (GF | Lg) = (G * f) by A9, RELAT_1: 83

      .= (g * f) by A6, A10, FUNCT_4: 2

      .= ( id Lg) by A4, A5, FUNCT_1: 39;

      then

       A11: GF = ( id L) by A1, Th8;

      then

       A12: F is one-to-one by FUNCT_2: 23;

      reconsider FG = (F * G) as CLHomomorphism of M, M by Th2;

      F is directed-sups-preserving by WAYBEL16:def 1;

      then

       A13: F is monotone by WAYBEL17: 3;

      G is directed-sups-preserving by WAYBEL16:def 1;

      then

       A14: G is monotone by WAYBEL17: 3;

      (FG | Mg) = (F * g) by A10, RELAT_1: 83

      .= (f * g) by A8, A9, FUNCT_4: 2

      .= ( id Mg) by A4, A6, FUNCT_1: 39;

      then FG = ( id M) by A2, Th8;

      then F is onto by FUNCT_2: 23;

      then ( rng F) = the carrier of M by FUNCT_2:def 3;

      then G = (F qua Function " ) by A11, A12, FUNCT_2: 30;

      then F is isomorphic by A12, A13, A14, WAYBEL_0:def 38;

      hence thesis by WAYBEL_1:def 8;

    end;

    ::$Notion-Name

    theorem :: WAYBEL22:18

    for L be continuous complete LATTICE, G be set st G is_FreeGen_set_of L & ( card G) = ( card X) holds (L,( InclPoset ( Filt ( BoolePoset X)))) are_isomorphic

    proof

      

       A1: ( FixedUltraFilters X) is_FreeGen_set_of ( InclPoset ( Filt ( BoolePoset X))) & ( card X) = ( card ( FixedUltraFilters X)) by Th10, Th16;

      let L be continuous complete LATTICE, G be set;

      assume G is_FreeGen_set_of L & ( card G) = ( card X);

      hence thesis by A1, Th17;

    end;