msualg_7.miz



    begin

    reserve I for non empty set;

    reserve M for ManySortedSet of I;

    reserve Y,x,y,i for set;

    reserve r,r1,r2 for Real;

    theorem :: MSUALG_7:1

    

     Th1: ( id M) is Equivalence_Relation of M

    proof

      set J = ( id M);

      for i be set st i in I holds (J . i) is Relation of (M . i)

      proof

        let i be set;

        assume i in I;

        then (J . i) = ( id (M . i)) by MSUALG_3:def 1;

        hence thesis;

      end;

      then

      reconsider J as ManySortedRelation of M by MSUALG_4:def 1;

      for i be set, R be Relation of (M . i) st i in I & (J . i) = R holds R is Equivalence_Relation of (M . i)

      proof

        let i be set;

        let R be Relation of (M . i);

        assume that

         A1: i in I and

         A2: (J . i) = R;

        (J . i) = ( id (M . i)) by A1, MSUALG_3:def 1;

        hence thesis by A2, EQREL_1: 3;

      end;

      hence thesis by MSUALG_4:def 2;

    end;

    theorem :: MSUALG_7:2

    

     Th2: [|M, M|] is Equivalence_Relation of M

    proof

      set J = [|M, M|];

      for i be set st i in I holds (J . i) is Relation of (M . i)

      proof

        let i be set;

        assume i in I;

        then (J . i) c= [:(M . i), (M . i):] by PBOOLE:def 16;

        hence thesis;

      end;

      then

      reconsider J as ManySortedRelation of M by MSUALG_4:def 1;

      for i be set, R be Relation of (M . i) st i in I & (J . i) = R holds R is Equivalence_Relation of (M . i)

      proof

        let i be set;

        let R be Relation of (M . i);

        assume that

         A1: i in I and

         A2: (J . i) = R;

        (J . i) = [:(M . i), (M . i):] by A1, PBOOLE:def 16

        .= ( nabla (M . i)) by EQREL_1:def 1;

        hence thesis by A2, EQREL_1: 4;

      end;

      hence thesis by MSUALG_4:def 2;

    end;

    registration

      let I, M;

      cluster ( EqRelLatt M) -> bounded;

      coherence

      proof

        ex c be Element of ( EqRelLatt M) st for a be Element of ( EqRelLatt M) holds (c "\/" a) = c & (a "\/" c) = c

        proof

          reconsider c9 = [|M, M|] as Equivalence_Relation of M by Th2;

          reconsider c = c9 as Element of ( EqRelLatt M) by MSUALG_5:def 5;

          take c;

          let a be Element of ( EqRelLatt M);

          reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

           A1:

          now

            let i be object;

            

             A2: ex K1 be ManySortedRelation of M st K1 = (c9 (\/) a9) & (c9 "\/" a9) = ( EqCl K1) by MSUALG_5:def 4;

            assume

             A3: i in I;

            then

            reconsider i9 = i as Element of I;

            reconsider K2 = (c9 . i9), a2 = (a9 . i9) as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

            ((c9 (\/) a9) . i) = ((c9 . i) \/ (a9 . i)) by A3, PBOOLE:def 4

            .= ( [:(M . i), (M . i):] \/ (a9 . i)) by A3, PBOOLE:def 16

            .= (( nabla (M . i)) \/ a2) by EQREL_1:def 1

            .= ( nabla (M . i)) by EQREL_1: 1

            .= [:(M . i), (M . i):] by EQREL_1:def 1

            .= (c9 . i) by A3, PBOOLE:def 16;

            

            hence ((c9 "\/" a9) . i) = ( EqCl K2) by A2, MSUALG_5:def 3

            .= (c9 . i) by MSUALG_5: 2;

          end;

          

          thus (c "\/" a) = (the L_join of ( EqRelLatt M) . (c,a)) by LATTICES:def 1

          .= (c9 "\/" a9) by MSUALG_5:def 5

          .= c by A1, PBOOLE: 3;

          hence thesis;

        end;

        then

         A4: ( EqRelLatt M) is upper-bounded by LATTICES:def 14;

        ex c be Element of ( EqRelLatt M) st for a be Element of ( EqRelLatt M) holds (c "/\" a) = c & (a "/\" c) = c

        proof

          reconsider c9 = ( id M) as Equivalence_Relation of M by Th1;

          reconsider c = c9 as Element of ( EqRelLatt M) by MSUALG_5:def 5;

          take c;

          let a be Element of ( EqRelLatt M);

          reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

           A5:

          now

            let i be object;

            assume

             A6: i in I;

            then

            reconsider i9 = i as Element of I;

            reconsider a2 = (a9 . i9) as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

            

            thus ((c9 (/\) a9) . i) = ((c9 . i) /\ (a9 . i)) by A6, PBOOLE:def 5

            .= (( id (M . i)) /\ a2) by MSUALG_3:def 1

            .= ( id (M . i)) by EQREL_1: 10

            .= (c9 . i) by A6, MSUALG_3:def 1;

          end;

          

          thus (c "/\" a) = (the L_meet of ( EqRelLatt M) . (c,a)) by LATTICES:def 2

          .= (c9 (/\) a9) by MSUALG_5:def 5

          .= c by A5, PBOOLE: 3;

          hence thesis;

        end;

        then ( EqRelLatt M) is lower-bounded by LATTICES:def 13;

        hence thesis by A4;

      end;

    end

    theorem :: MSUALG_7:3

    ( Bottom ( EqRelLatt M)) = ( id M)

    proof

      set K = ( id M);

      K is Equivalence_Relation of M by Th1;

      then

      reconsider K as Element of ( EqRelLatt M) by MSUALG_5:def 5;

      now

        let a be Element of ( EqRelLatt M);

        reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

         A1:

        now

          let i be object;

          assume

           A2: i in I;

          then

          reconsider i9 = i as Element of I;

          reconsider a2 = (a9 . i9) as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

          

          thus ((K9 (/\) a9) . i) = ((K9 . i) /\ (a9 . i)) by A2, PBOOLE:def 5

          .= (( id (M . i)) /\ a2) by MSUALG_3:def 1

          .= ( id (M . i)) by EQREL_1: 10

          .= (K9 . i) by A2, MSUALG_3:def 1;

        end;

        

        thus (K "/\" a) = (the L_meet of ( EqRelLatt M) . (K,a)) by LATTICES:def 2

        .= (K9 (/\) a9) by MSUALG_5:def 5

        .= K by A1, PBOOLE: 3;

        hence (a "/\" K) = K;

      end;

      hence thesis by LATTICES:def 16;

    end;

    theorem :: MSUALG_7:4

    ( Top ( EqRelLatt M)) = [|M, M|]

    proof

      set K = [|M, M|];

      K is Equivalence_Relation of M by Th2;

      then

      reconsider K as Element of ( EqRelLatt M) by MSUALG_5:def 5;

      now

        let a be Element of ( EqRelLatt M);

        reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

         A1:

        now

          let i be object;

          

           A2: ex K1 be ManySortedRelation of M st K1 = (K9 (\/) a9) & (K9 "\/" a9) = ( EqCl K1) by MSUALG_5:def 4;

          assume

           A3: i in I;

          then

          reconsider i9 = i as Element of I;

          reconsider K2 = (K9 . i9), a2 = (a9 . i9) as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

          ((K9 (\/) a9) . i) = ((K9 . i) \/ (a9 . i)) by A3, PBOOLE:def 4

          .= ( [:(M . i), (M . i):] \/ (a9 . i)) by A3, PBOOLE:def 16

          .= (( nabla (M . i)) \/ a2) by EQREL_1:def 1

          .= ( nabla (M . i)) by EQREL_1: 1

          .= [:(M . i), (M . i):] by EQREL_1:def 1

          .= (K9 . i) by A3, PBOOLE:def 16;

          

          hence ((K9 "\/" a9) . i) = ( EqCl K2) by A2, MSUALG_5:def 3

          .= (K9 . i) by MSUALG_5: 2;

        end;

        

        thus (K "\/" a) = (the L_join of ( EqRelLatt M) . (K,a)) by LATTICES:def 1

        .= (K9 "\/" a9) by MSUALG_5:def 5

        .= K by A1, PBOOLE: 3;

        hence (a "\/" K) = K;

      end;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: MSUALG_7:5

    

     Th5: for X be Subset of ( EqRelLatt M) holds X is SubsetFamily of [|M, M|]

    proof

      let X be Subset of ( EqRelLatt M);

      now

        let x be object;

        assume x in the carrier of ( EqRelLatt M);

        then

        reconsider x9 = x as Equivalence_Relation of M by MSUALG_5:def 5;

        now

          let i be object;

          assume i in I;

          then

          reconsider i9 = i as Element of I;

          (x9 . i9) c= [:(M . i9), (M . i9):];

          hence (x9 . i) c= ( [|M, M|] . i) by PBOOLE:def 16;

        end;

        then x9 c= [|M, M|] by PBOOLE:def 2;

        then x9 is ManySortedSubset of [|M, M|] by PBOOLE:def 18;

        hence x in ( Bool [|M, M|]) by CLOSURE2:def 1;

      end;

      then the carrier of ( EqRelLatt M) c= ( Bool [|M, M|]);

      then ( bool the carrier of ( EqRelLatt M)) c= ( bool ( Bool [|M, M|])) by ZFMISC_1: 67;

      hence thesis;

    end;

    theorem :: MSUALG_7:6

    

     Th6: for a,b be Element of ( EqRelLatt M), A,B be Equivalence_Relation of M st a = A & b = B holds a [= b iff A c= B

    proof

      let a,b be Element of ( EqRelLatt M);

      let A,B be Equivalence_Relation of M;

      assume that

       A1: a = A and

       A2: b = B;

      thus a [= b implies A c= B

      proof

        assume

         A3: a [= b;

        (A (/\) B) = (the L_meet of ( EqRelLatt M) . (A,B)) by MSUALG_5:def 5

        .= (a "/\" b) by A1, A2, LATTICES:def 2

        .= A by A1, A3, LATTICES: 4;

        hence thesis by PBOOLE: 15;

      end;

      thus A c= B implies a [= b

      proof

        assume

         A4: A c= B;

        (a "/\" b) = (the L_meet of ( EqRelLatt M) . (A,B)) by A1, A2, LATTICES:def 2

        .= (A (/\) B) by MSUALG_5:def 5

        .= a by A1, A4, PBOOLE: 23;

        hence thesis by LATTICES: 4;

      end;

    end;

    theorem :: MSUALG_7:7

    

     Th7: for X be Subset of ( EqRelLatt M), X1 be SubsetFamily of [|M, M|] st X1 = X holds for a,b be Equivalence_Relation of M st a = ( meet |:X1:|) & b in X holds a c= b

    proof

      let X be Subset of ( EqRelLatt M);

      let X1 be SubsetFamily of [|M, M|] such that

       A1: X1 = X;

      let a,b be Equivalence_Relation of M such that

       A2: a = ( meet |:X1:|) and

       A3: b in X;

      now

        reconsider b9 = b as Element of ( Bool [|M, M|]) by A1, A3;

        let i be object;

        assume

         A4: i in I;

        then ( |:X1:| . i) = { (x . i) where x be Element of ( Bool [|M, M|]) : x in X1 } by A1, A3, CLOSURE2: 14;

        then

         A5: (b9 . i) in ( |:X1:| . i) by A1, A3;

        then

         A6: for y be object st y in ( meet ( |:X1:| . i)) holds y in (b . i) by SETFAM_1:def 1;

        ex Q be Subset-Family of ( [|M, M|] . i) st Q = ( |:X1:| . i) & (( meet |:X1:|) . i) = ( Intersect Q) by A4, MSSUBFAM:def 1;

        then (a . i) = ( meet ( |:X1:| . i)) by A2, A5, SETFAM_1:def 9;

        hence (a . i) c= (b . i) by A6;

      end;

      hence thesis by PBOOLE:def 2;

    end;

    theorem :: MSUALG_7:8

    

     Th8: for X be Subset of ( EqRelLatt M), X1 be SubsetFamily of [|M, M|] st X1 = X & X is non empty holds ( meet |:X1:|) is Equivalence_Relation of M

    proof

      let X be Subset of ( EqRelLatt M);

      let X1 be SubsetFamily of [|M, M|];

      set a = ( meet |:X1:|);

      now

        let i be set;

        assume

         A1: i in I;

        a c= [|M, M|] by PBOOLE:def 18;

        then (a . i) c= ( [|M, M|] . i) by A1, PBOOLE:def 2;

        hence (a . i) is Relation of (M . i) by A1, PBOOLE:def 16;

      end;

      then

      reconsider a as ManySortedRelation of M by MSUALG_4:def 1;

      assume that

       A2: X1 = X and

       A3: X is non empty;

      now

        reconsider X19 = X1 as non empty SubsetFamily of [|M, M|] by A2, A3;

        let i be set, R be Relation of (M . i);

        assume that

         A4: i in I and

         A5: (a . i) = R;

        reconsider i9 = i as Element of I by A4;

        reconsider b = ( |:X1:| . i9) as Subset-Family of [:(M . i), (M . i):] by PBOOLE:def 16;

        consider Q be Subset-Family of ( [|M, M|] . i) such that

         A6: Q = ( |:X1:| . i) and

         A7: R = ( Intersect Q) by A4, A5, MSSUBFAM:def 1;

        reconsider Q as Subset-Family of [:(M . i), (M . i):] by A4, PBOOLE:def 16;

         |:X19:| is non-empty;

        then

         A8: Q <> {} by A4, A6, PBOOLE:def 13;

        

         A9: ( |:X19:| . i) = { (x . i) where x be Element of ( Bool [|M, M|]) : x in X1 } by A4, CLOSURE2: 14;

        now

          let Y;

          assume Y in b;

          then

          consider z be Element of ( Bool [|M, M|]) such that

           A10: Y = (z . i) and

           A11: z in X by A2, A9;

          z c= [|M, M|] by PBOOLE:def 18;

          then (z . i) c= ( [|M, M|] . i) by A4, PBOOLE:def 2;

          then

          reconsider Y1 = Y as Relation of (M . i) by A4, A10, PBOOLE:def 16;

          z is Equivalence_Relation of M by A11, MSUALG_5:def 5;

          then Y1 is Equivalence_Relation of (M . i) by A4, A10, MSUALG_4:def 2;

          hence Y is Equivalence_Relation of (M . i);

        end;

        then ( meet b) is Equivalence_Relation of (M . i) by A6, A8, EQREL_1: 11;

        hence R is Equivalence_Relation of (M . i) by A6, A7, A8, SETFAM_1:def 9;

      end;

      hence thesis by MSUALG_4:def 2;

    end;

    definition

      let L be non empty LattStr;

      :: original: complete

      redefine

      :: MSUALG_7:def1

      attr L is complete means for X be Subset of L holds ex a be Element of L st X is_less_than a & for b be Element of L st X is_less_than b holds a [= b;

      compatibility

      proof

        thus L is complete implies for X be Subset of L holds ex a be Element of L st X is_less_than a & for b be Element of L st X is_less_than b holds a [= b;

        assume

         A1: for X be Subset of L holds ex a be Element of L st X is_less_than a & for b be Element of L st X is_less_than b holds a [= b;

        let X be set;

        defpred P[ set] means $1 in X;

        set Y = { c where c be Element of L : P[c] };

        Y is Subset of L from DOMAIN_1:sch 7;

        then

        consider p be Element of L such that

         A2: Y is_less_than p and

         A3: for r be Element of L st Y is_less_than r holds p [= r by A1;

        take p;

        thus X is_less_than p

        proof

          let q be Element of L;

          assume q in X;

          then q in Y;

          hence thesis by A2;

        end;

        let r be Element of L;

        assume

         A4: X is_less_than r;

        now

          let q be Element of L;

          assume q in Y;

          then ex v be Element of L st q = v & v in X;

          hence q [= r by A4;

        end;

        then Y is_less_than r;

        hence thesis by A3;

      end;

    end

    theorem :: MSUALG_7:9

    

     Th9: ( EqRelLatt M) is complete

    proof

      for X be Subset of ( EqRelLatt M) holds ex a be Element of ( EqRelLatt M) st a is_less_than X & for b be Element of ( EqRelLatt M) st b is_less_than X holds b [= a

      proof

        let X be Subset of ( EqRelLatt M);

        reconsider X1 = X as SubsetFamily of [|M, M|] by Th5;

        per cases ;

          suppose

           A1: X is empty;

          take a = ( Top ( EqRelLatt M));

          for q be Element of ( EqRelLatt M) st q in X holds a [= q by A1;

          hence a is_less_than X;

          let b be Element of ( EqRelLatt M);

          assume b is_less_than X;

          thus thesis by LATTICES: 19;

        end;

          suppose

           A2: X is non empty;

          then

          reconsider a = ( meet |:X1:|) as Equivalence_Relation of M by Th8;

          set a9 = a;

          reconsider a as Element of ( EqRelLatt M) by MSUALG_5:def 5;

          take a;

          now

            let q be Element of ( EqRelLatt M);

            reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def 5;

            assume q in X;

            then a9 c= q9 by Th7;

            hence a [= q by Th6;

          end;

          hence a is_less_than X;

          now

            let b be Element of ( EqRelLatt M);

            reconsider b9 = b as Equivalence_Relation of M by MSUALG_5:def 5;

            assume

             A3: b is_less_than X;

            now

              reconsider X19 = X1 as non empty SubsetFamily of [|M, M|] by A2;

              let i be object;

              assume

               A4: i in I;

              then

               A5: ex Q be Subset-Family of ( [|M, M|] . i) st Q = ( |:X1:| . i) & (( meet |:X1:|) . i) = ( Intersect Q) by MSSUBFAM:def 1;

               |:X19:| is non-empty;

              then

               A6: ( |:X1:| . i) <> {} by A4, PBOOLE:def 13;

              now

                let Z be set;

                assume

                 A7: Z in ( |:X1:| . i);

                ( |:X19:| . i) = { (x . i) where x be Element of ( Bool [|M, M|]) : x in X1 } by A4, CLOSURE2: 14;

                then

                consider z be Element of ( Bool [|M, M|]) such that

                 A8: Z = (z . i) and

                 A9: z in X1 by A7;

                reconsider z9 = z as Element of ( EqRelLatt M) by A9;

                reconsider z99 = z9 as Equivalence_Relation of M by MSUALG_5:def 5;

                b [= z9 by A3, A9;

                then b9 c= z99 by Th6;

                hence (b9 . i) c= Z by A4, A8, PBOOLE:def 2;

              end;

              then (b9 . i) c= ( meet ( |:X1:| . i)) by A6, SETFAM_1: 5;

              hence (b9 . i) c= (( meet |:X1:|) . i) by A6, A5, SETFAM_1:def 9;

            end;

            then b9 c= ( meet |:X1:|) by PBOOLE:def 2;

            hence b [= a by Th6;

          end;

          hence thesis;

        end;

      end;

      hence thesis by VECTSP_8:def 6;

    end;

    registration

      let I, M;

      cluster ( EqRelLatt M) -> complete;

      coherence by Th9;

    end

    theorem :: MSUALG_7:10

    for X be Subset of ( EqRelLatt M), X1 be SubsetFamily of [|M, M|] st X1 = X & X is non empty holds for a,b be Equivalence_Relation of M st a = ( meet |:X1:|) & b = ( "/\" (X,( EqRelLatt M))) holds a = b

    proof

      let X be Subset of ( EqRelLatt M);

      let X1 be SubsetFamily of [|M, M|];

      assume that

       A1: X1 = X and

       A2: X is non empty;

      let a,b be Equivalence_Relation of M;

      reconsider a9 = a as Element of ( EqRelLatt M) by MSUALG_5:def 5;

      assume that

       A3: a = ( meet |:X1:|) and

       A4: b = ( "/\" (X,( EqRelLatt M)));

       A5:

      now

        reconsider X19 = X1 as non empty SubsetFamily of [|M, M|] by A1, A2;

        let c be Element of ( EqRelLatt M);

        reconsider c9 = c as Equivalence_Relation of M by MSUALG_5:def 5;

        reconsider S = |:X19:| as non-empty MSSubsetFamily of [|M, M|];

        assume

         A6: c is_less_than X;

        now

          let Z1 be ManySortedSet of I;

          assume

           A7: Z1 in S;

          now

            let i be object;

            assume

             A8: i in I;

            then (Z1 . i) in ( |:X1:| . i) & ( |:X19:| . i) = { (x1 . i) where x1 be Element of ( Bool [|M, M|]) : x1 in X1 } by A7, CLOSURE2: 14, PBOOLE:def 1;

            then

            consider z be Element of ( Bool [|M, M|]) such that

             A9: (Z1 . i) = (z . i) and

             A10: z in X1;

            reconsider z9 = z as Element of ( EqRelLatt M) by A1, A10;

            reconsider z1 = z9 as Equivalence_Relation of M by MSUALG_5:def 5;

            c [= z9 by A1, A6, A10;

            then c9 c= z1 by Th6;

            hence (c9 . i) c= (Z1 . i) by A8, A9, PBOOLE:def 2;

          end;

          hence c9 c= Z1 by PBOOLE:def 2;

        end;

        then c9 c= ( meet |:X1:|) by MSSUBFAM: 45;

        hence c [= a9 by A3, Th6;

      end;

      now

        let q be Element of ( EqRelLatt M);

        reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def 5;

        assume q in X;

        then a c= q9 by A1, A3, Th7;

        hence a9 [= q by Th6;

      end;

      then a9 is_less_than X;

      hence thesis by A4, A5, LATTICE3: 34;

    end;

    begin

    definition

      let L be Lattice;

      let IT be SubLattice of L;

      :: MSUALG_7:def2

      attr IT is /\-inheriting means for X be Subset of IT holds ( "/\" (X,L)) in the carrier of IT;

      :: MSUALG_7:def3

      attr IT is \/-inheriting means for X be Subset of IT holds ( "\/" (X,L)) in the carrier of IT;

    end

    theorem :: MSUALG_7:11

    

     Th11: for L be Lattice, L9 be SubLattice of L, a,b be Element of L, a9,b9 be Element of L9 st a = a9 & b = b9 holds (a "\/" b) = (a9 "\/" b9) & (a "/\" b) = (a9 "/\" b9)

    proof

      let L be Lattice;

      let L9 be SubLattice of L;

      let a,b be Element of L;

      let a9,b9 be Element of L9;

      assume

       A1: a = a9 & b = b9;

      

      thus (a "\/" b) = (the L_join of L . (a,b)) by LATTICES:def 1

      .= ((the L_join of L || the carrier of L9) . [a9, b9]) by A1, FUNCT_1: 49

      .= (the L_join of L9 . (a9,b9)) by NAT_LAT:def 12

      .= (a9 "\/" b9) by LATTICES:def 1;

      

      thus (a "/\" b) = (the L_meet of L . (a,b)) by LATTICES:def 2

      .= ((the L_meet of L || the carrier of L9) . [a9, b9]) by A1, FUNCT_1: 49

      .= (the L_meet of L9 . (a9,b9)) by NAT_LAT:def 12

      .= (a9 "/\" b9) by LATTICES:def 2;

    end;

    theorem :: MSUALG_7:12

    

     Th12: for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be Element of L, a9 be Element of L9 st a = a9 holds a is_less_than X iff a9 is_less_than X

    proof

      let L be Lattice;

      let L9 be SubLattice of L;

      let X be Subset of L9;

      let a be Element of L;

      let a9 be Element of L9;

      assume

       A1: a = a9;

      thus a is_less_than X implies a9 is_less_than X

      proof

        assume

         A2: a is_less_than X;

        now

          let q9 be Element of L9;

          the carrier of L9 c= the carrier of L by NAT_LAT:def 12;

          then

          reconsider q = q9 as Element of L;

          assume q9 in X;

          then

           A3: a [= q by A2;

          (a9 "/\" q9) = (a "/\" q) by A1, Th11

          .= a9 by A1, A3, LATTICES: 4;

          hence a9 [= q9 by LATTICES: 4;

        end;

        hence thesis;

      end;

      thus a9 is_less_than X implies a is_less_than X

      proof

        assume

         A4: a9 is_less_than X;

        now

          let q be Element of L;

          assume

           A5: q in X;

          then

          reconsider q9 = q as Element of L9;

          

           A6: a9 [= q9 by A4, A5;

          (a "/\" q) = (a9 "/\" q9) by A1, Th11

          .= a by A1, A6, LATTICES: 4;

          hence a [= q by LATTICES: 4;

        end;

        hence thesis;

      end;

    end;

    theorem :: MSUALG_7:13

    

     Th13: for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be Element of L, a9 be Element of L9 st a = a9 holds X is_less_than a iff X is_less_than a9

    proof

      let L be Lattice;

      let L9 be SubLattice of L;

      let X be Subset of L9;

      let a be Element of L;

      let a9 be Element of L9;

      assume

       A1: a = a9;

      thus X is_less_than a implies X is_less_than a9

      proof

        assume

         A2: X is_less_than a;

        now

          let q9 be Element of L9;

          the carrier of L9 c= the carrier of L by NAT_LAT:def 12;

          then

          reconsider q = q9 as Element of L;

          assume q9 in X;

          then

           A3: q [= a by A2;

          (q9 "/\" a9) = (q "/\" a) by A1, Th11

          .= q9 by A3, LATTICES: 4;

          hence q9 [= a9 by LATTICES: 4;

        end;

        hence thesis;

      end;

      thus X is_less_than a9 implies X is_less_than a

      proof

        assume

         A4: X is_less_than a9;

        now

          let q be Element of L;

          assume

           A5: q in X;

          then

          reconsider q9 = q as Element of L9;

          

           A6: q9 [= a9 by A4, A5;

          (q "/\" a) = (q9 "/\" a9) by A1, Th11

          .= q by A6, LATTICES: 4;

          hence q [= a by LATTICES: 4;

        end;

        hence thesis;

      end;

    end;

    theorem :: MSUALG_7:14

    

     Th14: for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting holds L9 is complete

    proof

      let L be complete Lattice;

      let L9 be SubLattice of L such that

       A1: L9 is /\-inheriting;

      for X be Subset of L9 holds ex a be Element of L9 st a is_less_than X & for b be Element of L9 st b is_less_than X holds b [= a

      proof

        let X be Subset of L9;

        set a = ( "/\" (X,L));

        reconsider a9 = a as Element of L9 by A1;

        take a9;

        a is_less_than X by LATTICE3: 34;

        hence a9 is_less_than X by Th12;

        let b9 be Element of L9;

        the carrier of L9 c= the carrier of L by NAT_LAT:def 12;

        then

        reconsider b = b9 as Element of L;

        assume b9 is_less_than X;

        then b is_less_than X by Th12;

        then

         A2: b [= a by LATTICE3: 39;

        (b9 "/\" a9) = (b "/\" a) by Th11

        .= b9 by A2, LATTICES: 4;

        hence thesis by LATTICES: 4;

      end;

      hence thesis by VECTSP_8:def 6;

    end;

    theorem :: MSUALG_7:15

    

     Th15: for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting holds L9 is complete

    proof

      let L be complete Lattice;

      let L9 be SubLattice of L such that

       A1: L9 is \/-inheriting;

      for X be Subset of L9 holds ex a be Element of L9 st X is_less_than a & for b be Element of L9 st X is_less_than b holds a [= b

      proof

        let X be Subset of L9;

        set a = ( "\/" (X,L));

        reconsider a9 = a as Element of L9 by A1;

        take a9;

        X is_less_than a by LATTICE3:def 21;

        hence X is_less_than a9 by Th13;

        let b9 be Element of L9;

        the carrier of L9 c= the carrier of L by NAT_LAT:def 12;

        then

        reconsider b = b9 as Element of L;

        assume X is_less_than b9;

        then X is_less_than b by Th13;

        then

         A2: a [= b by LATTICE3:def 21;

        (a9 "/\" b9) = (a "/\" b) by Th11

        .= a9 by A2, LATTICES: 4;

        hence thesis by LATTICES: 4;

      end;

      hence thesis;

    end;

    registration

      let L be complete Lattice;

      cluster complete for SubLattice of L;

      existence

      proof

        reconsider L1 = L as SubLattice of L by NAT_LAT: 15;

        take L1;

        thus thesis;

      end;

    end

    registration

      let L be complete Lattice;

      cluster /\-inheriting -> complete for SubLattice of L;

      coherence by Th14;

      cluster \/-inheriting -> complete for SubLattice of L;

      coherence by Th15;

    end

    theorem :: MSUALG_7:16

    

     Th16: for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting holds for A9 be Subset of L9 holds ( "/\" (A9,L)) = ( "/\" (A9,L9))

    proof

      let L be complete Lattice;

      let L9 be SubLattice of L;

      assume

       A1: L9 is /\-inheriting;

      then

      reconsider L91 = L9 as complete SubLattice of L;

      let A9 be Subset of L9;

      set a = ( "/\" (A9,L));

      reconsider a9 = a as Element of L91 by A1;

       A2:

      now

        let c9 be Element of L91;

        the carrier of L91 c= the carrier of L by NAT_LAT:def 12;

        then

        reconsider c = c9 as Element of L;

        assume c9 is_less_than A9;

        then c is_less_than A9 by Th12;

        then

         A3: c [= a by LATTICE3: 34;

        (c9 "/\" a9) = (c "/\" a) by Th11

        .= c9 by A3, LATTICES: 4;

        hence c9 [= a9 by LATTICES: 4;

      end;

      a is_less_than A9 by LATTICE3: 34;

      then a9 is_less_than A9 by Th12;

      hence thesis by A2, LATTICE3: 34;

    end;

    theorem :: MSUALG_7:17

    

     Th17: for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting holds for A9 be Subset of L9 holds ( "\/" (A9,L)) = ( "\/" (A9,L9))

    proof

      let L be complete Lattice;

      let L9 be SubLattice of L;

      assume

       A1: L9 is \/-inheriting;

      then

      reconsider L91 = L9 as complete SubLattice of L;

      let A9 be Subset of L9;

      set a = ( "\/" (A9,L));

      reconsider a9 = a as Element of L91 by A1;

       A2:

      now

        let c9 be Element of L91;

        the carrier of L91 c= the carrier of L by NAT_LAT:def 12;

        then

        reconsider c = c9 as Element of L;

        assume A9 is_less_than c9;

        then A9 is_less_than c by Th13;

        then

         A3: a [= c by LATTICE3:def 21;

        (a9 "/\" c9) = (a "/\" c) by Th11

        .= a9 by A3, LATTICES: 4;

        hence a9 [= c9 by LATTICES: 4;

      end;

      A9 is_less_than a by LATTICE3:def 21;

      then A9 is_less_than a9 by Th13;

      hence thesis by A2, LATTICE3:def 21;

    end;

    theorem :: MSUALG_7:18

    for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting holds for A be Subset of L, A9 be Subset of L9 st A = A9 holds ( "/\" A) = ( "/\" A9) by Th16;

    theorem :: MSUALG_7:19

    for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting holds for A be Subset of L, A9 be Subset of L9 st A = A9 holds ( "\/" A) = ( "\/" A9) by Th17;

    begin

    definition

      let r1, r2;

      :: MSUALG_7:def4

      func RealSubLatt (r1,r2) -> strict Lattice means

      : Def4: the carrier of it = [.r1, r2.] & the L_join of it = ( maxreal || [.r1, r2.]) & the L_meet of it = ( minreal || [.r1, r2.]);

      existence

      proof

        r2 in { r : r1 <= r & r <= r2 } by A1;

        then

        reconsider A = [.r1, r2.] as non empty set by RCOMP_1:def 1;

         [:A, A:] c= [: REAL , REAL :] by ZFMISC_1: 96;

        then

        reconsider Ma = ( maxreal || A), Mi = ( minreal || A) as Function of [:A, A:], REAL by FUNCT_2: 32;

        

         A2: ( dom Mi) = [:A, A:] by FUNCT_2:def 1;

         A3:

        now

          let x be object;

          assume

           A4: x in ( dom Mi);

          then

          consider x1,x2 be object such that

           A5: x = [x1, x2] by RELAT_1:def 1;

          x2 in A by A4, A5, ZFMISC_1: 87;

          then x2 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;

          then

          consider y2 be Real such that

           A6: x2 = y2 and

           A7: r1 <= y2 & y2 <= r2;

          reconsider y2 as Real;

          x1 in A by A4, A5, ZFMISC_1: 87;

          then x1 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;

          then

          consider y1 be Real such that

           A8: x1 = y1 and

           A9: r1 <= y1 & y1 <= r2;

          reconsider y1 as Real;

          (Mi . x) = ( minreal . (x1,x2)) by A4, A5, FUNCT_1: 49

          .= ( min (y1,y2)) by A8, A6, REAL_LAT:def 1;

          then (Mi . x) = y1 or (Mi . x) = y2 by XXREAL_0: 15;

          then (Mi . x) in { r : r1 <= r & r <= r2 } by A9, A7;

          hence (Mi . x) in A by RCOMP_1:def 1;

        end;

         A10:

        now

          let x be object;

          assume

           A11: x in ( dom Ma);

          then

          consider x1,x2 be object such that

           A12: x = [x1, x2] by RELAT_1:def 1;

          x2 in A by A11, A12, ZFMISC_1: 87;

          then x2 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;

          then

          consider y2 be Real such that

           A13: x2 = y2 and

           A14: r1 <= y2 & y2 <= r2;

          reconsider y2 as Real;

          x1 in A by A11, A12, ZFMISC_1: 87;

          then x1 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;

          then

          consider y1 be Real such that

           A15: x1 = y1 and

           A16: r1 <= y1 & y1 <= r2;

          reconsider y1 as Real;

          (Ma . x) = ( maxreal . (x1,x2)) by A11, A12, FUNCT_1: 49

          .= ( max (y1,y2)) by A15, A13, REAL_LAT:def 2;

          then (Ma . x) = y1 or (Ma . x) = y2 by XXREAL_0: 16;

          then (Ma . x) in { r : r1 <= r & r <= r2 } by A16, A14;

          hence (Ma . x) in A by RCOMP_1:def 1;

        end;

        reconsider Mi as BinOp of A by A2, A3, FUNCT_2: 3;

        ( dom Ma) = [:A, A:] by FUNCT_2:def 1;

        then

        reconsider Ma as BinOp of A by A10, FUNCT_2: 3;

        set R = Real_Lattice ;

        set L9 = LattStr (# A, Ma, Mi #);

        reconsider L = L9 as non empty LattStr;

         A17:

        now

          let a,b be Element of L;

          

          thus (a "\/" b) = (the L_join of L . (a,b)) by LATTICES:def 1

          .= ( maxreal . [a, b]) by FUNCT_1: 49

          .= ( maxreal . (a,b));

          

          thus (a "/\" b) = (the L_meet of L . (a,b)) by LATTICES:def 2

          .= ( minreal . [a, b]) by FUNCT_1: 49

          .= ( minreal . (a,b));

        end;

        

         A18: for x be Element of A holds x is Element of R by REAL_LAT:def 3, XREAL_0:def 1;

         A19:

        now

          let p,q be Element of L;

          reconsider p9 = p, q9 = q as Element of R by A18;

          

          thus (p "\/" q) = ( maxreal . (p,q)) by A17

          .= ( maxreal . (q9,p9)) by REAL_LAT: 1

          .= (q "\/" p) by A17;

        end;

         A20:

        now

          let p,q be Element of L;

          reconsider p9 = p, q9 = q as Element of R by A18;

          

          thus (p "/\" (p "\/" q)) = ( minreal . (p,(p "\/" q))) by A17

          .= ( minreal . (p9,( maxreal . (p9,q9)))) by A17

          .= p by REAL_LAT: 6;

        end;

         A21:

        now

          let p,q be Element of L;

          reconsider p9 = p, q9 = q as Element of R by A18;

          

          thus (p "/\" q) = ( minreal . (p,q)) by A17

          .= ( minreal . (q9,p9)) by REAL_LAT: 2

          .= (q "/\" p) by A17;

        end;

         A22:

        now

          let p,q be Element of L;

          reconsider p9 = p, q9 = q as Element of R by A18;

          

          thus ((p "/\" q) "\/" q) = ( maxreal . ((p "/\" q),q)) by A17

          .= ( maxreal . (( minreal . (p9,q9)),q9)) by A17

          .= q by REAL_LAT: 5;

        end;

         A23:

        now

          let p,q,r be Element of L;

          reconsider p9 = p, q9 = q, r9 = r as Element of R by A18;

          

          thus (p "/\" (q "/\" r)) = ( minreal . (p,(q "/\" r))) by A17

          .= ( minreal . (p,( minreal . (q,r)))) by A17

          .= ( minreal . (( minreal . (p9,q9)),r9)) by REAL_LAT: 4

          .= ( minreal . ((p "/\" q),r)) by A17

          .= ((p "/\" q) "/\" r) by A17;

        end;

        now

          let p,q,r be Element of L;

          reconsider p9 = p, q9 = q, r9 = r as Element of R by A18;

          

          thus (p "\/" (q "\/" r)) = ( maxreal . (p,(q "\/" r))) by A17

          .= ( maxreal . (p,( maxreal . (q,r)))) by A17

          .= ( maxreal . (( maxreal . (p9,q9)),r9)) by REAL_LAT: 3

          .= ( maxreal . ((p "\/" q),r)) by A17

          .= ((p "\/" q) "\/" r) by A17;

        end;

        then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A19, A22, A21, A23, A20, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

        then

        reconsider L9 as strict Lattice;

        take L9;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: MSUALG_7:20

    

     Th20: for r1, r2 st r1 <= r2 holds ( RealSubLatt (r1,r2)) is complete

    proof

      let r1, r2 such that

       A1: r1 <= r2;

      reconsider R1 = r1, R2 = r2 as R_eal by XXREAL_0:def 1;

      set A = [.r1, r2.];

      set L9 = ( RealSubLatt (r1,r2));

      

       A2: the carrier of L9 = [.r1, r2.] by A1, Def4;

      

       A3: the L_meet of L9 = ( minreal || [.r1, r2.]) by A1, Def4;

      now

        let X be Subset of L9;

        per cases ;

          suppose

           A4: X is empty;

          thus ex a be Element of L9 st a is_less_than X & for b be Element of L9 st b is_less_than X holds b [= a

          proof

            r2 in { r : r1 <= r & r <= r2 } by A1;

            then

            reconsider a = r2 as Element of L9 by A2, RCOMP_1:def 1;

            take a;

            for q be Element of L9 st q in X holds a [= q by A4;

            hence a is_less_than X;

            let b be Element of L9;

            assume b is_less_than X;

            

             A5: b in [.r1, r2.] by A2;

            then

            reconsider b9 = b as Element of REAL ;

            b in { r : r1 <= r & r <= r2 } by A5, RCOMP_1:def 1;

            then

            consider b1 be Real such that

             A6: b = b1 & r1 <= b1 & b1 <= r2;

            reconsider b1, r2 as Real;

            (b "/\" a) = (( minreal || A) . (b,a)) by A3, LATTICES:def 2

            .= ( minreal . [b, a]) by A2, FUNCT_1: 49

            .= ( minreal . (b,a))

            .= ( min (b9,r2)) by REAL_LAT:def 1

            .= b by A6, XXREAL_0:def 9;

            hence thesis by LATTICES: 4;

          end;

        end;

          suppose

           A7: X is non empty;

          X c= REAL by A2, XBOOLE_1: 1;

          then

          reconsider X1 = X as non empty Subset of ExtREAL by A7, NUMBERS: 31, XBOOLE_1: 1;

          thus ex a be Element of L9 st a is_less_than X & for b be Element of L9 st b is_less_than X holds b [= a

          proof

            set g = the Element of X1;

            set A1 = ( inf X1);

            set LB = (r1 - 1);

            LB is LowerBound of X1

            proof

              let v be ExtReal;

              assume v in X1;

              then v in the carrier of L9;

              then v in { r : r1 <= r & r <= r2 } by A2, RCOMP_1:def 1;

              then

              consider w be Real such that

               A8: v = w and

               A9: r1 <= w and w <= r2;

              (r1 - 1) <= (r1 - 0 ) by XREAL_1: 13;

              then ((r1 - 1) + r1) <= (r1 + w) by A9, XREAL_1: 7;

              hence LB <= v by A8, XREAL_1: 6;

            end;

            then

             A10: X1 is bounded_below;

            X <> { +infty }

            proof

              assume X = { +infty };

              then +infty in X by TARSKI:def 1;

              hence contradiction by A2;

            end;

            then

             A11: A1 in REAL by A10, XXREAL_2: 58;

            g in [.r1, r2.] by A2, TARSKI:def 3;

            then g in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;

            then

             A12: ex w be Real st g = w & r1 <= w & w <= r2;

            

             A13: A1 is LowerBound of X1 by XXREAL_2:def 4;

            then A1 <= g by XXREAL_2:def 2;

            then

            consider A9,R29 be Real such that

             A14: A9 = A1 and

             A15: R29 = R2 & A9 <= R29 by A11, A12, XXREAL_0: 2;

            now

              let v be ExtReal;

              assume v in X1;

              then v in A by A2;

              then v in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;

              then ex w be Real st v = w & r1 <= w & w <= r2;

              hence R1 <= v;

            end;

            then R1 is LowerBound of X1 by XXREAL_2:def 2;

            then R1 <= A1 by XXREAL_2:def 4;

            then A9 in { r : r1 <= r & r <= r2 } by A14, A15;

            then

            reconsider a = A1 as Element of L9 by A2, A14, RCOMP_1:def 1;

            take a;

            a in [.r1, r2.] by A2;

            then

            reconsider a9 = a as Element of REAL ;

            now

              let q be Element of L9;

              assume

               A16: q in X;

              q in [.r1, r2.] by A2;

              then

              reconsider q9 = q as Element of REAL ;

              reconsider Q = q9 as R_eal by NUMBERS: 31;

              A1 = a9;

              then

               A17: ex a1,q1 be Real st a1 = A1 & q1 = Q & a1 <= q1 by A13, A16, XXREAL_2:def 2;

              (a "/\" q) = (( minreal || A) . (a,q)) by A3, LATTICES:def 2

              .= ( minreal . [a, q]) by A2, FUNCT_1: 49

              .= ( minreal . (a,q))

              .= ( min (a9,q9)) by REAL_LAT:def 1

              .= a by A17, XXREAL_0:def 9;

              hence a [= q by LATTICES: 4;

            end;

            hence a is_less_than X;

            let b be Element of L9;

            b in [.r1, r2.] by A2;

            then

            reconsider b9 = b as Element of REAL ;

            reconsider B = b9 as R_eal by NUMBERS: 31;

            assume

             A18: b is_less_than X;

            now

              let h be ExtReal;

              assume

               A19: h in X;

              then

              reconsider h1 = h as Element of L9;

              h in [.r1, r2.] by A2, A19;

              then

              reconsider h9 = h as Real;

              

               A20: b [= h1 by A18, A19;

              ( min (b9,h9)) = ( minreal . (b,h1)) by REAL_LAT:def 1

              .= (( minreal || A) . [b, h1]) by A2, FUNCT_1: 49

              .= (( minreal || A) . (b,h1))

              .= (b "/\" h1) by A3, LATTICES:def 2

              .= b9 by A20, LATTICES: 4;

              hence B <= h by XXREAL_0:def 9;

            end;

            then B is LowerBound of X1 by XXREAL_2:def 2;

            then

             A21: B <= A1 by XXREAL_2:def 4;

            (b "/\" a) = (( minreal || A) . (b,a)) by A3, LATTICES:def 2

            .= ( minreal . [b, a]) by A2, FUNCT_1: 49

            .= ( minreal . (b,a))

            .= ( min (b9,a9)) by REAL_LAT:def 1

            .= b by A21, XXREAL_0:def 9;

            hence thesis by LATTICES: 4;

          end;

        end;

      end;

      hence thesis by VECTSP_8:def 6;

    end;

    reconsider jj = 1 as Real;

    reconsider jd = (1 / 2) as Real;

    theorem :: MSUALG_7:21

    

     Th21: ex L9 be SubLattice of ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL )))) st L9 is \/-inheriting non /\-inheriting

    proof

      set B = ( { 0 , 1} \/ ].(1 / 2), 1.[);

      set L = ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL ))));

      set R = Real_Lattice ;

      

       A1: B c= ( { 0 } \/ { x where x be Real : (1 / 2) < x & x <= 1 })

      proof

        let x1 be object;

        assume

         A2: x1 in B;

        now

          per cases by A2, XBOOLE_0:def 3;

            suppose x1 in { 0 , 1};

            then x1 = 0 or x1 = 1 by TARSKI:def 2;

            then x1 in { 0 } or x1 in { x where x be Real : (1 / 2) < x & x <= jj } by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose x1 in ].(1 / 2), 1.[;

            then x1 in { r : (1 / 2) < r & r < 1 } by RCOMP_1:def 2;

            then

            consider y be Real such that

             A3: x1 = y and

             A4: (1 / 2) < y & y < 1;

            y in { x where x be Real : (1 / 2) < x & x <= 1 } by A4;

            hence thesis by A3, XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

      ( { 0 } \/ { x where x be Real : (1 / 2) < x & x <= 1 }) c= B

      proof

        let x1 be object;

        assume

         A5: x1 in ( { 0 } \/ { x where x be Real : (1 / 2) < x & x <= 1 });

        now

          per cases by A5, XBOOLE_0:def 3;

            suppose x1 in { 0 };

            then x1 = 0 by TARSKI:def 1;

            then x1 in { 0 , 1} by TARSKI:def 2;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose x1 in { x where x be Real : (1 / 2) < x & x <= 1 };

            then

            consider y be Real such that

             A6: x1 = y and

             A7: (1 / 2) < y and

             A8: y <= 1;

            y < 1 or y = 1 by A8, XXREAL_0: 1;

            then y in { r : (1 / 2) < r & r < 1 } or y = 1 by A7;

            then y in ].(1 / 2), 1.[ or y in { 0 , 1} by RCOMP_1:def 2, TARSKI:def 2;

            hence thesis by A6, XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

      then

       A9: B = ( { 0 } \/ { x where x be Real : (1 / 2) < x & x <= 1 }) by A1, XBOOLE_0:def 10;

      

       A10: 0 in { r : 0 <= r & r <= 1 };

      then

      reconsider A = [. 0 , jj.] as non empty set by RCOMP_1:def 1;

      

       A11: the L_meet of L = ( minreal || [. 0 , jj.]) by Def4;

      reconsider B as non empty set;

      

       A12: the L_join of L = ( maxreal || [. 0 , jj.]) by Def4;

      

       A13: A = the carrier of L by Def4;

      then

      reconsider Ma = ( maxreal || A), Mi = ( minreal || A) as BinOp of A by Def4;

       A14:

      now

        let x1 be object;

        assume

         A15: x1 in B;

        now

          per cases by A1, A15, XBOOLE_0:def 3;

            suppose x1 in { 0 };

            then x1 = 0 by TARSKI:def 1;

            hence x1 in A by A10, RCOMP_1:def 1;

          end;

            suppose x1 in { x where x be Real : (1 / 2) < x & x <= 1 };

            then ex y be Real st x1 = y & (1 / 2) < y & y <= 1;

            then x1 in { r : 0 <= r & r <= 1 };

            hence x1 in A by RCOMP_1:def 1;

          end;

        end;

        hence x1 in A;

      end;

      then

       A16: B c= A;

      then

       A17: [:B, B:] c= [:A, A:] by ZFMISC_1: 96;

      then

      reconsider ma = (Ma || B), mi = (Mi || B) as Function of [:B, B:], A by FUNCT_2: 32;

      

       A18: for x1 be Element of A holds x1 is Element of R by REAL_LAT:def 3, XREAL_0:def 1;

      

       A19: ( dom mi) = [:B, B:] by FUNCT_2:def 1;

       A20:

      now

        let x9 be object;

        assume

         A21: x9 in ( dom mi);

        then

        consider x1,x2 be object such that

         A22: x9 = [x1, x2] by RELAT_1:def 1;

        

         A23: x2 in B by A21, A22, ZFMISC_1: 87;

        

         A24: x1 in B by A21, A22, ZFMISC_1: 87;

        now

          per cases by A1, A24, XBOOLE_0:def 3;

            suppose x1 in { 0 };

            then

             A25: x1 = 0 by TARSKI:def 1;

            now

              per cases by A1, A23, XBOOLE_0:def 3;

                suppose x2 in { 0 };

                then

                 A26: x2 = 0 by TARSKI:def 1;

                (mi . x9) = (Mi . [x1, x2]) by A21, A22, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A17, A21, A22, FUNCT_1: 49

                .= ( min ( 0 , 0 )) by A25, A26, REAL_LAT:def 1

                .= 0 ;

                then (mi . x9) in { 0 } by TARSKI:def 1;

                hence (mi . x9) in B by A9, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : (1 / 2) < x & x <= 1 };

                then

                consider y2 be Real such that

                 A27: x2 = y2 and

                 A28: (1 / 2) < y2 & y2 <= 1;

                reconsider y2 as Real;

                (mi . x9) = (Mi . [x1, x2]) by A21, A22, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A17, A21, A22, FUNCT_1: 49

                .= ( min ( 0 ,y2)) by A25, A27, REAL_LAT:def 1;

                then (mi . x9) = 0 or (mi . x9) = y2 by XXREAL_0: 15;

                then (mi . x9) in { 0 } or (mi . x9) in { x where x be Real : (1 / 2) < x & x <= 1 } by A28, TARSKI:def 1;

                hence (mi . x9) in B by A9, XBOOLE_0:def 3;

              end;

            end;

            hence (mi . x9) in B;

          end;

            suppose x1 in { x where x be Real : (1 / 2) < x & x <= 1 };

            then

            consider y1 be Real such that

             A29: x1 = y1 and

             A30: (1 / 2) < y1 & y1 <= 1;

            reconsider y1 as Real;

            now

              per cases by A1, A23, XBOOLE_0:def 3;

                suppose x2 in { 0 };

                then

                 A31: x2 = 0 by TARSKI:def 1;

                (mi . x9) = (Mi . [x1, x2]) by A21, A22, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A17, A21, A22, FUNCT_1: 49

                .= ( min (y1, 0 )) by A29, A31, REAL_LAT:def 1;

                then (mi . x9) = y1 or (mi . x9) = 0 by XXREAL_0: 15;

                then (mi . x9) in { x where x be Real : (1 / 2) < x & x <= 1 } or (mi . x9) in { 0 } by A30, TARSKI:def 1;

                hence (mi . x9) in B by A9, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : (1 / 2) < x & x <= 1 };

                then

                consider y2 be Real such that

                 A32: x2 = y2 and

                 A33: (1 / 2) < y2 & y2 <= 1;

                reconsider y2 as Real;

                (mi . x9) = (Mi . [x1, x2]) by A21, A22, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A17, A21, A22, FUNCT_1: 49

                .= ( min (y1,y2)) by A29, A32, REAL_LAT:def 1;

                then (mi . x9) = y1 or (mi . x9) = y2 by XXREAL_0: 15;

                then (mi . x9) in { x where x be Real : (1 / 2) < x & x <= 1 } by A30, A33;

                hence (mi . x9) in B by A9, XBOOLE_0:def 3;

              end;

            end;

            hence (mi . x9) in B;

          end;

        end;

        hence (mi . x9) in B;

      end;

      

       A34: ( dom ma) = [:B, B:] by FUNCT_2:def 1;

       A35:

      now

        let x9 be object;

        assume

         A36: x9 in ( dom ma);

        then

        consider x1,x2 be object such that

         A37: x9 = [x1, x2] by RELAT_1:def 1;

        

         A38: x2 in B by A36, A37, ZFMISC_1: 87;

        

         A39: x1 in B by A36, A37, ZFMISC_1: 87;

        now

          per cases by A1, A39, XBOOLE_0:def 3;

            suppose x1 in { 0 };

            then

             A40: x1 = 0 by TARSKI:def 1;

            now

              per cases by A1, A38, XBOOLE_0:def 3;

                suppose x2 in { 0 };

                then

                 A41: x2 = 0 by TARSKI:def 1;

                (ma . x9) = (Ma . [x1, x2]) by A36, A37, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A17, A36, A37, FUNCT_1: 49

                .= ( max ( 0 , 0 )) by A40, A41, REAL_LAT:def 2

                .= 0 ;

                then (ma . x9) in { 0 } by TARSKI:def 1;

                hence (ma . x9) in B by A9, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : (1 / 2) < x & x <= 1 };

                then

                consider y2 be Real such that

                 A42: x2 = y2 and

                 A43: (1 / 2) < y2 & y2 <= 1;

                reconsider y2 as Real;

                (ma . x9) = (Ma . [x1, x2]) by A36, A37, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A17, A36, A37, FUNCT_1: 49

                .= ( max ( 0 ,y2)) by A40, A42, REAL_LAT:def 2;

                then (ma . x9) = 0 or (ma . x9) = y2 by XXREAL_0: 16;

                then (ma . x9) in { 0 } or (ma . x9) in { x where x be Real : (1 / 2) < x & x <= 1 } by A43, TARSKI:def 1;

                hence (ma . x9) in B by A9, XBOOLE_0:def 3;

              end;

            end;

            hence (ma . x9) in B;

          end;

            suppose x1 in { x where x be Real : (1 / 2) < x & x <= 1 };

            then

            consider y1 be Real such that

             A44: x1 = y1 and

             A45: (1 / 2) < y1 & y1 <= 1;

            reconsider y1 as Real;

            now

              per cases by A1, A38, XBOOLE_0:def 3;

                suppose x2 in { 0 };

                then

                 A46: x2 = 0 by TARSKI:def 1;

                (ma . x9) = (Ma . [x1, x2]) by A36, A37, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A17, A36, A37, FUNCT_1: 49

                .= ( max (y1, 0 )) by A44, A46, REAL_LAT:def 2;

                then (ma . x9) = y1 or (ma . x9) = 0 by XXREAL_0: 16;

                then (ma . x9) in { x where x be Real : (1 / 2) < x & x <= 1 } or (ma . x9) in { 0 } by A45, TARSKI:def 1;

                hence (ma . x9) in B by A9, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : (1 / 2) < x & x <= 1 };

                then

                consider y2 be Real such that

                 A47: x2 = y2 and

                 A48: (1 / 2) < y2 & y2 <= 1;

                reconsider y2 as Real;

                (ma . x9) = (Ma . [x1, x2]) by A36, A37, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A17, A36, A37, FUNCT_1: 49

                .= ( max (y1,y2)) by A44, A47, REAL_LAT:def 2;

                then (ma . x9) = y1 or (ma . x9) = y2 by XXREAL_0: 16;

                then (ma . x9) in { x where x be Real : (1 / 2) < x & x <= 1 } by A45, A48;

                hence (ma . x9) in B by A9, XBOOLE_0:def 3;

              end;

            end;

            hence (ma . x9) in B;

          end;

        end;

        hence (ma . x9) in B;

      end;

      reconsider mi as BinOp of B by A19, A20, FUNCT_2: 3;

      reconsider ma as BinOp of B by A34, A35, FUNCT_2: 3;

      reconsider L9 = LattStr (# B, ma, mi #) as non empty LattStr;

       A49:

      now

        let a,b be Element of L9;

        

        thus (a "\/" b) = (the L_join of L9 . (a,b)) by LATTICES:def 1

        .= (( maxreal || A) . [a, b]) by FUNCT_1: 49

        .= ( maxreal . (a,b)) by A17, FUNCT_1: 49;

        

        thus (a "/\" b) = (the L_meet of L9 . (a,b)) by LATTICES:def 2

        .= (( minreal || A) . [a, b]) by FUNCT_1: 49

        .= ( minreal . (a,b)) by A17, FUNCT_1: 49;

      end;

      reconsider L as complete Lattice by Th20;

       A50:

      now

        let x1 be Element of B;

        now

          per cases by A9, XBOOLE_0:def 3;

            suppose x1 in { 0 };

            then x1 = 0 by TARSKI:def 1;

            hence x1 is Element of L by A10, A13, RCOMP_1:def 1;

          end;

            suppose x1 in { x where x be Real : (1 / 2) < x & x <= 1 };

            then ex y be Real st x1 = y & (1 / 2) < y & y <= 1;

            then x1 in { r : 0 <= r & r <= 1 };

            hence x1 is Element of L by A13, RCOMP_1:def 1;

          end;

        end;

        hence x1 is Element of L;

      end;

       A51:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A50;

        reconsider p9, q9 as Element of R by A13, A18;

        

        thus (p "\/" q) = ( maxreal . (p,q)) by A49

        .= ( maxreal . (q9,p9)) by REAL_LAT: 1

        .= (q "\/" p) by A49;

      end;

       A52:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A50;

        reconsider p9, q9 as Element of R by A13, A18;

        

        thus (p "/\" (p "\/" q)) = ( minreal . (p,(p "\/" q))) by A49

        .= ( minreal . (p9,( maxreal . (p9,q9)))) by A49

        .= p by REAL_LAT: 6;

      end;

       A53:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A50;

        reconsider p9, q9 as Element of R by A13, A18;

        

        thus (p "/\" q) = ( minreal . (p,q)) by A49

        .= ( minreal . (q9,p9)) by REAL_LAT: 2

        .= (q "/\" p) by A49;

      end;

       A54:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A50;

        reconsider p9, q9 as Element of R by A13, A18;

        

        thus ((p "/\" q) "\/" q) = ( maxreal . ((p "/\" q),q)) by A49

        .= ( maxreal . (( minreal . (p9,q9)),q9)) by A49

        .= q by REAL_LAT: 5;

      end;

       A55:

      now

        let p,q,r be Element of L9;

        reconsider p9 = p, q9 = q, r9 = r as Element of L by A50;

        reconsider p9, q9, r9 as Element of R by A13, A18;

        

        thus (p "/\" (q "/\" r)) = ( minreal . (p,(q "/\" r))) by A49

        .= ( minreal . (p,( minreal . (q,r)))) by A49

        .= ( minreal . (( minreal . (p9,q9)),r9)) by REAL_LAT: 4

        .= ( minreal . ((p "/\" q),r)) by A49

        .= ((p "/\" q) "/\" r) by A49;

      end;

      now

        let p,q,r be Element of L9;

        reconsider p9 = p, q9 = q, r9 = r as Element of L by A50;

        reconsider p9, q9, r9 as Element of R by A13, A18;

        

        thus (p "\/" (q "\/" r)) = ( maxreal . (p,(q "\/" r))) by A49

        .= ( maxreal . (p,( maxreal . (q,r)))) by A49

        .= ( maxreal . (( maxreal . (p9,q9)),r9)) by REAL_LAT: 3

        .= ( maxreal . ((p "\/" q),r)) by A49

        .= ((p "\/" q) "\/" r) by A49;

      end;

      then L9 is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A51, A54, A53, A55, A52, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

      then

      reconsider L9 as Lattice;

      reconsider L9 as SubLattice of ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL )))) by A13, A12, A11, A16, NAT_LAT:def 12;

      take L9;

      now

        let X be Subset of L9;

        thus ( "\/" (X,L)) in the carrier of L9

        proof

           0 in { r : 0 <= r & r <= 1 };

          then

          reconsider w = 0 as Element of L by A13, RCOMP_1:def 1;

          

           A56: X is_less_than ( "\/" (X,L)) by LATTICE3:def 21;

          ( "\/" (X,L)) in [. 0 , 1.] by A13;

          then ( "\/" (X,L)) in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

          then

          consider y be Real such that

           A57: y = ( "\/" (X,L)) and 0 <= y and

           A58: y <= 1;

          reconsider y as Real;

          assume

           A59: not ( "\/" (X,L)) in the carrier of L9;

          then not ( "\/" (X,L)) in { x where x be Real : (1 / 2) < x & x <= 1 } by A9, XBOOLE_0:def 3;

          then

           A60: y <= (1 / 2) by A57, A58;

          now

            let z9 be object;

            assume

             A61: z9 in X;

            then

            reconsider z = z9 as Element of L9;

            reconsider z as Element of L by A13, A14;

            

             A62: z [= ( "\/" (X,L)) by A56, A61;

            reconsider z1 = z as Real;

            reconsider z1 as Real;

            ( min (z1,y)) = ( minreal . (z1,( "\/" (X,L)))) by A57, REAL_LAT:def 1

            .= (( minreal || A) . [z, ( "\/" (X,L))]) by A13, FUNCT_1: 49

            .= (( minreal || A) . (z,( "\/" (X,L))))

            .= (z "/\" ( "\/" (X,L))) by A11, LATTICES:def 2

            .= z1 by A62, LATTICES: 4;

            then z1 <= y by XXREAL_0:def 9;

            then (y + z1) <= ((1 / 2) + y) by A60, XREAL_1: 7;

            then for v be Real holds not (z1 = v & (1 / 2) < v & v <= 1) by XREAL_1: 6;

            then not z1 in { x where x be Real : (1 / 2) < x & x <= 1 };

            hence z9 in { 0 } by A9, XBOOLE_0:def 3;

          end;

          then

           A63: X c= { 0 };

          now

            per cases by A63, ZFMISC_1: 33;

              suppose

               A64: X = {} ;

               A65:

              now

                let r1 be Element of L;

                assume X is_less_than r1;

                r1 in [. 0 , 1.] by A13;

                then r1 in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

                then

                consider e be Real such that

                 A66: r1 = e and

                 A67: 0 <= e and e <= 1;

                reconsider e as Real;

                (w "/\" r1) = (( minreal || A) . (w,r1)) by A11, LATTICES:def 2

                .= ( minreal . [w, r1]) by A13, FUNCT_1: 49

                .= ( minreal . (w,r1))

                .= ( min ( 0 ,e)) by A66, REAL_LAT:def 1

                .= w by A67, XXREAL_0:def 9;

                hence w [= r1 by LATTICES: 4;

              end;

              for q be Element of L st q in X holds q [= w by A64;

              then X is_less_than w;

              then ( "\/" (X,L)) = w by A65, LATTICE3:def 21;

              then ( "\/" (X,L)) in { 0 } by TARSKI:def 1;

              hence contradiction by A9, A59, XBOOLE_0:def 3;

            end;

              suppose X = { 0 };

              then ( "\/" (X,L)) = w by LATTICE3: 42;

              then ( "\/" (X,L)) in { 0 } by TARSKI:def 1;

              hence contradiction by A9, A59, XBOOLE_0:def 3;

            end;

          end;

          hence contradiction;

        end;

      end;

      hence L9 is \/-inheriting;

      now

        (1 / 2) in { x where x be Real : 0 <= x & x <= 1 };

        then

        reconsider z = (1 / 2) as Element of L by A13, RCOMP_1:def 1;

        set X = { x where x be Real : (1 / 2) < x & x <= 1 };

        for y be Real holds not (y = (1 / 2) & (1 / 2) < y & y <= 1);

        then

         A68: ( not (1 / 2) in { 0 }) & not (1 / 2) in { x where x be Real : (1 / 2) < x & x <= 1 } by TARSKI:def 1;

        for x1 be object st x1 in { x where x be Real : (1 / 2) < x & x <= 1 } holds x1 in B by A9, XBOOLE_0:def 3;

        then

        reconsider X as Subset of L9 by TARSKI:def 3;

        take X;

         A69:

        now

          let b be Element of L;

          b in A by A13;

          then b in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

          then

          consider b9 be Real such that

           A70: b = b9 and

           A71: 0 <= b9 and

           A72: b9 <= 1;

          reconsider b9 as Real;

          assume

           A73: b is_less_than X;

          

           A74: b9 <= (1 / 2)

          proof

            assume

             A75: (1 / 2) < b9;

            then b9 in X by A72;

            then

             A76: b = ( "/\" (X,L)) by A70, A73, LATTICE3: 41;

            ((1 / 2) + b9) < (b9 + b9) by A75, XREAL_1: 6;

            then

             A77: (((1 / 2) + b9) / 2) < ((b9 + b9) / 2) by XREAL_1: 74;

            then ((((1 / 2) + b9) / 2) + b9) <= (b9 + 1) by A72, XREAL_1: 7;

            then

             A78: (((1 / 2) + b9) / 2) <= 1 by XREAL_1: 6;

            then (((1 / 2) + b9) / 2) in { r : 0 <= r & r <= 1 } by A71;

            then

            reconsider c = (((1 / 2) + b9) / 2) as Element of L by A13, RCOMP_1:def 1;

            reconsider cc = c as Real;

            ((1 / 2) + (1 / 2)) < (b9 + (1 / 2)) by A75, XREAL_1: 6;

            then (1 / 2) < (((1 / 2) + b9) / 2) by XREAL_1: 74;

            then (((1 / 2) + b9) / 2) in X by A78;

            then b [= c by A76, LATTICE3: 38;

            

            then b9 = (b "/\" c) by A70, LATTICES: 4

            .= (( minreal || A) . (b,c)) by A11, LATTICES:def 2

            .= ( minreal . [b, c]) by A13, FUNCT_1: 49

            .= ( minreal . (b,cc))

            .= ( min (b9,(((1 / 2) + b9) / 2))) by A70, REAL_LAT:def 1;

            hence contradiction by A77, XXREAL_0:def 9;

          end;

          (b "/\" z) = (( minreal || A) . (b,z)) by A11, LATTICES:def 2

          .= ( minreal . [b, z]) by A13, FUNCT_1: 49

          .= ( minreal . (b,z))

          .= ( min (b9,jd)) by A70, REAL_LAT:def 1

          .= b by A70, A74, XXREAL_0:def 9;

          hence b [= z by LATTICES: 4;

        end;

        now

          let q be Element of L;

          assume q in X;

          then

           A79: ex y be Real st q = y & (1 / 2) < y & y <= 1;

          q in A by A13;

          then q in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

          then

          consider q9 be Real such that

           A80: q = q9 and 0 <= q9 and q9 <= 1;

          reconsider q9 as Real;

          (z "/\" q) = (( minreal || A) . (z,q)) by A11, LATTICES:def 2

          .= ( minreal . [z, q]) by A13, FUNCT_1: 49

          .= ( minreal . (z,q))

          .= ( min (jd,q9)) by A80, REAL_LAT:def 1

          .= z by A80, A79, XXREAL_0:def 9;

          hence z [= q by LATTICES: 4;

        end;

        then z is_less_than X;

        then ( "/\" (X,L)) = jd by A69, LATTICE3: 34;

        hence not ( "/\" (X,L)) in the carrier of L9 by A1, A68, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_7:22

    ex L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting non /\-inheriting

    proof

      reconsider L = ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL )))) as complete Lattice by Th20;

      take L;

      thus thesis by Th21;

    end;

    theorem :: MSUALG_7:23

    

     Th23: ex L9 be SubLattice of ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL )))) st L9 is /\-inheriting non \/-inheriting

    proof

      set B = ( { 0 , 1} \/ ]. 0 , (1 / 2).[);

      set L = ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL ))));

      set R = Real_Lattice ;

      

       A1: B c= ( {1} \/ { x where x be Real : 0 <= x & x < (1 / 2) })

      proof

        let x1 be object;

        assume

         A2: x1 in B;

        now

          per cases by A2, XBOOLE_0:def 3;

            suppose x1 in { 0 , 1};

            then x1 = 0 or x1 = 1 by TARSKI:def 2;

            then x1 in {1} or x1 in { x where x be Real : 0 <= x & x < (1 / 2) } by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose x1 in ]. 0 , (1 / 2).[;

            then x1 in { r : 0 < r & r < (1 / 2) } by RCOMP_1:def 2;

            then

            consider y be Real such that

             A3: x1 = y and

             A4: 0 < y & y < (1 / 2);

            y in { x where x be Real : 0 <= x & x < (1 / 2) } by A4;

            hence thesis by A3, XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

      ( {1} \/ { x where x be Real : 0 <= x & x < (1 / 2) }) c= B

      proof

        let x1 be object;

        assume

         A5: x1 in ( {1} \/ { x where x be Real : 0 <= x & x < (1 / 2) });

        now

          per cases by A5, XBOOLE_0:def 3;

            suppose x1 in {1};

            then x1 = 1 by TARSKI:def 1;

            then x1 in { 0 , 1} by TARSKI:def 2;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose x1 in { x where x be Real : 0 <= x & x < (1 / 2) };

            then

            consider y be Real such that

             A6: x1 = y and

             A7: 0 <= y & y < (1 / 2);

            y in { r : 0 < r & r < (1 / 2) } or y = 0 by A7;

            then y in ]. 0 , (1 / 2).[ or y in { 0 , 1} by RCOMP_1:def 2, TARSKI:def 2;

            hence thesis by A6, XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

      then

       A8: B = ( {1} \/ { x where x be Real : 0 <= x & x < (1 / 2) }) by A1, XBOOLE_0:def 10;

      

       A9: 1 in { r : 0 <= r & r <= 1 };

      then

      reconsider A = [. 0 , 1.] as non empty set by RCOMP_1:def 1;

      

       A10: for x1 be Element of A holds x1 is Element of R by REAL_LAT:def 3, XREAL_0:def 1;

      reconsider B as non empty set;

      

       A11: the L_meet of L = ( minreal || [. 0 , 1.]) by Def4;

      set Ma = ( maxreal || A), Mi = ( minreal || A);

      

       A12: the L_join of L = ( maxreal || [. 0 , 1.]) by Def4;

      

       A13: A = the carrier of L by Def4;

      then

      reconsider Ma, Mi as BinOp of A by Def4;

       A14:

      now

        let x1 be object;

        assume

         A15: x1 in B;

        now

          per cases by A1, A15, XBOOLE_0:def 3;

            suppose x1 in {1};

            then x1 = 1 by TARSKI:def 1;

            hence x1 in A by A9, RCOMP_1:def 1;

          end;

            suppose x1 in { x where x be Real : 0 <= x & x < (1 / 2) };

            then

            consider y be Real such that

             A16: x1 = y & 0 <= y and

             A17: y < (1 / 2);

            (y + (1 / 2)) <= ((1 / 2) + 1) by A17, XREAL_1: 7;

            then y <= 1 by XREAL_1: 6;

            then x1 in { r : 0 <= r & r <= 1 } by A16;

            hence x1 in A by RCOMP_1:def 1;

          end;

        end;

        hence x1 in A;

      end;

      then

       A18: B c= A;

      then

       A19: [:B, B:] c= [:A, A:] by ZFMISC_1: 96;

      then

      reconsider ma = (Ma || B), mi = (Mi || B) as Function of [:B, B:], A by FUNCT_2: 32;

      

       A20: ( dom ma) = [:B, B:] by FUNCT_2:def 1;

       A21:

      now

        let x9 be object;

        assume

         A22: x9 in ( dom ma);

        then

        consider x1,x2 be object such that

         A23: x9 = [x1, x2] by RELAT_1:def 1;

        

         A24: x2 in B by A22, A23, ZFMISC_1: 87;

        

         A25: x1 in B by A22, A23, ZFMISC_1: 87;

        now

          per cases by A1, A25, XBOOLE_0:def 3;

            suppose x1 in {1};

            then

             A26: x1 = 1 by TARSKI:def 1;

            now

              per cases by A1, A24, XBOOLE_0:def 3;

                suppose x2 in {1};

                then

                 A27: x2 = 1 by TARSKI:def 1;

                (ma . x9) = (Ma . [x1, x2]) by A22, A23, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A19, A22, A23, FUNCT_1: 49

                .= ( max (jj,jj)) by A26, A27, REAL_LAT:def 2

                .= 1;

                then (ma . x9) in {1} by TARSKI:def 1;

                hence (ma . x9) in B by A8, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : 0 <= x & x < (1 / 2) };

                then

                consider y2 be Real such that

                 A28: x2 = y2 and

                 A29: 0 <= y2 & y2 < (1 / 2);

                reconsider y2 as Real;

                (ma . x9) = (Ma . [x1, x2]) by A22, A23, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A19, A22, A23, FUNCT_1: 49

                .= ( max (jj,y2)) by A26, A28, REAL_LAT:def 2;

                then (ma . x9) = 1 or (ma . x9) = y2 by XXREAL_0: 16;

                then (ma . x9) in {1} or (ma . x9) in { x where x be Real : 0 <= x & x < (1 / 2) } by A29, TARSKI:def 1;

                hence (ma . x9) in B by A8, XBOOLE_0:def 3;

              end;

            end;

            hence (ma . x9) in B;

          end;

            suppose x1 in { x where x be Real : 0 <= x & x < (1 / 2) };

            then

            consider y1 be Real such that

             A30: x1 = y1 and

             A31: 0 <= y1 & y1 < (1 / 2);

            reconsider y1 as Real;

            now

              per cases by A1, A24, XBOOLE_0:def 3;

                suppose x2 in {1};

                then

                 A32: x2 = 1 by TARSKI:def 1;

                (ma . x9) = (Ma . [x1, x2]) by A22, A23, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A19, A22, A23, FUNCT_1: 49

                .= ( max (y1,jj)) by A30, A32, REAL_LAT:def 2;

                then (ma . x9) = y1 or (ma . x9) = 1 by XXREAL_0: 16;

                then (ma . x9) in { x where x be Real : 0 <= x & x < (1 / 2) } or (ma . x9) in {1} by A31, TARSKI:def 1;

                hence (ma . x9) in B by A8, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : 0 <= x & x < (1 / 2) };

                then

                consider y2 be Real such that

                 A33: x2 = y2 and

                 A34: 0 <= y2 & y2 < (1 / 2);

                reconsider y2 as Real;

                (ma . x9) = (Ma . [x1, x2]) by A22, A23, FUNCT_1: 49

                .= ( maxreal . (x1,x2)) by A19, A22, A23, FUNCT_1: 49

                .= ( max (y1,y2)) by A30, A33, REAL_LAT:def 2;

                then (ma . x9) = y1 or (ma . x9) = y2 by XXREAL_0: 16;

                then (ma . x9) in { x where x be Real : 0 <= x & x < (1 / 2) } by A31, A34;

                hence (ma . x9) in B by A8, XBOOLE_0:def 3;

              end;

            end;

            hence (ma . x9) in B;

          end;

        end;

        hence (ma . x9) in B;

      end;

      

       A35: ( dom mi) = [:B, B:] by FUNCT_2:def 1;

       A36:

      now

        let x9 be object;

        assume

         A37: x9 in ( dom mi);

        then

        consider x1,x2 be object such that

         A38: x9 = [x1, x2] by RELAT_1:def 1;

        

         A39: x2 in B by A37, A38, ZFMISC_1: 87;

        

         A40: x1 in B by A37, A38, ZFMISC_1: 87;

        now

          per cases by A1, A40, XBOOLE_0:def 3;

            suppose x1 in {1};

            then

             A41: x1 = 1 by TARSKI:def 1;

            now

              per cases by A1, A39, XBOOLE_0:def 3;

                suppose x2 in {1};

                then

                 A42: x2 = 1 by TARSKI:def 1;

                (mi . x9) = (Mi . [x1, x2]) by A37, A38, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A19, A37, A38, FUNCT_1: 49

                .= ( min (jj,jj)) by A41, A42, REAL_LAT:def 1

                .= 1;

                then (mi . x9) in {1} by TARSKI:def 1;

                hence (mi . x9) in B by A8, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : 0 <= x & x < (1 / 2) };

                then

                consider y2 be Real such that

                 A43: x2 = y2 and

                 A44: 0 <= y2 & y2 < (1 / 2);

                reconsider y2 as Real;

                (mi . x9) = (Mi . [x1, x2]) by A37, A38, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A19, A37, A38, FUNCT_1: 49

                .= ( min (jj,y2)) by A41, A43, REAL_LAT:def 1;

                then (mi . x9) = 1 or (mi . x9) = y2 by XXREAL_0: 15;

                then (mi . x9) in {1} or (mi . x9) in { x where x be Real : 0 <= x & x < (1 / 2) } by A44, TARSKI:def 1;

                hence (mi . x9) in B by A8, XBOOLE_0:def 3;

              end;

            end;

            hence (mi . x9) in B;

          end;

            suppose x1 in { x where x be Real : 0 <= x & x < (1 / 2) };

            then

            consider y1 be Real such that

             A45: x1 = y1 and

             A46: 0 <= y1 & y1 < (1 / 2);

            reconsider y1 as Real;

            now

              per cases by A1, A39, XBOOLE_0:def 3;

                suppose x2 in {1};

                then

                 A47: x2 = 1 by TARSKI:def 1;

                (mi . x9) = (Mi . [x1, x2]) by A37, A38, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A19, A37, A38, FUNCT_1: 49

                .= ( min (y1,jj)) by A45, A47, REAL_LAT:def 1;

                then (mi . x9) = y1 or (mi . x9) = 1 by XXREAL_0: 15;

                then (mi . x9) in { x where x be Real : 0 <= x & x < (1 / 2) } or (mi . x9) in {1} by A46, TARSKI:def 1;

                hence (mi . x9) in B by A8, XBOOLE_0:def 3;

              end;

                suppose x2 in { x where x be Real : 0 <= x & x < (1 / 2) };

                then

                consider y2 be Real such that

                 A48: x2 = y2 and

                 A49: 0 <= y2 & y2 < (1 / 2);

                reconsider y2 as Real;

                (mi . x9) = (Mi . [x1, x2]) by A37, A38, FUNCT_1: 49

                .= ( minreal . (x1,x2)) by A19, A37, A38, FUNCT_1: 49

                .= ( min (y1,y2)) by A45, A48, REAL_LAT:def 1;

                then (mi . x9) = y1 or (mi . x9) = y2 by XXREAL_0: 15;

                then (mi . x9) in { x where x be Real : 0 <= x & x < (1 / 2) } by A46, A49;

                hence (mi . x9) in B by A8, XBOOLE_0:def 3;

              end;

            end;

            hence (mi . x9) in B;

          end;

        end;

        hence (mi . x9) in B;

      end;

      reconsider L as complete Lattice by Th20;

      reconsider mi as BinOp of B by A35, A36, FUNCT_2: 3;

      reconsider ma as BinOp of B by A20, A21, FUNCT_2: 3;

      reconsider L9 = LattStr (# B, ma, mi #) as non empty LattStr;

       A50:

      now

        let a,b be Element of L9;

        

        thus (a "\/" b) = (the L_join of L9 . (a,b)) by LATTICES:def 1

        .= (( maxreal || A) . [a, b]) by FUNCT_1: 49

        .= ( maxreal . (a,b)) by A19, FUNCT_1: 49;

        

        thus (a "/\" b) = (the L_meet of L9 . (a,b)) by LATTICES:def 2

        .= (( minreal || A) . [a, b]) by FUNCT_1: 49

        .= ( minreal . (a,b)) by A19, FUNCT_1: 49;

      end;

       A51:

      now

        let x1 be Element of B;

        per cases by A8, XBOOLE_0:def 3;

          suppose x1 in {1};

          then x1 = 1 by TARSKI:def 1;

          hence x1 is Element of L by A9, A13, RCOMP_1:def 1;

        end;

          suppose x1 in { x where x be Real : 0 <= x & x < (1 / 2) };

          then

          consider y be Real such that

           A52: x1 = y & 0 <= y and

           A53: y < (1 / 2);

          (y + (1 / 2)) <= ((1 / 2) + 1) by A53, XREAL_1: 7;

          then y <= 1 by XREAL_1: 6;

          then x1 in { r : 0 <= r & r <= 1 } by A52;

          hence x1 is Element of L by A13, RCOMP_1:def 1;

        end;

      end;

       A54:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A51;

        reconsider p9, q9 as Element of R by A13, A10;

        

        thus (p "\/" q) = ( maxreal . (p,q)) by A50

        .= ( maxreal . (q9,p9)) by REAL_LAT: 1

        .= (q "\/" p) by A50;

      end;

       A55:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A51;

        reconsider p9, q9 as Element of R by A13, A10;

        

        thus (p "/\" (p "\/" q)) = ( minreal . (p,(p "\/" q))) by A50

        .= ( minreal . (p9,( maxreal . (p9,q9)))) by A50

        .= p by REAL_LAT: 6;

      end;

       A56:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A51;

        reconsider p9, q9 as Element of R by A13, A10;

        

        thus (p "/\" q) = ( minreal . (p,q)) by A50

        .= ( minreal . (q9,p9)) by REAL_LAT: 2

        .= (q "/\" p) by A50;

      end;

       A57:

      now

        let p,q be Element of L9;

        reconsider p9 = p, q9 = q as Element of L by A51;

        reconsider p9, q9 as Element of R by A13, A10;

        

        thus ((p "/\" q) "\/" q) = ( maxreal . ((p "/\" q),q)) by A50

        .= ( maxreal . (( minreal . (p9,q9)),q9)) by A50

        .= q by REAL_LAT: 5;

      end;

       A58:

      now

        let p,q,r be Element of L9;

        reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;

        reconsider p9, q9, r9 as Element of R by A13, A10;

        

        thus (p "/\" (q "/\" r)) = ( minreal . (p,(q "/\" r))) by A50

        .= ( minreal . (p,( minreal . (q,r)))) by A50

        .= ( minreal . (( minreal . (p9,q9)),r9)) by REAL_LAT: 4

        .= ( minreal . ((p "/\" q),r)) by A50

        .= ((p "/\" q) "/\" r) by A50;

      end;

      now

        let p,q,r be Element of L9;

        reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;

        reconsider p9, q9, r9 as Element of R by A13, A10;

        

        thus (p "\/" (q "\/" r)) = ( maxreal . (p,(q "\/" r))) by A50

        .= ( maxreal . (p,( maxreal . (q,r)))) by A50

        .= ( maxreal . (( maxreal . (p9,q9)),r9)) by REAL_LAT: 3

        .= ( maxreal . ((p "\/" q),r)) by A50

        .= ((p "\/" q) "\/" r) by A50;

      end;

      then L9 is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A54, A57, A56, A58, A55, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

      then

      reconsider L9 as Lattice;

      reconsider L9 as SubLattice of ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL )))) by A13, A12, A11, A18, NAT_LAT:def 12;

      take L9;

      now

        let X be Subset of L9;

        thus ( "/\" (X,L)) in the carrier of L9

        proof

          1 in { r : 0 <= r & r <= 1 };

          then

          reconsider w = 1 as Element of L by A13, RCOMP_1:def 1;

          

           A59: ( "/\" (X,L)) is_less_than X by LATTICE3: 34;

          ( "/\" (X,L)) in [. 0 , 1.] by A13;

          then ( "/\" (X,L)) in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

          then

          consider y be Real such that

           A60: y = ( "/\" (X,L)) and

           A61: 0 <= y and y <= 1;

          reconsider y as Real;

          assume

           A62: not ( "/\" (X,L)) in the carrier of L9;

          then not ( "/\" (X,L)) in { x where x be Real : 0 <= x & x < (1 / 2) } by A8, XBOOLE_0:def 3;

          then

           A63: (1 / 2) <= y by A60, A61;

          now

            let z9 be object;

            assume

             A64: z9 in X;

            then

            reconsider z = z9 as Element of L9;

            reconsider z as Element of L by A13, A14;

            

             A65: ( "/\" (X,L)) [= z by A59, A64;

            reconsider z1 = z as Real;

            reconsider z1 as Real;

            ( min (z1,y)) = ( minreal . (z1,( "/\" (X,L)))) by A60, REAL_LAT:def 1

            .= (( minreal || A) . [z, ( "/\" (X,L))]) by A13, FUNCT_1: 49

            .= (( minreal || A) . (z,( "/\" (X,L))))

            .= (z "/\" ( "/\" (X,L))) by A11, LATTICES:def 2

            .= y by A60, A65, LATTICES: 4;

            then y <= z1 by XXREAL_0:def 9;

            then (y + (1 / 2)) <= (z1 + y) by A63, XREAL_1: 7;

            then for v be Real holds not (z1 = v & 0 <= v & v < (1 / 2)) by XREAL_1: 6;

            then not z1 in { x where x be Real : 0 <= x & x < (1 / 2) };

            hence z9 in {1} by A8, XBOOLE_0:def 3;

          end;

          then

           A66: X c= {1};

          now

            per cases by A66, ZFMISC_1: 33;

              suppose

               A67: X = {} ;

               A68:

              now

                let r1 be Element of L;

                assume r1 is_less_than X;

                r1 in [. 0 , 1.] by A13;

                then r1 in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

                then

                consider e be Real such that

                 A69: r1 = e and 0 <= e and

                 A70: e <= 1;

                reconsider e as Real;

                (r1 "/\" w) = (( minreal || A) . (r1,w)) by A11, LATTICES:def 2

                .= ( minreal . [r1, w]) by A13, FUNCT_1: 49

                .= ( minreal . (r1,w))

                .= ( min (e,jj)) by A69, REAL_LAT:def 1

                .= r1 by A69, A70, XXREAL_0:def 9;

                hence r1 [= w by LATTICES: 4;

              end;

              for q be Element of L st q in X holds w [= q by A67;

              then w is_less_than X;

              then ( "/\" (X,L)) = w by A68, LATTICE3: 34;

              then ( "/\" (X,L)) in {1} by TARSKI:def 1;

              hence contradiction by A8, A62, XBOOLE_0:def 3;

            end;

              suppose X = {1};

              then ( "/\" (X,L)) = w by LATTICE3: 42;

              then ( "/\" (X,L)) in {1} by TARSKI:def 1;

              hence contradiction by A8, A62, XBOOLE_0:def 3;

            end;

          end;

          hence contradiction;

        end;

      end;

      hence L9 is /\-inheriting;

      now

        (1 / 2) in { x where x be Real : 0 <= x & x <= 1 };

        then

        reconsider z = (1 / 2) as Element of L by A13, RCOMP_1:def 1;

        set X = { x where x be Real : 0 <= x & x < (1 / 2) };

        for y be Real holds not (y = (1 / 2) & 0 <= y & y < (1 / 2));

        then

         A71: ( not (1 / 2) in {1}) & not (1 / 2) in { x where x be Real : 0 <= x & x < (1 / 2) } by TARSKI:def 1;

        for x1 be object st x1 in { x where x be Real : 0 <= x & x < (1 / 2) } holds x1 in B by A8, XBOOLE_0:def 3;

        then

        reconsider X as Subset of L9 by TARSKI:def 3;

        take X;

         A72:

        now

          let b be Element of L;

          b in A by A13;

          then b in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

          then

          consider b9 be Real such that

           A73: b = b9 and

           A74: 0 <= b9 and

           A75: b9 <= 1;

          reconsider b9 as Real;

          assume

           A76: X is_less_than b;

          

           A77: (1 / 2) <= b9

          proof

            ((1 / 2) + b9) <= (1 + 1) by A75, XREAL_1: 7;

            then (((1 / 2) + b9) / 2) <= ((1 + 1) / 2) by XREAL_1: 72;

            then (((1 / 2) + b9) / 2) in { r : 0 <= r & r <= 1 } by A74;

            then

            reconsider c = (((1 / 2) + b9) / 2) as Element of L by A13, RCOMP_1:def 1;

            reconsider cc = c as Real;

            assume

             A78: b9 < (1 / 2);

            then (b9 + b9) < ((1 / 2) + b9) by XREAL_1: 6;

            then

             A79: ((b9 + b9) / 2) < (((1 / 2) + b9) / 2) by XREAL_1: 74;

            (b9 + (1 / 2)) < ((1 / 2) + (1 / 2)) by A78, XREAL_1: 6;

            then (((1 / 2) + b9) / 2) < (1 / 2) by XREAL_1: 74;

            then

             A80: ((jd + b9) / 2) in X by A74;

            b9 in X by A74, A78;

            then b = ( "\/" (X,L)) by A73, A76, LATTICE3: 40;

            then c [= b by A80, LATTICE3: 38;

            

            then (((1 / 2) + b9) / 2) = (c "/\" b) by LATTICES: 4

            .= (( minreal || A) . (c,b)) by A11, LATTICES:def 2

            .= ( minreal . [c, b]) by A13, FUNCT_1: 49

            .= ( minreal . (cc,b))

            .= ( min ((((1 / 2) + b9) / 2),b9)) by A73, REAL_LAT:def 1;

            hence contradiction by A79, XXREAL_0:def 9;

          end;

          (z "/\" b) = (( minreal || A) . (z,b)) by A11, LATTICES:def 2

          .= ( minreal . [z, b]) by A13, FUNCT_1: 49

          .= ( minreal . (z,b))

          .= ( min (jd,b9)) by A73, REAL_LAT:def 1

          .= z by A77, XXREAL_0:def 9;

          hence z [= b by LATTICES: 4;

        end;

        now

          let q be Element of L;

          assume q in X;

          then

           A81: ex y be Real st q = y & 0 <= y & y < (1 / 2);

          q in A by A13;

          then q in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;

          then

          consider q9 be Real such that

           A82: q = q9 and 0 <= q9 and q9 <= 1;

          reconsider q9 as Real;

          (q "/\" z) = (( minreal || A) . (q,z)) by A11, LATTICES:def 2

          .= ( minreal . [q, z]) by A13, FUNCT_1: 49

          .= ( minreal . (q,z))

          .= ( min (q9,jd)) by A82, REAL_LAT:def 1

          .= q by A82, A81, XXREAL_0:def 9;

          hence q [= z by LATTICES: 4;

        end;

        then X is_less_than z;

        then ( "\/" (X,L)) = (1 / 2) by A72, LATTICE3:def 21;

        hence not ( "\/" (X,L)) in the carrier of L9 by A1, A71, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_7:24

    ex L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting non \/-inheriting

    proof

      reconsider L = ( RealSubLatt (( In ( 0 , REAL )),( In (1, REAL )))) as complete Lattice by Th20;

      take L;

      thus thesis by Th23;

    end;