yellow11.miz



    begin

    reserve x for set;

    theorem :: YELLOW11:1

    3 = { 0 , 1, 2} by CARD_1: 51;

    theorem :: YELLOW11:2

    

     Th2: (2 \ 1) = {1}

    proof

      thus (2 \ 1) c= {1}

      proof

        let x be object;

        assume

         A1: x in (2 \ 1);

        then

         A2: x = 0 or x = 1 by CARD_1: 50, TARSKI:def 2;

         not x in { 0 } by A1, CARD_1: 49, XBOOLE_0:def 5;

        hence thesis by A2, TARSKI:def 1;

      end;

      let x be object;

      assume x in {1};

      then

       A3: x = 1 by TARSKI:def 1;

      then

       A4: not x in { 0 } by TARSKI:def 1;

      x in { 0 , 1} by A3, TARSKI:def 2;

      hence thesis by A4, CARD_1: 49, CARD_1: 50, XBOOLE_0:def 5;

    end;

    theorem :: YELLOW11:3

    

     Th3: (3 \ 1) = {1, 2}

    proof

      thus (3 \ 1) c= {1, 2}

      proof

        let x be object;

        assume

         A1: x in (3 \ 1);

        then

         A2: x = 0 or x = 1 or x = 2 by CARD_1: 51, ENUMSET1:def 1;

         not x in { 0 } by A1, CARD_1: 49, XBOOLE_0:def 5;

        hence thesis by A2, TARSKI:def 1, TARSKI:def 2;

      end;

      thus {1, 2} c= (3 \ 1)

      proof

        let x be object;

        assume x in {1, 2};

        then

         A3: x = 1 or x = 2 by TARSKI:def 2;

        then

         A4: not x in { 0 } by TARSKI:def 1;

        x in { 0 , 1, 2} by A3, ENUMSET1:def 1;

        hence thesis by A4, CARD_1: 49, CARD_1: 51, XBOOLE_0:def 5;

      end;

    end;

    theorem :: YELLOW11:4

    

     Th4: (3 \ 2) = {2}

    proof

      thus (3 \ 2) c= {2}

      proof

        let x be object;

        assume

         A1: x in (3 \ 2);

        then

         A2: x = 0 or x = 1 or x = 2 by CARD_1: 51, ENUMSET1:def 1;

         not x in { 0 , 1} by A1, CARD_1: 50, XBOOLE_0:def 5;

        hence thesis by A2, TARSKI:def 1, TARSKI:def 2;

      end;

      thus {2} c= (3 \ 2)

      proof

        let x be object;

        assume x in {2};

        then

         A3: x = 2 by TARSKI:def 1;

        then

         A4: not x in { 0 , 1} by TARSKI:def 2;

        x in { 0 , 1, 2} by A3, ENUMSET1:def 1;

        hence thesis by A4, CARD_1: 50, CARD_1: 51, XBOOLE_0:def 5;

      end;

    end;

    

     Lm1: (3 \ 2) c= (3 \ 1)

    proof

      let x be object;

      assume x in (3 \ 2);

      then x = 2 by Th4, TARSKI:def 1;

      hence thesis by Th3, TARSKI:def 2;

    end;

    begin

    theorem :: YELLOW11:5

    

     Th5: for L be antisymmetric reflexive with_infima with_suprema RelStr holds for a,b be Element of L holds (a "/\" b) = b iff (a "\/" b) = a

    proof

      let L be antisymmetric reflexive with_infima with_suprema RelStr;

      let a,b be Element of L;

      thus (a "/\" b) = b implies (a "\/" b) = a

      proof

        assume (a "/\" b) = b;

        then b <= a by YELLOW_0: 23;

        hence thesis by YELLOW_0: 24;

      end;

      assume (a "\/" b) = a;

      then b <= a by YELLOW_0: 22;

      hence thesis by YELLOW_0: 25;

    end;

    theorem :: YELLOW11:6

    

     Th6: for L be LATTICE holds for a,b,c be Element of L holds ((a "/\" b) "\/" (a "/\" c)) <= (a "/\" (b "\/" c))

    proof

      let L be LATTICE;

      let a,b,c be Element of L;

      

       A1: a <= a;

      c <= (b "\/" c) by YELLOW_0: 22;

      then

       A2: (a "/\" c) <= (a "/\" (b "\/" c)) by A1, YELLOW_3: 2;

      b <= (b "\/" c) by YELLOW_0: 22;

      then (a "/\" b) <= (a "/\" (b "\/" c)) by A1, YELLOW_3: 2;

      hence thesis by A2, YELLOW_5: 9;

    end;

    theorem :: YELLOW11:7

    

     Th7: for L be LATTICE holds for a,b,c be Element of L holds (a "\/" (b "/\" c)) <= ((a "\/" b) "/\" (a "\/" c))

    proof

      let L be LATTICE;

      let a,b,c be Element of L;

      

       A1: a <= a;

      (b "/\" c) <= c by YELLOW_0: 23;

      then

       A2: (a "\/" (b "/\" c)) <= (a "\/" c) by A1, YELLOW_3: 3;

      (b "/\" c) <= b by YELLOW_0: 23;

      then (a "\/" (b "/\" c)) <= (a "\/" b) by A1, YELLOW_3: 3;

      hence thesis by A2, YELLOW_0: 23;

    end;

    theorem :: YELLOW11:8

    

     Th8: for L be LATTICE holds for a,b,c be Element of L holds a <= c implies (a "\/" (b "/\" c)) <= ((a "\/" b) "/\" c)

    proof

      let L be LATTICE;

      let a,b,c be Element of L;

      

       A1: (b "/\" c) <= c by YELLOW_0: 23;

      

       A2: a <= a;

      (b "/\" c) <= b by YELLOW_0: 23;

      then

       A3: (a "\/" (b "/\" c)) <= (a "\/" b) by A2, YELLOW_3: 3;

      assume a <= c;

      then (a "\/" (b "/\" c)) <= c by A1, YELLOW_0: 22;

      hence thesis by A3, YELLOW_0: 23;

    end;

    definition

      :: YELLOW11:def1

      func N_5 -> RelStr equals ( InclPoset { 0 , (3 \ 1), 2, (3 \ 2), 3});

      correctness ;

    end

    registration

      cluster N_5 -> strict reflexive transitive antisymmetric;

      correctness ;

      cluster N_5 -> with_infima with_suprema;

      correctness

      proof

        set Z = { 0 , (3 \ 1), 2, (3 \ 2), 3};

        set N = ( InclPoset Z);

        

         A1: N is with_infima

        proof

          let x,y be Element of N;

          

           A2: Z = the carrier of N by YELLOW_1: 1;

          thus ex z be Element of N st z <= x & z <= y & for z9 be Element of N st z9 <= x & z9 <= y holds z9 <= z

          proof

            per cases by A2, ENUMSET1:def 3;

              suppose x = 0 & y = 0 ;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A3: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A3, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A4: w <= x and

               A5: w <= y;

              

               A6: w c= y by A5, YELLOW_1: 3;

              w c= x by A4, YELLOW_1: 3;

              then w c= (x /\ y) by A6, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = (3 \ 1);

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A7: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A7, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A8: w <= x and

               A9: w <= y;

              

               A10: w c= y by A9, YELLOW_1: 3;

              w c= x by A8, YELLOW_1: 3;

              then w c= (x /\ y) by A10, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = 2;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A11: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A11, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A12: w <= x and

               A13: w <= y;

              

               A14: w c= y by A13, YELLOW_1: 3;

              w c= x by A12, YELLOW_1: 3;

              then w c= (x /\ y) by A14, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = (3 \ 2);

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A15: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A15, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A16: w <= x and

               A17: w <= y;

              

               A18: w c= y by A17, YELLOW_1: 3;

              w c= x by A16, YELLOW_1: 3;

              then w c= (x /\ y) by A18, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = 3;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A19: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A19, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A20: w <= x and

               A21: w <= y;

              

               A22: w c= y by A21, YELLOW_1: 3;

              w c= x by A20, YELLOW_1: 3;

              then w c= (x /\ y) by A22, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (3 \ 1) & y = 0 ;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A23: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A23, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A24: w <= x and

               A25: w <= y;

              

               A26: w c= y by A25, YELLOW_1: 3;

              w c= x by A24, YELLOW_1: 3;

              then w c= (x /\ y) by A26, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (3 \ 1) & y = (3 \ 1);

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A27: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A27, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A28: w <= x and

               A29: w <= y;

              

               A30: w c= y by A29, YELLOW_1: 3;

              w c= x by A28, YELLOW_1: 3;

              then w c= (x /\ y) by A30, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A31: x = (3 \ 1) & y = 2;

               0 in Z by ENUMSET1:def 3;

              then

              reconsider z = 0 as Element of N by YELLOW_1: 1;

              take z;

              

               A32: z c= y;

              z c= x;

              hence z <= x & z <= y by A32, YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A33: z9 <= x and

               A34: z9 <= y;

              

               A35: z9 c= (3 \ 1) by A31, A33, YELLOW_1: 3;

               A36:

              now

                assume z9 = 2;

                then 0 in z9 by CARD_1: 50, TARSKI:def 2;

                hence contradiction by A35, Th3, TARSKI:def 2;

              end;

              

               A37: z9 c= 2 by A31, A34, YELLOW_1: 3;

               A38:

              now

                assume z9 = 3;

                then

                 A39: 2 in z9 by CARD_1: 51, ENUMSET1:def 1;

                 not 2 in 2;

                hence contradiction by A37, A39;

              end;

               A40:

              now

                assume z9 = (3 \ 2);

                then

                 A41: 2 in z9 by Th4, TARSKI:def 1;

                 not 2 in 2;

                hence contradiction by A37, A41;

              end;

               A42:

              now

                assume z9 = (3 \ 1);

                then

                 A43: 2 in z9 by Th3, TARSKI:def 2;

                 not 2 in 2;

                hence contradiction by A37, A43;

              end;

              z9 is Element of Z by YELLOW_1: 1;

              hence thesis by A42, A36, A40, A38, ENUMSET1:def 3;

            end;

              suppose x = (3 \ 1) & y = (3 \ 2);

              then

              reconsider z = (x /\ y) as Element of N by Th3, Th4, ZFMISC_1: 13;

              take z;

              

               A44: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A44, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A45: w <= x and

               A46: w <= y;

              

               A47: w c= y by A46, YELLOW_1: 3;

              w c= x by A45, YELLOW_1: 3;

              then w c= (x /\ y) by A47, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A48: x = (3 \ 1) & y = 3;

              ((3 \ 1) /\ 3) = ((3 /\ 3) \ 1) by XBOOLE_1: 49

              .= (3 \ 1);

              then

              reconsider z = (x /\ y) as Element of N by A48;

              take z;

              

               A49: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A49, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A50: w <= x and

               A51: w <= y;

              

               A52: w c= y by A51, YELLOW_1: 3;

              w c= x by A50, YELLOW_1: 3;

              then w c= (x /\ y) by A52, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 2 & y = 0 ;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A53: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A53, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A54: w <= x and

               A55: w <= y;

              

               A56: w c= y by A55, YELLOW_1: 3;

              w c= x by A54, YELLOW_1: 3;

              then w c= (x /\ y) by A56, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A57: x = 2 & y = (3 \ 1);

               0 in Z by ENUMSET1:def 3;

              then

              reconsider z = 0 as Element of N by YELLOW_1: 1;

              take z;

              

               A58: z c= y;

              z c= x;

              hence z <= x & z <= y by A58, YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A59: z9 <= x and

               A60: z9 <= y;

              

               A61: z9 c= (3 \ 1) by A57, A60, YELLOW_1: 3;

               A62:

              now

                assume z9 = 2;

                then 0 in z9 by CARD_1: 50, TARSKI:def 2;

                hence contradiction by A61, Th3, TARSKI:def 2;

              end;

              

               A63: z9 c= 2 by A57, A59, YELLOW_1: 3;

               A64:

              now

                assume z9 = 3;

                then

                 A65: 2 in z9 by CARD_1: 51, ENUMSET1:def 1;

                 not 2 in 2;

                hence contradiction by A63, A65;

              end;

               A66:

              now

                assume z9 = (3 \ 2);

                then

                 A67: 2 in z9 by Th4, TARSKI:def 1;

                 not 2 in 2;

                hence contradiction by A63, A67;

              end;

               A68:

              now

                assume z9 = (3 \ 1);

                then

                 A69: 2 in z9 by Th3, TARSKI:def 2;

                 not 2 in 2;

                hence contradiction by A63, A69;

              end;

              z9 is Element of Z by YELLOW_1: 1;

              hence thesis by A68, A62, A66, A64, ENUMSET1:def 3;

            end;

              suppose x = 2 & y = 2;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A70: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A70, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A71: w <= x and

               A72: w <= y;

              

               A73: w c= y by A72, YELLOW_1: 3;

              w c= x by A71, YELLOW_1: 3;

              then w c= (x /\ y) by A73, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A74: x = 2 & y = (3 \ 2);

              2 misses (3 \ 2) by XBOOLE_1: 79;

              then (2 /\ (3 \ 2)) = 0 ;

              then (x /\ y) in Z by A74, ENUMSET1:def 3;

              then

              reconsider z = (x /\ y) as Element of N by YELLOW_1: 1;

              take z;

              

               A75: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A75, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A76: w <= x and

               A77: w <= y;

              

               A78: w c= y by A77, YELLOW_1: 3;

              w c= x by A76, YELLOW_1: 3;

              then w c= (x /\ y) by A78, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A79: x = 2 & y = 3;

              ( Segm 2) c= ( Segm 3) by NAT_1: 39;

              then

              reconsider z = (x /\ y) as Element of N by A79, XBOOLE_1: 28;

              take z;

              

               A80: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A80, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A81: w <= x and

               A82: w <= y;

              

               A83: w c= y by A82, YELLOW_1: 3;

              w c= x by A81, YELLOW_1: 3;

              then w c= (x /\ y) by A83, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (3 \ 2) & y = 0 ;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A84: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A84, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A85: w <= x and

               A86: w <= y;

              

               A87: w c= y by A86, YELLOW_1: 3;

              w c= x by A85, YELLOW_1: 3;

              then w c= (x /\ y) by A87, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (3 \ 2) & y = (3 \ 1);

              then

              reconsider z = (x /\ y) as Element of N by Th3, Th4, ZFMISC_1: 13;

              take z;

              

               A88: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A88, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A89: w <= x and

               A90: w <= y;

              

               A91: w c= y by A90, YELLOW_1: 3;

              w c= x by A89, YELLOW_1: 3;

              then w c= (x /\ y) by A91, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A92: x = (3 \ 2) & y = 2;

              2 misses (3 \ 2) by XBOOLE_1: 79;

              then (2 /\ (3 \ 2)) = 0 ;

              then (x /\ y) in Z by A92, ENUMSET1:def 3;

              then

              reconsider z = (x /\ y) as Element of N by YELLOW_1: 1;

              take z;

              

               A93: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A93, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A94: w <= x and

               A95: w <= y;

              

               A96: w c= y by A95, YELLOW_1: 3;

              w c= x by A94, YELLOW_1: 3;

              then w c= (x /\ y) by A96, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (3 \ 2) & y = (3 \ 2);

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A97: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A97, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A98: w <= x and

               A99: w <= y;

              

               A100: w c= y by A99, YELLOW_1: 3;

              w c= x by A98, YELLOW_1: 3;

              then w c= (x /\ y) by A100, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A101: x = (3 \ 2) & y = 3;

              ((3 \ 2) /\ 3) = ((3 /\ 3) \ 2) by XBOOLE_1: 49

              .= (3 \ 2);

              then

              reconsider z = (x /\ y) as Element of N by A101;

              take z;

              

               A102: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A102, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A103: w <= x and

               A104: w <= y;

              

               A105: w c= y by A104, YELLOW_1: 3;

              w c= x by A103, YELLOW_1: 3;

              then w c= (x /\ y) by A105, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 3 & y = 0 ;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A106: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A106, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A107: w <= x and

               A108: w <= y;

              

               A109: w c= y by A108, YELLOW_1: 3;

              w c= x by A107, YELLOW_1: 3;

              then w c= (x /\ y) by A109, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A110: x = 3 & y = (3 \ 1);

              ((3 \ 1) /\ 3) = ((3 /\ 3) \ 1) by XBOOLE_1: 49

              .= (3 \ 1);

              then

              reconsider z = (x /\ y) as Element of N by A110;

              take z;

              

               A111: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A111, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A112: w <= x and

               A113: w <= y;

              

               A114: w c= y by A113, YELLOW_1: 3;

              w c= x by A112, YELLOW_1: 3;

              then w c= (x /\ y) by A114, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A115: x = 3 & y = 2;

              ( Segm 2) c= ( Segm 3) by NAT_1: 39;

              then

              reconsider z = (x /\ y) as Element of N by A115, XBOOLE_1: 28;

              take z;

              

               A116: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A116, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A117: w <= x and

               A118: w <= y;

              

               A119: w c= y by A118, YELLOW_1: 3;

              w c= x by A117, YELLOW_1: 3;

              then w c= (x /\ y) by A119, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A120: x = 3 & y = (3 \ 2);

              ((3 \ 2) /\ 3) = ((3 /\ 3) \ 2) by XBOOLE_1: 49

              .= (3 \ 2);

              then

              reconsider z = (x /\ y) as Element of N by A120;

              take z;

              

               A121: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A121, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A122: w <= x and

               A123: w <= y;

              

               A124: w c= y by A123, YELLOW_1: 3;

              w c= x by A122, YELLOW_1: 3;

              then w c= (x /\ y) by A124, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 3 & y = 3;

              then

              reconsider z = (x /\ y) as Element of N;

              take z;

              

               A125: z c= y by XBOOLE_1: 17;

              z c= x by XBOOLE_1: 17;

              hence z <= x & z <= y by A125, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A126: w <= x and

               A127: w <= y;

              

               A128: w c= y by A127, YELLOW_1: 3;

              w c= x by A126, YELLOW_1: 3;

              then w c= (x /\ y) by A128, XBOOLE_1: 19;

              hence thesis by YELLOW_1: 3;

            end;

          end;

        end;

        now

          let x,y be set;

          assume that

           A129: x in Z and

           A130: y in Z;

          

           A131: x = 0 or x = (3 \ 1) or x = 2 or x = (3 \ 2) or x = 3 by A129, ENUMSET1:def 3;

          ( Segm 2) c= ( Segm 3) by NAT_1: 39;

          then

           A132: (2 \/ 3) = 3 by XBOOLE_1: 12;

          

           A133: (2 \/ (3 \ 2)) = (2 \/ 3) by XBOOLE_1: 39;

          

           A134: ((3 \ 1) \/ 2) = { 0 , 1, 1, 2} by Th3, CARD_1: 50, ENUMSET1: 5

          .= {1, 1, 0 , 2} by ENUMSET1: 67

          .= {1, 0 , 2} by ENUMSET1: 31

          .= { 0 , 1, 2} by ENUMSET1: 58;

          

           A135: ((3 \ 1) \/ 3) = 3 by XBOOLE_1: 12;

          

           A136: y = 0 or y = (3 \ 1) or y = 2 or y = (3 \ 2) or y = 3 by A130, ENUMSET1:def 3;

          

           A137: ((3 \ 2) \/ 3) = 3 by XBOOLE_1: 12;

          ((3 \ 1) \/ (3 \ 2)) = {1, 2} by Th3, Th4, ZFMISC_1: 9;

          hence (x \/ y) in Z by A131, A136, A134, A135, A133, A132, A137, Th3, CARD_1: 51, ENUMSET1:def 3;

        end;

        hence thesis by A1, YELLOW_1: 11;

      end;

    end

    definition

      :: YELLOW11:def2

      func M_3 -> RelStr equals ( InclPoset { 0 , 1, (2 \ 1), (3 \ 2), 3});

      correctness ;

    end

    registration

      cluster M_3 -> strict reflexive transitive antisymmetric;

      correctness ;

      cluster M_3 -> with_infima with_suprema;

      correctness

      proof

        set Z = { 0 , 1, (2 \ 1), (3 \ 2), 3};

        set N = ( InclPoset Z);

        

         A1: N is with_suprema

        proof

          let x,y be Element of N;

          

           A2: Z = the carrier of N by YELLOW_1: 1;

          thus ex z be Element of N st x <= z & y <= z & for z9 be Element of N st x <= z9 & y <= z9 holds z <= z9

          proof

            per cases by A2, ENUMSET1:def 3;

              suppose x = 0 & y = 0 ;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A3: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A3, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A4: x <= w and

               A5: y <= w;

              

               A6: y c= w by A5, YELLOW_1: 3;

              x c= w by A4, YELLOW_1: 3;

              then (x \/ y) c= w by A6, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = 1;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A7: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A7, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A8: x <= w and

               A9: y <= w;

              

               A10: y c= w by A9, YELLOW_1: 3;

              x c= w by A8, YELLOW_1: 3;

              then (x \/ y) c= w by A10, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = (2 \ 1);

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A11: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A11, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A12: x <= w and

               A13: y <= w;

              

               A14: y c= w by A13, YELLOW_1: 3;

              x c= w by A12, YELLOW_1: 3;

              then (x \/ y) c= w by A14, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = (3 \ 2);

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A15: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A15, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A16: x <= w and

               A17: y <= w;

              

               A18: y c= w by A17, YELLOW_1: 3;

              x c= w by A16, YELLOW_1: 3;

              then (x \/ y) c= w by A18, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 0 & y = 3;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A19: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A19, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A20: x <= w and

               A21: y <= w;

              

               A22: y c= w by A21, YELLOW_1: 3;

              x c= w by A20, YELLOW_1: 3;

              then (x \/ y) c= w by A22, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 1 & y = 0 ;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A23: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A23, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A24: x <= w and

               A25: y <= w;

              

               A26: y c= w by A25, YELLOW_1: 3;

              x c= w by A24, YELLOW_1: 3;

              then (x \/ y) c= w by A26, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 1 & y = 1;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A27: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A27, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A28: x <= w and

               A29: y <= w;

              

               A30: y c= w by A29, YELLOW_1: 3;

              x c= w by A28, YELLOW_1: 3;

              then (x \/ y) c= w by A30, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A31: x = 1 & y = (2 \ 1);

              3 in Z by ENUMSET1:def 3;

              then

              reconsider z = 3 as Element of N by YELLOW_1: 1;

              take z;

              x c= z & y c= z

              proof

                thus x c= z

                proof

                  let X be object;

                  assume X in x;

                  then X = 0 by A31, CARD_1: 49, TARSKI:def 1;

                  hence thesis by CARD_1: 51, ENUMSET1:def 1;

                end;

                let X be object;

                assume X in y;

                then X = 1 by A31, Th2, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              hence x <= z & y <= z by YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A32: x <= z9 and

               A33: y <= z9;

              

               A34: z9 is Element of Z by YELLOW_1: 1;

              

               A35: (2 \ 1) c= z9 by A31, A33, YELLOW_1: 3;

               A36:

              now

                1 in (2 \ 1) by Th2, TARSKI:def 1;

                then

                 A37: 1 in z9 by A35;

                assume z9 = 1;

                hence contradiction by A37;

              end;

              

               A38: 1 c= z9 by A31, A32, YELLOW_1: 3;

               A39:

              now

                

                 A40: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (2 \ 1);

                hence contradiction by A38, A40, Th2, TARSKI:def 1;

              end;

               A41:

              now

                

                 A42: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (3 \ 2);

                hence contradiction by A38, A42, Th4, TARSKI:def 1;

              end;

              z9 <> 0 by A38;

              hence thesis by A34, A36, A39, A41, ENUMSET1:def 3;

            end;

              suppose

               A43: x = 1 & y = (3 \ 2);

              3 in Z by ENUMSET1:def 3;

              then

              reconsider z = 3 as Element of N by YELLOW_1: 1;

              take z;

              x c= z

              proof

                let X be object;

                assume X in x;

                then X = 0 by A43, CARD_1: 49, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              hence x <= z & y <= z by A43, YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A44: x <= z9 and

               A45: y <= z9;

              

               A46: z9 is Element of Z by YELLOW_1: 1;

              

               A47: (3 \ 2) c= z9 by A43, A45, YELLOW_1: 3;

               A48:

              now

                assume

                 A49: z9 = 1;

                2 in (3 \ 2) by Th4, TARSKI:def 1;

                hence contradiction by A47, A49, CARD_1: 49, TARSKI:def 1;

              end;

              

               A50: 1 c= z9 by A43, A44, YELLOW_1: 3;

               A51:

              now

                

                 A52: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (2 \ 1);

                hence contradiction by A50, A52, Th2, TARSKI:def 1;

              end;

               A53:

              now

                

                 A54: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (3 \ 2);

                hence contradiction by A50, A54, Th4, TARSKI:def 1;

              end;

              z9 <> 0 by A50;

              hence thesis by A46, A48, A51, A53, ENUMSET1:def 3;

            end;

              suppose

               A55: x = 1 & y = 3;

              ( Segm 1) c= ( Segm 3)

              proof

                let X be object;

                assume X in ( Segm 1);

                then X = 0 by CARD_1: 49, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              then

              reconsider z = (x \/ y) as Element of N by A55, XBOOLE_1: 12;

              take z;

              

               A56: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A56, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A57: x <= w and

               A58: y <= w;

              

               A59: y c= w by A58, YELLOW_1: 3;

              x c= w by A57, YELLOW_1: 3;

              then (x \/ y) c= w by A59, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (2 \ 1) & y = 0 ;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A60: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A60, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A61: x <= w and

               A62: y <= w;

              

               A63: y c= w by A62, YELLOW_1: 3;

              x c= w by A61, YELLOW_1: 3;

              then (x \/ y) c= w by A63, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A64: x = (2 \ 1) & y = 1;

              3 in Z by ENUMSET1:def 3;

              then

              reconsider z = 3 as Element of N by YELLOW_1: 1;

              take z;

              x c= z & y c= z

              proof

                thus x c= z

                proof

                  let X be object;

                  assume X in x;

                  then X = 1 by A64, Th2, TARSKI:def 1;

                  hence thesis by CARD_1: 51, ENUMSET1:def 1;

                end;

                let X be object;

                assume X in y;

                then X = 0 by A64, CARD_1: 49, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              hence x <= z & y <= z by YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A65: x <= z9 and

               A66: y <= z9;

              

               A67: z9 is Element of Z by YELLOW_1: 1;

              

               A68: (2 \ 1) c= z9 by A64, A65, YELLOW_1: 3;

               A69:

              now

                1 in (2 \ 1) by Th2, TARSKI:def 1;

                then

                 A70: 1 in z9 by A68;

                assume z9 = 1;

                hence contradiction by A70;

              end;

              

               A71: 1 c= z9 by A64, A66, YELLOW_1: 3;

               A72:

              now

                

                 A73: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (2 \ 1);

                hence contradiction by A71, A73, Th2, TARSKI:def 1;

              end;

               A74:

              now

                

                 A75: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (3 \ 2);

                hence contradiction by A71, A75, Th4, TARSKI:def 1;

              end;

              z9 <> 0 by A71;

              hence thesis by A67, A69, A72, A74, ENUMSET1:def 3;

            end;

              suppose x = (2 \ 1) & y = (2 \ 1);

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A76: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A76, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A77: x <= w and

               A78: y <= w;

              

               A79: y c= w by A78, YELLOW_1: 3;

              x c= w by A77, YELLOW_1: 3;

              then (x \/ y) c= w by A79, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A80: x = (2 \ 1) & y = (3 \ 2);

              3 in Z by ENUMSET1:def 3;

              then

              reconsider z = 3 as Element of N by YELLOW_1: 1;

              take z;

              x c= z & y c= z

              proof

                thus x c= z

                proof

                  let X be object;

                  assume X in x;

                  then X = 1 by A80, Th2, TARSKI:def 1;

                  hence thesis by CARD_1: 51, ENUMSET1:def 1;

                end;

                let X be object;

                assume X in y;

                hence thesis by A80;

              end;

              hence x <= z & y <= z by YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A81: x <= z9 and

               A82: y <= z9;

              

               A83: z9 is Element of Z by YELLOW_1: 1;

              

               A84: (3 \ 2) c= z9 by A80, A82, YELLOW_1: 3;

               A85:

              now

                assume

                 A86: z9 = (2 \ 1);

                2 in (3 \ 2) by Th4, TARSKI:def 1;

                hence contradiction by A84, A86, Th2, TARSKI:def 1;

              end;

              

               A87: (2 \ 1) c= z9 by A80, A81, YELLOW_1: 3;

               A88:

              now

                assume

                 A89: z9 = (3 \ 2);

                1 in (2 \ 1) by Th2, TARSKI:def 1;

                hence contradiction by A87, A89, Th4, TARSKI:def 1;

              end;

               A90:

              now

                1 in (2 \ 1) by Th2, TARSKI:def 1;

                then

                 A91: 1 in z9 by A87;

                assume z9 = 1;

                hence contradiction by A91;

              end;

              z9 <> 0 by A87, Th2;

              hence thesis by A83, A90, A85, A88, ENUMSET1:def 3;

            end;

              suppose

               A92: x = (2 \ 1) & y = 3;

              (2 \ 1) c= 3

              proof

                let X be object;

                assume X in (2 \ 1);

                then X = 1 by Th2, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              then

              reconsider z = (x \/ y) as Element of N by A92, XBOOLE_1: 12;

              take z;

              

               A93: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A93, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A94: x <= w and

               A95: y <= w;

              

               A96: y c= w by A95, YELLOW_1: 3;

              x c= w by A94, YELLOW_1: 3;

              then (x \/ y) c= w by A96, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (3 \ 2) & y = 0 ;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A97: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A97, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A98: x <= w and

               A99: y <= w;

              

               A100: y c= w by A99, YELLOW_1: 3;

              x c= w by A98, YELLOW_1: 3;

              then (x \/ y) c= w by A100, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A101: x = (3 \ 2) & y = 1;

              3 in Z by ENUMSET1:def 3;

              then

              reconsider z = 3 as Element of N by YELLOW_1: 1;

              take z;

              y c= z

              proof

                let X be object;

                assume X in y;

                then X = 0 by A101, CARD_1: 49, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              hence x <= z & y <= z by A101, YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A102: x <= z9 and

               A103: y <= z9;

              

               A104: z9 is Element of Z by YELLOW_1: 1;

              

               A105: (3 \ 2) c= z9 by A101, A102, YELLOW_1: 3;

               A106:

              now

                assume

                 A107: z9 = 1;

                2 in (3 \ 2) by Th4, TARSKI:def 1;

                hence contradiction by A105, A107, CARD_1: 49, TARSKI:def 1;

              end;

              

               A108: 1 c= z9 by A101, A103, YELLOW_1: 3;

               A109:

              now

                

                 A110: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (2 \ 1);

                hence contradiction by A108, A110, Th2, TARSKI:def 1;

              end;

               A111:

              now

                

                 A112: 0 in 1 by CARD_1: 49, TARSKI:def 1;

                assume z9 = (3 \ 2);

                hence contradiction by A108, A112, Th4, TARSKI:def 1;

              end;

              z9 <> 0 by A108;

              hence thesis by A104, A106, A109, A111, ENUMSET1:def 3;

            end;

              suppose

               A113: x = (3 \ 2) & y = (2 \ 1);

              3 in Z by ENUMSET1:def 3;

              then

              reconsider z = 3 as Element of N by YELLOW_1: 1;

              take z;

              x c= z & y c= z

              proof

                thus x c= z by A113;

                let X be object;

                assume X in y;

                then X = 1 by A113, Th2, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              hence x <= z & y <= z by YELLOW_1: 3;

              let z9 be Element of N;

              assume that

               A114: x <= z9 and

               A115: y <= z9;

              

               A116: z9 is Element of Z by YELLOW_1: 1;

              

               A117: (3 \ 2) c= z9 by A113, A114, YELLOW_1: 3;

               A118:

              now

                assume

                 A119: z9 = (2 \ 1);

                2 in (3 \ 2) by Th4, TARSKI:def 1;

                hence contradiction by A117, A119, Th2, TARSKI:def 1;

              end;

              

               A120: (2 \ 1) c= z9 by A113, A115, YELLOW_1: 3;

               A121:

              now

                assume

                 A122: z9 = (3 \ 2);

                1 in (2 \ 1) by Th2, TARSKI:def 1;

                hence contradiction by A120, A122, Th4, TARSKI:def 1;

              end;

               A123:

              now

                1 in (2 \ 1) by Th2, TARSKI:def 1;

                then

                 A124: 1 in z9 by A120;

                assume z9 = 1;

                hence contradiction by A124;

              end;

              z9 <> 0 by A120, Th2;

              hence thesis by A116, A123, A118, A121, ENUMSET1:def 3;

            end;

              suppose x = (3 \ 2) & y = (3 \ 2);

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A125: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A125, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A126: x <= w and

               A127: y <= w;

              

               A128: y c= w by A127, YELLOW_1: 3;

              x c= w by A126, YELLOW_1: 3;

              then (x \/ y) c= w by A128, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = (3 \ 2) & y = 3;

              then

              reconsider z = (x \/ y) as Element of N by XBOOLE_1: 12;

              take z;

              

               A129: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A129, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A130: x <= w and

               A131: y <= w;

              

               A132: y c= w by A131, YELLOW_1: 3;

              x c= w by A130, YELLOW_1: 3;

              then (x \/ y) c= w by A132, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 3 & y = 0 ;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A133: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A133, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A134: x <= w and

               A135: y <= w;

              

               A136: y c= w by A135, YELLOW_1: 3;

              x c= w by A134, YELLOW_1: 3;

              then (x \/ y) c= w by A136, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A137: x = 3 & y = 1;

              ( Segm 1) c= ( Segm 3)

              proof

                let X be object;

                assume X in ( Segm 1);

                then X = 0 by CARD_1: 49, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              then

              reconsider z = (x \/ y) as Element of N by A137, XBOOLE_1: 12;

              take z;

              

               A138: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A138, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A139: x <= w and

               A140: y <= w;

              

               A141: y c= w by A140, YELLOW_1: 3;

              x c= w by A139, YELLOW_1: 3;

              then (x \/ y) c= w by A141, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose

               A142: x = 3 & y = (2 \ 1);

              (2 \ 1) c= 3

              proof

                let X be object;

                assume X in (2 \ 1);

                then X = 1 by Th2, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              then

              reconsider z = (x \/ y) as Element of N by A142, XBOOLE_1: 12;

              take z;

              

               A143: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A143, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A144: x <= w and

               A145: y <= w;

              

               A146: y c= w by A145, YELLOW_1: 3;

              x c= w by A144, YELLOW_1: 3;

              then (x \/ y) c= w by A146, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 3 & y = (3 \ 2);

              then

              reconsider z = (x \/ y) as Element of N by XBOOLE_1: 12;

              take z;

              

               A147: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A147, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A148: x <= w and

               A149: y <= w;

              

               A150: y c= w by A149, YELLOW_1: 3;

              x c= w by A148, YELLOW_1: 3;

              then (x \/ y) c= w by A150, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

              suppose x = 3 & y = 3;

              then

              reconsider z = (x \/ y) as Element of N;

              take z;

              

               A151: y c= z by XBOOLE_1: 7;

              x c= z by XBOOLE_1: 7;

              hence x <= z & y <= z by A151, YELLOW_1: 3;

              let w be Element of N;

              assume that

               A152: x <= w and

               A153: y <= w;

              

               A154: y c= w by A153, YELLOW_1: 3;

              x c= w by A152, YELLOW_1: 3;

              then (x \/ y) c= w by A154, XBOOLE_1: 8;

              hence thesis by YELLOW_1: 3;

            end;

          end;

        end;

        now

          now

            let x be object;

            assume

             A155: x in ((2 \ 1) /\ (3 \ 2));

            then x in (2 \ 1) by XBOOLE_0:def 4;

            then

             A156: x = 1 by Th2, TARSKI:def 1;

            x in (3 \ 2) by A155, XBOOLE_0:def 4;

            hence contradiction by A156, Th4, TARSKI:def 1;

          end;

          then

           A157: ((2 \ 1) /\ (3 \ 2)) = 0 by XBOOLE_0:def 1;

          

           A158: ((3 \ 2) /\ 3) = (3 \ 2) by XBOOLE_1: 28;

          (2 \ 1) c= 3

          proof

            let x be object;

            assume x in (2 \ 1);

            then x = 1 by Th2, TARSKI:def 1;

            hence thesis by CARD_1: 51, ENUMSET1:def 1;

          end;

          then

           A159: ((2 \ 1) /\ 3) = (2 \ 1) by XBOOLE_1: 28;

          ( Segm 1) c= ( Segm 3) by NAT_1: 39;

          then

           A160: (1 /\ 3) = 1 by XBOOLE_1: 28;

          now

            let x be object;

            assume

             A161: x in (1 /\ (3 \ 2));

            then x in 1 by XBOOLE_0:def 4;

            then

             A162: x = 0 by CARD_1: 49, TARSKI:def 1;

            x in (3 \ 2) by A161, XBOOLE_0:def 4;

            hence contradiction by A162, Th4, TARSKI:def 1;

          end;

          then

           A163: (1 /\ (3 \ 2)) = 0 by XBOOLE_0:def 1;

          1 misses (2 \ 1) by XBOOLE_1: 79;

          then

           A164: (1 /\ (2 \ 1)) = 0 ;

          let x,y be set;

          assume that

           A165: x in Z and

           A166: y in Z;

          

           A167: y = 0 or y = 1 or y = (2 \ 1) or y = (3 \ 2) or y = 3 by A166, ENUMSET1:def 3;

          x = 0 or x = 1 or x = (2 \ 1) or x = (3 \ 2) or x = 3 by A165, ENUMSET1:def 3;

          hence (x /\ y) in Z by A167, A164, A163, A160, A157, A159, A158, ENUMSET1:def 3;

        end;

        hence thesis by A1, YELLOW_1: 12;

      end;

    end

    theorem :: YELLOW11:9

    

     Th9: for L be LATTICE holds (ex K be full Sublattice of L st ( N_5 ,K) are_isomorphic ) iff ex a,b,c,d,e be Element of L st (a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e

    proof

      set cn = the carrier of N_5 ;

      let L be LATTICE;

      

       A1: cn = { 0 , (3 \ 1), 2, (3 \ 2), 3} by YELLOW_1: 1;

      thus (ex K be full Sublattice of L st ( N_5 ,K) are_isomorphic ) implies ex a,b,c,d,e be Element of L st (a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e

      proof

        reconsider td = (3 \ 2) as Element of N_5 by A1, ENUMSET1:def 3;

        reconsider dw = 2 as Element of N_5 by A1, ENUMSET1:def 3;

        reconsider t = 3 as Element of N_5 by A1, ENUMSET1:def 3;

        reconsider tj = (3 \ 1) as Element of N_5 by A1, ENUMSET1:def 3;

        reconsider cl = the carrier of L as non empty set;

        reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;

        given K be full Sublattice of L such that

         A2: ( N_5 ,K) are_isomorphic ;

        consider f be Function of N_5 , K such that

         A3: f is isomorphic by A2;

        

         A4: K is non empty by A3, WAYBEL_0:def 38;

        then

         A5: f is one-to-one monotone by A3, WAYBEL_0:def 38;

        reconsider K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;

        reconsider ck = the carrier of K as non empty set;

        

         A6: ck = ( rng f) by A3, WAYBEL_0: 66;

        reconsider g = f as Function of cn, ck;

        reconsider a = (g . z), b = (g . td), c = (g . dw), d = (g . tj), e = (g . t) as Element of K;

        reconsider ck as non empty Subset of cl by YELLOW_0:def 13;

        

         A7: b in ck;

        

         A8: c in ck;

        

         A9: e in ck;

        

         A10: d in ck;

        a in ck;

        then

        reconsider A = a, B = b, C = c, D = d, E = e as Element of L by A7, A8, A10, A9;

        take A, B, C, D, E;

        thus A <> B by A5, Th4, WAYBEL_1:def 1;

        thus A <> C by A5, WAYBEL_1:def 1;

        thus A <> D by A5, Th3, WAYBEL_1:def 1;

        thus A <> E by A5, WAYBEL_1:def 1;

        now

          assume (f . td) = (f . dw);

          then

           A11: td = dw by A4, A5, WAYBEL_1:def 1;

          2 in td by Th4, TARSKI:def 1;

          hence contradiction by A11;

        end;

        hence B <> C;

        now

          

           A12: 1 in tj by Th3, TARSKI:def 2;

          assume

           A13: (f . td) = (f . tj);

           not 1 in td by Th4, TARSKI:def 1;

          hence contradiction by A4, A5, A13, A12, WAYBEL_1:def 1;

        end;

        hence B <> D;

        now

          

           A14: 1 in t by CARD_1: 51, ENUMSET1:def 1;

          assume

           A15: (f . td) = (f . t);

           not 1 in td by Th4, TARSKI:def 1;

          hence contradiction by A4, A5, A15, A14, WAYBEL_1:def 1;

        end;

        hence B <> E;

        now

          assume (f . dw) = (f . tj);

          then

           A16: dw = tj by A4, A5, WAYBEL_1:def 1;

          2 in tj by Th3, TARSKI:def 2;

          hence contradiction by A16;

        end;

        hence C <> D;

        thus C <> E by A5, WAYBEL_1:def 1;

        now

          

           A17: 0 in t by CARD_1: 51, ENUMSET1:def 1;

          assume

           A18: (f . tj) = (f . t);

           not 0 in tj by Th3, TARSKI:def 2;

          hence contradiction by A4, A5, A18, A17, WAYBEL_1:def 1;

        end;

        hence D <> E;

        z c= td;

        then z <= td by YELLOW_1: 3;

        then a <= b by A3, WAYBEL_0: 66;

        then A <= B by YELLOW_0: 59;

        hence (A "/\" B) = A by YELLOW_0: 25;

        z c= dw;

        then z <= dw by YELLOW_1: 3;

        then a <= c by A3, WAYBEL_0: 66;

        then A <= C by YELLOW_0: 59;

        hence (A "/\" C) = A by YELLOW_0: 25;

        ( Segm 2) c= ( Segm 3) by NAT_1: 39;

        then dw <= t by YELLOW_1: 3;

        then c <= e by A3, WAYBEL_0: 66;

        then C <= E by YELLOW_0: 59;

        hence (C "/\" E) = C by YELLOW_0: 25;

        tj <= t by YELLOW_1: 3;

        then d <= e by A3, WAYBEL_0: 66;

        then D <= E by YELLOW_0: 59;

        hence (D "/\" E) = D by YELLOW_0: 25;

        thus (B "/\" C) = A

        proof

           A19:

          now

            assume (B "/\" C) = D;

            then D <= C by YELLOW_0: 23;

            then d <= c by YELLOW_0: 60;

            then tj <= dw by A3, WAYBEL_0: 66;

            then

             A20: tj c= dw by YELLOW_1: 3;

            2 in tj by Th3, TARSKI:def 2;

            then 2 in 2 by A20;

            hence contradiction;

          end;

           A21:

          now

            assume (B "/\" C) = E;

            then E <= C by YELLOW_0: 23;

            then e <= c by YELLOW_0: 60;

            then t <= dw by A3, WAYBEL_0: 66;

            then

             A22: t c= dw by YELLOW_1: 3;

            2 in t by CARD_1: 51, ENUMSET1:def 1;

            then 2 in 2 by A22;

            hence contradiction;

          end;

           A23:

          now

            assume (B "/\" C) = B;

            then B <= C by YELLOW_0: 25;

            then b <= c by YELLOW_0: 60;

            then td <= dw by A3, WAYBEL_0: 66;

            then

             A24: td c= dw by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            then 2 in 2 by A24;

            hence contradiction;

          end;

           A25:

          now

            assume (B "/\" C) = C;

            then C <= B by YELLOW_0: 25;

            then c <= b by YELLOW_0: 60;

            then dw <= td by A3, WAYBEL_0: 66;

            then

             A26: dw c= td by YELLOW_1: 3;

             0 in dw by CARD_1: 50, TARSKI:def 2;

            hence contradiction by A26, Th4, TARSKI:def 1;

          end;

           ex_inf_of ( {B, C},L) by YELLOW_0: 21;

          then ( inf {B, C}) in the carrier of K by YELLOW_0:def 16;

          then (B "/\" C) in ( rng f) by A6, YELLOW_0: 40;

          then ex x be object st x in ( dom f) & (B "/\" C) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A23, A25, A19, A21, ENUMSET1:def 3;

        end;

        td <= tj by Lm1, YELLOW_1: 3;

        then b <= d by A3, WAYBEL_0: 66;

        then B <= D by YELLOW_0: 59;

        hence (B "/\" D) = B by YELLOW_0: 25;

        thus (C "/\" D) = A

        proof

           A27:

          now

            assume (C "/\" D) = D;

            then D <= C by YELLOW_0: 23;

            then d <= c by YELLOW_0: 60;

            then tj <= dw by A3, WAYBEL_0: 66;

            then

             A28: tj c= dw by YELLOW_1: 3;

            2 in tj by Th3, TARSKI:def 2;

            then 2 in 2 by A28;

            hence contradiction;

          end;

           A29:

          now

            assume (C "/\" D) = E;

            then E <= C by YELLOW_0: 23;

            then e <= c by YELLOW_0: 60;

            then t <= dw by A3, WAYBEL_0: 66;

            then

             A30: t c= dw by YELLOW_1: 3;

            2 in t by CARD_1: 51, ENUMSET1:def 1;

            then 2 in 2 by A30;

            hence contradiction;

          end;

           A31:

          now

            assume (C "/\" D) = B;

            then B <= C by YELLOW_0: 23;

            then b <= c by YELLOW_0: 60;

            then td <= dw by A3, WAYBEL_0: 66;

            then

             A32: td c= dw by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            then 2 in 2 by A32;

            hence contradiction;

          end;

           A33:

          now

            assume (C "/\" D) = C;

            then C <= D by YELLOW_0: 25;

            then c <= d by YELLOW_0: 60;

            then dw <= tj by A3, WAYBEL_0: 66;

            then

             A34: dw c= tj by YELLOW_1: 3;

             0 in dw by CARD_1: 50, TARSKI:def 2;

            hence contradiction by A34, Th3, TARSKI:def 2;

          end;

           ex_inf_of ( {C, D},L) by YELLOW_0: 21;

          then ( inf {C, D}) in the carrier of K by YELLOW_0:def 16;

          then (C "/\" D) in ( rng f) by A6, YELLOW_0: 40;

          then ex x be object st x in ( dom f) & (C "/\" D) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A31, A33, A27, A29, ENUMSET1:def 3;

        end;

        thus (B "\/" C) = E

        proof

           A35:

          now

            assume (B "\/" C) = C;

            then C >= B by YELLOW_0: 24;

            then c >= b by YELLOW_0: 60;

            then dw >= td by A3, WAYBEL_0: 66;

            then

             A36: td c= dw by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            then 2 in 2 by A36;

            hence contradiction;

          end;

           A37:

          now

            assume (B "\/" C) = D;

            then D >= C by YELLOW_0: 22;

            then d >= c by YELLOW_0: 60;

            then tj >= dw by A3, WAYBEL_0: 66;

            then

             A38: dw c= tj by YELLOW_1: 3;

             0 in dw by CARD_1: 50, TARSKI:def 2;

            hence contradiction by A38, Th3, TARSKI:def 2;

          end;

           A39:

          now

            assume (B "\/" C) = B;

            then B >= C by YELLOW_0: 24;

            then b >= c by YELLOW_0: 60;

            then td >= dw by A3, WAYBEL_0: 66;

            then

             A40: dw c= td by YELLOW_1: 3;

             0 in dw by CARD_1: 50, TARSKI:def 2;

            hence contradiction by A40, Th4, TARSKI:def 1;

          end;

           A41:

          now

            assume (B "\/" C) = A;

            then A >= C by YELLOW_0: 22;

            then a >= c by YELLOW_0: 60;

            then z >= dw by A3, WAYBEL_0: 66;

            then dw c= z by YELLOW_1: 3;

            hence contradiction;

          end;

           ex_sup_of ( {B, C},L) by YELLOW_0: 20;

          then ( sup {B, C}) in the carrier of K by YELLOW_0:def 17;

          then (B "\/" C) in ( rng f) by A6, YELLOW_0: 41;

          then ex x be object st x in ( dom f) & (B "\/" C) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A39, A35, A37, A41, ENUMSET1:def 3;

        end;

        thus (C "\/" D) = E

        proof

           A42:

          now

            assume (C "\/" D) = D;

            then D >= C by YELLOW_0: 22;

            then d >= c by YELLOW_0: 60;

            then tj >= dw by A3, WAYBEL_0: 66;

            then

             A43: dw c= tj by YELLOW_1: 3;

             0 in dw by CARD_1: 50, TARSKI:def 2;

            hence contradiction by A43, Th3, TARSKI:def 2;

          end;

           A44:

          now

            assume (C "\/" D) = C;

            then C >= D by YELLOW_0: 24;

            then c >= d by YELLOW_0: 60;

            then dw >= tj by A3, WAYBEL_0: 66;

            then

             A45: tj c= dw by YELLOW_1: 3;

            2 in tj by Th3, TARSKI:def 2;

            hence contradiction by A45, CARD_1: 50, TARSKI:def 2;

          end;

           A46:

          now

            assume (C "\/" D) = B;

            then B >= C by YELLOW_0: 22;

            then b >= c by YELLOW_0: 60;

            then td >= dw by A3, WAYBEL_0: 66;

            then

             A47: dw c= td by YELLOW_1: 3;

             0 in dw by CARD_1: 50, TARSKI:def 2;

            hence contradiction by A47, Th4, TARSKI:def 1;

          end;

           A48:

          now

            assume (C "\/" D) = A;

            then A >= C by YELLOW_0: 22;

            then a >= c by YELLOW_0: 60;

            then z >= dw by A3, WAYBEL_0: 66;

            then dw c= z by YELLOW_1: 3;

            hence contradiction;

          end;

           ex_sup_of ( {C, D},L) by YELLOW_0: 20;

          then ( sup {C, D}) in the carrier of K by YELLOW_0:def 17;

          then (C "\/" D) in ( rng f) by A6, YELLOW_0: 41;

          then ex x be object st x in ( dom f) & (C "\/" D) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A46, A44, A42, A48, ENUMSET1:def 3;

        end;

      end;

      thus (ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e)) implies ex K be full Sublattice of L st ( N_5 ,K) are_isomorphic

      proof

        given a,b,c,d,e be Element of L such that

         AAA: (a,b,c,d,e) are_mutually_distinct and

         A59: (a "/\" b) = a and

         A60: (a "/\" c) = a and

         A61: (c "/\" e) = c and

         A62: (d "/\" e) = d and

         A63: (b "/\" c) = a and

         A64: (b "/\" d) = b and

         A65: (c "/\" d) = a and

         A66: (b "\/" c) = e and

         A67: (c "\/" d) = e;

        set ck = {a, b, c, d, e};

        reconsider ck as Subset of L;

        set K = ( subrelstr ck);

        

         A68: the carrier of K = ck by YELLOW_0:def 15;

        

         A69: K is meet-inheriting

        proof

          let x,y be Element of L;

          assume that

           A70: x in the carrier of K and

           A71: y in the carrier of K and ex_inf_of ( {x, y},L);

          per cases by A68, A70, A71, ENUMSET1:def 3;

            suppose x = a & y = a;

            then ( inf {x, y}) = (a "/\" a) by YELLOW_0: 40;

            then ( inf {x, y}) = a by YELLOW_5: 2;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = a & y = b;

            then ( inf {x, y}) = (a "/\" b) by YELLOW_0: 40;

            hence thesis by A59, A68, ENUMSET1:def 3;

          end;

            suppose x = a & y = c;

            then ( inf {x, y}) = (a "/\" c) by YELLOW_0: 40;

            hence thesis by A60, A68, ENUMSET1:def 3;

          end;

            suppose

             A72: x = a & y = d;

            

             A73: b <= d by A64, YELLOW_0: 25;

            a <= b by A59, YELLOW_0: 25;

            then a <= d by A73, ORDERS_2: 3;

            then (a "/\" d) = a by YELLOW_0: 25;

            then ( inf {x, y}) = a by A72, YELLOW_0: 40;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A74: x = a & y = e;

            

             A75: c <= e by A61, YELLOW_0: 25;

            a <= c by A60, YELLOW_0: 25;

            then a <= e by A75, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then ( inf {x, y}) = a by A74, YELLOW_0: 40;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = b & y = a;

            then ( inf {x, y}) = (a "/\" b) by YELLOW_0: 40;

            hence thesis by A59, A68, ENUMSET1:def 3;

          end;

            suppose x = b & y = b;

            then ( inf {x, y}) = (b "/\" b) by YELLOW_0: 40;

            then ( inf {x, y}) = b by YELLOW_5: 2;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = b & y = c;

            then ( inf {x, y}) = (b "/\" c) by YELLOW_0: 40;

            hence thesis by A63, A68, ENUMSET1:def 3;

          end;

            suppose x = b & y = d;

            then ( inf {x, y}) = (b "/\" d) by YELLOW_0: 40;

            hence thesis by A64, A68, ENUMSET1:def 3;

          end;

            suppose

             A76: x = b & y = e;

            

             A77: d <= e by A62, YELLOW_0: 25;

            b <= d by A64, YELLOW_0: 25;

            then b <= e by A77, ORDERS_2: 3;

            then (b "/\" e) = b by YELLOW_0: 25;

            then ( inf {x, y}) = b by A76, YELLOW_0: 40;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = a;

            then ( inf {x, y}) = (a "/\" c) by YELLOW_0: 40;

            hence thesis by A60, A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = b;

            then ( inf {x, y}) = (b "/\" c) by YELLOW_0: 40;

            hence thesis by A63, A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = c;

            then ( inf {x, y}) = (c "/\" c) by YELLOW_0: 40;

            then ( inf {x, y}) = c by YELLOW_5: 2;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = d;

            then ( inf {x, y}) = (c "/\" d) by YELLOW_0: 40;

            hence thesis by A65, A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = e;

            then ( inf {x, y}) = (c "/\" e) by YELLOW_0: 40;

            hence thesis by A61, A68, ENUMSET1:def 3;

          end;

            suppose

             A78: x = d & y = a;

            

             A79: b <= d by A64, YELLOW_0: 25;

            a <= b by A59, YELLOW_0: 25;

            then a <= d by A79, ORDERS_2: 3;

            then (a "/\" d) = a by YELLOW_0: 25;

            then ( inf {x, y}) = a by A78, YELLOW_0: 40;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = d & y = b;

            then ( inf {x, y}) = (b "/\" d) by YELLOW_0: 40;

            hence thesis by A64, A68, ENUMSET1:def 3;

          end;

            suppose x = d & y = c;

            then ( inf {x, y}) = (c "/\" d) by YELLOW_0: 40;

            hence thesis by A65, A68, ENUMSET1:def 3;

          end;

            suppose x = d & y = d;

            then ( inf {x, y}) = (d "/\" d) by YELLOW_0: 40;

            then ( inf {x, y}) = d by YELLOW_5: 2;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = d & y = e;

            then ( inf {x, y}) = (d "/\" e) by YELLOW_0: 40;

            hence thesis by A62, A68, ENUMSET1:def 3;

          end;

            suppose

             A80: x = e & y = a;

            

             A81: c <= e by A61, YELLOW_0: 25;

            a <= c by A60, YELLOW_0: 25;

            then a <= e by A81, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then ( inf {x, y}) = a by A80, YELLOW_0: 40;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A82: x = e & y = b;

            

             A83: d <= e by A62, YELLOW_0: 25;

            b <= d by A64, YELLOW_0: 25;

            then b <= e by A83, ORDERS_2: 3;

            then (b "/\" e) = b by YELLOW_0: 25;

            then ( inf {x, y}) = b by A82, YELLOW_0: 40;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = e & y = c;

            then ( inf {x, y}) = (c "/\" e) by YELLOW_0: 40;

            hence thesis by A61, A68, ENUMSET1:def 3;

          end;

            suppose x = e & y = d;

            then ( inf {x, y}) = (d "/\" e) by YELLOW_0: 40;

            hence thesis by A62, A68, ENUMSET1:def 3;

          end;

            suppose x = e & y = e;

            then ( inf {x, y}) = (e "/\" e) by YELLOW_0: 40;

            then ( inf {x, y}) = e by YELLOW_5: 2;

            hence thesis by A68, ENUMSET1:def 3;

          end;

        end;

        K is join-inheriting

        proof

          let x,y be Element of L;

          assume that

           A84: x in the carrier of K and

           A85: y in the carrier of K and ex_sup_of ( {x, y},L);

          per cases by A68, A84, A85, ENUMSET1:def 3;

            suppose x = a & y = a;

            then ( sup {x, y}) = (a "\/" a) by YELLOW_0: 41;

            then ( sup {x, y}) = a by YELLOW_5: 1;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = a & y = b;

            then (x "\/" y) = b by A59, Th5;

            then ( sup {x, y}) = b by YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = a & y = c;

            then (x "\/" y) = c by A60, Th5;

            then ( sup {x, y}) = c by YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A86: x = a & y = d;

            

             A87: b <= d by A64, YELLOW_0: 25;

            a <= b by A59, YELLOW_0: 25;

            then a <= d by A87, ORDERS_2: 3;

            then (a "/\" d) = a by YELLOW_0: 25;

            then (a "\/" d) = d by Th5;

            then ( sup {x, y}) = d by A86, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A88: x = a & y = e;

            

             A89: c <= e by A61, YELLOW_0: 25;

            a <= c by A60, YELLOW_0: 25;

            then a <= e by A89, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then (a "\/" e) = e by Th5;

            then ( sup {x, y}) = e by A88, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A90: x = b & y = a;

            (a "\/" b) = b by A59, Th5;

            then ( sup {x, y}) = b by A90, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = b & y = b;

            then ( sup {x, y}) = (b "\/" b) by YELLOW_0: 41;

            then ( sup {x, y}) = b by YELLOW_5: 1;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = b & y = c;

            then ( sup {x, y}) = (b "\/" c) by YELLOW_0: 41;

            hence thesis by A66, A68, ENUMSET1:def 3;

          end;

            suppose

             A91: x = b & y = d;

            (b "\/" d) = d by A64, Th5;

            then ( sup {x, y}) = d by A91, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A92: x = b & y = e;

            

             A93: d <= e by A62, YELLOW_0: 25;

            b <= d by A64, YELLOW_0: 25;

            then b <= e by A93, ORDERS_2: 3;

            then (b "/\" e) = b by YELLOW_0: 25;

            then (b "\/" e) = e by Th5;

            then ( sup {x, y}) = e by A92, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A94: x = c & y = a;

            (c "\/" a) = c by A60, Th5;

            then ( sup {x, y}) = c by A94, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = b;

            then ( sup {x, y}) = (b "\/" c) by YELLOW_0: 41;

            hence thesis by A66, A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = c;

            then ( sup {x, y}) = (c "\/" c) by YELLOW_0: 41;

            then ( sup {x, y}) = c by YELLOW_5: 1;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = c & y = d;

            then ( sup {x, y}) = (c "\/" d) by YELLOW_0: 41;

            hence thesis by A67, A68, ENUMSET1:def 3;

          end;

            suppose

             A95: x = c & y = e;

            (c "\/" e) = e by A61, Th5;

            then ( sup {x, y}) = e by A95, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A96: x = d & y = a;

            

             A97: b <= d by A64, YELLOW_0: 25;

            a <= b by A59, YELLOW_0: 25;

            then a <= d by A97, ORDERS_2: 3;

            then (a "/\" d) = a by YELLOW_0: 25;

            then (a "\/" d) = d by Th5;

            then ( sup {x, y}) = d by A96, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A98: x = d & y = b;

            (b "\/" d) = d by A64, Th5;

            then ( sup {x, y}) = d by A98, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = d & y = c;

            then ( sup {x, y}) = (c "\/" d) by YELLOW_0: 41;

            hence thesis by A67, A68, ENUMSET1:def 3;

          end;

            suppose x = d & y = d;

            then ( sup {x, y}) = (d "\/" d) by YELLOW_0: 41;

            then ( sup {x, y}) = d by YELLOW_5: 1;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A99: x = d & y = e;

            (d "\/" e) = e by A62, Th5;

            then ( sup {x, y}) = e by A99, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A100: x = e & y = a;

            

             A101: c <= e by A61, YELLOW_0: 25;

            a <= c by A60, YELLOW_0: 25;

            then a <= e by A101, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then (a "\/" e) = e by Th5;

            then ( sup {x, y}) = e by A100, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A102: x = e & y = b;

            

             A103: d <= e by A62, YELLOW_0: 25;

            b <= d by A64, YELLOW_0: 25;

            then b <= e by A103, ORDERS_2: 3;

            then (b "/\" e) = b by YELLOW_0: 25;

            then (b "\/" e) = e by Th5;

            then ( sup {x, y}) = e by A102, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A104: x = e & y = c;

            (c "\/" e) = e by A61, Th5;

            then ( sup {x, y}) = e by A104, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose

             A105: x = e & y = d;

            (d "\/" e) = e by A62, Th5;

            then ( sup {x, y}) = e by A105, YELLOW_0: 41;

            hence thesis by A68, ENUMSET1:def 3;

          end;

            suppose x = e & y = e;

            then ( sup {x, y}) = (e "\/" e) by YELLOW_0: 41;

            then ( sup {x, y}) = e by YELLOW_5: 1;

            hence thesis by A68, ENUMSET1:def 3;

          end;

        end;

        then

        reconsider K as non empty full Sublattice of L by A69, YELLOW_0:def 15;

        take K;

        thus ( N_5 ,K) are_isomorphic

        proof

          reconsider t = 3 as Element of N_5 by A1, ENUMSET1:def 3;

          reconsider td = (3 \ 2) as Element of N_5 by A1, ENUMSET1:def 3;

          reconsider dw = 2 as Element of N_5 by A1, ENUMSET1:def 3;

           A106:

          now

            assume

             A107: dw = td;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A107;

          end;

           A108:

          now

            assume

             A109: td = t;

             not 1 in td by Th4, TARSKI:def 1;

            hence contradiction by A109, CARD_1: 51, ENUMSET1:def 1;

          end;

          reconsider tj = (3 \ 1) as Element of N_5 by A1, ENUMSET1:def 3;

          reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;

          defpred P[ object, object] means for X be Element of N_5 st X = $1 holds ((X = z implies $2 = a) & (X = td implies $2 = b) & (X = dw implies $2 = c) & (X = tj implies $2 = d) & (X = t implies $2 = e));

           A110:

          now

            assume

             A111: tj = dw;

            2 in tj by Th3, TARSKI:def 2;

            hence contradiction by A111;

          end;

           A112:

          now

            assume

             A113: tj = t;

             not 0 in tj by Th3, TARSKI:def 2;

            hence contradiction by A113, CARD_1: 51, ENUMSET1:def 1;

          end;

           A114:

          now

            assume

             A115: tj = td;

             not 1 in td by Th4, TARSKI:def 1;

            hence contradiction by A115, Th3, TARSKI:def 2;

          end;

          

           A116: for x be object st x in cn holds ex y be object st y in ck & P[x, y]

          proof

            let x be object;

            assume

             A117: x in cn;

            per cases by A1, A117, ENUMSET1:def 3;

              suppose

               A118: x = 0 ;

              take y = a;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of N_5 ;

              thus thesis by A118, Th3, Th4;

            end;

              suppose

               A119: x = (3 \ 1);

              take y = d;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of N_5 ;

              thus thesis by A110, A114, A112, A119, Th3;

            end;

              suppose

               A120: x = 2;

              take y = c;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of N_5 ;

              thus thesis by A110, A106, A120;

            end;

              suppose

               A121: x = (3 \ 2);

              take y = b;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of N_5 ;

              thus thesis by A114, A106, A108, A121, Th4;

            end;

              suppose

               A122: x = 3;

              take y = e;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of N_5 ;

              thus thesis by A112, A108, A122;

            end;

          end;

          consider f be Function of cn, ck such that

           A123: for x be object st x in cn holds P[x, (f . x)] from FUNCT_2:sch 1( A116);

          reconsider f as Function of N_5 , K by A68;

           A124:

          now

            let x,y be Element of N_5 ;

            assume

             A125: (f . x) = (f . y);

            thus x = y

            proof

              per cases by A1, ENUMSET1:def 3;

                suppose x = z & y = z;

                hence thesis;

              end;

                suppose x = tj & y = tj;

                hence thesis;

              end;

                suppose x = td & y = td;

                hence thesis;

              end;

                suppose x = dw & y = dw;

                hence thesis;

              end;

                suppose x = t & y = t;

                hence thesis;

              end;

                suppose

                 A126: x = z & y = tj;

                then (f . x) = a by A123;

                hence thesis by AAA, A123, A125, A126;

              end;

                suppose

                 A127: x = z & y = dw;

                then (f . x) = a by A123;

                hence thesis by AAA, A123, A125, A127;

              end;

                suppose

                 A128: x = z & y = td;

                then (f . x) = a by A123;

                hence thesis by AAA, A123, A125, A128;

              end;

                suppose

                 A129: x = z & y = t;

                then (f . x) = a by A123;

                hence thesis by AAA, A123, A125, A129;

              end;

                suppose

                 A130: x = tj & y = z;

                then (f . x) = d by A123;

                hence thesis by AAA, A123, A125, A130;

              end;

                suppose

                 A131: x = tj & y = dw;

                then (f . x) = d by A123;

                hence thesis by AAA, A123, A125, A131;

              end;

                suppose

                 A132: x = tj & y = td;

                then (f . x) = d by A123;

                hence thesis by AAA, A123, A125, A132;

              end;

                suppose

                 A133: x = tj & y = t;

                then (f . x) = d by A123;

                hence thesis by AAA, A123, A125, A133;

              end;

                suppose

                 A134: x = dw & y = z;

                then (f . x) = c by A123;

                hence thesis by AAA, A123, A125, A134;

              end;

                suppose

                 A135: x = dw & y = tj;

                then (f . x) = c by A123;

                hence thesis by AAA, A123, A125, A135;

              end;

                suppose

                 A136: x = dw & y = td;

                then (f . x) = c by A123;

                hence thesis by AAA, A123, A125, A136;

              end;

                suppose

                 A137: x = dw & y = t;

                then (f . x) = c by A123;

                hence thesis by AAA, A123, A125, A137;

              end;

                suppose

                 A138: x = td & y = z;

                then (f . x) = b by A123;

                hence thesis by AAA, A123, A125, A138;

              end;

                suppose

                 A139: x = td & y = tj;

                then (f . x) = b by A123;

                hence thesis by AAA, A123, A125, A139;

              end;

                suppose

                 A140: x = td & y = dw;

                then (f . x) = b by A123;

                hence thesis by AAA, A123, A125, A140;

              end;

                suppose

                 A141: x = td & y = t;

                then (f . x) = b by A123;

                hence thesis by AAA, A123, A125, A141;

              end;

                suppose

                 A142: x = t & y = z;

                then (f . x) = e by A123;

                hence thesis by AAA, A123, A125, A142;

              end;

                suppose

                 A143: x = t & y = tj;

                then (f . x) = e by A123;

                hence thesis by AAA, A123, A125, A143;

              end;

                suppose

                 A144: x = t & y = dw;

                then (f . x) = e by A123;

                hence thesis by AAA, A123, A125, A144;

              end;

                suppose

                 A145: x = t & y = td;

                then (f . x) = e by A123;

                hence thesis by AAA, A123, A125, A145;

              end;

            end;

          end;

          

           A146: ( rng f) c= ck

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

             A147: x in ( dom f) and

             A148: y = (f . x) by FUNCT_1:def 3;

            reconsider x as Element of N_5 by A147;

            x = z or x = tj or x = dw or x = td or x = t by A1, ENUMSET1:def 3;

            then y = a or y = d or y = c or y = b or y = e by A123, A148;

            hence thesis by ENUMSET1:def 3;

          end;

          

           A149: ( dom f) = the carrier of N_5 by FUNCT_2:def 1;

          ck c= ( rng f)

          proof

            let y be object;

            assume

             A150: y in ck;

            per cases by A150, ENUMSET1:def 3;

              suppose

               A151: y = a;

              a = (f . z) by A123;

              hence thesis by A149, A151, FUNCT_1:def 3;

            end;

              suppose

               A152: y = b;

              b = (f . td) by A123;

              hence thesis by A149, A152, FUNCT_1:def 3;

            end;

              suppose

               A153: y = c;

              c = (f . dw) by A123;

              hence thesis by A149, A153, FUNCT_1:def 3;

            end;

              suppose

               A154: y = d;

              d = (f . tj) by A123;

              hence thesis by A149, A154, FUNCT_1:def 3;

            end;

              suppose

               A155: y = e;

              e = (f . t) by A123;

              hence thesis by A149, A155, FUNCT_1:def 3;

            end;

          end;

          then

           A156: ( rng f) = ck by A146;

          

           A157: for x,y be Element of N_5 holds x <= y iff (f . x) <= (f . y)

          proof

            let x,y be Element of N_5 ;

            thus x <= y implies (f . x) <= (f . y)

            proof

              assume

               A158: x <= y;

              per cases by A1, ENUMSET1:def 3;

                suppose x = z & y = z;

                hence thesis;

              end;

                suppose

                 A159: x = z & y = td;

                then

                 A160: (f . y) = b by A123;

                

                 A161: a <= b by A59, YELLOW_0: 25;

                (f . x) = a by A123, A159;

                hence thesis by A160, A161, YELLOW_0: 60;

              end;

                suppose

                 A162: x = z & y = dw;

                then

                 A163: (f . y) = c by A123;

                

                 A164: a <= c by A60, YELLOW_0: 25;

                (f . x) = a by A123, A162;

                hence thesis by A163, A164, YELLOW_0: 60;

              end;

                suppose

                 A165: x = z & y = tj;

                

                 A166: b <= d by A64, YELLOW_0: 25;

                a <= b by A59, YELLOW_0: 25;

                then

                 A167: a <= d by A166, ORDERS_2: 3;

                

                 A168: (f . y) = d by A123, A165;

                (f . x) = a by A123, A165;

                hence thesis by A168, A167, YELLOW_0: 60;

              end;

                suppose

                 A169: x = z & y = t;

                

                 A170: c <= e by A61, YELLOW_0: 25;

                a <= c by A60, YELLOW_0: 25;

                then

                 A171: a <= e by A170, ORDERS_2: 3;

                

                 A172: (f . y) = e by A123, A169;

                (f . x) = a by A123, A169;

                hence thesis by A172, A171, YELLOW_0: 60;

              end;

                suppose x = td & y = z;

                then td c= z by A158, YELLOW_1: 3;

                hence thesis by Th4;

              end;

                suppose x = td & y = td;

                hence thesis;

              end;

                suppose

                 A173: x = td & y = dw;

                

                 A174: not 2 in dw;

                2 in td by Th4, TARSKI:def 1;

                then not td c= dw by A174;

                hence thesis by A158, A173, YELLOW_1: 3;

              end;

                suppose x = td & y = z;

                then td c= z by A158, YELLOW_1: 3;

                hence thesis by Th4;

              end;

                suppose

                 A175: x = td & y = tj;

                then

                 A176: (f . y) = d by A123;

                

                 A177: b <= d by A64, YELLOW_0: 25;

                (f . x) = b by A123, A175;

                hence thesis by A176, A177, YELLOW_0: 60;

              end;

                suppose

                 A178: x = td & y = t;

                

                 A179: d <= e by A62, YELLOW_0: 25;

                b <= d by A64, YELLOW_0: 25;

                then

                 A180: b <= e by A179, ORDERS_2: 3;

                

                 A181: (f . y) = e by A123, A178;

                (f . x) = b by A123, A178;

                hence thesis by A181, A180, YELLOW_0: 60;

              end;

                suppose x = dw & y = z;

                then dw c= z by A158, YELLOW_1: 3;

                hence thesis;

              end;

                suppose

                 A182: x = dw & y = td;

                 0 in dw by CARD_1: 50, TARSKI:def 2;

                then not dw c= td by Th4, TARSKI:def 1;

                hence thesis by A158, A182, YELLOW_1: 3;

              end;

                suppose x = dw & y = dw;

                hence thesis;

              end;

                suppose

                 A183: x = dw & y = tj;

                 0 in dw by CARD_1: 50, TARSKI:def 2;

                then not dw c= tj by Th3, TARSKI:def 2;

                hence thesis by A158, A183, YELLOW_1: 3;

              end;

                suppose

                 A184: x = dw & y = t;

                then

                 A185: (f . y) = e by A123;

                

                 A186: c <= e by A61, YELLOW_0: 25;

                (f . x) = c by A123, A184;

                hence thesis by A185, A186, YELLOW_0: 60;

              end;

                suppose x = tj & y = z;

                then tj c= z by A158, YELLOW_1: 3;

                hence thesis by Th3;

              end;

                suppose

                 A187: x = tj & y = td;

                1 in tj by Th3, TARSKI:def 2;

                then not tj c= td by Th4, TARSKI:def 1;

                hence thesis by A158, A187, YELLOW_1: 3;

              end;

                suppose

                 A188: x = tj & y = dw;

                

                 A189: not 2 in dw;

                2 in tj by Th3, TARSKI:def 2;

                then not tj c= dw by A189;

                hence thesis by A158, A188, YELLOW_1: 3;

              end;

                suppose x = tj & y = tj;

                hence thesis;

              end;

                suppose

                 A190: x = tj & y = t;

                then

                 A191: (f . y) = e by A123;

                

                 A192: d <= e by A62, YELLOW_0: 25;

                (f . x) = d by A123, A190;

                hence thesis by A191, A192, YELLOW_0: 60;

              end;

                suppose x = t & y = z;

                then t c= z by A158, YELLOW_1: 3;

                hence thesis;

              end;

                suppose

                 A193: x = t & y = td;

                 0 in t by CARD_1: 51, ENUMSET1:def 1;

                then not t c= td by Th4, TARSKI:def 1;

                hence thesis by A158, A193, YELLOW_1: 3;

              end;

                suppose

                 A194: x = t & y = dw;

                

                 A195: not 2 in dw;

                2 in t by CARD_1: 51, ENUMSET1:def 1;

                then not t c= dw by A195;

                hence thesis by A158, A194, YELLOW_1: 3;

              end;

                suppose

                 A196: x = t & y = tj;

                 0 in t by CARD_1: 51, ENUMSET1:def 1;

                then not t c= tj by Th3, TARSKI:def 2;

                hence thesis by A158, A196, YELLOW_1: 3;

              end;

                suppose x = t & y = t;

                hence thesis;

              end;

            end;

            thus (f . x) <= (f . y) implies x <= y

            proof

              

               A197: (f . y) in ck by A149, A156, FUNCT_1:def 3;

              

               A198: (f . x) in ck by A149, A156, FUNCT_1:def 3;

              assume

               A199: (f . x) <= (f . y);

              per cases by A198, A197, ENUMSET1:def 3;

                suppose (f . x) = a & (f . y) = a;

                hence thesis by A124;

              end;

                suppose

                 A200: (f . x) = a & (f . y) = b;

                (f . z) = a by A123;

                then z = x by A124, A200;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose

                 A201: (f . x) = a & (f . y) = c;

                (f . z) = a by A123;

                then z = x by A124, A201;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose

                 A202: (f . x) = a & (f . y) = d;

                (f . z) = a by A123;

                then z = x by A124, A202;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose

                 A203: (f . x) = a & (f . y) = e;

                (f . z) = a by A123;

                then z = x by A124, A203;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose (f . x) = b & (f . y) = a;

                then b <= a by A199, YELLOW_0: 59;

                hence thesis by AAA, A59, YELLOW_0: 25;

              end;

                suppose (f . x) = b & (f . y) = b;

                hence thesis by A124;

              end;

                suppose (f . x) = b & (f . y) = c;

                then b <= c by A199, YELLOW_0: 59;

                hence thesis by AAA, A63, YELLOW_0: 25;

              end;

                suppose

                 A204: (f . x) = b & (f . y) = d;

                (f . tj) = d by A123;

                then

                 A205: y = tj by A124, A204;

                (f . td) = b by A123;

                then

                 A206: x = td by A124, A204;

                ( Segm 1) c= ( Segm 2) by NAT_1: 39;

                then x c= y by A206, A205, XBOOLE_1: 34;

                hence thesis by YELLOW_1: 3;

              end;

                suppose

                 A207: (f . x) = b & (f . y) = e;

                (f . t) = e by A123;

                then

                 A208: t = y by A124, A207;

                (f . td) = b by A123;

                then td = x by A124, A207;

                hence thesis by A208, YELLOW_1: 3;

              end;

                suppose (f . x) = c & (f . y) = a;

                then c <= a by A199, YELLOW_0: 59;

                hence thesis by AAA, A60, YELLOW_0: 25;

              end;

                suppose (f . x) = c & (f . y) = b;

                then c <= b by A199, YELLOW_0: 59;

                hence thesis by AAA, A63, YELLOW_0: 25;

              end;

                suppose (f . x) = c & (f . y) = c;

                hence thesis by A124;

              end;

                suppose (f . x) = c & (f . y) = d;

                then c <= d by A199, YELLOW_0: 59;

                hence thesis by AAA, A65, YELLOW_0: 25;

              end;

                suppose

                 A209: (f . x) = c & (f . y) = e;

                

                 A210: dw c= t

                proof

                  let X be object;

                  assume X in dw;

                  then X = 0 or X = 1 by CARD_1: 50, TARSKI:def 2;

                  hence thesis by CARD_1: 51, ENUMSET1:def 1;

                end;

                (f . t) = e by A123;

                then

                 A211: t = y by A124, A209;

                (f . dw) = c by A123;

                then dw = x by A124, A209;

                hence thesis by A210, A211, YELLOW_1: 3;

              end;

                suppose

                 A212: (f . x) = d & (f . y) = a;

                

                 A213: a <= b by A59, YELLOW_0: 25;

                d <= a by A199, A212, YELLOW_0: 59;

                then d <= b by A213, ORDERS_2: 3;

                hence thesis by AAA, A64, YELLOW_0: 25;

              end;

                suppose (f . x) = d & (f . y) = b;

                then d <= b by A199, YELLOW_0: 59;

                hence thesis by AAA, A64, YELLOW_0: 25;

              end;

                suppose (f . x) = d & (f . y) = c;

                then d <= c by A199, YELLOW_0: 59;

                hence thesis by AAA, A65, YELLOW_0: 25;

              end;

                suppose (f . x) = d & (f . y) = d;

                hence thesis by A124;

              end;

                suppose

                 A214: (f . x) = d & (f . y) = e;

                (f . t) = e by A123;

                then

                 A215: t = y by A124, A214;

                (f . tj) = d by A123;

                then tj = x by A124, A214;

                hence thesis by A215, YELLOW_1: 3;

              end;

                suppose

                 A216: (f . x) = e & (f . y) = a;

                

                 A217: b <= d by A64, YELLOW_0: 25;

                

                 A218: d <= e by A62, YELLOW_0: 25;

                a <= b by A59, YELLOW_0: 25;

                then a <= d by A217, ORDERS_2: 3;

                then

                 A219: a <= e by A218, ORDERS_2: 3;

                e <= a by A199, A216, YELLOW_0: 59;

                hence thesis by AAA, A219, ORDERS_2: 2;

              end;

                suppose

                 A220: (f . x) = e & (f . y) = b;

                

                 A221: d <= e by A62, YELLOW_0: 25;

                b <= d by A64, YELLOW_0: 25;

                then

                 A222: b <= e by A221, ORDERS_2: 3;

                e <= b by A199, A220, YELLOW_0: 59;

                hence thesis by AAA, A222, ORDERS_2: 2;

              end;

                suppose (f . x) = e & (f . y) = c;

                then e <= c by A199, YELLOW_0: 59;

                hence thesis by AAA, A61, YELLOW_0: 25;

              end;

                suppose (f . x) = e & (f . y) = d;

                then e <= d by A199, YELLOW_0: 59;

                hence thesis by AAA, A62, YELLOW_0: 25;

              end;

                suppose (f . x) = e & (f . y) = e;

                hence thesis by A124;

              end;

            end;

          end;

          take f;

          f is one-to-one by A124;

          hence thesis by A68, A156, A157, WAYBEL_0: 66;

        end;

      end;

    end;

    theorem :: YELLOW11:10

    

     Th10: for L be LATTICE holds (ex K be full Sublattice of L st ( M_3 ,K) are_isomorphic ) iff ex a,b,c,d,e be Element of L st (a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e

    proof

      set cn = the carrier of M_3 ;

      let L be LATTICE;

      

       A1: cn = { 0 , 1, (2 \ 1), (3 \ 2), 3} by YELLOW_1: 1;

      thus (ex K be full Sublattice of L st ( M_3 ,K) are_isomorphic ) implies ex a,b,c,d,e be Element of L st (a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e

      proof

        reconsider td = (3 \ 2) as Element of M_3 by A1, ENUMSET1:def 3;

        reconsider dj = (2 \ 1) as Element of M_3 by A1, ENUMSET1:def 3;

        reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;

        reconsider j = 1 as Element of M_3 by A1, ENUMSET1:def 3;

        reconsider cl = the carrier of L as non empty set;

        reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;

        given K be full Sublattice of L such that

         A2: ( M_3 ,K) are_isomorphic ;

        consider f be Function of M_3 , K such that

         A3: f is isomorphic by A2;

        

         A4: K is non empty by A3, WAYBEL_0:def 38;

        then

         A5: f is one-to-one monotone by A3, WAYBEL_0:def 38;

        reconsider K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;

        reconsider ck = the carrier of K as non empty set;

        

         A6: ck = ( rng f) by A3, WAYBEL_0: 66;

        reconsider g = f as Function of cn, ck;

        reconsider a = (g . z), b = (g . j), c = (g . dj), d = (g . td), e = (g . t) as Element of K;

        reconsider ck as non empty Subset of cl by YELLOW_0:def 13;

        

         A7: b in ck;

        

         A8: c in ck;

        

         A9: e in ck;

        

         A10: d in ck;

        a in ck;

        then

        reconsider A = a, B = b, C = c, D = d, E = e as Element of L by A7, A8, A10, A9;

        take A, B, C, D, E;

        thus A <> B by A5, WAYBEL_1:def 1;

        thus A <> C by A5, Th2, WAYBEL_1:def 1;

        thus A <> D by A5, Th4, WAYBEL_1:def 1;

        thus A <> E by A5, WAYBEL_1:def 1;

        now

          assume (f . j) = (f . dj);

          then j = dj by A4, A5, WAYBEL_1:def 1;

          then 1 in 1 by Th2, TARSKI:def 1;

          hence contradiction;

        end;

        hence B <> C;

        now

          assume (f . j) = (f . td);

          then

           A11: j = td by A4, A5, WAYBEL_1:def 1;

           0 in j by CARD_1: 49, TARSKI:def 1;

          hence contradiction by A11, Th4, TARSKI:def 1;

        end;

        hence B <> D;

        thus B <> E by A5, WAYBEL_1:def 1;

        now

          assume (f . dj) = (f . td);

          then

           A12: dj = td by A4, A5, WAYBEL_1:def 1;

          1 in dj by Th2, TARSKI:def 1;

          hence contradiction by A12, Th4, TARSKI:def 1;

        end;

        hence C <> D;

        now

          assume (f . dj) = (f . t);

          then

           A13: dj = t by A4, A5, WAYBEL_1:def 1;

           0 in t by CARD_1: 51, ENUMSET1:def 1;

          hence contradiction by A13, Th2, TARSKI:def 1;

        end;

        hence C <> E;

        now

          assume (f . td) = (f . t);

          then

           A14: td = t by A4, A5, WAYBEL_1:def 1;

           0 in t by CARD_1: 51, ENUMSET1:def 1;

          hence contradiction by A14, Th4, TARSKI:def 1;

        end;

        hence D <> E;

        z c= j;

        then z <= j by YELLOW_1: 3;

        then a <= b by A3, WAYBEL_0: 66;

        then A <= B by YELLOW_0: 59;

        hence (A "/\" B) = A by YELLOW_0: 25;

        z c= dj;

        then z <= dj by YELLOW_1: 3;

        then a <= c by A3, WAYBEL_0: 66;

        then A <= C by YELLOW_0: 59;

        hence (A "/\" C) = A by YELLOW_0: 25;

        z c= td;

        then z <= td by YELLOW_1: 3;

        then a <= d by A3, WAYBEL_0: 66;

        then A <= D by YELLOW_0: 59;

        hence (A "/\" D) = A by YELLOW_0: 25;

        ( Segm 1) c= ( Segm 3) by NAT_1: 39;

        then j <= t by YELLOW_1: 3;

        then b <= e by A3, WAYBEL_0: 66;

        then B <= E by YELLOW_0: 59;

        hence (B "/\" E) = B by YELLOW_0: 25;

        dj c= t

        proof

          let x be object;

          assume x in dj;

          then x = 1 by Th2, TARSKI:def 1;

          hence thesis by CARD_1: 51, ENUMSET1:def 1;

        end;

        then dj <= t by YELLOW_1: 3;

        then c <= e by A3, WAYBEL_0: 66;

        then C <= E by YELLOW_0: 59;

        hence (C "/\" E) = C by YELLOW_0: 25;

        td <= t by YELLOW_1: 3;

        then d <= e by A3, WAYBEL_0: 66;

        then D <= E by YELLOW_0: 59;

        hence (D "/\" E) = D by YELLOW_0: 25;

        thus (B "/\" C) = A

        proof

           A15:

          now

            assume (B "/\" C) = D;

            then D <= C by YELLOW_0: 23;

            then d <= c by YELLOW_0: 60;

            then td <= dj by A3, WAYBEL_0: 66;

            then

             A16: td c= dj by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A16, Th2, TARSKI:def 1;

          end;

           A17:

          now

            assume (B "/\" C) = B;

            then B <= C by YELLOW_0: 25;

            then b <= c by YELLOW_0: 60;

            then j <= dj by A3, WAYBEL_0: 66;

            then

             A18: j c= dj by YELLOW_1: 3;

             0 in j by CARD_1: 49, TARSKI:def 1;

            hence contradiction by A18, Th2, TARSKI:def 1;

          end;

           A19:

          now

            assume (B "/\" C) = E;

            then E <= C by YELLOW_0: 23;

            then e <= c by YELLOW_0: 60;

            then t <= dj by A3, WAYBEL_0: 66;

            then

             A20: t c= dj by YELLOW_1: 3;

            2 in t by CARD_1: 51, ENUMSET1:def 1;

            hence contradiction by A20, Th2, TARSKI:def 1;

          end;

           A21:

          now

            assume (B "/\" C) = C;

            then C <= B by YELLOW_0: 25;

            then c <= b by YELLOW_0: 60;

            then dj <= j by A3, WAYBEL_0: 66;

            then

             A22: dj c= j by YELLOW_1: 3;

            1 in dj by Th2, TARSKI:def 1;

            hence contradiction by A22, CARD_1: 49, TARSKI:def 1;

          end;

           ex_inf_of ( {B, C},L) by YELLOW_0: 21;

          then ( inf {B, C}) in the carrier of K by YELLOW_0:def 16;

          then (B "/\" C) in ( rng f) by A6, YELLOW_0: 40;

          then ex x be object st x in ( dom f) & (B "/\" C) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A17, A21, A15, A19, ENUMSET1:def 3;

        end;

        thus (B "/\" D) = A

        proof

           A23:

          now

            assume (B "/\" D) = D;

            then D <= B by YELLOW_0: 23;

            then d <= b by YELLOW_0: 60;

            then td <= j by A3, WAYBEL_0: 66;

            then

             A24: td c= j by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A24, CARD_1: 49, TARSKI:def 1;

          end;

           A25:

          now

            assume (B "/\" D) = C;

            then C <= B by YELLOW_0: 23;

            then c <= b by YELLOW_0: 60;

            then dj <= j by A3, WAYBEL_0: 66;

            then

             A26: dj c= j by YELLOW_1: 3;

            1 in dj by Th2, TARSKI:def 1;

            hence contradiction by A26, CARD_1: 49, TARSKI:def 1;

          end;

           A27:

          now

            assume (B "/\" D) = B;

            then B <= D by YELLOW_0: 25;

            then b <= d by YELLOW_0: 60;

            then j <= td by A3, WAYBEL_0: 66;

            then

             A28: j c= td by YELLOW_1: 3;

             0 in j by CARD_1: 49, TARSKI:def 1;

            hence contradiction by A28, Th4, TARSKI:def 1;

          end;

           A29:

          now

            assume (B "/\" D) = E;

            then E <= B by YELLOW_0: 23;

            then e <= b by YELLOW_0: 60;

            then t <= j by A3, WAYBEL_0: 66;

            then

             A30: t c= j by YELLOW_1: 3;

            2 in t by CARD_1: 51, ENUMSET1:def 1;

            hence contradiction by A30, CARD_1: 49, TARSKI:def 1;

          end;

           ex_inf_of ( {B, D},L) by YELLOW_0: 21;

          then ( inf {B, D}) in the carrier of K by YELLOW_0:def 16;

          then (B "/\" D) in ( rng f) by A6, YELLOW_0: 40;

          then ex x be object st x in ( dom f) & (B "/\" D) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A27, A25, A23, A29, ENUMSET1:def 3;

        end;

        thus (C "/\" D) = A

        proof

           A31:

          now

            assume (C "/\" D) = D;

            then D <= C by YELLOW_0: 23;

            then d <= c by YELLOW_0: 60;

            then td <= dj by A3, WAYBEL_0: 66;

            then

             A32: td c= dj by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A32, Th2, TARSKI:def 1;

          end;

           A33:

          now

            assume (C "/\" D) = E;

            then E <= C by YELLOW_0: 23;

            then e <= c by YELLOW_0: 60;

            then t <= dj by A3, WAYBEL_0: 66;

            then

             A34: t c= dj by YELLOW_1: 3;

            2 in t by CARD_1: 51, ENUMSET1:def 1;

            hence contradiction by A34, Th2, TARSKI:def 1;

          end;

           A35:

          now

            assume (C "/\" D) = C;

            then C <= D by YELLOW_0: 25;

            then c <= d by YELLOW_0: 60;

            then dj <= td by A3, WAYBEL_0: 66;

            then

             A36: dj c= td by YELLOW_1: 3;

            1 in dj by Th2, TARSKI:def 1;

            hence contradiction by A36, Th4, TARSKI:def 1;

          end;

           A37:

          now

            assume (C "/\" D) = B;

            then B <= C by YELLOW_0: 23;

            then b <= c by YELLOW_0: 60;

            then j <= dj by A3, WAYBEL_0: 66;

            then

             A38: j c= dj by YELLOW_1: 3;

             0 in j by CARD_1: 49, TARSKI:def 1;

            hence contradiction by A38, Th2, TARSKI:def 1;

          end;

           ex_inf_of ( {C, D},L) by YELLOW_0: 21;

          then ( inf {C, D}) in the carrier of K by YELLOW_0:def 16;

          then (C "/\" D) in ( rng f) by A6, YELLOW_0: 40;

          then ex x be object st x in ( dom f) & (C "/\" D) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A37, A35, A31, A33, ENUMSET1:def 3;

        end;

        thus (B "\/" C) = E

        proof

           A39:

          now

            assume (B "\/" C) = C;

            then C >= B by YELLOW_0: 24;

            then c >= b by YELLOW_0: 60;

            then dj >= j by A3, WAYBEL_0: 66;

            then

             A40: j c= dj by YELLOW_1: 3;

             0 in j by CARD_1: 49, TARSKI:def 1;

            hence contradiction by A40, Th2, TARSKI:def 1;

          end;

           A41:

          now

            assume (B "\/" C) = B;

            then B >= C by YELLOW_0: 24;

            then b >= c by YELLOW_0: 60;

            then j >= dj by A3, WAYBEL_0: 66;

            then

             A42: dj c= j by YELLOW_1: 3;

            1 in dj by Th2, TARSKI:def 1;

            hence contradiction by A42, CARD_1: 49, TARSKI:def 1;

          end;

           A43:

          now

            assume (B "\/" C) = D;

            then D >= C by YELLOW_0: 22;

            then d >= c by YELLOW_0: 60;

            then td >= dj by A3, WAYBEL_0: 66;

            then

             A44: dj c= td by YELLOW_1: 3;

            1 in dj by Th2, TARSKI:def 1;

            hence contradiction by A44, Th4, TARSKI:def 1;

          end;

           A45:

          now

            assume (B "\/" C) = A;

            then A >= C by YELLOW_0: 22;

            then a >= c by YELLOW_0: 60;

            then z >= dj by A3, WAYBEL_0: 66;

            then dj c= z by YELLOW_1: 3;

            hence contradiction by Th2;

          end;

           ex_sup_of ( {B, C},L) by YELLOW_0: 20;

          then ( sup {B, C}) in the carrier of K by YELLOW_0:def 17;

          then (B "\/" C) in ( rng f) by A6, YELLOW_0: 41;

          then ex x be object st x in ( dom f) & (B "\/" C) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A41, A39, A43, A45, ENUMSET1:def 3;

        end;

        thus (B "\/" D) = E

        proof

           A46:

          now

            assume (B "\/" D) = D;

            then D >= B by YELLOW_0: 22;

            then d >= b by YELLOW_0: 60;

            then td >= j by A3, WAYBEL_0: 66;

            then

             A47: j c= td by YELLOW_1: 3;

             0 in j by CARD_1: 49, TARSKI:def 1;

            hence contradiction by A47, Th4, TARSKI:def 1;

          end;

           A48:

          now

            assume (B "\/" D) = B;

            then B >= D by YELLOW_0: 22;

            then b >= d by YELLOW_0: 60;

            then j >= td by A3, WAYBEL_0: 66;

            then

             A49: td c= j by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A49, CARD_1: 49, TARSKI:def 1;

          end;

           A50:

          now

            assume (B "\/" D) = C;

            then C >= D by YELLOW_0: 22;

            then c >= d by YELLOW_0: 60;

            then dj >= td by A3, WAYBEL_0: 66;

            then

             A51: td c= dj by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A51, Th2, TARSKI:def 1;

          end;

           A52:

          now

            assume (B "\/" D) = A;

            then A >= B by YELLOW_0: 22;

            then a >= b by YELLOW_0: 60;

            then z >= j by A3, WAYBEL_0: 66;

            then j c= z by YELLOW_1: 3;

            hence contradiction;

          end;

           ex_sup_of ( {B, D},L) by YELLOW_0: 20;

          then ( sup {B, D}) in the carrier of K by YELLOW_0:def 17;

          then (B "\/" D) in ( rng f) by A6, YELLOW_0: 41;

          then ex x be object st x in ( dom f) & (B "\/" D) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A48, A50, A46, A52, ENUMSET1:def 3;

        end;

        thus (C "\/" D) = E

        proof

           A53:

          now

            assume (C "\/" D) = B;

            then B >= C by YELLOW_0: 22;

            then b >= c by YELLOW_0: 60;

            then j >= dj by A3, WAYBEL_0: 66;

            then

             A54: dj c= j by YELLOW_1: 3;

            1 in dj by Th2, TARSKI:def 1;

            then 1 in 1 by A54;

            hence contradiction;

          end;

           A55:

          now

            assume (C "\/" D) = D;

            then D >= C by YELLOW_0: 22;

            then d >= c by YELLOW_0: 60;

            then td >= dj by A3, WAYBEL_0: 66;

            then

             A56: dj c= td by YELLOW_1: 3;

            1 in dj by Th2, TARSKI:def 1;

            hence contradiction by A56, Th4, TARSKI:def 1;

          end;

           A57:

          now

            assume (C "\/" D) = C;

            then C >= D by YELLOW_0: 24;

            then c >= d by YELLOW_0: 60;

            then dj >= td by A3, WAYBEL_0: 66;

            then

             A58: td c= dj by YELLOW_1: 3;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A58, Th2, TARSKI:def 1;

          end;

           A59:

          now

            assume (C "\/" D) = A;

            then A >= C by YELLOW_0: 22;

            then a >= c by YELLOW_0: 60;

            then z >= dj by A3, WAYBEL_0: 66;

            then dj c= z by YELLOW_1: 3;

            hence contradiction by Th2;

          end;

           ex_sup_of ( {C, D},L) by YELLOW_0: 20;

          then ( sup {C, D}) in the carrier of K by YELLOW_0:def 17;

          then (C "\/" D) in ( rng f) by A6, YELLOW_0: 41;

          then ex x be object st x in ( dom f) & (C "\/" D) = (f . x) by FUNCT_1:def 3;

          hence thesis by A1, A53, A57, A55, A59, ENUMSET1:def 3;

        end;

      end;

      thus (ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e)) implies ex K be full Sublattice of L st ( M_3 ,K) are_isomorphic

      proof

        given a,b,c,d,e be Element of L such that

         AAA: (a,b,c,d,e) are_mutually_distinct and

         A70: (a "/\" b) = a and

         A71: (a "/\" c) = a and

         A72: (a "/\" d) = a and

         A73: (b "/\" e) = b and

         A74: (c "/\" e) = c and

         A75: (d "/\" e) = d and

         A76: (b "/\" c) = a and

         A77: (b "/\" d) = a and

         A78: (c "/\" d) = a and

         A79: (b "\/" c) = e and

         A80: (b "\/" d) = e and

         A81: (c "\/" d) = e;

        set ck = {a, b, c, d, e};

        reconsider ck as Subset of L;

        set K = ( subrelstr ck);

        

         A82: the carrier of K = ck by YELLOW_0:def 15;

        

         A83: K is meet-inheriting

        proof

          let x,y be Element of L;

          assume that

           A84: x in the carrier of K and

           A85: y in the carrier of K and ex_inf_of ( {x, y},L);

          per cases by A82, A84, A85, ENUMSET1:def 3;

            suppose x = a & y = a;

            then ( inf {x, y}) = (a "/\" a) by YELLOW_0: 40;

            then ( inf {x, y}) = a by YELLOW_5: 2;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = a & y = b;

            then ( inf {x, y}) = (a "/\" b) by YELLOW_0: 40;

            hence thesis by A70, A82, ENUMSET1:def 3;

          end;

            suppose x = a & y = c;

            then ( inf {x, y}) = (a "/\" c) by YELLOW_0: 40;

            hence thesis by A71, A82, ENUMSET1:def 3;

          end;

            suppose x = a & y = d;

            then ( inf {x, y}) = (a "/\" d) by YELLOW_0: 40;

            hence thesis by A72, A82, ENUMSET1:def 3;

          end;

            suppose

             A86: x = a & y = e;

            

             A87: c <= e by A74, YELLOW_0: 25;

            a <= c by A71, YELLOW_0: 25;

            then a <= e by A87, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then ( inf {x, y}) = a by A86, YELLOW_0: 40;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = a;

            then ( inf {x, y}) = (a "/\" b) by YELLOW_0: 40;

            hence thesis by A70, A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = b;

            then ( inf {x, y}) = (b "/\" b) by YELLOW_0: 40;

            then ( inf {x, y}) = b by YELLOW_5: 2;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = c;

            then ( inf {x, y}) = (b "/\" c) by YELLOW_0: 40;

            hence thesis by A76, A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = d;

            then ( inf {x, y}) = (b "/\" d) by YELLOW_0: 40;

            hence thesis by A77, A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = e;

            then ( inf {x, y}) = (b "/\" e) by YELLOW_0: 40;

            hence thesis by A73, A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = a;

            then ( inf {x, y}) = (a "/\" c) by YELLOW_0: 40;

            hence thesis by A71, A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = b;

            then ( inf {x, y}) = (b "/\" c) by YELLOW_0: 40;

            hence thesis by A76, A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = c;

            then ( inf {x, y}) = (c "/\" c) by YELLOW_0: 40;

            then ( inf {x, y}) = c by YELLOW_5: 2;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = d;

            then ( inf {x, y}) = (c "/\" d) by YELLOW_0: 40;

            hence thesis by A78, A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = e;

            then ( inf {x, y}) = (c "/\" e) by YELLOW_0: 40;

            hence thesis by A74, A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = a;

            then ( inf {x, y}) = (a "/\" d) by YELLOW_0: 40;

            hence thesis by A72, A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = b;

            then ( inf {x, y}) = (b "/\" d) by YELLOW_0: 40;

            hence thesis by A77, A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = c;

            then ( inf {x, y}) = (c "/\" d) by YELLOW_0: 40;

            hence thesis by A78, A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = d;

            then ( inf {x, y}) = (d "/\" d) by YELLOW_0: 40;

            then ( inf {x, y}) = d by YELLOW_5: 2;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = e;

            then ( inf {x, y}) = (d "/\" e) by YELLOW_0: 40;

            hence thesis by A75, A82, ENUMSET1:def 3;

          end;

            suppose

             A88: x = e & y = a;

            

             A89: c <= e by A74, YELLOW_0: 25;

            a <= c by A71, YELLOW_0: 25;

            then a <= e by A89, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then ( inf {x, y}) = a by A88, YELLOW_0: 40;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = e & y = b;

            then ( inf {x, y}) = (b "/\" e) by YELLOW_0: 40;

            hence thesis by A73, A82, ENUMSET1:def 3;

          end;

            suppose x = e & y = c;

            then ( inf {x, y}) = (c "/\" e) by YELLOW_0: 40;

            hence thesis by A74, A82, ENUMSET1:def 3;

          end;

            suppose x = e & y = d;

            then ( inf {x, y}) = (d "/\" e) by YELLOW_0: 40;

            hence thesis by A75, A82, ENUMSET1:def 3;

          end;

            suppose x = e & y = e;

            then ( inf {x, y}) = (e "/\" e) by YELLOW_0: 40;

            then ( inf {x, y}) = e by YELLOW_5: 2;

            hence thesis by A82, ENUMSET1:def 3;

          end;

        end;

        K is join-inheriting

        proof

          let x,y be Element of L;

          assume that

           A90: x in the carrier of K and

           A91: y in the carrier of K and ex_sup_of ( {x, y},L);

          per cases by A82, A90, A91, ENUMSET1:def 3;

            suppose x = a & y = a;

            then ( sup {x, y}) = (a "\/" a) by YELLOW_0: 41;

            then ( sup {x, y}) = a by YELLOW_5: 1;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = a & y = b;

            then (x "\/" y) = b by A70, Th5;

            then ( sup {x, y}) = b by YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = a & y = c;

            then (x "\/" y) = c by A71, Th5;

            then ( sup {x, y}) = c by YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = a & y = d;

            then (x "\/" y) = d by A72, Th5;

            then ( sup {x, y}) = d by YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A92: x = a & y = e;

            

             A93: c <= e by A74, YELLOW_0: 25;

            a <= c by A71, YELLOW_0: 25;

            then a <= e by A93, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then (a "\/" e) = e by Th5;

            then ( sup {x, y}) = e by A92, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A94: x = b & y = a;

            (a "\/" b) = b by A70, Th5;

            then ( sup {x, y}) = b by A94, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = b;

            then ( sup {x, y}) = (b "\/" b) by YELLOW_0: 41;

            then ( sup {x, y}) = b by YELLOW_5: 1;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = c;

            then ( sup {x, y}) = (b "\/" c) by YELLOW_0: 41;

            hence thesis by A79, A82, ENUMSET1:def 3;

          end;

            suppose x = b & y = d;

            then ( sup {x, y}) = (b "\/" d) by YELLOW_0: 41;

            hence thesis by A80, A82, ENUMSET1:def 3;

          end;

            suppose

             A95: x = b & y = e;

            (b "\/" e) = e by A73, Th5;

            then ( sup {x, y}) = e by A95, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A96: x = c & y = a;

            (c "\/" a) = c by A71, Th5;

            then ( sup {x, y}) = c by A96, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = b;

            then ( sup {x, y}) = (b "\/" c) by YELLOW_0: 41;

            hence thesis by A79, A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = c;

            then ( sup {x, y}) = (c "\/" c) by YELLOW_0: 41;

            then ( sup {x, y}) = c by YELLOW_5: 1;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = c & y = d;

            then ( sup {x, y}) = (c "\/" d) by YELLOW_0: 41;

            hence thesis by A81, A82, ENUMSET1:def 3;

          end;

            suppose

             A97: x = c & y = e;

            (c "\/" e) = e by A74, Th5;

            then ( sup {x, y}) = e by A97, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = a;

            then (x "\/" y) = d by A72, Th5;

            then ( sup {x, y}) = d by YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = b;

            then ( sup {x, y}) = (b "\/" d) by YELLOW_0: 41;

            hence thesis by A80, A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = c;

            then ( sup {x, y}) = (c "\/" d) by YELLOW_0: 41;

            hence thesis by A81, A82, ENUMSET1:def 3;

          end;

            suppose x = d & y = d;

            then ( sup {x, y}) = (d "\/" d) by YELLOW_0: 41;

            then ( sup {x, y}) = d by YELLOW_5: 1;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A98: x = d & y = e;

            (d "\/" e) = e by A75, Th5;

            then ( sup {x, y}) = e by A98, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A99: x = e & y = a;

            

             A100: c <= e by A74, YELLOW_0: 25;

            a <= c by A71, YELLOW_0: 25;

            then a <= e by A100, ORDERS_2: 3;

            then (a "/\" e) = a by YELLOW_0: 25;

            then (a "\/" e) = e by Th5;

            then ( sup {x, y}) = e by A99, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A101: x = e & y = b;

            (b "\/" e) = e by A73, Th5;

            then ( sup {x, y}) = e by A101, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A102: x = e & y = c;

            (c "\/" e) = e by A74, Th5;

            then ( sup {x, y}) = e by A102, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose

             A103: x = e & y = d;

            (d "\/" e) = e by A75, Th5;

            then ( sup {x, y}) = e by A103, YELLOW_0: 41;

            hence thesis by A82, ENUMSET1:def 3;

          end;

            suppose x = e & y = e;

            then ( sup {x, y}) = (e "\/" e) by YELLOW_0: 41;

            then ( sup {x, y}) = e by YELLOW_5: 1;

            hence thesis by A82, ENUMSET1:def 3;

          end;

        end;

        then

        reconsider K as non empty full Sublattice of L by A83, YELLOW_0:def 15;

        take K;

        thus ( M_3 ,K) are_isomorphic

        proof

          reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;

          reconsider td = (3 \ 2) as Element of M_3 by A1, ENUMSET1:def 3;

          reconsider dj = (2 \ 1) as Element of M_3 by A1, ENUMSET1:def 3;

           A104:

          now

            

             A105: 2 in t by CARD_1: 51, ENUMSET1:def 1;

            assume dj = t;

            hence contradiction by A105, Th2, TARSKI:def 1;

          end;

           A106:

          now

            

             A107: 0 in t by CARD_1: 51, ENUMSET1:def 1;

            assume td = t;

            hence contradiction by A107, Th4, TARSKI:def 1;

          end;

          reconsider j = 1 as Element of M_3 by A1, ENUMSET1:def 3;

          reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;

          defpred P[ object, object] means for X be Element of M_3 st X = $1 holds ((X = z implies $2 = a) & (X = j implies $2 = b) & (X = dj implies $2 = c) & (X = td implies $2 = d) & (X = t implies $2 = e));

           A108:

          now

            assume

             A109: j = dj;

            1 in dj by Th2, TARSKI:def 1;

            hence contradiction by A109;

          end;

           A110:

          now

            assume

             A111: j = td;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A111, CARD_1: 49, TARSKI:def 1;

          end;

           A112:

          now

            assume

             A113: dj = td;

            2 in td by Th4, TARSKI:def 1;

            hence contradiction by A113, Th2, TARSKI:def 1;

          end;

          

           A114: for x be object st x in cn holds ex y be object st y in ck & P[x, y]

          proof

            let x be object;

            assume

             A115: x in cn;

            per cases by A1, A115, ENUMSET1:def 3;

              suppose

               A116: x = 0 ;

              take y = a;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of M_3 ;

              thus thesis by A116, Th2, Th4;

            end;

              suppose

               A117: x = 1;

              take y = b;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of M_3 ;

              thus thesis by A108, A110, A117;

            end;

              suppose

               A118: x = (2 \ 1);

              take y = c;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of M_3 ;

              thus thesis by A108, A112, A104, A118, Th2;

            end;

              suppose

               A119: x = (3 \ 2);

              take y = d;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of M_3 ;

              thus thesis by A110, A112, A106, A119, Th4;

            end;

              suppose

               A120: x = 3;

              take y = e;

              thus y in ck by ENUMSET1:def 3;

              let X be Element of M_3 ;

              thus thesis by A104, A106, A120;

            end;

          end;

          consider f be Function of cn, ck such that

           A121: for x be object st x in cn holds P[x, (f . x)] from FUNCT_2:sch 1( A114);

          reconsider f as Function of M_3 , K by A82;

           A122:

          now

            let x,y be Element of M_3 ;

            assume

             A123: (f . x) = (f . y);

            thus x = y

            proof

              per cases by A1, ENUMSET1:def 3;

                suppose x = z & y = z;

                hence thesis;

              end;

                suppose x = j & y = j;

                hence thesis;

              end;

                suppose x = dj & y = dj;

                hence thesis;

              end;

                suppose x = td & y = td;

                hence thesis;

              end;

                suppose x = t & y = t;

                hence thesis;

              end;

                suppose

                 A124: x = z & y = j;

                then (f . x) = a by A121;

                hence thesis by AAA, A121, A123, A124;

              end;

                suppose

                 A125: x = z & y = dj;

                then (f . x) = a by A121;

                hence thesis by AAA, A121, A123, A125;

              end;

                suppose

                 A126: x = z & y = td;

                then (f . x) = a by A121;

                hence thesis by AAA, A121, A123, A126;

              end;

                suppose

                 A127: x = z & y = t;

                then (f . x) = a by A121;

                hence thesis by AAA, A121, A123, A127;

              end;

                suppose

                 A128: x = j & y = z;

                then (f . x) = b by A121;

                hence thesis by AAA, A121, A123, A128;

              end;

                suppose

                 A129: x = j & y = dj;

                then (f . x) = b by A121;

                hence thesis by AAA, A121, A123, A129;

              end;

                suppose

                 A130: x = j & y = td;

                then (f . x) = b by A121;

                hence thesis by AAA, A121, A123, A130;

              end;

                suppose

                 A131: x = j & y = t;

                then (f . x) = b by A121;

                hence thesis by AAA, A121, A123, A131;

              end;

                suppose

                 A132: x = dj & y = z;

                then (f . x) = c by A121;

                hence thesis by AAA, A121, A123, A132;

              end;

                suppose

                 A133: x = dj & y = j;

                then (f . x) = c by A121;

                hence thesis by AAA, A121, A123, A133;

              end;

                suppose

                 A134: x = dj & y = td;

                then (f . x) = c by A121;

                hence thesis by AAA, A121, A123, A134;

              end;

                suppose

                 A135: x = dj & y = t;

                then (f . x) = c by A121;

                hence thesis by AAA, A121, A123, A135;

              end;

                suppose

                 A136: x = td & y = z;

                then (f . x) = d by A121;

                hence thesis by AAA, A121, A123, A136;

              end;

                suppose

                 A137: x = td & y = j;

                then (f . x) = d by A121;

                hence thesis by AAA, A121, A123, A137;

              end;

                suppose

                 A138: x = td & y = dj;

                then (f . x) = d by A121;

                hence thesis by AAA, A121, A123, A138;

              end;

                suppose

                 A139: x = td & y = t;

                then (f . x) = d by A121;

                hence thesis by AAA, A121, A123, A139;

              end;

                suppose

                 A140: x = t & y = z;

                then (f . x) = e by A121;

                hence thesis by AAA, A121, A123, A140;

              end;

                suppose

                 A141: x = t & y = j;

                then (f . x) = e by A121;

                hence thesis by AAA, A121, A123, A141;

              end;

                suppose

                 A142: x = t & y = dj;

                then (f . x) = e by A121;

                hence thesis by AAA, A121, A123, A142;

              end;

                suppose

                 A143: x = t & y = td;

                then (f . x) = e by A121;

                hence thesis by AAA, A121, A123, A143;

              end;

            end;

          end;

          

           A144: ( rng f) c= ck

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

             A145: x in ( dom f) and

             A146: y = (f . x) by FUNCT_1:def 3;

            reconsider x as Element of M_3 by A145;

            x = z or x = j or x = dj or x = td or x = t by A1, ENUMSET1:def 3;

            then y = a or y = d or y = c or y = b or y = e by A121, A146;

            hence thesis by ENUMSET1:def 3;

          end;

          

           A147: ( dom f) = the carrier of M_3 by FUNCT_2:def 1;

          ck c= ( rng f)

          proof

            let y be object;

            assume

             A148: y in ck;

            per cases by A148, ENUMSET1:def 3;

              suppose

               A149: y = a;

              a = (f . z) by A121;

              hence thesis by A147, A149, FUNCT_1:def 3;

            end;

              suppose

               A150: y = b;

              b = (f . j) by A121;

              hence thesis by A147, A150, FUNCT_1:def 3;

            end;

              suppose

               A151: y = c;

              c = (f . dj) by A121;

              hence thesis by A147, A151, FUNCT_1:def 3;

            end;

              suppose

               A152: y = d;

              d = (f . td) by A121;

              hence thesis by A147, A152, FUNCT_1:def 3;

            end;

              suppose

               A153: y = e;

              e = (f . t) by A121;

              hence thesis by A147, A153, FUNCT_1:def 3;

            end;

          end;

          then

           A154: ( rng f) = ck by A144;

          

           A155: for x,y be Element of M_3 holds x <= y iff (f . x) <= (f . y)

          proof

            let x,y be Element of M_3 ;

            thus x <= y implies (f . x) <= (f . y)

            proof

              assume

               A156: x <= y;

              per cases by A1, ENUMSET1:def 3;

                suppose x = z & y = z;

                hence thesis;

              end;

                suppose

                 A157: x = z & y = j;

                then

                 A158: (f . y) = b by A121;

                

                 A159: a <= b by A70, YELLOW_0: 25;

                (f . x) = a by A121, A157;

                hence thesis by A158, A159, YELLOW_0: 60;

              end;

                suppose

                 A160: x = z & y = dj;

                then

                 A161: (f . y) = c by A121;

                

                 A162: a <= c by A71, YELLOW_0: 25;

                (f . x) = a by A121, A160;

                hence thesis by A161, A162, YELLOW_0: 60;

              end;

                suppose

                 A163: x = z & y = td;

                then

                 A164: (f . y) = d by A121;

                

                 A165: a <= d by A72, YELLOW_0: 25;

                (f . x) = a by A121, A163;

                hence thesis by A164, A165, YELLOW_0: 60;

              end;

                suppose

                 A166: x = z & y = t;

                

                 A167: c <= e by A74, YELLOW_0: 25;

                a <= c by A71, YELLOW_0: 25;

                then

                 A168: a <= e by A167, ORDERS_2: 3;

                

                 A169: (f . y) = e by A121, A166;

                (f . x) = a by A121, A166;

                hence thesis by A169, A168, YELLOW_0: 60;

              end;

                suppose x = j & y = z;

                then j c= z by A156, YELLOW_1: 3;

                hence thesis;

              end;

                suppose x = j & y = j;

                hence thesis;

              end;

                suppose

                 A170: x = j & y = dj;

                 0 in j by CARD_1: 49, TARSKI:def 1;

                then not j c= dj by Th2, TARSKI:def 1;

                hence thesis by A156, A170, YELLOW_1: 3;

              end;

                suppose

                 A171: x = j & y = td;

                 0 in j by CARD_1: 49, TARSKI:def 1;

                then not j c= td by Th4, TARSKI:def 1;

                hence thesis by A156, A171, YELLOW_1: 3;

              end;

                suppose

                 A172: x = j & y = t;

                then

                 A173: (f . y) = e by A121;

                

                 A174: b <= e by A73, YELLOW_0: 25;

                (f . x) = b by A121, A172;

                hence thesis by A173, A174, YELLOW_0: 60;

              end;

                suppose x = dj & y = z;

                then dj c= z by A156, YELLOW_1: 3;

                hence thesis by Th2;

              end;

                suppose

                 A175: x = dj & y = j;

                

                 A176: not 1 in j;

                1 in dj by Th2, TARSKI:def 1;

                then not dj c= j by A176;

                hence thesis by A156, A175, YELLOW_1: 3;

              end;

                suppose x = dj & y = dj;

                hence thesis;

              end;

                suppose

                 A177: x = dj & y = td;

                1 in dj by Th2, TARSKI:def 1;

                then not dj c= td by Th4, TARSKI:def 1;

                hence thesis by A156, A177, YELLOW_1: 3;

              end;

                suppose

                 A178: x = dj & y = t;

                then

                 A179: (f . y) = e by A121;

                

                 A180: c <= e by A74, YELLOW_0: 25;

                (f . x) = c by A121, A178;

                hence thesis by A179, A180, YELLOW_0: 60;

              end;

                suppose x = td & y = z;

                then td c= z by A156, YELLOW_1: 3;

                hence thesis by Th4;

              end;

                suppose

                 A181: x = td & y = j;

                2 in td by Th4, TARSKI:def 1;

                then not td c= j by CARD_1: 49, TARSKI:def 1;

                hence thesis by A156, A181, YELLOW_1: 3;

              end;

                suppose

                 A182: x = td & y = dj;

                2 in td by Th4, TARSKI:def 1;

                then not td c= dj by Th2, TARSKI:def 1;

                hence thesis by A156, A182, YELLOW_1: 3;

              end;

                suppose x = td & y = td;

                hence thesis;

              end;

                suppose

                 A183: x = td & y = t;

                then

                 A184: (f . y) = e by A121;

                

                 A185: d <= e by A75, YELLOW_0: 25;

                (f . x) = d by A121, A183;

                hence thesis by A184, A185, YELLOW_0: 60;

              end;

                suppose x = t & y = z;

                then t c= z by A156, YELLOW_1: 3;

                hence thesis;

              end;

                suppose

                 A186: x = t & y = j;

                

                 A187: not 1 in j;

                1 in t by CARD_1: 51, ENUMSET1:def 1;

                then not t c= j by A187;

                hence thesis by A156, A186, YELLOW_1: 3;

              end;

                suppose

                 A188: x = t & y = dj;

                2 in t by CARD_1: 51, ENUMSET1:def 1;

                then not t c= dj by Th2, TARSKI:def 1;

                hence thesis by A156, A188, YELLOW_1: 3;

              end;

                suppose

                 A189: x = t & y = td;

                 0 in t by CARD_1: 51, ENUMSET1:def 1;

                then not t c= td by Th4, TARSKI:def 1;

                hence thesis by A156, A189, YELLOW_1: 3;

              end;

                suppose x = t & y = t;

                hence thesis;

              end;

            end;

            thus (f . x) <= (f . y) implies x <= y

            proof

              

               A190: dj c= t

              proof

                let X be object;

                assume X in dj;

                then X = 1 by Th2, TARSKI:def 1;

                hence thesis by CARD_1: 51, ENUMSET1:def 1;

              end;

              

               A191: (f . y) in ck by A147, A154, FUNCT_1:def 3;

              

               A192: (f . x) in ck by A147, A154, FUNCT_1:def 3;

              assume

               A193: (f . x) <= (f . y);

              per cases by A192, A191, ENUMSET1:def 3;

                suppose (f . x) = a & (f . y) = a;

                hence thesis by A122;

              end;

                suppose

                 A194: (f . x) = a & (f . y) = b;

                (f . z) = a by A121;

                then z = x by A122, A194;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose

                 A195: (f . x) = a & (f . y) = c;

                (f . z) = a by A121;

                then z = x by A122, A195;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose

                 A196: (f . x) = a & (f . y) = d;

                (f . z) = a by A121;

                then z = x by A122, A196;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose

                 A197: (f . x) = a & (f . y) = e;

                (f . z) = a by A121;

                then z = x by A122, A197;

                then x c= y;

                hence thesis by YELLOW_1: 3;

              end;

                suppose (f . x) = b & (f . y) = a;

                then b <= a by A193, YELLOW_0: 59;

                hence thesis by AAA, A70, YELLOW_0: 25;

              end;

                suppose (f . x) = b & (f . y) = b;

                hence thesis by A122;

              end;

                suppose (f . x) = b & (f . y) = c;

                then b <= c by A193, YELLOW_0: 59;

                hence thesis by AAA, A76, YELLOW_0: 25;

              end;

                suppose (f . x) = b & (f . y) = d;

                then b <= d by A193, YELLOW_0: 59;

                hence thesis by AAA, A77, YELLOW_0: 25;

              end;

                suppose

                 A198: (f . x) = b & (f . y) = e;

                (f . t) = e by A121;

                then

                 A199: t = y by A122, A198;

                (f . j) = b by A121;

                then

                 A200: j = x by A122, A198;

                ( Segm 1) c= ( Segm 3) by NAT_1: 39;

                hence thesis by YELLOW_1: 3, A200, A199;

              end;

                suppose (f . x) = c & (f . y) = a;

                then c <= a by A193, YELLOW_0: 59;

                hence thesis by AAA, A71, YELLOW_0: 25;

              end;

                suppose (f . x) = c & (f . y) = b;

                then c <= b by A193, YELLOW_0: 59;

                hence thesis by AAA, A76, YELLOW_0: 25;

              end;

                suppose (f . x) = c & (f . y) = c;

                hence thesis by A122;

              end;

                suppose (f . x) = c & (f . y) = d;

                then c <= d by A193, YELLOW_0: 59;

                hence thesis by AAA, A78, YELLOW_0: 25;

              end;

                suppose

                 A201: (f . x) = c & (f . y) = e;

                (f . t) = e by A121;

                then

                 A202: t = y by A122, A201;

                (f . dj) = c by A121;

                then dj = x by A122, A201;

                hence thesis by A190, A202, YELLOW_1: 3;

              end;

                suppose (f . x) = d & (f . y) = a;

                then d <= a by A193, YELLOW_0: 59;

                hence thesis by AAA, A72, YELLOW_0: 25;

              end;

                suppose (f . x) = d & (f . y) = b;

                then d <= b by A193, YELLOW_0: 59;

                hence thesis by AAA, A77, YELLOW_0: 25;

              end;

                suppose (f . x) = d & (f . y) = c;

                then d <= c by A193, YELLOW_0: 59;

                hence thesis by AAA, A78, YELLOW_0: 25;

              end;

                suppose (f . x) = d & (f . y) = d;

                hence thesis by A122;

              end;

                suppose

                 A203: (f . x) = d & (f . y) = e;

                (f . t) = e by A121;

                then

                 A204: t = y by A122, A203;

                (f . td) = d by A121;

                then td = x by A122, A203;

                hence thesis by A204, YELLOW_1: 3;

              end;

                suppose

                 A205: (f . x) = e & (f . y) = a;

                

                 A206: a <= b by A70, YELLOW_0: 25;

                e <= a by A193, A205, YELLOW_0: 59;

                then e <= b by A206, ORDERS_2: 3;

                hence thesis by AAA, A73, YELLOW_0: 25;

              end;

                suppose (f . x) = e & (f . y) = b;

                then e <= b by A193, YELLOW_0: 59;

                hence thesis by AAA, A73, YELLOW_0: 25;

              end;

                suppose (f . x) = e & (f . y) = c;

                then e <= c by A193, YELLOW_0: 59;

                hence thesis by AAA, A74, YELLOW_0: 25;

              end;

                suppose (f . x) = e & (f . y) = d;

                then e <= d by A193, YELLOW_0: 59;

                hence thesis by AAA, A75, YELLOW_0: 25;

              end;

                suppose (f . x) = e & (f . y) = e;

                hence thesis by A122;

              end;

            end;

          end;

          take f;

          f is one-to-one by A122;

          hence thesis by A82, A154, A155, WAYBEL_0: 66;

        end;

      end;

    end;

    begin

    definition

      let L be non empty RelStr;

      :: YELLOW11:def3

      attr L is modular means for a,b,c be Element of L st a <= c holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" c);

    end

    registration

      cluster distributive -> modular for non empty antisymmetric reflexive with_infima RelStr;

      coherence

      proof

        let L be non empty antisymmetric reflexive with_infima RelStr;

        assume

         A1: L is distributive;

        now

          let a,b,c be Element of L;

          assume a <= c;

          

          hence (a "\/" (b "/\" c)) = ((a "/\" c) "\/" (b "/\" c)) by YELLOW_0: 25

          .= ((a "\/" b) "/\" c) by A1;

        end;

        hence thesis;

      end;

    end

    

     Lm2: for L be LATTICE holds L is modular iff not ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e)

    proof

      let L be LATTICE;

      now

        given a,b,c,d,e be Element of L such that

         A1: b <> d and

         A2: (a "/\" b) = a and

         A3: (d "/\" e) = d and

         A4: (b "/\" d) = b and

         A5: (c "/\" d) = a and

         A6: (b "\/" c) = e;

        

         A7: b <= d by A4, YELLOW_0: 23;

        (b "\/" (c "/\" d)) = b by A2, A5, Th5;

        hence not L is modular by A1, A3, A6, A7;

      end;

      hence L is modular implies not ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e);

      now

        assume not L is modular;

        then

        consider x,y,z be Element of L such that

         A8: x <= z and

         A9: (x "\/" (y "/\" z)) <> ((x "\/" y) "/\" z);

        (x "\/" (y "/\" z)) <= (z "\/" (y "/\" z)) by A8, YELLOW_5: 7;

        then

         A10: (x "\/" (y "/\" z)) <= z by LATTICE3: 17;

        set z1 = ((x "\/" y) "/\" z);

        set y1 = y;

        (x "\/" y) <= (x "\/" y);

        then ((x "\/" y) "/\" x) <= ((x "\/" y) "/\" z) by A8, YELLOW_3: 2;

        then x <= ((x "\/" y) "/\" z) by LATTICE3: 18;

        then

         A11: (x "\/" y) <= (z1 "\/" y1) by YELLOW_5: 7;

        set x1 = (x "\/" (y "/\" z));

        

         A12: (y "/\" z) <= y1 by YELLOW_0: 23;

        y <= y;

        then

         A13: (x1 "/\" y1) <= (y "/\" z) by A10, YELLOW_3: 2;

        set t = (x "\/" y);

        set b = (y "/\" z);

         A14:

        now

          assume

           A15: b = t;

          

          then ((x "\/" y) "/\" z) = (y "/\" (z "/\" z)) by LATTICE3: 16

          .= (x "\/" y) by A15, YELLOW_5: 2

          .= ((x "\/" x) "\/" y) by YELLOW_5: 1

          .= (x "\/" (y "/\" z)) by A15, LATTICE3: 14;

          hence contradiction by A9;

        end;

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

        then ((y "/\" z) "/\" (y "/\" z)) <= (x1 "/\" y1) by A12, YELLOW_3: 2;

        then

         A16: (y "/\" z) <= (x1 "/\" y1) by YELLOW_5: 2;

        

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

        thus ex a,b,c,d,e be Element of L st (a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e

        proof

          take b, x1, y1, z1, t;

          

           A18: y1 <= (x "\/" y) by YELLOW_0: 22;

          now

            

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

            assume

             A20: b = x1;

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

            then x <= y by A19, YELLOW_0:def 2;

            hence contradiction by A9, A20, YELLOW_5: 8;

          end;

          hence b <> x1;

          now

            assume

             A21: b = y1;

            then y <= z by YELLOW_0: 23;

            hence contradiction by A8, A9, A21, YELLOW_5: 9, YELLOW_5: 10;

          end;

          hence b <> y1;

          now

            assume b = z1;

            then

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

            (x "\/" (y "/\" z)) <= ((x "\/" y) "/\" z) by A8, Th8;

            hence contradiction by A9, A22, YELLOW_0:def 3;

          end;

          hence b <> z1;

          thus b <> t by A14;

          now

            

             A23: (x1 "\/" y1) = (x "\/" ((y "/\" z) "\/" y)) by LATTICE3: 14

            .= t by LATTICE3: 17;

            assume

             A24: x1 = y1;

            then

             A25: (x1 "\/" y1) = x1 by YELLOW_5: 1;

            (x1 "/\" y1) = x1 by A24, YELLOW_5: 2;

            hence contradiction by A16, A13, A14, A25, A23, YELLOW_0:def 3;

          end;

          hence x1 <> y1;

          thus x1 <> z1 by A9;

          now

            assume t = x1;

            then

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

            (x "\/" (y "/\" z)) <= ((x "\/" y) "/\" z) by A8, Th8;

            hence contradiction by A9, A26, YELLOW_0:def 3;

          end;

          hence x1 <> t;

          now

            

             A27: (y1 "/\" z1) = (((x "\/" y) "/\" y) "/\" z) by LATTICE3: 16

            .= b by LATTICE3: 18;

            assume

             A28: y1 = z1;

            then

             A29: (z1 "\/" y1) = z1 by YELLOW_5: 1;

            (z1 "/\" y1) = z1 by A28, YELLOW_5: 2;

            hence contradiction by A14, A17, A11, A29, A27, YELLOW_0:def 3;

          end;

          hence y1 <> z1;

          now

            assume

             A30: y1 = t;

            then x <= y by YELLOW_0: 22;

            then (x "/\" x) <= (y "/\" z) by A8, YELLOW_3: 2;

            then x <= (y "/\" z) by YELLOW_5: 2;

            hence contradiction by A9, A30, YELLOW_5: 8;

          end;

          hence y1 <> t;

          now

            

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

            assume

             A32: z1 = t;

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

            then y <= z by A31, YELLOW_0:def 2;

            hence contradiction by A9, A32, YELLOW_5: 10;

          end;

          hence z1 <> t;

          b <= x1 by YELLOW_0: 22;

          hence (b "/\" x1) = b by YELLOW_5: 10;

          b <= y1 by YELLOW_0: 23;

          hence (b "/\" y1) = b by YELLOW_5: 10;

          y1 <= t by YELLOW_0: 22;

          hence (y1 "/\" t) = y1 by YELLOW_5: 10;

          z1 <= t by YELLOW_0: 23;

          hence (z1 "/\" t) = z1 by YELLOW_5: 10;

          thus (x1 "/\" y1) = b by A16, A13, YELLOW_0:def 3;

          thus (x1 "/\" z1) = x1 by A8, Th8, YELLOW_5: 10;

          

          thus (y1 "/\" z1) = ((y "/\" (x "\/" y)) "/\" z) by LATTICE3: 16

          .= b by LATTICE3: 18;

          

          thus (x1 "\/" y1) = (x "\/" ((y "/\" z) "\/" y)) by LATTICE3: 14

          .= t by LATTICE3: 17;

          (x "\/" y) <= (x "\/" y);

          then ((x "\/" y) "/\" x) <= ((x "\/" y) "/\" z) by A8, YELLOW_3: 2;

          then x <= ((x "\/" y) "/\" z) by LATTICE3: 18;

          then

           A33: (x "\/" y) <= (z1 "\/" y1) by YELLOW_5: 7;

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

          then (y1 "\/" z1) <= (x "\/" y) by A18, YELLOW_5: 9;

          hence thesis by A33, YELLOW_0:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: YELLOW11:11

    for L be LATTICE holds L is modular iff not ex K be full Sublattice of L st ( N_5 ,K) are_isomorphic

    proof

      let L be LATTICE;

      thus L is modular implies not ex K be full Sublattice of L st ( N_5 ,K) are_isomorphic

      proof

        assume L is modular;

        then not ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e) by Lm2;

        hence thesis by Th9;

      end;

      assume not ex K be full Sublattice of L st ( N_5 ,K) are_isomorphic ;

      then not ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = b & (c "/\" d) = a & (b "\/" c) = e & (c "\/" d) = e) by Th9;

      hence thesis by Lm2;

    end;

    

     Lm3: for L be LATTICE st L is modular holds L is distributive iff not ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e)

    proof

      let L be LATTICE;

      assume

       A1: L is modular;

      now

        given a,b,c,d,e be Element of L such that

         A2: a <> d and

         A3: (d "/\" e) = d and

         A4: (b "/\" c) = a and

         A5: (b "/\" d) = a and

         A6: (c "/\" d) = a and

         A7: (b "\/" c) = e;

        ((b "/\" c) "\/" (b "/\" d)) = a by A4, A5, YELLOW_5: 1;

        hence not L is distributive by A2, A3, A4, A6, A7;

      end;

      hence L is distributive implies not ex a,b,c,d,e be Element of L st (a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e;

      now

        assume not L is distributive;

        then

        consider x,y,z be Element of L such that

         A8: (x "/\" (y "\/" z)) <> ((x "/\" y) "\/" (x "/\" z));

        set t = (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x));

        set b = (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x));

        

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

        

         A10: (x "/\" t) = ((x "/\" ((x "\/" y) "/\" (y "\/" z))) "/\" (z "\/" x)) by LATTICE3: 16

        .= (((x "/\" (x "\/" y)) "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3: 16

        .= ((x "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3: 18

        .= ((x "/\" (z "\/" x)) "/\" (y "\/" z)) by LATTICE3: 16

        .= (x "/\" (y "\/" z)) by LATTICE3: 18;

        

         A11: x <= x;

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

        then

         A12: (((y "/\" z) "/\" x) "\/" (z "/\" x)) = (z "/\" x) by A11, YELLOW_3: 2, YELLOW_5: 8;

        

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

         A14:

        now

          assume b = t;

          

          then (x "/\" (y "\/" z)) = (((x "/\" y) "\/" ((y "/\" z) "\/" (z "/\" x))) "/\" x) by A10, LATTICE3: 14

          .= ((x "/\" y) "\/" (((y "/\" z) "\/" (z "/\" x)) "/\" x)) by A1, A9

          .= ((x "/\" y) "\/" (z "/\" x)) by A1, A13, A12;

          hence contradiction by A8;

        end;

        set y1 = ((y "\/" b) "/\" t);

        

         A15: (y "/\" z) <= (y "\/" z) by YELLOW_5: 5;

        (y "/\" z) <= (x "\/" y) by YELLOW_5: 5;

        then ((y "/\" z) "/\" (y "/\" z)) <= ((x "\/" y) "/\" (y "\/" z)) by A15, YELLOW_3: 2;

        then

         A16: (y "/\" z) <= ((x "\/" y) "/\" (y "\/" z)) by YELLOW_5: 2;

        (y "/\" z) <= (z "\/" x) by YELLOW_5: 5;

        then ((y "/\" z) "/\" (y "/\" z)) <= (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A16, YELLOW_3: 2;

        then

         A17: (y "/\" z) <= t by YELLOW_5: 2;

        

         A18: (x "/\" t) = ((x "/\" ((x "\/" y) "/\" (y "\/" z))) "/\" (z "\/" x)) by LATTICE3: 16

        .= (((x "/\" (x "\/" y)) "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3: 16

        .= ((x "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3: 18

        .= (((z "\/" x) "/\" x) "/\" (y "\/" z)) by LATTICE3: 16

        .= (x "/\" (y "\/" z)) by LATTICE3: 18;

        set z1 = ((z "\/" b) "/\" t);

        

         A19: (z "/\" x) <= (y "\/" z) by YELLOW_5: 5;

        (z "/\" x) <= (x "\/" y) by YELLOW_5: 5;

        then ((z "/\" x) "/\" (z "/\" x)) <= ((x "\/" y) "/\" (y "\/" z)) by A19, YELLOW_3: 2;

        then

         A20: (z "/\" x) <= ((x "\/" y) "/\" (y "\/" z)) by YELLOW_5: 2;

        (z "/\" x) <= (z "\/" x) by YELLOW_5: 5;

        then ((z "/\" x) "/\" (z "/\" x)) <= (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A20, YELLOW_3: 2;

        then

         A21: (z "/\" x) <= t by YELLOW_5: 2;

        

         A22: (y "/\" t) = ((y "/\" ((x "\/" y) "/\" (y "\/" z))) "/\" (z "\/" x)) by LATTICE3: 16

        .= (((y "/\" (x "\/" y)) "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3: 16

        .= ((y "/\" (y "\/" z)) "/\" (z "\/" x)) by LATTICE3: 18

        .= (y "/\" (x "\/" z)) by LATTICE3: 18;

        

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

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

        then

         A24: (x "/\" z) <= (x "\/" (y "/\" z)) by A23, YELLOW_0:def 2;

        

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

        

         A26: (z "\/" (x "/\" y)) <= ((z "\/" x) "/\" (z "\/" y)) by Th7;

        

         A27: (y "\/" (x "/\" z)) <= ((y "\/" x) "/\" (y "\/" z)) by Th7;

        

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

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

        then

         A29: (x "/\" (z "\/" y)) <= (x "\/" y) by A28, YELLOW_0:def 2;

        

         A30: (y "\/" b) = ((y "\/" ((x "/\" y) "\/" (y "/\" z))) "\/" (z "/\" x)) by LATTICE3: 14

        .= (((y "\/" (x "/\" y)) "\/" (y "/\" z)) "\/" (z "/\" x)) by LATTICE3: 14

        .= ((y "\/" (y "/\" z)) "\/" (z "/\" x)) by LATTICE3: 17

        .= (y "\/" (x "/\" z)) by LATTICE3: 17;

        

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

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

        then

         A32: (x "/\" y) <= (x "\/" (z "/\" y)) by A31, YELLOW_0:def 2;

        

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

        

         A34: (y "\/" (z "/\" x)) <= ((y "\/" z) "/\" (y "\/" x)) by Th7;

        

         A35: ((x "/\" y) "\/" (y "/\" z)) <= (y "/\" (x "\/" z)) by Th6;

        

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

        

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

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

        then

         A38: (z "/\" (y "\/" x)) <= (z "\/" x) by A37, YELLOW_0:def 2;

        

         A39: (z "\/" b) = ((z "\/" (z "/\" x)) "\/" ((x "/\" y) "\/" (y "/\" z))) by LATTICE3: 14

        .= (z "\/" ((y "/\" z) "\/" (x "/\" y))) by LATTICE3: 17

        .= ((z "\/" (y "/\" z)) "\/" (x "/\" y)) by LATTICE3: 14

        .= (z "\/" (x "/\" y)) by LATTICE3: 17;

        ((x "/\" y) "\/" (x "/\" z)) <= (x "/\" (y "\/" z)) by Th6;

        then (((x "/\" y) "\/" (x "/\" z)) "\/" ((x "/\" y) "\/" (y "/\" z))) <= ((x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z))) by A35, YELLOW_3: 3;

        then ((x "/\" z) "\/" ((x "/\" y) "\/" ((x "/\" y) "\/" (y "/\" z)))) <= ((x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z))) by LATTICE3: 14;

        then ((x "/\" z) "\/" (((x "/\" y) "\/" (x "/\" y)) "\/" (y "/\" z))) <= ((x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z))) by LATTICE3: 14;

        then ((((x "/\" y) "\/" (x "/\" y)) "\/" (x "/\" z)) "\/" (y "/\" z)) <= ((x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z))) by LATTICE3: 14;

        then (((x "/\" y) "\/" (x "/\" z)) "\/" (y "/\" z)) <= ((x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z))) by YELLOW_5: 1;

        then

         A40: b <= ((x "/\" t) "\/" (y "/\" t)) by A18, A22, LATTICE3: 14;

        z1 <= t by YELLOW_0: 23;

        then

         A41: (t "/\" z1) = z1 by YELLOW_5: 10;

        

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

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

        then

         A43: (z "/\" x) <= (z "\/" (y "/\" x)) by A42, YELLOW_0:def 2;

        

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

        

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

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

        then

         A46: (x "/\" (y "\/" z)) <= (x "\/" z) by A45, YELLOW_0:def 2;

        

         A47: (x "\/" b) = ((x "\/" ((x "/\" y) "\/" (y "/\" z))) "\/" (z "/\" x)) by LATTICE3: 14

        .= (((x "\/" (x "/\" y)) "\/" (y "/\" z)) "\/" (z "/\" x)) by LATTICE3: 14

        .= ((x "\/" (y "/\" z)) "\/" (z "/\" x)) by LATTICE3: 17

        .= (((z "/\" x) "\/" x) "\/" (y "/\" z)) by LATTICE3: 14

        .= (x "\/" (y "/\" z)) by LATTICE3: 17;

        (z "\/" (y "/\" x)) <= ((z "\/" y) "/\" (z "\/" x)) by Th7;

        then ((z "\/" (y "/\" x)) "/\" (y "\/" (z "/\" x))) <= (((z "\/" y) "/\" (z "\/" x)) "/\" ((y "\/" z) "/\" (y "\/" x))) by A34, YELLOW_3: 2;

        then ((z "\/" b) "/\" (y "\/" b)) <= ((((z "\/" x) "/\" (z "\/" y)) "/\" (z "\/" y)) "/\" (y "\/" x)) by A30, A39, LATTICE3: 16;

        then ((z "\/" b) "/\" (y "\/" b)) <= (((z "\/" x) "/\" ((z "\/" y) "/\" (z "\/" y))) "/\" (y "\/" x)) by LATTICE3: 16;

        then ((z "\/" b) "/\" (y "\/" b)) <= (((z "\/" x) "/\" (z "\/" y)) "/\" (y "\/" x)) by YELLOW_5: 2;

        then

         A48: ((z "\/" b) "/\" (y "\/" b)) <= t by LATTICE3: 16;

        y1 <= t by YELLOW_0: 23;

        then

         A49: (t "/\" y1) = y1 by YELLOW_5: 10;

        set x1 = ((x "\/" b) "/\" t);

        

         A50: (x "/\" y) <= (y "\/" z) by YELLOW_5: 5;

        (x "/\" y) <= (x "\/" y) by YELLOW_5: 5;

        then ((x "/\" y) "/\" (x "/\" y)) <= ((x "\/" y) "/\" (y "\/" z)) by A50, YELLOW_3: 2;

        then

         A51: (x "/\" y) <= ((x "\/" y) "/\" (y "\/" z)) by YELLOW_5: 2;

        

         A52: (z "/\" t) = ((z "/\" (z "\/" x)) "/\" ((x "\/" y) "/\" (y "\/" z))) by LATTICE3: 16

        .= (z "/\" ((y "\/" z) "/\" (x "\/" y))) by LATTICE3: 18

        .= ((z "/\" (y "\/" z)) "/\" (x "\/" y)) by LATTICE3: 16

        .= (z "/\" (x "\/" y)) by LATTICE3: 18;

        (x "\/" (y "/\" z)) <= ((x "\/" y) "/\" (x "\/" z)) by Th7;

        then ((x "\/" (y "/\" z)) "/\" (y "\/" (x "/\" z))) <= (((x "\/" y) "/\" (x "\/" z)) "/\" ((y "\/" x) "/\" (y "\/" z))) by A27, YELLOW_3: 2;

        then ((x "\/" b) "/\" (y "\/" b)) <= ((((x "\/" z) "/\" (x "\/" y)) "/\" (x "\/" y)) "/\" (y "\/" z)) by A47, A30, LATTICE3: 16;

        then ((x "\/" b) "/\" (y "\/" b)) <= (((x "\/" z) "/\" ((x "\/" y) "/\" (x "\/" y))) "/\" (y "\/" z)) by LATTICE3: 16;

        then ((x "\/" b) "/\" (y "\/" b)) <= (((x "\/" z) "/\" (x "\/" y)) "/\" (y "\/" z)) by YELLOW_5: 2;

        then

         A53: ((x "\/" b) "/\" (y "\/" b)) <= t by LATTICE3: 16;

        

         A54: ((z "/\" y) "\/" (y "/\" x)) <= (y "/\" (z "\/" x)) by Th6;

        

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

        

         A56: (x1 "/\" y1) = ((x "\/" b) "/\" (t "/\" ((y "\/" b) "/\" t))) by LATTICE3: 16

        .= ((x "\/" b) "/\" ((t "/\" t) "/\" (y "\/" b))) by LATTICE3: 16

        .= ((x "\/" b) "/\" ((y "\/" b) "/\" t)) by YELLOW_5: 2

        .= (((x "\/" b) "/\" (y "\/" b)) "/\" t) by LATTICE3: 16

        .= ((x "\/" (y "/\" z)) "/\" (y "\/" (x "/\" z))) by A47, A30, A53, YELLOW_5: 10

        .= ((y "/\" (x "\/" (y "/\" z))) "\/" (x "/\" z)) by A1, A24

        .= b by A1, A36;

        then b <= y1 by YELLOW_0: 23;

        then

         A57: (b "\/" y1) = y1 by YELLOW_5: 8;

        (x "\/" (z "/\" y)) <= ((x "\/" z) "/\" (x "\/" y)) by Th7;

        then ((x "\/" (z "/\" y)) "/\" (z "\/" (x "/\" y))) <= (((x "\/" z) "/\" (x "\/" y)) "/\" ((z "\/" x) "/\" (z "\/" y))) by A26, YELLOW_3: 2;

        then ((x "\/" b) "/\" (z "\/" b)) <= ((((x "\/" y) "/\" (x "\/" z)) "/\" (x "\/" z)) "/\" (z "\/" y)) by A47, A39, LATTICE3: 16;

        then ((x "\/" b) "/\" (z "\/" b)) <= (((x "\/" y) "/\" ((x "\/" z) "/\" (x "\/" z))) "/\" (z "\/" y)) by LATTICE3: 16;

        then ((x "\/" b) "/\" (z "\/" b)) <= (((x "\/" y) "/\" (x "\/" z)) "/\" (z "\/" y)) by YELLOW_5: 2;

        then

         A58: ((x "\/" b) "/\" (z "\/" b)) <= t by LATTICE3: 16;

        x1 <= t by YELLOW_0: 23;

        then

         A59: (t "/\" x1) = x1 by YELLOW_5: 10;

        

         A60: (z1 "/\" y1) = ((z "\/" b) "/\" (t "/\" ((y "\/" b) "/\" t))) by LATTICE3: 16

        .= ((z "\/" b) "/\" ((t "/\" t) "/\" (y "\/" b))) by LATTICE3: 16

        .= ((z "\/" b) "/\" ((y "\/" b) "/\" t)) by YELLOW_5: 2

        .= (((z "\/" b) "/\" (y "\/" b)) "/\" t) by LATTICE3: 16

        .= ((z "\/" (y "/\" x)) "/\" (y "\/" (z "/\" x))) by A30, A39, A48, YELLOW_5: 10

        .= ((y "/\" (z "\/" (y "/\" x))) "\/" (z "/\" x)) by A1, A43

        .= b by A1, A55;

        ((z "/\" y) "\/" (z "/\" x)) <= (z "/\" (y "\/" x)) by Th6;

        then (((z "/\" y) "\/" (z "/\" x)) "\/" ((z "/\" y) "\/" (y "/\" x))) <= ((z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x))) by A54, YELLOW_3: 3;

        then ((z "/\" x) "\/" ((z "/\" y) "\/" ((z "/\" y) "\/" (y "/\" x)))) <= ((z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x))) by LATTICE3: 14;

        then ((z "/\" x) "\/" (((z "/\" y) "\/" (z "/\" y)) "\/" (y "/\" x))) <= ((z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x))) by LATTICE3: 14;

        then ((((z "/\" y) "\/" (z "/\" y)) "\/" (z "/\" x)) "\/" (y "/\" x)) <= ((z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x))) by LATTICE3: 14;

        then (((z "/\" y) "\/" (z "/\" x)) "\/" (y "/\" x)) <= ((z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x))) by YELLOW_5: 1;

        then

         A61: b <= ((z "/\" t) "\/" (y "/\" t)) by A22, A52, LATTICE3: 14;

        

         A62: ((x "/\" z) "\/" (z "/\" y)) <= (z "/\" (x "\/" y)) by Th6;

        

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

        ((x "/\" z) "\/" (x "/\" y)) <= (x "/\" (z "\/" y)) by Th6;

        then (((x "/\" z) "\/" (x "/\" y)) "\/" ((x "/\" z) "\/" (z "/\" y))) <= ((x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y))) by A62, YELLOW_3: 3;

        then ((x "/\" y) "\/" ((x "/\" z) "\/" ((x "/\" z) "\/" (z "/\" y)))) <= ((x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y))) by LATTICE3: 14;

        then ((x "/\" y) "\/" (((x "/\" z) "\/" (x "/\" z)) "\/" (z "/\" y))) <= ((x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y))) by LATTICE3: 14;

        then ((((x "/\" z) "\/" (x "/\" z)) "\/" (x "/\" y)) "\/" (z "/\" y)) <= ((x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y))) by LATTICE3: 14;

        then (((x "/\" z) "\/" (x "/\" y)) "\/" (z "/\" y)) <= ((x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y))) by YELLOW_5: 1;

        then

         A64: b <= ((x "/\" t) "\/" (z "/\" t)) by A18, A52, LATTICE3: 14;

        (x "/\" y) <= (z "\/" x) by YELLOW_5: 5;

        then ((x "/\" y) "/\" (x "/\" y)) <= (((x "\/" y) "/\" (y "\/" z)) "/\" (z "\/" x)) by A51, YELLOW_3: 2;

        then (x "/\" y) <= t by YELLOW_5: 2;

        then ((x "/\" y) "\/" (y "/\" z)) <= (t "\/" t) by A17, YELLOW_3: 3;

        then ((x "/\" y) "\/" (y "/\" z)) <= t by YELLOW_5: 1;

        then (((x "/\" y) "\/" (y "/\" z)) "\/" (z "/\" x)) <= (t "\/" t) by A21, YELLOW_3: 3;

        then

         A65: b <= t by YELLOW_5: 1;

        then z1 = ((z "/\" t) "\/" b) by A1;

        

        then

         A66: (x1 "\/" z1) = (((x "/\" t) "\/" b) "\/" ((z "/\" t) "\/" b)) by A1, A65

        .= ((x "/\" t) "\/" (b "\/" ((z "/\" t) "\/" b))) by LATTICE3: 14

        .= ((x "/\" t) "\/" ((b "\/" b) "\/" (z "/\" t))) by LATTICE3: 14

        .= ((x "/\" t) "\/" ((z "/\" t) "\/" b)) by YELLOW_5: 1

        .= (((x "/\" t) "\/" (z "/\" t)) "\/" b) by LATTICE3: 14

        .= ((x "/\" (z "\/" y)) "\/" (z "/\" (x "\/" y))) by A18, A52, A64, YELLOW_5: 8

        .= ((z "\/" (x "/\" (z "\/" y))) "/\" (x "\/" y)) by A1, A29

        .= (((z "\/" x) "/\" (z "\/" y)) "/\" (x "\/" y)) by A1, A33

        .= t by LATTICE3: 16;

        

         A67: y1 = ((y "/\" t) "\/" b) by A1, A65;

        

        then

         A68: (x1 "\/" y1) = (((x "/\" t) "\/" b) "\/" ((y "/\" t) "\/" b)) by A1, A65

        .= ((x "/\" t) "\/" (b "\/" ((y "/\" t) "\/" b))) by LATTICE3: 14

        .= ((x "/\" t) "\/" ((b "\/" b) "\/" (y "/\" t))) by LATTICE3: 14

        .= ((x "/\" t) "\/" ((y "/\" t) "\/" b)) by YELLOW_5: 1

        .= (((x "/\" t) "\/" (y "/\" t)) "\/" b) by LATTICE3: 14

        .= ((x "/\" (y "\/" z)) "\/" (y "/\" (x "\/" z))) by A18, A22, A40, YELLOW_5: 8

        .= ((y "\/" (x "/\" (y "\/" z))) "/\" (x "\/" z)) by A1, A46

        .= t by A1, A25;

        

         A69: (z1 "\/" y1) = (((z "/\" t) "\/" b) "\/" ((y "/\" t) "\/" b)) by A1, A65, A67

        .= ((z "/\" t) "\/" (b "\/" ((y "/\" t) "\/" b))) by LATTICE3: 14

        .= ((z "/\" t) "\/" ((b "\/" b) "\/" (y "/\" t))) by LATTICE3: 14

        .= ((z "/\" t) "\/" ((y "/\" t) "\/" b)) by YELLOW_5: 1

        .= (((z "/\" t) "\/" (y "/\" t)) "\/" b) by LATTICE3: 14

        .= ((z "/\" (y "\/" x)) "\/" (y "/\" (z "\/" x))) by A22, A52, A61, YELLOW_5: 8

        .= ((y "\/" (z "/\" (y "\/" x))) "/\" (z "\/" x)) by A1, A38

        .= t by A1, A44;

        

         A70: (x1 "/\" z1) = ((x "\/" b) "/\" (t "/\" ((z "\/" b) "/\" t))) by LATTICE3: 16

        .= ((x "\/" b) "/\" ((t "/\" t) "/\" (z "\/" b))) by LATTICE3: 16

        .= ((x "\/" b) "/\" ((z "\/" b) "/\" t)) by YELLOW_5: 2

        .= (((x "\/" b) "/\" (z "\/" b)) "/\" t) by LATTICE3: 16

        .= ((x "\/" (z "/\" y)) "/\" (z "\/" (x "/\" y))) by A47, A39, A58, YELLOW_5: 10

        .= ((z "/\" (x "\/" (z "/\" y))) "\/" (x "/\" y)) by A1, A32

        .= (((z "/\" x) "\/" (z "/\" y)) "\/" (x "/\" y)) by A1, A63

        .= b by LATTICE3: 14;

        then b <= z1 by YELLOW_0: 23;

        then

         A71: (b "\/" z1) = z1 by YELLOW_5: 8;

        b <= x1 by A56, YELLOW_0: 23;

        then

         A72: (b "\/" x1) = x1 by YELLOW_5: 8;

        thus ex a,b,c,d,e be Element of L st (a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e

        proof

          take b, x1, y1, z1, t;

          thus b <> x1 by A14, A68, A66, A60, A57, A71, YELLOW_5: 2;

          thus b <> y1 by A14, A68, A70, A69, A72, A71, YELLOW_5: 2;

          thus b <> z1 by A14, A56, A66, A69, A72, A57, YELLOW_5: 2;

          thus b <> t by A14;

          now

            assume

             A73: x1 = y1;

            then (x1 "/\" y1) = x1 by YELLOW_5: 2;

            hence contradiction by A14, A68, A56, A73, YELLOW_5: 1;

          end;

          hence x1 <> y1;

          now

            assume

             A74: x1 = z1;

            then (x1 "/\" z1) = x1 by YELLOW_5: 2;

            hence contradiction by A14, A66, A70, A74, YELLOW_5: 1;

          end;

          hence x1 <> z1;

          thus x1 <> t by A14, A56, A70, A69, A49, A41, YELLOW_5: 1;

          now

            assume

             A75: y1 = z1;

            then (y1 "/\" z1) = y1 by YELLOW_5: 2;

            hence contradiction by A14, A69, A60, A75, YELLOW_5: 1;

          end;

          hence y1 <> z1;

          thus y1 <> t by A14, A56, A66, A60, A59, A41, YELLOW_5: 1;

          thus z1 <> t by A14, A68, A70, A60, A59, A49, YELLOW_5: 1;

          b <= x1 by A56, YELLOW_0: 23;

          hence (b "/\" x1) = b by YELLOW_5: 10;

          b <= y1 by A56, YELLOW_0: 23;

          hence (b "/\" y1) = b by YELLOW_5: 10;

          b <= z1 by A70, YELLOW_0: 23;

          hence (b "/\" z1) = b by YELLOW_5: 10;

          x1 <= t by A68, YELLOW_0: 22;

          hence (x1 "/\" t) = x1 by YELLOW_5: 10;

          y1 <= t by A68, YELLOW_0: 22;

          hence (y1 "/\" t) = y1 by YELLOW_5: 10;

          z1 <= t by A66, YELLOW_0: 22;

          hence (z1 "/\" t) = z1 by YELLOW_5: 10;

          thus (x1 "/\" y1) = b by A56;

          thus (x1 "/\" z1) = b by A70;

          thus (y1 "/\" z1) = b by A60;

          thus (x1 "\/" y1) = t by A68;

          thus (x1 "\/" z1) = t by A66;

          thus thesis by A69;

        end;

      end;

      hence thesis;

    end;

    theorem :: YELLOW11:12

    for L be LATTICE st L is modular holds L is distributive iff not ex K be full Sublattice of L st ( M_3 ,K) are_isomorphic

    proof

      let L be LATTICE;

      assume

       A1: L is modular;

      thus L is distributive implies not ex K be full Sublattice of L st ( M_3 ,K) are_isomorphic

      proof

        assume L is distributive;

        then not ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e) by Lm3;

        hence thesis by Th10;

      end;

      assume not ex K be full Sublattice of L st ( M_3 ,K) are_isomorphic ;

      then not ex a,b,c,d,e be Element of L st ((a,b,c,d,e) are_mutually_distinct & (a "/\" b) = a & (a "/\" c) = a & (a "/\" d) = a & (b "/\" e) = b & (c "/\" e) = c & (d "/\" e) = d & (b "/\" c) = a & (b "/\" d) = a & (c "/\" d) = a & (b "\/" c) = e & (b "\/" d) = e & (c "\/" d) = e) by Th10;

      hence thesis by A1, Lm3;

    end;

    begin

    definition

      let L be non empty RelStr;

      let a,b be Element of L;

      :: YELLOW11:def4

      func [#a,b#] -> Subset of L means

      : Def4: for c be Element of L holds c in it iff a <= c & c <= b;

      existence

      proof

        defpred P[ object] means ex c1 be Element of L st c1 = $1 & a <= c1 & c1 <= b;

        consider S be set such that

         A1: for c be object holds c in S iff c in the carrier of L & P[c] from XBOOLE_0:sch 1;

        for c be object holds c in S implies c in the carrier of L by A1;

        then

        reconsider S as Subset of L by TARSKI:def 3;

        reconsider S as Subset of L;

        take S;

        thus for c be Element of L holds c in S iff a <= c & c <= b

        proof

          let c be Element of L;

          thus c in S implies a <= c & c <= b

          proof

            assume c in S;

            then ex c1 be Element of L st c1 = c & a <= c1 & c1 <= b by A1;

            hence thesis;

          end;

          thus thesis by A1;

        end;

      end;

      uniqueness

      proof

        let x,y be Subset of L;

        assume that

         A2: for c be Element of L holds c in x iff a <= c & c <= b and

         A3: for c be Element of L holds c in y iff a <= c & c <= b;

        now

          let c1 be object;

          assume

           A4: c1 in y;

          then

          reconsider c = c1 as Element of L;

          c in y iff a <= c & c <= b by A3;

          hence c1 in x by A2, A4;

        end;

        then

         A5: y c= x;

        now

          let c1 be object;

          assume

           A6: c1 in x;

          then

          reconsider c = c1 as Element of L;

          c in x iff a <= c & c <= b by A2;

          hence c1 in y by A3, A6;

        end;

        then x c= y;

        hence thesis by A5;

      end;

    end

    definition

      let L be non empty RelStr;

      let IT be Subset of L;

      :: YELLOW11:def5

      attr IT is interval means ex a,b be Element of L st IT = [#a, b#];

    end

    registration

      let L be non empty reflexive transitive RelStr;

      cluster non empty interval -> directed for Subset of L;

      coherence

      proof

        let M be Subset of L;

        assume

         A1: M is non empty interval;

        then

        consider z be object such that

         A2: z in M;

        reconsider z as Element of L by A2;

        consider a,b be Element of L such that

         A3: M = [#a, b#] by A1;

        

         A4: z <= b by A3, A2, Def4;

        a <= z by A3, A2, Def4;

        then

         A5: a <= b by A4, ORDERS_2: 3;

        let x,y be Element of L;

        assume that

         A6: x in M and

         A7: y in M;

        take b;

        b <= b;

        hence b in M by A3, A5, Def4;

        thus x <= b & y <= b by A3, A6, A7, Def4;

      end;

      cluster non empty interval -> filtered for Subset of L;

      coherence

      proof

        let M be Subset of L;

        assume

         A8: M is non empty interval;

        then

        consider z be object such that

         A9: z in M;

        reconsider z as Element of L by A9;

        consider a,b be Element of L such that

         A10: M = [#a, b#] by A8;

        

         A11: z <= b by A10, A9, Def4;

        a <= z by A10, A9, Def4;

        then

         A12: a <= b by A11, ORDERS_2: 3;

        let x,y be Element of L;

        assume that

         A13: x in M and

         A14: y in M;

        take a;

        a <= a;

        hence a in M by A10, A12, Def4;

        thus a <= x & a <= y by A10, A13, A14, Def4;

      end;

    end

    registration

      let L be non empty RelStr;

      let a,b be Element of L;

      cluster [#a, b#] -> interval;

      coherence ;

    end

    theorem :: YELLOW11:13

    for L be non empty reflexive transitive RelStr, a,b be Element of L holds [#a, b#] = (( uparrow a) /\ ( downarrow b))

    proof

      let L be non empty reflexive transitive RelStr;

      let a,b be Element of L;

      thus [#a, b#] c= (( uparrow a) /\ ( downarrow b))

      proof

        let x be object;

        

         A1: a in {a} by TARSKI:def 1;

        

         A2: b in {b} by TARSKI:def 1;

        assume

         A3: x in [#a, b#];

        then

        reconsider y = x as Element of L;

        y <= b by A3, Def4;

        then y in { z where z be Element of L : ex w be Element of L st z <= w & w in {b} } by A2;

        then

         A4: y in ( downarrow {b}) by WAYBEL_0: 14;

        a <= y by A3, Def4;

        then y in { z where z be Element of L : ex w be Element of L st z >= w & w in {a} } by A1;

        then y in ( uparrow {a}) by WAYBEL_0: 15;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      thus (( uparrow a) /\ ( downarrow b)) c= [#a, b#]

      proof

        let x be object;

        assume

         A5: x in (( uparrow a) /\ ( downarrow b));

        then x in ( uparrow {a}) by XBOOLE_0:def 4;

        then x in { z where z be Element of L : ex w be Element of L st z >= w & w in {a} } by WAYBEL_0: 15;

        then

        consider y1 be Element of L such that

         A6: x = y1 and

         A7: ex w be Element of L st y1 >= w & w in {a};

        

         A8: a <= y1 by A7, TARSKI:def 1;

        x in ( downarrow {b}) by A5, XBOOLE_0:def 4;

        then x in { z where z be Element of L : ex w be Element of L st z <= w & w in {b} } by WAYBEL_0: 14;

        then ex y2 be Element of L st x = y2 & ex w be Element of L st y2 <= w & w in {b};

        then y1 <= b by A6, TARSKI:def 1;

        hence thesis by A6, A8, Def4;

      end;

    end;

    registration

      let L be with_infima Poset;

      let a,b be Element of L;

      cluster ( subrelstr [#a, b#]) -> meet-inheriting;

      coherence

      proof

        let x,y be Element of L;

        set ab = ( subrelstr [#a, b#]);

        assume that

         A1: x in the carrier of ab and

         A2: y in the carrier of ab and ex_inf_of ( {x, y},L);

        

         A3: x in [#a, b#] by A1, YELLOW_0:def 15;

        then

         A4: x <= b by Def4;

        

         A5: ( inf {x, y}) = (x "/\" y) by YELLOW_0: 40;

        then ( inf {x, y}) <= x by YELLOW_0: 23;

        then

         A6: ( inf {x, y}) <= b by A4, YELLOW_0:def 2;

        y in [#a, b#] by A2, YELLOW_0:def 15;

        then

         A7: a <= y by Def4;

        a <= x by A3, Def4;

        then a <= ( inf {x, y}) by A7, A5, YELLOW_0: 23;

        then ( inf {x, y}) in [#a, b#] by A6, Def4;

        hence thesis by YELLOW_0:def 15;

      end;

    end

    registration

      let L be with_suprema Poset;

      let a,b be Element of L;

      cluster ( subrelstr [#a, b#]) -> join-inheriting;

      coherence

      proof

        let x,y be Element of L;

        set ab = ( subrelstr [#a, b#]);

        assume that

         A1: x in the carrier of ab and

         A2: y in the carrier of ab and ex_sup_of ( {x, y},L);

        

         A3: x in [#a, b#] by A1, YELLOW_0:def 15;

        then

         A4: a <= x by Def4;

        

         A5: ( sup {x, y}) = (x "\/" y) by YELLOW_0: 41;

        then x <= ( sup {x, y}) by YELLOW_0: 22;

        then

         A6: a <= ( sup {x, y}) by A4, YELLOW_0:def 2;

        y in [#a, b#] by A2, YELLOW_0:def 15;

        then

         A7: y <= b by Def4;

        x <= b by A3, Def4;

        then ( sup {x, y}) <= b by A7, A5, YELLOW_0: 22;

        then ( sup {x, y}) in [#a, b#] by A6, Def4;

        hence thesis by YELLOW_0:def 15;

      end;

    end

    theorem :: YELLOW11:14

    for L be LATTICE, a,b be Element of L holds L is modular implies (( subrelstr [#b, (a "\/" b)#]),( subrelstr [#(a "/\" b), a#])) are_isomorphic

    proof

      let L be LATTICE;

      let a,b be Element of L;

      assume

       A1: L is modular;

      defpred P[ object, object] means ($2 is Element of L & (for X be Element of L, Y be Element of L holds ($1 = X & $2 = Y) implies Y = (X "/\" a)));

      

       A2: for x be object st x in the carrier of ( subrelstr [#b, (a "\/" b)#]) holds ex y be object st y in the carrier of ( subrelstr [#(a "/\" b), a#]) & P[x, y]

      proof

        let x be object;

        assume x in the carrier of ( subrelstr [#b, (a "\/" b)#]);

        then

         A3: x in [#b, (a "\/" b)#] by YELLOW_0:def 15;

        then

        reconsider x1 = x as Element of L;

        take y = (a "/\" x1);

        x1 <= (a "\/" b) by A3, Def4;

        then y <= (a "/\" (a "\/" b)) by YELLOW_5: 6;

        then

         A4: y <= a by LATTICE3: 18;

        b <= x1 by A3, Def4;

        then (a "/\" b) <= y by YELLOW_5: 6;

        then y in [#(a "/\" b), a#] by A4, Def4;

        hence y in the carrier of ( subrelstr [#(a "/\" b), a#]) by YELLOW_0:def 15;

        thus thesis;

      end;

      consider f be Function of the carrier of ( subrelstr [#b, (a "\/" b)#]), the carrier of ( subrelstr [#(a "/\" b), a#]) such that

       A5: for x be object st x in the carrier of ( subrelstr [#b, (a "\/" b)#]) holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

      reconsider f as Function of ( subrelstr [#b, (a "\/" b)#]), ( subrelstr [#(a "/\" b), a#]);

      take f;

      thus f is isomorphic

      proof

        

         A6: b <= (a "\/" b) by YELLOW_0: 22;

        b <= b;

        then b in [#b, (a "\/" b)#] by A6, Def4;

        then

        reconsider s1 = ( subrelstr [#b, (b "\/" a)#]) as non empty full Sublattice of L by YELLOW_0:def 15;

        

         A7: (a "/\" b) <= a by YELLOW_0: 23;

        (a "/\" b) <= (a "/\" b);

        then (a "/\" b) in [#(a "/\" b), a#] by A7, Def4;

        then

        reconsider s2 = ( subrelstr [#(a "/\" b), a#]) as non empty full Sublattice of L by YELLOW_0:def 15;

        reconsider f1 = f as Function of s1, s2;

        ( dom f1) = the carrier of ( subrelstr [#b, (a "\/" b)#]) by FUNCT_2:def 1;

        then

         A8: ( dom f1) = [#b, (a "\/" b)#] by YELLOW_0:def 15;

        the carrier of ( subrelstr [#(a "/\" b), a#]) c= ( rng f1)

        proof

          let y be object;

          assume y in the carrier of ( subrelstr [#(a "/\" b), a#]);

          then

           A9: y in [#(a "/\" b), a#] by YELLOW_0:def 15;

          then

          reconsider Y = y as Element of L;

          

           A10: (a "/\" b) <= Y by A9, Def4;

          then ((a "/\" b) "\/" b) <= (Y "\/" b) by WAYBEL_1: 2;

          then

           A11: b <= (Y "\/" b) by LATTICE3: 17;

          

           A12: Y <= a by A9, Def4;

          then (Y "\/" b) <= (a "\/" b) by WAYBEL_1: 2;

          then

           A13: (Y "\/" b) in [#b, (a "\/" b)#] by A11, Def4;

          then

           A14: (Y "\/" b) in the carrier of ( subrelstr [#b, (a "\/" b)#]) by YELLOW_0:def 15;

          then

          reconsider f1yb = (f1 . (Y "\/" b)) as Element of L by A5;

          f1yb = ((Y "\/" b) "/\" a) by A5, A14

          .= (Y "\/" (b "/\" a)) by A1, A12

          .= Y by A10, YELLOW_5: 8;

          hence thesis by A8, A13, FUNCT_1:def 3;

        end;

        then

         A15: ( rng f1) = the carrier of ( subrelstr [#(a "/\" b), a#]);

        

         A16: for x,y be Element of s1 holds x <= y iff (f1 . x) <= (f1 . y)

        proof

          let x,y be Element of s1;

          

           A17: the carrier of s1 = [#b, (a "\/" b)#] by YELLOW_0:def 15;

          then x in [#b, (a "\/" b)#];

          then

          reconsider X = x as Element of L;

          y in [#b, (a "\/" b)#] by A17;

          then

          reconsider Y = y as Element of L;

          reconsider f1Y = (f1 . Y) as Element of L by A5;

          reconsider f1X = (f1 . X) as Element of L by A5;

          thus x <= y implies (f1 . x) <= (f1 . y)

          proof

            assume x <= y;

            then

             A18: [x, y] in the InternalRel of s1 by ORDERS_2:def 5;

            the InternalRel of s1 c= the InternalRel of L by YELLOW_0:def 13;

            then

             A19: X <= Y by A18, ORDERS_2:def 5;

            

             A20: f1Y = (Y "/\" a) by A5;

            f1X = (X "/\" a) by A5;

            then f1X <= f1Y by A19, A20, WAYBEL_1: 1;

            hence thesis by YELLOW_0: 60;

          end;

          thus (f1 . x) <= (f1 . y) implies x <= y

          proof

            assume (f1 . x) <= (f1 . y);

            then

             A21: [(f1 . x), (f1 . y)] in the InternalRel of s2 by ORDERS_2:def 5;

            the InternalRel of s2 c= the InternalRel of L by YELLOW_0:def 13;

            then

             A22: f1X <= f1Y by A21, ORDERS_2:def 5;

            

             A23: f1Y = (Y "/\" a) by A5;

            

             A24: b <= X by A17, Def4;

            f1X = (X "/\" a) by A5;

            then (b "\/" (a "/\" X)) <= (b "\/" (a "/\" Y)) by A22, A23, WAYBEL_1: 2;

            then

             A25: ((b "\/" a) "/\" X) <= (b "\/" (a "/\" Y)) by A1, A24;

            

             A26: X <= (b "\/" a) by A17, Def4;

            b <= Y by A17, Def4;

            then ((b "\/" a) "/\" X) <= ((b "\/" a) "/\" Y) by A1, A25;

            then

             A27: X <= ((b "\/" a) "/\" Y) by A26, YELLOW_5: 10;

            Y <= (b "\/" a) by A17, Def4;

            then X <= Y by A27, YELLOW_5: 10;

            hence thesis by YELLOW_0: 60;

          end;

        end;

        f1 is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A28: x1 in ( dom f1) and

           A29: x2 in ( dom f1) and

           A30: (f1 . x1) = (f1 . x2);

          reconsider X2 = x2 as Element of L by A8, A29;

          

           A31: b <= X2 by A8, A29, Def4;

          reconsider X1 = x1 as Element of L by A8, A28;

          

           A32: b <= X1 by A8, A28, Def4;

          reconsider f1X1 = (f1 . X1) as Element of L by A5, A28;

          

           A33: f1X1 = (X1 "/\" a) by A5, A28;

          reconsider f1X2 = (f1 . X2) as Element of L by A5, A29;

          

           A34: f1X2 = (X2 "/\" a) by A5, A29;

          

           A35: X2 <= (a "\/" b) by A8, A29, Def4;

          X1 <= (a "\/" b) by A8, A28, Def4;

          

          then X1 = ((b "\/" a) "/\" X1) by YELLOW_5: 10

          .= (b "\/" (a "/\" X2)) by A1, A30, A32, A33, A34

          .= ((b "\/" a) "/\" X2) by A1, A31

          .= X2 by A35, YELLOW_5: 10;

          hence thesis;

        end;

        hence thesis by A15, A16, WAYBEL_0: 66;

      end;

    end;

    registration

      cluster finite non empty for LATTICE;

      existence

      proof

        set D = { {} };

        set R = the Order of D;

        reconsider A = RelStr (# D, R #) as with_infima with_suprema Poset;

        take A;

        thus thesis;

      end;

    end

    registration

      cluster finite -> lower-bounded for Semilattice;

      coherence

      proof

        let L be Semilattice;

        defpred P[ set] means ex x be Element of L st x is_<=_than $1;

        

         A1: P[ {} ]

        proof

          set a = the Element of L;

          take a;

          let b be Element of L;

          assume b in {} ;

          hence thesis;

        end;

        

         A2: for x,B be set st x in the carrier of L & B c= the carrier of L & P[B] holds P[(B \/ {x})]

        proof

          let x,B be set;

          assume that

           A3: x in the carrier of L and B c= the carrier of L;

          reconsider y = x as Element of L by A3;

          given a be Element of L such that

           A4: a is_<=_than B;

          take b = (a "/\" y);

          let c be Element of L;

           A5:

          now

            assume c in B;

            then

             A6: a <= c by A4;

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

            hence (a "/\" y) <= c by A6, ORDERS_2: 3;

          end;

           A7:

          now

            assume c in {x};

            then c = y by TARSKI:def 1;

            hence b <= c by YELLOW_0: 23;

          end;

          assume c in (B \/ {x});

          hence thesis by A5, A7, XBOOLE_0:def 3;

        end;

        assume L is finite;

        then

         A8: the carrier of L is finite;

        thus P[the carrier of L] from FINSET_1:sch 2( A8, A1, A2);

      end;

    end

    registration

      cluster finite -> complete for LATTICE;

      coherence

      proof

        let L be LATTICE;

        assume

         A1: L is finite;

        for x be Subset of L holds ex_sup_of (x,L)

        proof

          let x be Subset of L;

          per cases ;

            suppose x = {} ;

            hence thesis by A1, YELLOW_0: 42;

          end;

            suppose

             A2: x <> {} ;

            x is finite by A1, FINSET_1: 1;

            hence thesis by A2, YELLOW_0: 54;

          end;

        end;

        hence thesis by YELLOW_0: 53;

      end;

    end