waybel15.miz



    begin

    theorem :: WAYBEL15:1

    

     Th1: for R be RelStr holds for S be full SubRelStr of R holds for T be full SubRelStr of S holds T is full SubRelStr of R

    proof

      let R be RelStr;

      let S be full SubRelStr of R;

      let T be full SubRelStr of S;

      reconsider T1 = T as SubRelStr of R by YELLOW_6: 7;

      

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

      the InternalRel of S = (the InternalRel of R |_2 the carrier of S) by YELLOW_0:def 14;

      

      then the InternalRel of T = ((the InternalRel of R |_2 the carrier of S) |_2 the carrier of T) by YELLOW_0:def 14

      .= (the InternalRel of R |_2 the carrier of T) by A1, WELLORD1: 22;

      then T1 is full by YELLOW_0:def 14;

      hence thesis;

    end;

    

     Lm1: for X be set, Y,Z be non empty set holds for f be Function of X, Y holds for g be Function of Y, Z holds f is onto & g is onto implies (g * f) is onto by FUNCT_2: 27;

    theorem :: WAYBEL15:2

    for X be set holds for a be Element of ( BoolePoset X) holds ( uparrow a) = { Y where Y be Subset of X : a c= Y }

    proof

      let X be set;

      let a be Element of ( BoolePoset X);

      

       A1: { Y where Y be Subset of X : a c= Y } c= ( uparrow a)

      proof

        let x be object;

        assume x in { Y where Y be Subset of X : a c= Y };

        then

        consider x9 be Subset of X such that

         A2: x9 = x and

         A3: a c= x9;

        reconsider x9 as Element of ( BoolePoset X) by WAYBEL_8: 26;

        a <= x9 by A3, YELLOW_1: 2;

        hence thesis by A2, WAYBEL_0: 18;

      end;

      ( uparrow a) c= { Y where Y be Subset of X : a c= Y }

      proof

        let x be object;

        assume

         A4: x in ( uparrow a);

        then

        reconsider x9 = x as Element of ( BoolePoset X);

        a <= x9 by A4, WAYBEL_0: 18;

        then x9 is Subset of X & a c= x9 by WAYBEL_8: 26, YELLOW_1: 2;

        hence thesis;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL15:3

    for L be upper-bounded non empty antisymmetric RelStr holds for a be Element of L holds ( Top L) <= a implies a = ( Top L)

    proof

      let L be upper-bounded non empty antisymmetric RelStr;

      let a be Element of L;

      

       A1: a <= ( Top L) by YELLOW_0: 45;

      assume ( Top L) <= a;

      hence thesis by A1, YELLOW_0:def 3;

    end;

    theorem :: WAYBEL15:4

    

     Th4: for S,T be non empty Poset holds for g be Function of S, T holds for d be Function of T, S holds g is onto & [g, d] is Galois implies (T,( Image d)) are_isomorphic

    proof

      let S,T be non empty Poset;

      let g be Function of S, T;

      let d be Function of T, S;

      assume that

       A1: g is onto and

       A2: [g, d] is Galois;

      d is one-to-one by A1, A2, WAYBEL_1: 24;

      then

       A3: (the carrier of ( Image d) |` d) is one-to-one by FUNCT_1: 58;

      

       A4: d is monotone by A2, WAYBEL_1: 8;

       A5:

      now

        let x,y be Element of T;

        thus x <= y implies (( corestr d) . x) <= (( corestr d) . y) by A4, WAYBEL_1:def 2;

        thus (( corestr d) . x) <= (( corestr d) . y) implies x <= y

        proof

          for t be Element of T holds (d . t) is_minimum_of (g " {t}) by A1, A2, WAYBEL_1: 22;

          then

           A6: (g * d) = ( id T) by WAYBEL_1: 23;

          assume

           A7: (( corestr d) . x) <= (( corestr d) . y);

          y in the carrier of T;

          then

           A8: y in ( dom d) by FUNCT_2:def 1;

          

           A9: g is monotone by A2, WAYBEL_1: 8;

          (d . x) = (( corestr d) . x) & (d . y) = (( corestr d) . y) by WAYBEL_1: 30;

          then (d . x) <= (d . y) by A7, YELLOW_0: 59;

          then

           A10: (g . (d . x)) <= (g . (d . y)) by A9;

          x in the carrier of T;

          then x in ( dom d) by FUNCT_2:def 1;

          then ((g * d) . x) <= (g . (d . y)) by A10, FUNCT_1: 13;

          then ((g * d) . x) <= ((g * d) . y) by A8, FUNCT_1: 13;

          then (( id T) . x) <= y by A6;

          hence thesis;

        end;

      end;

      ( rng ( corestr d)) = the carrier of ( Image d) by FUNCT_2:def 3;

      then ( corestr d) is isomorphic by A3, A5, WAYBEL_0: 66;

      hence thesis;

    end;

    theorem :: WAYBEL15:5

    

     Th5: for L1,L2,L3 be non empty Poset holds for g1 be Function of L1, L2 holds for g2 be Function of L2, L3 holds for d1 be Function of L2, L1 holds for d2 be Function of L3, L2 st [g1, d1] is Galois & [g2, d2] is Galois holds [(g2 * g1), (d1 * d2)] is Galois

    proof

      let L1,L2,L3 be non empty Poset;

      let g1 be Function of L1, L2;

      let g2 be Function of L2, L3;

      let d1 be Function of L2, L1;

      let d2 be Function of L3, L2;

      assume that

       A1: [g1, d1] is Galois and

       A2: [g2, d2] is Galois;

      

       A3: d1 is monotone by A1, WAYBEL_1: 8;

      

       A4: g2 is monotone by A2, WAYBEL_1: 8;

       A5:

      now

        let s be Element of L3, t be Element of L1;

        s in the carrier of L3;

        then

         A6: s in ( dom d2) by FUNCT_2:def 1;

        t in the carrier of L1;

        then

         A7: t in ( dom g1) by FUNCT_2:def 1;

        thus s <= ((g2 * g1) . t) implies ((d1 * d2) . s) <= t

        proof

          assume s <= ((g2 * g1) . t);

          then s <= (g2 . (g1 . t)) by A7, FUNCT_1: 13;

          then (d2 . s) <= (g1 . t) by A2, WAYBEL_1: 8;

          then (d1 . (d2 . s)) <= (d1 . (g1 . t)) by A3;

          then

           A8: (d1 . (d2 . s)) <= ((d1 * g1) . t) by A7, FUNCT_1: 13;

          (d1 * g1) <= ( id L1) by A1, WAYBEL_1: 18;

          then ((d1 * g1) . t) <= (( id L1) . t) by YELLOW_2: 9;

          then (d1 . (d2 . s)) <= (( id L1) . t) by A8, ORDERS_2: 3;

          then (d1 . (d2 . s)) <= t;

          hence thesis by A6, FUNCT_1: 13;

        end;

        thus ((d1 * d2) . s) <= t implies s <= ((g2 * g1) . t)

        proof

          assume ((d1 * d2) . s) <= t;

          then (d1 . (d2 . s)) <= t by A6, FUNCT_1: 13;

          then (d2 . s) <= (g1 . t) by A1, WAYBEL_1: 8;

          then (g2 . (d2 . s)) <= (g2 . (g1 . t)) by A4;

          then

           A9: ((g2 * d2) . s) <= (g2 . (g1 . t)) by A6, FUNCT_1: 13;

          ( id L3) <= (g2 * d2) by A2, WAYBEL_1: 18;

          then (( id L3) . s) <= ((g2 * d2) . s) by YELLOW_2: 9;

          then (( id L3) . s) <= (g2 . (g1 . t)) by A9, ORDERS_2: 3;

          then s <= (g2 . (g1 . t));

          hence thesis by A7, FUNCT_1: 13;

        end;

      end;

      d2 is monotone by A2, WAYBEL_1: 8;

      then

       A10: (d1 * d2) is monotone by A3, YELLOW_2: 12;

      g1 is monotone by A1, WAYBEL_1: 8;

      then (g2 * g1) is monotone by A4, YELLOW_2: 12;

      hence thesis by A10, A5;

    end;

    theorem :: WAYBEL15:6

    

     Th6: for L1,L2 be non empty Poset holds for f be Function of L1, L2 holds for f1 be Function of L2, L1 st f1 = (f qua Function " ) & f is isomorphic holds [f, f1] is Galois & [f1, f] is Galois

    proof

      let L1,L2 be non empty Poset;

      let f be Function of L1, L2;

      let f1 be Function of L2, L1;

      assume that

       A1: f1 = (f qua Function " ) and

       A2: f is isomorphic;

      

       A3: f1 is isomorphic by A1, A2, WAYBEL_0: 68;

      now

        let t be Element of L2, s be Element of L1;

        s in the carrier of L1;

        then

         A4: s in ( dom f) by FUNCT_2:def 1;

        

         A5: (f1 * f) = ( id ( dom f)) by A1, A2, FUNCT_1: 39

        .= ( id L1) by FUNCT_2:def 1;

        thus t <= (f . s) implies (f1 . t) <= s

        proof

          assume t <= (f . s);

          then (f1 . t) <= (f1 . (f . s)) by A3, WAYBEL_1:def 2;

          then (f1 . t) <= ((f1 * f) . s) by A4, FUNCT_1: 13;

          hence thesis by A5;

        end;

        t in the carrier of L2;

        then

         A6: t in ( dom f1) by FUNCT_2:def 1;

        

         A7: (f * f1) = ( id ( rng f)) by A1, A2, FUNCT_1: 39

        .= ( id L2) by A2, WAYBEL_0: 66;

        thus (f1 . t) <= s implies t <= (f . s)

        proof

          assume (f1 . t) <= s;

          then (f . (f1 . t)) <= (f . s) by A2, WAYBEL_1:def 2;

          then ((f * f1) . t) <= (f . s) by A6, FUNCT_1: 13;

          hence thesis by A7;

        end;

      end;

      hence [f, f1] is Galois by A2, A3;

      now

        let t be Element of L1, s be Element of L2;

        s in the carrier of L2;

        then

         A8: s in ( dom f1) by FUNCT_2:def 1;

        

         A9: (f * f1) = ( id ( rng f)) by A1, A2, FUNCT_1: 39

        .= ( id L2) by A2, WAYBEL_0: 66;

        thus t <= (f1 . s) implies (f . t) <= s

        proof

          assume t <= (f1 . s);

          then (f . t) <= (f . (f1 . s)) by A2, WAYBEL_1:def 2;

          then (f . t) <= ((f * f1) . s) by A8, FUNCT_1: 13;

          hence thesis by A9;

        end;

        t in the carrier of L1;

        then

         A10: t in ( dom f) by FUNCT_2:def 1;

        

         A11: (f1 * f) = ( id ( dom f)) by A1, A2, FUNCT_1: 39

        .= ( id L1) by FUNCT_2:def 1;

        thus (f . t) <= s implies t <= (f1 . s)

        proof

          assume (f . t) <= s;

          then (f1 . (f . t)) <= (f1 . s) by A3, WAYBEL_1:def 2;

          then ((f1 * f) . t) <= (f1 . s) by A10, FUNCT_1: 13;

          hence thesis by A11;

        end;

      end;

      hence thesis by A2, A3;

    end;

    theorem :: WAYBEL15:7

    

     Th7: for X be set holds ( BoolePoset X) is arithmetic

    proof

      let X be set;

      now

        let x,y be Element of ( CompactSublatt ( BoolePoset X));

        reconsider x9 = x, y9 = y as Element of ( BoolePoset X) by YELLOW_0: 58;

        x9 is compact by WAYBEL_8:def 1;

        then x9 is finite by WAYBEL_8: 28;

        then (x9 /\ y9) is finite;

        then (x9 "/\" y9) is finite by YELLOW_1: 17;

        then (x9 "/\" y9) is compact by WAYBEL_8: 28;

        then

        reconsider xy = (x9 "/\" y9) as Element of ( CompactSublatt ( BoolePoset X)) by WAYBEL_8:def 1;

         A1:

        now

          let z be Element of ( CompactSublatt ( BoolePoset X));

          reconsider z9 = z as Element of ( BoolePoset X) by YELLOW_0: 58;

          assume that

           A2: z <= x and

           A3: z <= y;

          z9 <= y9 by A3, YELLOW_0: 59;

          then

           A4: z9 c= y9 by YELLOW_1: 2;

          z9 <= x9 by A2, YELLOW_0: 59;

          then z9 c= x9 by YELLOW_1: 2;

          then z9 c= (x9 /\ y9) by A4, XBOOLE_1: 19;

          then z9 c= (x9 "/\" y9) by YELLOW_1: 17;

          then z9 <= (x9 "/\" y9) by YELLOW_1: 2;

          hence xy >= z by YELLOW_0: 60;

        end;

        (x9 /\ y9) c= y9 by XBOOLE_1: 17;

        then (x9 "/\" y9) c= y9 by YELLOW_1: 17;

        then (x9 "/\" y9) <= y9 by YELLOW_1: 2;

        then

         A5: xy <= y by YELLOW_0: 60;

        (x9 /\ y9) c= x9 by XBOOLE_1: 17;

        then (x9 "/\" y9) c= x9 by YELLOW_1: 17;

        then (x9 "/\" y9) <= x9 by YELLOW_1: 2;

        then xy <= x by YELLOW_0: 60;

        hence ex_inf_of ( {x, y},( CompactSublatt ( BoolePoset X))) by A5, A1, YELLOW_0: 19;

      end;

      then ( CompactSublatt ( BoolePoset X)) is with_infima by YELLOW_0: 21;

      hence thesis by WAYBEL_8: 19;

    end;

    registration

      let X be set;

      cluster ( BoolePoset X) -> arithmetic;

      coherence by Th7;

    end

    theorem :: WAYBEL15:8

    

     Th8: for L1,L2 be up-complete non empty Poset holds for f be Function of L1, L2 st f is isomorphic holds for x be Element of L1 holds (f .: ( waybelow x)) = ( waybelow (f . x))

    proof

      let L1,L2 be up-complete non empty Poset;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      then

      reconsider g = (f qua Function " ) as Function of L2, L1 by WAYBEL_0: 67;

      let x be Element of L1;

      

       A2: ( waybelow (f . x)) c= (f .: ( waybelow x))

      proof

        let z be object;

        assume z in ( waybelow (f . x));

        then z in { y where y be Element of L2 : y << (f . x) } by WAYBEL_3:def 3;

        then

        consider z1 be Element of L2 such that

         A3: z1 = z and

         A4: z1 << (f . x);

        (g . z1) in the carrier of L1;

        then

         A5: (g . z1) in ( dom f) by FUNCT_2:def 1;

        z1 in the carrier of L2;

        then z1 in ( dom g) by FUNCT_2:def 1;

        then z1 in ( rng f) by A1, FUNCT_1: 33;

        then

         A6: z1 = (f . (g . z1)) by A1, FUNCT_1: 35;

        then (g . z1) << x by A1, A4, WAYBEL13: 27;

        then (g . z1) in ( waybelow x) by WAYBEL_3: 7;

        hence thesis by A3, A5, A6, FUNCT_1:def 6;

      end;

      (f .: ( waybelow x)) c= ( waybelow (f . x))

      proof

        let z be object;

        assume z in (f .: ( waybelow x));

        then

        consider v be object such that v in ( dom f) and

         A7: v in ( waybelow x) and

         A8: z = (f . v) by FUNCT_1:def 6;

        v in { y where y be Element of L1 : y << x } by A7, WAYBEL_3:def 3;

        then

        consider v1 be Element of L1 such that

         A9: v1 = v and

         A10: v1 << x;

        (f . v1) << (f . x) by A1, A10, WAYBEL13: 27;

        hence thesis by A8, A9, WAYBEL_3: 7;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL15:9

    

     Th9: for L1,L2 be non empty Poset st (L1,L2) are_isomorphic & L1 is continuous holds L2 is continuous

    proof

      let L1,L2 be non empty Poset;

      assume that

       A1: (L1,L2) are_isomorphic and

       A2: L1 is continuous;

      consider f be Function of L1, L2 such that

       A3: f is isomorphic by A1;

      reconsider g = (f qua Function " ) as Function of L2, L1 by A3, WAYBEL_0: 67;

      

       A4: L1 is up-complete non empty Poset & L2 is up-complete non empty Poset by A1, A2, WAYBEL13: 30;

      now

        let y be Element of L2;

        

         A5: ex_sup_of (( waybelow (g . y)),L1) by A2, WAYBEL_0: 75;

        f is sups-preserving by A3, WAYBEL13: 20;

        then

         A6: f preserves_sup_of ( waybelow (g . y)) by WAYBEL_0:def 33;

        y in the carrier of L2;

        then

         A7: y in ( rng f) by A3, WAYBEL_0: 66;

        

        hence y = (f . (g . y)) by A3, FUNCT_1: 35

        .= (f . ( sup ( waybelow (g . y)))) by A2, WAYBEL_3:def 5

        .= ( sup (f .: ( waybelow (g . y)))) by A6, A5, WAYBEL_0:def 31

        .= ( sup ( waybelow (f . (g . y)))) by A3, A4, Th8

        .= ( sup ( waybelow y)) by A3, A7, FUNCT_1: 35;

      end;

      then

       A8: L2 is satisfying_axiom_of_approximation by WAYBEL_3:def 5;

      

       A9: g is isomorphic by A3, WAYBEL_0: 68;

       A10:

      now

        let y be Element of L2;

        for Y be finite Subset of ( waybelow y) holds ex z be Element of L2 st z in ( waybelow y) & z is_>=_than Y

        proof

          let Y be finite Subset of ( waybelow y);

          Y c= the carrier of L2 by XBOOLE_1: 1;

          then

           A11: Y c= ( rng f) by A3, WAYBEL_0: 66;

          now

            let u be object;

            assume u in (g .: Y);

            then

            consider v be object such that v in ( dom g) and

             A12: v in Y and

             A13: u = (g . v) by FUNCT_1:def 6;

            v in ( waybelow y) by A12;

            then v in { k where k be Element of L2 : k << y } by WAYBEL_3:def 3;

            then

            consider v1 be Element of L2 such that

             A14: v1 = v and

             A15: v1 << y;

            (g . v1) << (g . y) by A9, A4, A15, WAYBEL13: 27;

            hence u in ( waybelow (g . y)) by A13, A14, WAYBEL_3: 7;

          end;

          then

          reconsider X = (g .: Y) as finite Subset of ( waybelow (g . y)) by TARSKI:def 3;

          consider x be Element of L1 such that

           A16: x in ( waybelow (g . y)) and

           A17: x is_>=_than X by A2, WAYBEL_0: 1;

          y in the carrier of L2;

          then y in ( rng f) by A3, WAYBEL_0: 66;

          then

           A18: (f . (g . y)) = y by A3, FUNCT_1: 35;

          take z = (f . x);

          x << (g . y) by A16, WAYBEL_3: 7;

          then z << y by A3, A4, A18, WAYBEL13: 27;

          hence z in ( waybelow y) by WAYBEL_3: 7;

          (f .: X) = (f .: (f " Y)) by A3, FUNCT_1: 85

          .= Y by A11, FUNCT_1: 77;

          hence thesis by A3, A17, WAYBEL13: 19;

        end;

        hence ( waybelow y) is non empty directed by WAYBEL_0: 1;

      end;

      L2 is up-complete by A1, A2, WAYBEL13: 30;

      hence thesis by A8, A10, WAYBEL_3:def 6;

    end;

    theorem :: WAYBEL15:10

    

     Th10: for L1,L2 be LATTICE st (L1,L2) are_isomorphic & L1 is lower-bounded arithmetic holds L2 is arithmetic

    proof

      let L1,L2 be LATTICE;

      assume that

       A1: (L1,L2) are_isomorphic and

       A2: L1 is lower-bounded arithmetic;

      consider f be Function of L1, L2 such that

       A3: f is isomorphic by A1;

      reconsider g = (f qua Function " ) as Function of L2, L1 by A3, WAYBEL_0: 67;

      

       A4: g is isomorphic by A3, WAYBEL_0: 68;

      

       A5: L2 is up-complete LATTICE by A1, A2, WAYBEL13: 30;

      now

        let x2,y2 be Element of L2;

        assume that

         A6: x2 in the carrier of ( CompactSublatt L2) and

         A7: y2 in the carrier of ( CompactSublatt L2) and

         A8: ex_inf_of ( {x2, y2},L2);

        x2 is compact by A6, WAYBEL_8:def 1;

        then (g . x2) is compact by A2, A4, A5, WAYBEL13: 28;

        then

         A9: (g . x2) in the carrier of ( CompactSublatt L1) by WAYBEL_8:def 1;

        y2 is compact by A7, WAYBEL_8:def 1;

        then (g . y2) is compact by A2, A4, A5, WAYBEL13: 28;

        then

         A10: (g . y2) in the carrier of ( CompactSublatt L1) by WAYBEL_8:def 1;

        x2 in the carrier of L2;

        then

         A11: x2 in ( dom g) by FUNCT_2:def 1;

        

         A12: ( CompactSublatt L1) is meet-inheriting by A2, WAYBEL_8:def 5;

        y2 in the carrier of L2;

        then

         A13: y2 in ( dom g) by FUNCT_2:def 1;

        g is infs-preserving by A4, WAYBEL13: 20;

        then

         A14: g preserves_inf_of {x2, y2} by WAYBEL_0:def 32;

        then ex_inf_of ((g .: {x2, y2}),L1) by A8, WAYBEL_0:def 30;

        then ex_inf_of ( {(g . x2), (g . y2)},L1) by A11, A13, FUNCT_1: 60;

        then ( inf {(g . x2), (g . y2)}) in the carrier of ( CompactSublatt L1) by A9, A10, A12, YELLOW_0:def 16;

        then

         A15: ( inf {(g . x2), (g . y2)}) is compact by WAYBEL_8:def 1;

        (g . ( inf {x2, y2})) = ( inf (g .: {x2, y2})) by A8, A14, WAYBEL_0:def 30

        .= ( inf {(g . x2), (g . y2)}) by A11, A13, FUNCT_1: 60;

        then ( inf {x2, y2}) is compact by A2, A4, A5, A15, WAYBEL13: 28;

        hence ( inf {x2, y2}) in the carrier of ( CompactSublatt L2) by WAYBEL_8:def 1;

      end;

      then

       A16: ( CompactSublatt L2) is meet-inheriting by YELLOW_0:def 16;

      L2 is algebraic by A1, A2, WAYBEL13: 32;

      hence thesis by A16, WAYBEL_8:def 5;

    end;

    

     Lm2: for L be lower-bounded LATTICE holds L is continuous implies ex A be arithmetic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving

    proof

      let L be lower-bounded LATTICE;

      assume

       A1: L is continuous;

      reconsider A = ( InclPoset ( Ids L)) as arithmetic lower-bounded LATTICE by WAYBEL13: 14;

      take A;

      reconsider g = ( SupMap L) as Function of A, L;

      take g;

      the carrier of L c= ( rng g)

      proof

        let y be object;

        assume y in the carrier of L;

        then

        reconsider y9 = y as Element of L;

        ( downarrow y9) is Element of A by YELLOW_2: 41;

        then ( downarrow y9) in the carrier of A;

        then

         A2: ( downarrow y9) in ( dom g) by FUNCT_2:def 1;

        (g . ( downarrow y9)) = ( sup ( downarrow y9)) by YELLOW_2:def 3

        .= y9 by WAYBEL_0: 34;

        hence thesis by A2, FUNCT_1:def 3;

      end;

      then ( rng g) = the carrier of L by XBOOLE_0:def 10;

      hence g is onto by FUNCT_2:def 3;

      thus g is infs-preserving by A1, WAYBEL13: 33;

      g is sups-preserving by A1, WAYBEL13: 33;

      hence thesis;

    end;

    theorem :: WAYBEL15:11

    

     Th11: for L1,L2,L3 be non empty Poset holds for f be Function of L1, L2 holds for g be Function of L2, L3 st f is directed-sups-preserving & g is directed-sups-preserving holds (g * f) is directed-sups-preserving

    proof

      let L1,L2,L3 be non empty Poset;

      let f be Function of L1, L2;

      let g be Function of L2, L3;

      assume that

       A1: f is directed-sups-preserving and

       A2: g is directed-sups-preserving;

      now

        let X be Subset of L1;

        assume

         A3: X is non empty directed;

        for X1 be Ideal of L1 holds f preserves_sup_of X1 by A1, WAYBEL_0:def 37;

        then

         A4: (f .: X) is non empty directed by A3, WAYBEL_0: 72, YELLOW_2: 15;

        now

          ( sup X) in the carrier of L1;

          then

           A5: ( sup X) in ( dom f) by FUNCT_2:def 1;

          assume

           A6: ex_sup_of (X,L1);

          

           A7: f preserves_sup_of X by A1, A3, WAYBEL_0:def 37;

          then

           A8: ex_sup_of ((f .: X),L2) by A6, WAYBEL_0:def 31;

          

           A9: g preserves_sup_of (f .: X) by A2, A4, WAYBEL_0:def 37;

          then

           A10: ( sup (g .: (f .: X))) = (g . ( sup (f .: X))) by A8, WAYBEL_0:def 31;

           ex_sup_of ((g .: (f .: X)),L3) by A8, A9, WAYBEL_0:def 31;

          hence ex_sup_of (((g * f) .: X),L3) by RELAT_1: 126;

          ( sup (f .: X)) = (f . ( sup X)) by A6, A7, WAYBEL_0:def 31;

          

          hence ( sup ((g * f) .: X)) = (g . (f . ( sup X))) by A10, RELAT_1: 126

          .= ((g * f) . ( sup X)) by A5, FUNCT_1: 13;

        end;

        hence (g * f) preserves_sup_of X by WAYBEL_0:def 31;

      end;

      hence thesis by WAYBEL_0:def 37;

    end;

    begin

    theorem :: WAYBEL15:12

    for L1,L2 be non empty RelStr holds for f be Function of L1, L2 holds for X be Subset of ( Image f) holds (( inclusion f) .: X) = X by FUNCT_1: 92;

    theorem :: WAYBEL15:13

    

     Th13: for X be set holds for c be Function of ( BoolePoset X), ( BoolePoset X) st c is idempotent directed-sups-preserving holds ( inclusion c) is directed-sups-preserving

    proof

      let X be set;

      let c be Function of ( BoolePoset X), ( BoolePoset X);

      assume

       A1: c is idempotent directed-sups-preserving;

      now

        let Y be Ideal of ( Image c);

        now

          ( "\/" (Y,( BoolePoset X))) in the carrier of ( BoolePoset X);

          then ( "\/" (Y,( BoolePoset X))) in ( dom c) by FUNCT_2:def 1;

          then

           A2: (c . ( "\/" (Y,( BoolePoset X)))) in ( rng c) by FUNCT_1:def 3;

          Y c= the carrier of ( Image c);

          then

           A3: Y c= ( rng c) by YELLOW_0:def 15;

          reconsider Y9 = Y as non empty directed Subset of ( BoolePoset X) by YELLOW_2: 7;

          assume ex_sup_of (Y,( Image c));

          

           A4: ex_sup_of (Y,( BoolePoset X)) by YELLOW_0: 17;

          c preserves_sup_of Y9 by A1, WAYBEL_0:def 37;

          then ( "\/" ((c .: Y),( BoolePoset X))) in ( rng c) by A4, A2, WAYBEL_0:def 31;

          then ( "\/" (Y,( BoolePoset X))) in ( rng c) by A1, A3, YELLOW_2: 20;

          then

           A5: ( "\/" (Y,( BoolePoset X))) in the carrier of ( Image c) by YELLOW_0:def 15;

          thus ex_sup_of ((( inclusion c) .: Y),( BoolePoset X)) by YELLOW_0: 17;

          

          thus ( sup (( inclusion c) .: Y)) = ( "\/" (Y,( BoolePoset X))) by FUNCT_1: 92

          .= ( sup Y) by A4, A5, YELLOW_0: 64

          .= (( inclusion c) . ( sup Y));

        end;

        hence ( inclusion c) preserves_sup_of Y by WAYBEL_0:def 31;

      end;

      hence thesis by WAYBEL_0: 73;

    end;

    

     Lm3: for L be lower-bounded LATTICE holds (ex A be algebraic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving) implies ex X be non empty set, p be projection Function of ( BoolePoset X), ( BoolePoset X) st p is directed-sups-preserving & (L,( Image p)) are_isomorphic

    proof

      let L be lower-bounded LATTICE;

      given A be algebraic lower-bounded LATTICE, g be Function of A, L such that

       A1: g is onto and

       A2: g is infs-preserving and

       A3: g is directed-sups-preserving;

      g is upper_adjoint by A2, WAYBEL_1: 16;

      then

      consider d be Function of L, A such that

       A4: [g, d] is Galois;

      g is monotone & d is monotone by A4, WAYBEL_1: 8;

      then (d * g) is monotone by YELLOW_2: 12;

      then

      reconsider k = (d * g) as kernel Function of A, A by A4, WAYBEL_1: 41;

      d is lower_adjoint by A4;

      then

       A5: k is directed-sups-preserving by A3, Th11;

      consider X be non empty set, c be closure Function of ( BoolePoset X), ( BoolePoset X) such that

       A6: c is directed-sups-preserving and

       A7: (A,( Image c)) are_isomorphic by WAYBEL13: 35;

      consider f be Function of A, ( Image c) such that

       A8: f is isomorphic by A7;

      reconsider f1 = (f qua Function " ) as Function of ( Image c), A by A8, WAYBEL_0: 67;

      reconsider p = ((((( inclusion c) * f) * k) * f1) * ( corestr c)) as Function of ( BoolePoset X), ( BoolePoset X);

      

       A9: (f1 * f) = ( id ( dom f)) by A8, FUNCT_1: 39

      .= ( id A) by FUNCT_2:def 1;

      

       A10: f1 is isomorphic by A8, WAYBEL_0: 68;

      then ( rng f1) = the carrier of A by WAYBEL_0: 66;

      then f1 is onto by FUNCT_2:def 3;

      then

       A11: (g * f1) is onto by A1, Lm1;

      then ((g * f1) * ( corestr c)) is onto by Lm1;

      

      then

       A12: ( rng ((g * f1) * ( corestr c))) = the carrier of L by FUNCT_2:def 3

      .= ( dom ((( inclusion c) * f) * d)) by FUNCT_2:def 1;

      

       A13: f is sups-preserving by A8, WAYBEL13: 20;

      ( inclusion c) is directed-sups-preserving by A6, Th13;

      then (( inclusion c) * f) is directed-sups-preserving by A13, Th11;

      then

       A14: ((( inclusion c) * f) * k) is directed-sups-preserving by A5, Th11;

      take X;

      

       A15: ( dom (f * d)) = the carrier of L by FUNCT_2:def 1;

       A16:

      now

        let x be object;

        assume

         A17: x in the carrier of L;

        then ((f * d) . x) in the carrier of ( Image c) by FUNCT_2: 5;

        

        hence ((f * d) . x) = (( inclusion c) . ((f * d) . x)) by FUNCT_1: 18

        .= ((( inclusion c) * (f * d)) . x) by A15, A17, FUNCT_1: 13

        .= (((( inclusion c) * f) * d) . x) by RELAT_1: 36;

      end;

      

       A18: ((((( inclusion c) * f) * k) * (f1 * ( id ( Image c)))) * (f * (k * (f1 * ( corestr c))))) = ((((( inclusion c) * f) * k) * f1) * (f * (k * (f1 * ( corestr c))))) by FUNCT_2: 17

      .= (((((( inclusion c) * f) * k) * f1) * f) * (k * (f1 * ( corestr c)))) by RELAT_1: 36

      .= ((((( inclusion c) * f) * k) * ( id A)) * (k * (f1 * ( corestr c)))) by A9, RELAT_1: 36

      .= (((( inclusion c) * f) * k) * (k * (f1 * ( corestr c)))) by FUNCT_2: 17

      .= ((((( inclusion c) * f) * k) * k) * (f1 * ( corestr c))) by RELAT_1: 36

      .= (((( inclusion c) * f) * (k * k)) * (f1 * ( corestr c))) by RELAT_1: 36

      .= (((( inclusion c) * f) * k) * (f1 * ( corestr c))) by QUANTAL1:def 9

      .= p by RELAT_1: 36;

      (p * p) = (((((( inclusion c) * f) * k) * f1) * ( corestr c)) * (((( inclusion c) * f) * k) * (f1 * ( corestr c)))) by RELAT_1: 36

      .= (((((( inclusion c) * f) * k) * f1) * ( corestr c)) * ((( inclusion c) * f) * (k * (f1 * ( corestr c))))) by RELAT_1: 36

      .= (((((( inclusion c) * f) * k) * f1) * ( corestr c)) * (( inclusion c) * (f * (k * (f1 * ( corestr c)))))) by RELAT_1: 36

      .= ((((((( inclusion c) * f) * k) * f1) * ( corestr c)) * ( inclusion c)) * (f * (k * (f1 * ( corestr c))))) by RELAT_1: 36

      .= (((((( inclusion c) * f) * k) * f1) * (( corestr c) * ( inclusion c))) * (f * (k * (f1 * ( corestr c))))) by RELAT_1: 36

      .= (((((( inclusion c) * f) * k) * f1) * ( id ( Image c))) * (f * (k * (f1 * ( corestr c))))) by WAYBEL_1: 33

      .= p by A18, RELAT_1: 36;

      then

       A19: p is idempotent by QUANTAL1:def 9;

      (( inclusion c) * f) is monotone by A8, YELLOW_2: 12;

      then ((( inclusion c) * f) * k) is monotone by YELLOW_2: 12;

      then (((( inclusion c) * f) * k) * f1) is monotone by A10, YELLOW_2: 12;

      then p is monotone by YELLOW_2: 12;

      then

      reconsider p as projection Function of ( BoolePoset X), ( BoolePoset X) by A19, WAYBEL_1:def 13;

      take p;

      p = (((((( inclusion c) * f) * d) * g) * f1) * ( corestr c)) by RELAT_1: 36

      .= ((((( inclusion c) * f) * d) * g) * (f1 * ( corestr c))) by RELAT_1: 36

      .= (((( inclusion c) * f) * d) * (g * (f1 * ( corestr c)))) by RELAT_1: 36

      .= (((( inclusion c) * f) * d) * ((g * f1) * ( corestr c))) by RELAT_1: 36;

      then

       A20: ( rng ((( inclusion c) * f) * d)) = ( rng p) by A12, RELAT_1: 28;

      ( dom ((( inclusion c) * f) * d)) = the carrier of L by FUNCT_2:def 1;

      then ( rng (f * d)) = ( rng ((( inclusion c) * f) * d)) by A15, A16, FUNCT_1: 2;

      then

       A21: the carrier of ( subrelstr ( rng (f * d))) = ( rng ((( inclusion c) * f) * d)) by YELLOW_0:def 15;

       [f1, f] is Galois by A8, Th6;

      then [(g * f1), (f * d)] is Galois by A4, Th5;

      then

       A22: (L,( Image (f * d))) are_isomorphic by A11, Th4;

      f1 is sups-preserving by A10, WAYBEL13: 20;

      then ( corestr c) is sups-preserving & (((( inclusion c) * f) * k) * f1) is directed-sups-preserving by A14, Th11, WAYBEL_1: 55;

      hence p is directed-sups-preserving by Th11;

      ( subrelstr ( rng (f * d))) is full strict SubRelStr of ( BoolePoset X) by Th1;

      hence thesis by A22, A21, A20, YELLOW_0:def 15;

    end;

    theorem :: WAYBEL15:14

    

     Th14: for L be continuous complete LATTICE holds for p be kernel Function of L, L st p is directed-sups-preserving holds ( Image p) is continuous LATTICE

    proof

      let L be continuous complete LATTICE;

      let p be kernel Function of L, L such that

       A1: p is directed-sups-preserving;

      now

        let X be Subset of L;

        assume X is non empty directed;

        then

         A2: p preserves_sup_of X by A1, WAYBEL_0:def 37;

        

         A3: ( Image p) is sups-inheriting by WAYBEL_1: 53;

        now

          assume

           A4: ex_sup_of (X,L);

          ( Image p) is complete by WAYBEL_1: 54;

          hence ex_sup_of ((( corestr p) .: X),( Image p)) by YELLOW_0: 17;

          

           A5: (( corestr p) .: X) = (p .: X) by WAYBEL_1: 30;

           ex_sup_of ((p .: X),L) by YELLOW_0: 17;

          then ( "\/" ((( corestr p) .: X),L)) in the carrier of ( Image p) by A3, A5, YELLOW_0:def 19;

          

          hence ( sup (( corestr p) .: X)) = ( sup (p .: X)) by A5, YELLOW_0: 68

          .= (p . ( sup X)) by A2, A4, WAYBEL_0:def 31

          .= (( corestr p) . ( sup X)) by WAYBEL_1: 30;

        end;

        hence ( corestr p) preserves_sup_of X by WAYBEL_0:def 31;

      end;

      then ( corestr p) is directed-sups-preserving by WAYBEL_0:def 37;

      hence thesis by WAYBEL_1: 56, WAYBEL_5: 33;

    end;

    theorem :: WAYBEL15:15

    

     Th15: for L be continuous complete LATTICE holds for p be projection Function of L, L st p is directed-sups-preserving holds ( Image p) is continuous LATTICE

    proof

      let L be continuous complete LATTICE;

      let p be projection Function of L, L such that

       A1: p is directed-sups-preserving;

      reconsider Lk = { k where k be Element of L : (p . k) <= k } as non empty Subset of L by WAYBEL_1: 43;

      

       A2: ( subrelstr Lk) is infs-inheriting by WAYBEL_1: 50;

      reconsider pk = (p | Lk) as Function of ( subrelstr Lk), ( subrelstr Lk) by WAYBEL_1: 46;

      

       A3: pk is kernel by WAYBEL_1: 48;

      now

        let X be Subset of ( subrelstr Lk);

        reconsider X9 = X as Subset of L by WAYBEL13: 3;

        assume

         A4: X is non empty directed;

        then

        reconsider X9 as non empty directed Subset of L by YELLOW_2: 7;

        

         A5: p preserves_sup_of X9 by A1, WAYBEL_0:def 37;

        now

          X c= the carrier of ( subrelstr Lk);

          then X c= Lk by YELLOW_0:def 15;

          then

           A6: (pk .: X) = (p .: X) by RELAT_1: 129;

          assume ex_sup_of (X,( subrelstr Lk));

          ( subrelstr Lk) is infs-inheriting by WAYBEL_1: 50;

          then ( subrelstr Lk) is complete LATTICE by YELLOW_2: 30;

          hence ex_sup_of ((pk .: X),( subrelstr Lk)) by YELLOW_0: 17;

          

           A7: ex_sup_of (X,L) by YELLOW_0: 17;

          

           A8: ( subrelstr Lk) is directed-sups-inheriting by A1, WAYBEL_1: 52;

          then

           A9: ( dom pk) = the carrier of ( subrelstr Lk) & ( sup X9) = ( sup X) by A4, A7, FUNCT_2:def 1, WAYBEL_0: 7;

           ex_sup_of ((p .: X),L) & (pk .: X) is directed Subset of ( subrelstr Lk) by A3, A4, YELLOW_0: 17, YELLOW_2: 15;

          

          hence ( sup (pk .: X)) = ( sup (p .: X)) by A4, A8, A6, WAYBEL_0: 7

          .= (p . ( sup X9)) by A5, A7, WAYBEL_0:def 31

          .= (pk . ( sup X)) by A9, FUNCT_1: 47;

        end;

        hence pk preserves_sup_of X by WAYBEL_0:def 31;

      end;

      then

       A10: pk is directed-sups-preserving by WAYBEL_0:def 37;

      ( subrelstr Lk) is directed-sups-inheriting by A1, WAYBEL_1: 52;

      then

       A11: ( subrelstr Lk) is continuous LATTICE by A2, WAYBEL_5: 28;

      

       A12: the carrier of ( subrelstr ( rng p)) = ( rng p) by YELLOW_0:def 15

      .= ( rng pk) by WAYBEL_1: 44

      .= the carrier of ( subrelstr ( rng pk)) by YELLOW_0:def 15;

      ( subrelstr ( rng pk)) is full SubRelStr of L by Th1;

      then

       A13: ( Image p) = ( Image pk) by A12, YELLOW_0: 57;

      ( subrelstr Lk) is complete by A2, YELLOW_2: 30;

      hence thesis by A11, A3, A13, A10, Th14;

    end;

    

     Lm4: for L be LATTICE holds (ex X be set, p be projection Function of ( BoolePoset X), ( BoolePoset X) st p is directed-sups-preserving & (L,( Image p)) are_isomorphic ) implies L is continuous

    proof

      let L be LATTICE;

      given X be set, p be projection Function of ( BoolePoset X), ( BoolePoset X) such that

       A1: p is directed-sups-preserving and

       A2: (L,( Image p)) are_isomorphic ;

      ( Image p) is continuous by A1, Th15;

      hence thesis by A2, Th9, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL15:16

    for L be lower-bounded LATTICE holds L is continuous iff ex A be arithmetic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving

    proof

      let L be lower-bounded LATTICE;

      thus L is continuous implies ex A be arithmetic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving by Lm2;

      thus (ex A be arithmetic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving) implies L is continuous

      proof

        assume ex A be arithmetic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving;

        then ex X be non empty set, p be projection Function of ( BoolePoset X), ( BoolePoset X) st p is directed-sups-preserving & (L,( Image p)) are_isomorphic by Lm3;

        hence thesis by Lm4;

      end;

    end;

    theorem :: WAYBEL15:17

    for L be lower-bounded LATTICE holds L is continuous iff ex A be algebraic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving

    proof

      let L be lower-bounded LATTICE;

      thus L is continuous implies ex A be algebraic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving

      proof

        assume L is continuous;

        then ex A be arithmetic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving by Lm2;

        hence thesis;

      end;

      thus (ex A be algebraic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving) implies L is continuous

      proof

        assume ex A be algebraic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving;

        then ex X be non empty set, p be projection Function of ( BoolePoset X), ( BoolePoset X) st p is directed-sups-preserving & (L,( Image p)) are_isomorphic by Lm3;

        hence thesis by Lm4;

      end;

    end;

    theorem :: WAYBEL15:18

    for L be lower-bounded LATTICE holds (L is continuous implies ex X be non empty set, p be projection Function of ( BoolePoset X), ( BoolePoset X) st p is directed-sups-preserving & (L,( Image p)) are_isomorphic ) & ((ex X be set, p be projection Function of ( BoolePoset X), ( BoolePoset X) st p is directed-sups-preserving & (L,( Image p)) are_isomorphic ) implies L is continuous)

    proof

      let L be lower-bounded LATTICE;

      thus L is continuous implies ex X be non empty set, p be projection Function of ( BoolePoset X), ( BoolePoset X) st p is directed-sups-preserving & (L,( Image p)) are_isomorphic

      proof

        assume L is continuous;

        then ex A be arithmetic lower-bounded LATTICE, g be Function of A, L st g is onto & g is infs-preserving & g is directed-sups-preserving by Lm2;

        hence thesis by Lm3;

      end;

      thus thesis by Lm4;

    end;

    begin

    theorem :: WAYBEL15:19

    for L be non empty RelStr holds for x be Element of L holds x in ( PRIME (L opp )) iff x is co-prime

    proof

      let L be non empty RelStr;

      let x be Element of L;

      hereby

        assume x in ( PRIME (L opp ));

        then (x ~ ) in ( PRIME (L opp )) by LATTICE3:def 6;

        then (x ~ ) is prime by WAYBEL_6:def 7;

        hence x is co-prime by WAYBEL_6:def 8;

      end;

      assume x is co-prime;

      then (x ~ ) is prime by WAYBEL_6:def 8;

      then (x ~ ) in ( PRIME (L opp )) by WAYBEL_6:def 7;

      hence thesis by LATTICE3:def 6;

    end;

    definition

      let L be non empty RelStr;

      let a be Element of L;

      :: WAYBEL15:def1

      attr a is atom means ( Bottom L) < a & for b be Element of L st ( Bottom L) < b & b <= a holds b = a;

    end

    definition

      let L be non empty RelStr;

      :: WAYBEL15:def2

      func ATOM L -> Subset of L means

      : Def2: for x be Element of L holds x in it iff x is atom;

      existence

      proof

        defpred P[ Element of L] means $1 is atom;

        consider X be Subset of L such that

         A1: for x be Element of L holds x in X iff P[x] from SUBSET_1:sch 3;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let A1,A2 be Subset of L such that

         A2: for x be Element of L holds x in A1 iff x is atom and

         A3: for x be Element of L holds x in A2 iff x is atom;

        for x be object holds x in A1 iff x in A2 by A2, A3;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: WAYBEL15:20

    

     Th20: for L be Boolean LATTICE holds for a be Element of L holds a is atom iff a is co-prime & a <> ( Bottom L)

    proof

      let L be Boolean LATTICE;

      let a be Element of L;

      thus a is atom implies a is co-prime & a <> ( Bottom L)

      proof

        assume

         A1: a is atom;

        now

          let x,y be Element of L;

          assume that

           A2: a <= (x "\/" y) and

           A3: not a <= x;

          

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

          (a "/\" x) <> a by A3, YELLOW_0: 25;

          then not ( Bottom L) < (a "/\" x) by A1, A4;

          then

           A5: ( not ( Bottom L) <= (a "/\" x)) or not ( Bottom L) <> (a "/\" x) by ORDERS_2:def 6;

          a = (a "/\" (x "\/" y)) by A2, YELLOW_0: 25

          .= ((a "/\" x) "\/" (a "/\" y)) by WAYBEL_1:def 3

          .= (a "/\" y) by A5, WAYBEL_1: 3, YELLOW_0: 44;

          hence a <= y by YELLOW_0: 25;

        end;

        hence a is co-prime by WAYBEL14: 14;

        thus thesis by A1;

      end;

      assume that

       A6: a is co-prime and

       A7: a <> ( Bottom L);

       A8:

      now

        let b be Element of L;

        assume that

         A9: ( Bottom L) < b and

         A10: b <= a;

        consider c be Element of L such that

         A11: c is_a_complement_of b by WAYBEL_1:def 24;

        

         A12: (b "/\" c) = ( Bottom L) by A11;

        

         A13: not a <= c by A10, ORDERS_2: 3, A9, A12, YELLOW_0: 25;

        (b "\/" c) = ( Top L) by A11;

        then a <= (b "\/" c) by YELLOW_0: 45;

        then a <= b by A6, A13, WAYBEL14: 14;

        hence b = a by A10, ORDERS_2: 2;

      end;

      ( Bottom L) <= a by YELLOW_0: 44;

      then ( Bottom L) < a by A7, ORDERS_2:def 6;

      hence thesis by A8;

    end;

    registration

      let L be Boolean LATTICE;

      cluster atom -> co-prime for Element of L;

      coherence by Th20;

    end

    theorem :: WAYBEL15:21

    for L be Boolean LATTICE holds ( ATOM L) = (( PRIME (L opp )) \ {( Bottom L)})

    proof

      let L be Boolean LATTICE;

      

       A1: (( PRIME (L opp )) \ {( Bottom L)}) c= ( ATOM L)

      proof

        let x be object;

        assume

         A2: x in (( PRIME (L opp )) \ {( Bottom L)});

        then

        reconsider x9 = x as Element of (L opp );

        x in ( PRIME (L opp )) by A2, XBOOLE_0:def 5;

        then

         A3: x9 is prime by WAYBEL_6:def 7;

         not x in {( Bottom L)} by A2, XBOOLE_0:def 5;

        then x9 <> ( Bottom L) by TARSKI:def 1;

        then

         A4: ( ~ x9) <> ( Bottom L) by LATTICE3:def 7;

        (( ~ x9) ~ ) = ( ~ x9) by LATTICE3:def 6

        .= x9 by LATTICE3:def 7;

        then ( ~ x9) is co-prime by A3, WAYBEL_6:def 8;

        then ( ~ x9) is atom by A4, Th20;

        then ( ~ x9) in ( ATOM L) by Def2;

        hence thesis by LATTICE3:def 7;

      end;

      ( ATOM L) c= (( PRIME (L opp )) \ {( Bottom L)})

      proof

        let x be object;

        assume

         A5: x in ( ATOM L);

        then

        reconsider x9 = x as Element of L;

        

         A6: x9 is atom by A5, Def2;

        then (x9 ~ ) is prime by WAYBEL_6:def 8;

        then (x9 ~ ) in ( PRIME (L opp )) by WAYBEL_6:def 7;

        then

         A7: x in ( PRIME (L opp )) by LATTICE3:def 6;

        x <> ( Bottom L) by A6;

        then not x in {( Bottom L)} by TARSKI:def 1;

        hence thesis by A7, XBOOLE_0:def 5;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL15:22

    for L be Boolean LATTICE holds for x,a be Element of L st a is atom holds a <= x iff not a <= ( 'not' x)

    proof

      let L be Boolean LATTICE;

      let x,a be Element of L;

      assume

       A1: a is atom;

      thus a <= x implies not a <= ( 'not' x)

      proof

        assume that

         A2: a <= x and

         A3: a <= ( 'not' x);

        a = (a "\/" ( Bottom L)) by WAYBEL_1: 3

        .= (a "\/" (x "/\" ( 'not' x))) by YELLOW_5: 34

        .= ((a "\/" x) "/\" (( 'not' x) "\/" a)) by WAYBEL_1: 5

        .= (x "/\" (( 'not' x) "\/" a)) by A2, YELLOW_0: 24

        .= (x "/\" ( 'not' x)) by A3, YELLOW_0: 24

        .= ( Bottom L) by YELLOW_5: 34;

        hence contradiction by A1;

      end;

      thus not a <= ( 'not' x) implies a <= x

      proof

        a <= ( Top L) by YELLOW_0: 45;

        then

         A4: a <= (x "\/" ( 'not' x)) by YELLOW_5: 34;

        assume ( not a <= ( 'not' x)) & not a <= x;

        hence contradiction by A1, A4, WAYBEL14: 14;

      end;

    end;

    theorem :: WAYBEL15:23

    

     Th23: for L be complete Boolean LATTICE holds for X be Subset of L holds for x be Element of L holds (x "/\" ( sup X)) = ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L))

    proof

      let L be complete Boolean LATTICE;

      let X be Subset of L;

      let x be Element of L;

      for y be Element of L holds (y "/\" ) is lower_adjoint by WAYBEL_1:def 19;

      hence thesis by WAYBEL_1: 64;

    end;

    theorem :: WAYBEL15:24

    

     Th24: for L be lower-bounded with_infima antisymmetric non empty RelStr holds for x,y be Element of L st x is atom & y is atom & x <> y holds (x "/\" y) = ( Bottom L)

    proof

      let L be lower-bounded with_infima antisymmetric non empty RelStr;

      let x,y be Element of L;

      assume that

       A1: x is atom and

       A2: y is atom and

       A3: x <> y and

       A4: (x "/\" y) <> ( Bottom L);

      ( Bottom L) <= (x "/\" y) by YELLOW_0: 44;

      then

       A5: ( Bottom L) < (x "/\" y) by A4, ORDERS_2:def 6;

      

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

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

      

      then x = (x "/\" y) by A1, A5

      .= y by A2, A5, A6;

      hence contradiction by A3;

    end;

    theorem :: WAYBEL15:25

    

     Th25: for L be complete Boolean LATTICE holds for x be Element of L holds for A be Subset of L st A c= ( ATOM L) holds x in A iff x is atom & x <= ( sup A)

    proof

      let L be complete Boolean LATTICE;

      let x be Element of L;

      let A be Subset of L;

      assume

       A1: A c= ( ATOM L);

      thus x in A implies x is atom & x <= ( sup A)

      proof

        assume

         A2: x in A;

        hence x is atom by A1, Def2;

        ( sup A) is_>=_than A by YELLOW_0: 32;

        hence thesis by A2, LATTICE3:def 9;

      end;

      thus x is atom & x <= ( sup A) implies x in A

      proof

        assume that

         A3: x is atom and

         A4: x <= ( sup A) and

         A5: not x in A;

        now

          let b be Element of L;

          assume b in { (x "/\" y) where y be Element of L : y in A };

          then

          consider y be Element of L such that

           A6: b = (x "/\" y) and

           A7: y in A;

          y is atom by A1, A7, Def2;

          hence b <= ( Bottom L) by A3, A5, A6, A7, Th24;

        end;

        then

         A8: ( Bottom L) is_>=_than { (x "/\" y) where y be Element of L : y in A } by LATTICE3:def 9;

        x = (x "/\" ( sup A)) by A4, YELLOW_0: 25

        .= ( "\/" ({ (x "/\" y) where y be Element of L : y in A },L)) by Th23;

        then x <= ( Bottom L) by A8, YELLOW_0: 32;

        then x = ( Bottom L) by YELLOW_5: 19;

        hence contradiction by A3;

      end;

    end;

    theorem :: WAYBEL15:26

    

     Th26: for L be complete Boolean LATTICE holds for X,Y be Subset of L st X c= ( ATOM L) & Y c= ( ATOM L) holds X c= Y iff ( sup X) <= ( sup Y)

    proof

      let L be complete Boolean LATTICE;

      let X,Y be Subset of L;

      assume that

       A1: X c= ( ATOM L) and

       A2: Y c= ( ATOM L);

      thus X c= Y implies ( sup X) <= ( sup Y)

      proof

        

         A3: ex_sup_of (X,L) & ex_sup_of (Y,L) by YELLOW_0: 17;

        assume X c= Y;

        hence thesis by A3, YELLOW_0: 34;

      end;

      thus ( sup X) <= ( sup Y) implies X c= Y

      proof

        assume

         A4: ( sup X) <= ( sup Y);

        thus X c= Y

        proof

          let z be object;

          assume

           A5: z in X;

          then

          reconsider z1 = z as Element of L;

          ( sup X) is_>=_than X by YELLOW_0: 32;

          then z1 <= ( sup X) by A5, LATTICE3:def 9;

          then

           A6: z1 <= ( sup Y) by A4, ORDERS_2: 3;

          z1 is atom by A1, A5, Def2;

          hence thesis by A2, A6, Th25;

        end;

      end;

    end;

    

     Lm5: for L be Boolean LATTICE holds L is completely-distributive implies (L is complete & for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X))

    proof

      let L be Boolean LATTICE;

      assume

       A1: L is completely-distributive;

      hence L is complete;

      let x be Element of L;

      consider X1 be Subset of L such that

       A2: x = ( sup X1) and

       A3: for y be Element of L st y in X1 holds y is co-prime by A1, WAYBEL_6: 38;

      reconsider X = (X1 \ {( Bottom L)}) as Subset of L;

       A4:

      now

        let b be Element of L;

        assume

         A5: b is_>=_than X;

        now

          let c be Element of L;

          assume

           A6: c in X1;

          now

            per cases ;

              suppose c <> ( Bottom L);

              then not c in {( Bottom L)} by TARSKI:def 1;

              then c in X by A6, XBOOLE_0:def 5;

              hence c <= b by A5, LATTICE3:def 9;

            end;

              suppose c = ( Bottom L);

              hence c <= b by YELLOW_0: 44;

            end;

          end;

          hence c <= b;

        end;

        then b is_>=_than X1 by LATTICE3:def 9;

        hence x <= b by A1, A2, YELLOW_0: 32;

      end;

      take X;

      thus X c= ( ATOM L)

      proof

        let z be object;

        assume

         A7: z in X;

        then

        reconsider z9 = z as Element of L;

         not z in {( Bottom L)} by A7, XBOOLE_0:def 5;

        then

         A8: z9 <> ( Bottom L) by TARSKI:def 1;

        z in X1 by A7, XBOOLE_0:def 5;

        then z9 is co-prime by A3;

        then z9 is atom by A8, Th20;

        hence thesis by Def2;

      end;

      

       A9: x is_>=_than X1 by A1, A2, YELLOW_0: 32;

      now

        let c be Element of L;

        assume c in X;

        then c in X1 by XBOOLE_0:def 5;

        hence c <= x by A9, LATTICE3:def 9;

      end;

      then x is_>=_than X by LATTICE3:def 9;

      hence thesis by A1, A4, YELLOW_0: 32;

    end;

    

     Lm6: for L be Boolean LATTICE holds (L is complete & for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X)) implies ex Y be set st (L,( BoolePoset Y)) are_isomorphic

    proof

      let L be Boolean LATTICE;

      assume that

       A1: L is complete and

       A2: for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X);

      defpred P[ set, set] means ex x9 be Subset of L st x9 = $1 & $2 = ( sup x9);

      take Y = ( ATOM L);

      

       A3: for x be Element of ( BoolePoset Y) holds ex y be Element of L st P[x, y]

      proof

        let x be Element of ( BoolePoset Y);

        x c= Y by WAYBEL_8: 26;

        then

        reconsider x9 = x as Subset of L by XBOOLE_1: 1;

        take ( sup x9);

        take x9;

        thus thesis;

      end;

      consider f be Function of ( BoolePoset Y), L such that

       A4: for x be Element of ( BoolePoset Y) holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

       A5:

      now

        let z,v be Element of ( BoolePoset Y);

        consider z9 be Subset of L such that

         A6: z9 = z and

         A7: (f . z) = ( sup z9) by A4;

        consider v9 be Subset of L such that

         A8: v9 = v and

         A9: (f . v) = ( sup v9) by A4;

        

         A10: ex_sup_of (z9,L) & ex_sup_of (v9,L) by A1, YELLOW_0: 17;

        thus z <= v implies (f . z) <= (f . v) by YELLOW_1: 2, A6, A7, A8, A9, A10, YELLOW_0: 34;

        

         A11: v9 c= ( ATOM L) by A8, WAYBEL_8: 26;

        

         A12: z9 c= ( ATOM L) by A6, WAYBEL_8: 26;

        thus (f . z) <= (f . v) implies z <= v

        proof

          assume (f . z) <= (f . v);

          then z c= v by A1, A6, A7, A8, A9, A12, A11, Th26;

          hence thesis by YELLOW_1: 2;

        end;

      end;

      the carrier of L c= ( rng f)

      proof

        let k be object;

        assume k in the carrier of L;

        then

        consider K be Subset of L such that

         A13: K c= ( ATOM L) and

         A14: k = ( sup K) by A2;

        

         A15: K is Element of ( BoolePoset Y) by A13, WAYBEL_8: 26;

        then K in the carrier of ( BoolePoset Y);

        then

         A16: K in ( dom f) by FUNCT_2:def 1;

        ex K9 be Subset of L st K9 = K & (f . K) = ( sup K9) by A4, A15;

        hence thesis by A14, A16, FUNCT_1:def 3;

      end;

      then

       A17: ( rng f) = the carrier of L by XBOOLE_0:def 10;

      now

        let z,v be Element of ( BoolePoset Y);

        assume

         A18: (f . z) = (f . v);

        consider z9 be Subset of L such that

         A19: z9 = z and

         A20: (f . z) = ( sup z9) by A4;

        consider v9 be Subset of L such that

         A21: v9 = v and

         A22: (f . v) = ( sup v9) by A4;

        

         A23: v9 c= ( ATOM L) by A21, WAYBEL_8: 26;

        z9 c= ( ATOM L) by A19, WAYBEL_8: 26;

        then z c= v & v c= z by A1, A19, A20, A21, A22, A23, A18, Th26;

        hence z = v by XBOOLE_0:def 10;

      end;

      then f is one-to-one;

      then f is isomorphic by A17, A5, WAYBEL_0: 66;

      then (( BoolePoset Y),L) are_isomorphic ;

      hence thesis by WAYBEL_1: 6;

    end;

    begin

    theorem :: WAYBEL15:27

    for L be Boolean LATTICE holds L is arithmetic iff ex X be set st (L,( BoolePoset X)) are_isomorphic

    proof

      let L be Boolean LATTICE;

      hereby

        assume

         A1: L is arithmetic;

        then (L opp ) is continuous by Th9, YELLOW_7: 38;

        then L is completely-distributive by A1, WAYBEL_6: 39;

        then for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X) by Lm5;

        hence ex X be set st (L,( BoolePoset X)) are_isomorphic by A1, Lm6;

      end;

      thus thesis by Th10, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL15:28

    for L be Boolean LATTICE holds L is arithmetic iff L is algebraic

    proof

      let L be Boolean LATTICE;

      thus L is arithmetic implies L is algebraic;

      assume

       A1: L is algebraic;

      then (L opp ) is continuous by Th9, YELLOW_7: 38;

      then L is completely-distributive by A1, WAYBEL_6: 39;

      then for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X) by Lm5;

      then ex X be set st (L,( BoolePoset X)) are_isomorphic by A1, Lm6;

      hence thesis by Th10, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL15:29

    for L be Boolean LATTICE holds L is arithmetic iff L is continuous

    proof

      let L be Boolean LATTICE;

      thus L is arithmetic implies L is continuous;

      assume

       A1: L is continuous;

      then (L opp ) is continuous by Th9, YELLOW_7: 38;

      then L is completely-distributive by A1, WAYBEL_6: 39;

      then for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X) by Lm5;

      then ex X be set st (L,( BoolePoset X)) are_isomorphic by A1, Lm6;

      hence thesis by Th10, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL15:30

    for L be Boolean LATTICE holds L is arithmetic iff L is continuous & (L opp ) is continuous

    proof

      let L be Boolean LATTICE;

      thus L is arithmetic implies L is continuous & (L opp ) is continuous by Th9, YELLOW_7: 38;

      assume that

       A1: L is continuous and

       A2: (L opp ) is continuous;

      L is completely-distributive by A1, A2, WAYBEL_6: 39;

      then for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X) by Lm5;

      then ex X be set st (L,( BoolePoset X)) are_isomorphic by A1, Lm6;

      hence thesis by Th10, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL15:31

    for L be Boolean LATTICE holds L is arithmetic iff L is completely-distributive

    proof

      let L be Boolean LATTICE;

      thus L is arithmetic implies L is completely-distributive

      proof

        assume

         A1: L is arithmetic;

        then (L opp ) is continuous by Th9, YELLOW_7: 38;

        hence thesis by A1, WAYBEL_6: 39;

      end;

      assume

       A2: L is completely-distributive;

      then for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X) by Lm5;

      then ex X be set st (L,( BoolePoset X)) are_isomorphic by A2, Lm6;

      hence thesis by Th10, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL15:32

    for L be Boolean LATTICE holds L is arithmetic iff (L is complete & for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X))

    proof

      let L be Boolean LATTICE;

      hereby

        assume

         A1: L is arithmetic;

        then (L opp ) is continuous by Th9, YELLOW_7: 38;

        then L is completely-distributive by A1, WAYBEL_6: 39;

        hence L is complete & for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X) by Lm5;

      end;

      assume L is complete & for x be Element of L holds ex X be Subset of L st X c= ( ATOM L) & x = ( sup X);

      then ex X be set st (L,( BoolePoset X)) are_isomorphic by Lm6;

      hence thesis by Th10, WAYBEL_1: 6;

    end;