robbins5.miz



    begin

    reserve L for non empty LattStr;

    reserve v64,v65,v66,v67,v103,v3,v102,v101,v100,v2,v1,v0 for Element of L;

    definition

      let L;

      :: ROBBINS5:def1

      attr L is satisfying_Sholander_1 means for v0, v1, v2 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

    end

    theorem :: ROBBINS5:1

    

     Lemma1: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0 holds (v0 "/\" v0) = v0

    proof

      assume

       A2: L is join-absorbing;

      assume

       A3: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A7: for v65, v66 holds v65 = ((v66 "/\" v65) "\/" (v65 "/\" v65))

      proof

        let v65, v66;

        (v65 "/\" (v65 "\/" v66)) = v65 by A2;

        hence thesis by A3;

      end;

      

       A11: for v1, v0 holds ((v0 "/\" v1) "/\" v1) = (v0 "/\" v1)

      proof

        let v1, v0;

        ((v0 "/\" v1) "\/" (v1 "/\" v1)) = v1 by A7;

        hence thesis by A2;

      end;

      

       A18: for v65, v64, v0 holds ((v0 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" (v0 "/\" v64)))

      proof

        let v65, v64, v0;

        ((v0 "/\" v64) "/\" v64) = (v0 "/\" v64) by A11;

        hence thesis by A3;

      end;

      

       A35: for v65, v64, v66 holds (v65 "/\" (v66 "\/" v64)) = (v65 "/\" (v66 "\/" (v64 "/\" v65)))

      proof

        let v65, v64, v66;

        ((v64 "/\" v65) "\/" (v66 "/\" v65)) = (v65 "/\" (v66 "\/" v64)) by A3;

        hence thesis by A18;

      end;

      

       A40: for v64, v0 holds (v64 "/\" v64) = (v64 "/\" ((v0 "/\" v64) "\/" v64))

      proof

        let v64, v0;

        ((v0 "/\" v64) "\/" (v64 "/\" v64)) = v64 by A7;

        hence thesis by A35;

      end;

      

       A49: for v64, v65 holds ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        (v64 "/\" ((v65 "/\" v64) "\/" v64)) = ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) by A3;

        hence thesis by A40;

      end;

      

       A51: for v64, v65 holds ((v64 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        ((v65 "/\" v64) "/\" v64) = (v65 "/\" v64) by A11;

        hence thesis by A49;

      end;

      let v65;

      ((v65 "/\" v65) "\/" (v65 "/\" v65)) = v65 by A7;

      hence thesis by A51;

    end;

    theorem :: ROBBINS5:2

    

     JoinIdem: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0 holds (v0 "\/" v0) = v0

    proof

      assume

       A3: L is join-absorbing;

      assume

       A4: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A8: for v65, v66 holds v65 = ((v66 "/\" v65) "\/" (v65 "/\" v65))

      proof

        let v65, v66;

        (v65 "/\" (v65 "\/" v66)) = v65 by A3;

        hence thesis by A4;

      end;

      

       A12: for v1, v0 holds ((v0 "/\" v1) "/\" v1) = (v0 "/\" v1)

      proof

        let v1, v0;

        ((v0 "/\" v1) "\/" (v1 "/\" v1)) = v1 by A8;

        hence thesis by A3;

      end;

      

       A15: for v65, v64, v0 holds ((v0 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" (v0 "/\" v64)))

      proof

        let v65, v64, v0;

        ((v0 "/\" v64) "/\" v64) = (v0 "/\" v64) by A12;

        hence thesis by A4;

      end;

      

       A19: for v65, v64, v66 holds (v65 "/\" (v66 "\/" v64)) = (v65 "/\" (v66 "\/" (v64 "/\" v65)))

      proof

        let v65, v64, v66;

        ((v64 "/\" v65) "\/" (v66 "/\" v65)) = (v65 "/\" (v66 "\/" v64)) by A4;

        hence thesis by A15;

      end;

      

       A24: for v64, v0 holds (v64 "/\" v64) = (v64 "/\" ((v0 "/\" v64) "\/" v64))

      proof

        let v64, v0;

        ((v0 "/\" v64) "\/" (v64 "/\" v64)) = v64 by A8;

        hence thesis by A19;

      end;

      

       A35: for v64, v1 holds ((v64 "/\" v64) "\/" (((v1 "/\" v64) "\/" v64) "/\" ((v1 "/\" v64) "\/" v64))) = ((v1 "/\" v64) "\/" v64)

      proof

        let v64, v1;

        (v64 "/\" ((v1 "/\" v64) "\/" v64)) = (v64 "/\" v64) by A24;

        hence thesis by A8;

      end;

      

       A42: for v0, v1 holds (v0 "\/" (((v1 "/\" v0) "\/" v0) "/\" ((v1 "/\" v0) "\/" v0))) = ((v1 "/\" v0) "\/" v0)

      proof

        let v0, v1;

        (v0 "/\" v0) = v0 by A3, A4, Lemma1;

        hence thesis by A35;

      end;

      

       A44: for v0, v1 holds (v0 "\/" ((v1 "/\" v0) "\/" v0)) = ((v1 "/\" v0) "\/" v0)

      proof

        let v0, v1;

        (((v1 "/\" v0) "\/" v0) "/\" ((v1 "/\" v0) "\/" v0)) = ((v1 "/\" v0) "\/" v0) by A3, A4, Lemma1;

        hence thesis by A42;

      end;

      

       A46: for v1, v0 holds ((v0 "/\" v1) "\/" v1) = v1

      proof

        let v1, v0;

        (v1 "/\" v1) = v1 by A3, A4, Lemma1;

        hence thesis by A8;

      end;

      

       A48: for v0, v1 holds (v0 "\/" v0) = ((v1 "/\" v0) "\/" v0)

      proof

        let v0, v1;

        ((v1 "/\" v0) "\/" v0) = v0 by A46;

        hence thesis by A44;

      end;

      now

        let v0, v1;

        ((v1 "/\" v0) "\/" v0) = v0 by A46;

        hence (v0 "\/" v0) = v0 by A48;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS5:3

    

     MeetCom: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0, v1 holds (v0 "/\" v1) = (v1 "/\" v0)

    proof

      assume

       A3: L is join-absorbing;

      assume

       A4: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A53: for v2, v0 holds (v0 "/\" (v2 "\/" v2)) = (v2 "/\" v0)

      proof

        let v2, v0;

        ((v2 "/\" v0) "\/" (v2 "/\" v0)) = (v0 "/\" (v2 "\/" v2)) by A4;

        hence thesis by A3, A4, JoinIdem;

      end;

      let v2, v0;

      (v2 "\/" v2) = v2 by A3, A4, JoinIdem;

      hence thesis by A53;

    end;

    theorem :: ROBBINS5:4

    

     JoinCom: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0, v1 holds (v0 "\/" v1) = (v1 "\/" v0)

    proof

      assume

       A3: L is join-absorbing;

      assume

       A4: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A8: for v65, v66 holds v65 = ((v66 "/\" v65) "\/" (v65 "/\" v65))

      proof

        let v65, v66;

        (v65 "/\" (v65 "\/" v66)) = v65 by A3;

        hence thesis by A4;

      end;

      

       A12: for v1, v0 holds ((v0 "/\" v1) "/\" v1) = (v0 "/\" v1)

      proof

        let v1, v0;

        ((v0 "/\" v1) "\/" (v1 "/\" v1)) = v1 by A8;

        hence thesis by A3;

      end;

      

       A15: for v65, v64, v0 holds ((v0 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" (v0 "/\" v64)))

      proof

        let v65, v64, v0;

        ((v0 "/\" v64) "/\" v64) = (v0 "/\" v64) by A12;

        hence thesis by A4;

      end;

      

       A19: for v65, v64, v66 holds (v65 "/\" (v66 "\/" v64)) = (v65 "/\" (v66 "\/" (v64 "/\" v65)))

      proof

        let v65, v64, v66;

        ((v64 "/\" v65) "\/" (v66 "/\" v65)) = (v65 "/\" (v66 "\/" v64)) by A4;

        hence thesis by A15;

      end;

      

       A24: for v64, v0 holds (v64 "/\" v64) = (v64 "/\" ((v0 "/\" v64) "\/" v64))

      proof

        let v64, v0;

        ((v0 "/\" v64) "\/" (v64 "/\" v64)) = v64 by A8;

        hence thesis by A19;

      end;

      

       A29: for v64, v65 holds ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        (v64 "/\" ((v65 "/\" v64) "\/" v64)) = ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) by A4;

        hence thesis by A24;

      end;

      

       A31: for v64, v65 holds ((v64 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        ((v65 "/\" v64) "/\" v64) = (v65 "/\" v64) by A12;

        hence thesis by A29;

      end;

      

       A42: for v64, v65 holds (v64 "/\" (v65 "\/" v64)) = v64

      proof

        let v64, v65;

        ((v64 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" v64)) by A4;

        

        then (v64 "/\" (v65 "\/" v64)) = (v64 "/\" v64) by A31

        .= v64 by A4, A3, Lemma1;

        hence thesis;

      end;

      

       A46: for v2, v1 holds ((v2 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" v2))) = (v1 "\/" v2)

      proof

        let v2, v1;

        ((v1 "\/" v2) "/\" (v1 "\/" v2)) = ((v2 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" v2))) by A4;

        hence thesis by A4, A3, Lemma1;

      end;

      

       A48: for v2, v1 holds (v2 "\/" (v1 "/\" (v1 "\/" v2))) = (v1 "\/" v2)

      proof

        let v2, v1;

        (v2 "/\" (v1 "\/" v2)) = v2 by A42;

        hence thesis by A46;

      end;

      let v1, v2;

      (v1 "/\" (v1 "\/" v2)) = v1 by A3;

      hence thesis by A48;

    end;

    theorem :: ROBBINS5:5

    

     MeetAssoc: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0, v1, v2 holds ((v0 "/\" v1) "/\" v2) = (v0 "/\" (v1 "/\" v2))

    proof

      assume

       A2: L is join-absorbing;

      assume

       A3: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A7: for v65, v66 holds v65 = ((v66 "/\" v65) "\/" (v65 "/\" v65))

      proof

        let v65, v66;

        (v65 "/\" (v65 "\/" v66)) = v65 by A2;

        hence thesis by A3;

      end;

      

       A11: for v1, v0 holds ((v0 "/\" v1) "/\" v1) = (v0 "/\" v1)

      proof

        let v1, v0;

        ((v0 "/\" v1) "\/" (v1 "/\" v1)) = v1 by A7;

        hence thesis by A2;

      end;

      

       A14: for v1, v64, v2 holds (((v2 "/\" v64) "\/" (v1 "/\" v64)) "/\" (v1 "\/" v2)) = (v64 "/\" (v1 "\/" v2))

      proof

        let v1, v64, v2;

        (v64 "/\" (v1 "\/" v2)) = ((v2 "/\" v64) "\/" (v1 "/\" v64)) by A3;

        hence thesis by A11;

      end;

      

       A18: for v65, v64, v0 holds ((v0 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" (v0 "/\" v64)))

      proof

        let v65, v64, v0;

        ((v0 "/\" v64) "/\" v64) = (v0 "/\" v64) by A11;

        hence thesis by A3;

      end;

      

       A22: for v65, v64, v66 holds (v65 "/\" (v66 "\/" v64)) = (v65 "/\" (v66 "\/" (v64 "/\" v65)))

      proof

        let v65, v64, v66;

        ((v64 "/\" v65) "\/" (v66 "/\" v65)) = (v65 "/\" (v66 "\/" v64)) by A3;

        hence thesis by A18;

      end;

      

       A27: for v64, v0 holds (v64 "/\" v64) = (v64 "/\" ((v0 "/\" v64) "\/" v64))

      proof

        let v64, v0;

        ((v0 "/\" v64) "\/" (v64 "/\" v64)) = v64 by A7;

        hence thesis by A22;

      end;

      

       A32: for v64, v65 holds ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        (v64 "/\" ((v65 "/\" v64) "\/" v64)) = ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) by A3;

        hence thesis by A27;

      end;

      

       A34: for v64, v65 holds ((v64 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        ((v65 "/\" v64) "/\" v64) = (v65 "/\" v64) by A11;

        hence thesis by A32;

      end;

      

       A55: for v0, v1 holds (v0 "\/" (v1 "/\" v0)) = v0

      proof

        let v0, v1;

        (v0 "/\" v0) = v0 by A2, A3, Lemma1;

        hence thesis by A34;

      end;

      

       A57: for v1, v0 holds ((v0 "/\" v1) "\/" v1) = v1

      proof

        let v1, v0;

        (v1 "/\" v1) = v1 by A2, A3, Lemma1;

        hence thesis by A7;

      end;

      

       A72: for v66, v65, v64 holds ((v64 "/\" ((v64 "/\" v65) "\/" (v66 "/\" v65))) "\/" (v66 "/\" ((v64 "/\" v65) "\/" (v66 "/\" v65)))) = (v65 "/\" (v66 "\/" v64))

      proof

        let v66, v65, v64;

        (((v64 "/\" v65) "\/" (v66 "/\" v65)) "/\" (v66 "\/" v64)) = ((v64 "/\" ((v64 "/\" v65) "\/" (v66 "/\" v65))) "\/" (v66 "/\" ((v64 "/\" v65) "\/" (v66 "/\" v65)))) by A3;

        hence thesis by A14;

      end;

      

       A82: for v65, v66 holds ((v66 "/\" v65) "/\" (v66 "\/" v66)) = (v65 "/\" (v66 "\/" v66))

      proof

        let v65, v66;

        ((v66 "/\" v65) "\/" (v66 "/\" v65)) = (v66 "/\" v65) by JoinIdem, A2, A3;

        hence thesis by A14;

      end;

      

       A84: for v65, v66 holds ((v66 "/\" v65) "/\" v66) = (v65 "/\" (v66 "\/" v66))

      proof

        let v65, v66;

        (v66 "\/" v66) = v66 by JoinIdem, A2, A3;

        hence thesis by A82;

      end;

      

       A86: for v65, v66 holds ((v66 "/\" v65) "/\" v66) = (v65 "/\" v66)

      proof

        let v65, v66;

        (v66 "\/" v66) = v66 by JoinIdem, A2, A3;

        hence thesis by A84;

      end;

      

       A89: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v1 "/\" v0) "\/" (v2 "/\" v0))

      proof

        let v0, v2, v1;

        ((v2 "/\" v0) "\/" (v1 "/\" v0)) = (v0 "/\" (v1 "\/" v2)) by A3;

        hence thesis by A2, A3, JoinCom;

      end;

      

       A92: for v1, v2, v0 holds ((v0 "/\" (v1 "/\" (v0 "\/" v2))) "\/" (v2 "/\" ((v0 "/\" v1) "\/" (v2 "/\" v1)))) = (v1 "/\" (v2 "\/" v0))

      proof

        let v1, v2, v0;

        ((v0 "/\" v1) "\/" (v2 "/\" v1)) = (v1 "/\" (v0 "\/" v2)) by A89;

        hence thesis by A72;

      end;

      

       A93: for v1, v2, v0 holds ((v0 "/\" (v1 "/\" (v0 "\/" v2))) "\/" (v2 "/\" (v1 "/\" (v0 "\/" v2)))) = (v1 "/\" (v2 "\/" v0))

      proof

        let v1, v2, v0;

        ((v0 "/\" v1) "\/" (v2 "/\" v1)) = (v1 "/\" (v0 "\/" v2)) by A89;

        hence thesis by A92;

      end;

      

       A95: for v1, v2, v0 holds ((v1 "/\" (v0 "\/" v2)) "/\" (v0 "\/" v2)) = (v1 "/\" (v2 "\/" v0))

      proof

        let v1, v2, v0;

        ((v0 "/\" (v1 "/\" (v0 "\/" v2))) "\/" (v2 "/\" (v1 "/\" (v0 "\/" v2)))) = ((v1 "/\" (v0 "\/" v2)) "/\" (v0 "\/" v2)) by A89;

        hence thesis by A93;

      end;

      

       A97: for v1, v2, v0 holds (v1 "/\" (v0 "\/" v2)) = (v1 "/\" (v2 "\/" v0))

      proof

        let v1, v2, v0;

        ((v1 "/\" (v0 "\/" v2)) "/\" (v0 "\/" v2)) = (v1 "/\" (v0 "\/" v2)) by A11;

        hence thesis by A95;

      end;

      

       A101: for v64, v65 holds ((v65 "/\" v64) "\/" v65) = v65

      proof

        let v64, v65;

        (v64 "/\" v65) = (v65 "/\" v64) by A2, A3, MeetCom;

        hence thesis by A57;

      end;

      

       A105: for v65, v64 holds (v64 "\/" (v64 "/\" v65)) = v64

      proof

        let v65, v64;

        (v65 "/\" v64) = (v64 "/\" v65) by A2, A3, MeetCom;

        hence thesis by A55;

      end;

      

       A109: for v65, v66, v64 holds (v64 "/\" (v65 "\/" (v64 "/\" v66))) = (v64 "/\" (v65 "\/" v66))

      proof

        let v65, v66, v64;

        (v66 "/\" v64) = (v64 "/\" v66) by A2, A3, MeetCom;

        hence thesis by A22;

      end;

      

       A115: for v1, v65 holds ((v65 "/\" v1) "\/" (v1 "/\" v65)) = (v65 "/\" v1)

      proof

        let v1, v65;

        ((v65 "/\" v1) "/\" v65) = (v1 "/\" v65) by A86;

        hence thesis by A105;

      end;

      

       A119: for v64, v66, v65 holds ((v65 "\/" v66) "/\" v64) = (v64 "/\" (v66 "\/" v65))

      proof

        let v64, v66, v65;

        (v64 "/\" (v65 "\/" v66)) = ((v65 "\/" v66) "/\" v64) by A2, A3, MeetCom;

        hence thesis by A97;

      end;

      

       A123: for v66, v1, v0 holds ((v0 "/\" v1) "/\" v66) = (v66 "/\" ((v1 "/\" v0) "\/" (v0 "/\" v1)))

      proof

        let v66, v1, v0;

        ((v0 "/\" v1) "\/" (v1 "/\" v0)) = (v0 "/\" v1) by A115;

        hence thesis by A119;

      end;

      

       A125: for v66, v1, v0 holds ((v0 "/\" v1) "/\" v66) = (v66 "/\" (v1 "/\" v0))

      proof

        let v66, v1, v0;

        ((v1 "/\" v0) "\/" (v0 "/\" v1)) = (v1 "/\" v0) by A115;

        hence thesis by A123;

      end;

      

       A130: for v66, v64, v0 holds (v64 "/\" (v66 "/\" (v0 "\/" v64))) = (v64 "/\" ((v0 "/\" v66) "\/" v66))

      proof

        let v66, v64, v0;

        ((v0 "/\" v66) "\/" (v64 "/\" v66)) = (v66 "/\" (v0 "\/" v64)) by A89;

        hence thesis by A109;

      end;

      

       A132: for v66, v64, v0 holds (v64 "/\" (v66 "/\" (v0 "\/" v64))) = (v64 "/\" v66)

      proof

        let v66, v64, v0;

        ((v0 "/\" v66) "\/" v66) = v66 by A57;

        hence thesis by A130;

      end;

      

       A136: for v65, v66, v64 holds (v64 "/\" ((v64 "\/" v66) "/\" v65)) = (v64 "/\" v65)

      proof

        let v65, v66, v64;

        (v65 "/\" (v66 "\/" v64)) = ((v64 "\/" v66) "/\" v65) by A119;

        hence thesis by A132;

      end;

      

       A140: for v65, v64, v66 holds (((v66 "\/" v64) "/\" v65) "/\" v64) = (v64 "/\" v65)

      proof

        let v65, v64, v66;

        (v64 "/\" (v65 "/\" (v66 "\/" v64))) = (((v66 "\/" v64) "/\" v65) "/\" v64) by A125;

        hence thesis by A132;

      end;

      

       A144: for v66, v1, v65 holds ((v65 "/\" v1) "/\" (v65 "/\" v66)) = ((v65 "/\" v1) "/\" v66)

      proof

        let v66, v1, v65;

        ((v65 "/\" v1) "\/" v65) = v65 by A101;

        hence thesis by A136;

      end;

      

       A148: for v1, v66, v64 holds ((v64 "/\" v66) "/\" (v64 "/\" v1)) = ((v64 "/\" v1) "/\" v66)

      proof

        let v1, v66, v64;

        (v64 "\/" (v64 "/\" v1)) = v64 by A105;

        hence thesis by A140;

      end;

      

       A150: for v1, v66, v64 holds ((v64 "/\" v66) "/\" v1) = ((v64 "/\" v1) "/\" v66)

      proof

        let v1, v66, v64;

        ((v64 "/\" v66) "/\" (v64 "/\" v1)) = ((v64 "/\" v66) "/\" v1) by A144;

        hence thesis by A148;

      end;

      

       AA: for v66, v65, v64 holds (v66 "/\" (v64 "/\" v65)) = ((v64 "/\" v66) "/\" v65)

      proof

        let v66, v65, v64;

        ((v64 "/\" v65) "/\" v66) = (v66 "/\" (v64 "/\" v65)) by A2, A3, MeetCom;

        hence thesis by A150;

      end;

      let v0, v1, v2;

      (v0 "/\" (v1 "/\" v2)) = ((v1 "/\" v0) "/\" v2) by AA

      .= ((v0 "/\" v1) "/\" v2) by A2, A3, MeetCom;

      hence thesis;

    end;

    theorem :: ROBBINS5:6

    (for v1, v0 holds (v0 "/\" (v0 "\/" v1)) = v0) implies for v0, v1 holds (v0 "/\" (v0 "\/" v1)) = v0;

    theorem :: ROBBINS5:7

    

     MeetAbsor: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v1, v0 holds (v0 "\/" (v0 "/\" v1)) = v0

    proof

      assume

       A2: L is join-absorbing;

      assume

       A3: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A7: for v65, v66 holds v65 = ((v66 "/\" v65) "\/" (v65 "/\" v65))

      proof

        let v65, v66;

        (v65 "/\" (v65 "\/" v66)) = v65 by A2;

        hence thesis by A3;

      end;

      

       A51: for v1, v0 holds ((v0 "/\" v1) "\/" v1) = v1

      proof

        let v1, v0;

        (v1 "/\" v1) = v1 by A2, A3, Lemma1;

        hence thesis by A7;

      end;

      

       A74: for v64, v65 holds ((v65 "/\" v64) "\/" v65) = v65

      proof

        let v64, v65;

        (v64 "/\" v65) = (v65 "/\" v64) by A2, A3, MeetCom;

        hence thesis by A51;

      end;

      let v1, v0;

      ((v0 "/\" v1) "\/" v0) = v0 by A74;

      hence thesis by A2, A3, JoinCom;

    end;

    theorem :: ROBBINS5:8

    

     JoinAssoc: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0, v1, v2 holds ((v0 "\/" v1) "\/" v2) = (v0 "\/" (v1 "\/" v2))

    proof

      assume

       A2: L is join-absorbing;

      assume

       A3: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A7: for v65, v66 holds v65 = ((v66 "/\" v65) "\/" (v65 "/\" v65))

      proof

        let v65, v66;

        (v65 "/\" (v65 "\/" v66)) = v65 by A2;

        hence thesis by A3;

      end;

      

       A11: for v1, v0 holds ((v0 "/\" v1) "/\" v1) = (v0 "/\" v1)

      proof

        let v1, v0;

        ((v0 "/\" v1) "\/" (v1 "/\" v1)) = v1 by A7;

        hence thesis by A2;

      end;

      

       A14: for v64, v2, v1 holds ((v2 "/\" (v64 "/\" (v1 "\/" v2))) "\/" (v1 "/\" (v64 "/\" (v1 "\/" v2)))) = (v64 "/\" (v1 "\/" v2))

      proof

        let v64, v2, v1;

        ((v64 "/\" (v1 "\/" v2)) "/\" (v1 "\/" v2)) = ((v2 "/\" (v64 "/\" (v1 "\/" v2))) "\/" (v1 "/\" (v64 "/\" (v1 "\/" v2)))) by A3;

        hence thesis by A11;

      end;

      

       A18: for v65, v64, v0 holds ((v0 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" (v0 "/\" v64)))

      proof

        let v65, v64, v0;

        ((v0 "/\" v64) "/\" v64) = (v0 "/\" v64) by A11;

        hence thesis by A3;

      end;

      

       A22: for v65, v1, v66 holds (v66 "\/" (v65 "/\" (v66 "\/" v1))) = ((v66 "\/" v1) "/\" (v65 "\/" v66))

      proof

        let v65, v1, v66;

        (v66 "/\" (v66 "\/" v1)) = v66 by A2;

        hence thesis by A3;

      end;

      

       A25: for v0, v2, v1 holds ((v2 "/\" v0) "/\" (v0 "/\" (v1 "\/" v2))) = (v2 "/\" v0)

      proof

        let v0, v2, v1;

        ((v2 "/\" v0) "\/" (v1 "/\" v0)) = (v0 "/\" (v1 "\/" v2)) by A3;

        hence thesis by A2;

      end;

      

       A29: for v66, v1, v64 holds (v64 "/\" ((v64 "\/" v1) "/\" (v66 "\/" v64))) = (v64 "/\" (v64 "\/" v1))

      proof

        let v66, v1, v64;

        (v64 "/\" (v64 "\/" v1)) = v64 by A2;

        hence thesis by A25;

      end;

      

       A31: for v66, v1, v64 holds (v64 "/\" ((v64 "\/" v1) "/\" (v66 "\/" v64))) = v64

      proof

        let v66, v1, v64;

        (v64 "/\" (v64 "\/" v1)) = v64 by A2;

        hence thesis by A29;

      end;

      

       A35: for v65, v64, v66 holds (v65 "/\" (v66 "\/" v64)) = (v65 "/\" (v66 "\/" (v64 "/\" v65)))

      proof

        let v65, v64, v66;

        ((v64 "/\" v65) "\/" (v66 "/\" v65)) = (v65 "/\" (v66 "\/" v64)) by A3;

        hence thesis by A18;

      end;

      

       A40: for v64, v0 holds (v64 "/\" v64) = (v64 "/\" ((v0 "/\" v64) "\/" v64))

      proof

        let v64, v0;

        ((v0 "/\" v64) "\/" (v64 "/\" v64)) = v64 by A7;

        hence thesis by A35;

      end;

      

       A49: for v64, v65 holds ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        (v64 "/\" ((v65 "/\" v64) "\/" v64)) = ((v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64)) by A3;

        hence thesis by A40;

      end;

      

       A51: for v64, v65 holds ((v64 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        ((v65 "/\" v64) "/\" v64) = (v65 "/\" v64) by A11;

        hence thesis by A49;

      end;

      

       A64: for v64, v65 holds (v64 "/\" (v65 "\/" v64)) = (v64 "/\" v64)

      proof

        let v64, v65;

        ((v64 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" v64)) by A3;

        hence thesis by A51;

      end;

      

       A66: for v64, v65 holds (v64 "/\" (v65 "\/" v64)) = v64

      proof

        let v64, v65;

        (v64 "/\" v64) = v64 by A2, A3, Lemma1;

        hence thesis by A64;

      end;

      

       A72: for v0, v1 holds (v0 "\/" (v1 "/\" v0)) = v0

      proof

        let v0, v1;

        (v0 "\/" (v1 "/\" v0)) = (v0 "\/" (v0 "/\" v1)) by A2, A3, MeetCom

        .= v0 by A2, A3, MeetAbsor;

        hence thesis;

      end;

      

       A76: for v1, v0 holds ((v0 "/\" v1) "\/" v1) = v1

      proof

        let v1, v0;

        (v1 "/\" v1) = v1 by A2, A3, Lemma1;

        hence thesis by A7;

      end;

      

       A91: for v2, v0 holds (v0 "/\" (v2 "\/" v2)) = (v2 "/\" v0)

      proof

        let v2, v0;

        ((v2 "/\" v0) "\/" (v2 "/\" v0)) = (v0 "/\" (v2 "\/" v2)) by A3;

        hence thesis by JoinIdem, A2, A3;

      end;

      

       A93: for v2, v0 holds (v0 "/\" v2) = (v2 "/\" v0)

      proof

        let v2, v0;

        (v2 "\/" v2) = v2 by JoinIdem, A2, A3;

        hence thesis by A91;

      end;

      

       A97: for v66, v65, v1 holds ((v66 "/\" (v1 "\/" v65)) "\/" v65) = ((v1 "\/" v65) "/\" (v65 "\/" v66))

      proof

        let v66, v65, v1;

        (v65 "/\" (v1 "\/" v65)) = v65 by A66;

        hence thesis by A3;

      end;

      

       A101: for v1, v65 holds ((v65 "\/" v1) "\/" v65) = (v65 "\/" v1)

      proof

        let v1, v65;

        (v65 "/\" (v65 "\/" v1)) = v65 by A2;

        hence thesis by A72;

      end;

      

       A111: for v64, v65 holds (v64 "/\" (v65 "/\" v64)) = (v65 "/\" v64)

      proof

        let v64, v65;

        (v64 "/\" (v65 "/\" v64)) = (v64 "/\" (v64 "/\" v65)) by A2, A3, MeetCom

        .= ((v64 "/\" v64) "/\" v65) by MeetAssoc, A2, A3

        .= (v64 "/\" v65) by A2, A3, Lemma1

        .= (v65 "/\" v64) by MeetCom, A2, A3;

        hence thesis;

      end;

      

       A115: for v1, v64 holds ((v64 "/\" ((v64 "\/" v1) "/\" (v64 "\/" v64))) "\/" v64) = ((v64 "\/" v1) "/\" (v64 "\/" v64))

      proof

        let v1, v64;

        (v64 "/\" ((v64 "\/" v1) "/\" (v64 "\/" v64))) = v64 by A31;

        hence thesis by A14;

      end;

      

       A117: for v1, v64 holds ((v64 "/\" ((v64 "\/" v1) "/\" v64)) "\/" v64) = ((v64 "\/" v1) "/\" (v64 "\/" v64))

      proof

        let v1, v64;

        (v64 "\/" v64) = v64 by JoinIdem, A2, A3;

        hence thesis by A115;

      end;

      

       A119: for v1, v64 holds (((v64 "\/" v1) "/\" v64) "\/" v64) = ((v64 "\/" v1) "/\" (v64 "\/" v64))

      proof

        let v1, v64;

        (v64 "/\" ((v64 "\/" v1) "/\" v64)) = ((v64 "\/" v1) "/\" v64) by A111;

        hence thesis by A117;

      end;

      

       A121: for v1, v64 holds v64 = ((v64 "\/" v1) "/\" (v64 "\/" v64))

      proof

        let v1, v64;

        (((v64 "\/" v1) "/\" v64) "\/" v64) = v64 by A76;

        hence thesis by A119;

      end;

      

       A123: for v1, v64 holds v64 = ((v64 "\/" v1) "/\" v64)

      proof

        let v1, v64;

        (v64 "\/" v64) = v64 by JoinIdem, A2, A3;

        hence thesis by A121;

      end;

      

       A134: for v65, v1, v64 holds (v64 "/\" (v65 "\/" v64)) = (v64 "/\" (v65 "\/" (v64 "\/" v1)))

      proof

        let v65, v1, v64;

        ((v64 "\/" v1) "/\" v64) = v64 by A123;

        hence thesis by A35;

      end;

      

       A136: for v65, v1, v64 holds v64 = (v64 "/\" (v65 "\/" (v64 "\/" v1)))

      proof

        let v65, v1, v64;

        (v64 "/\" (v65 "\/" v64)) = v64 by A66;

        hence thesis by A134;

      end;

      

       A141: for v65, v66, v64 holds (v64 "\/" ((v64 "\/" v66) "/\" v65)) = ((v64 "\/" v66) "/\" (v65 "\/" v64))

      proof

        let v65, v66, v64;

        (v65 "/\" (v64 "\/" v66)) = ((v64 "\/" v66) "/\" v65) by A93;

        hence thesis by A22;

      end;

      

       A150: for v1, v66, v64 holds (v64 "/\" ((v64 "\/" v66) "\/" v1)) = v64

      proof

        let v1, v66, v64;

        (((v64 "\/" v66) "\/" v1) "\/" (v64 "\/" v66)) = ((v64 "\/" v66) "\/" v1) by A101;

        hence thesis by A136;

      end;

      

       A160: for v66, v1, v64 holds (v64 "\/" v66) = (((v64 "\/" v1) "\/" v66) "/\" (v66 "\/" v64))

      proof

        let v66, v1, v64;

        (v64 "/\" ((v64 "\/" v1) "\/" v66)) = v64 by A150;

        hence thesis by A97;

      end;

      

       A176: for v64, v66, v65 holds ((v65 "\/" v66) "\/" v64) = (v64 "\/" (v66 "\/" v65))

      proof

        let v64, v66, v65;

        (v64 "\/" (v65 "\/" v66)) = ((v65 "\/" v66) "\/" v64) by A2, A3, JoinCom;

        hence thesis by A2, A3, JoinCom;

      end;

      

       A180: for v66, v65, v64 holds ((v66 "\/" v64) "/\" ((v64 "\/" v65) "\/" v66)) = (v64 "\/" v66)

      proof

        let v66, v65, v64;

        (((v64 "\/" v65) "\/" v66) "/\" (v66 "\/" v64)) = ((v66 "\/" v64) "/\" ((v64 "\/" v65) "\/" v66)) by A93;

        hence thesis by A160;

      end;

      

       A184: for v65, v1, v0 holds ((v0 "\/" v1) "\/" (v0 "\/" v65)) = (((v0 "\/" v1) "\/" v65) "/\" ((v65 "\/" v0) "\/" (v0 "\/" v1)))

      proof

        let v65, v1, v0;

        (((v0 "\/" v1) "\/" v65) "/\" (v65 "\/" v0)) = (v0 "\/" v65) by A160;

        hence thesis by A141;

      end;

      

       A186: for v65, v1, v0 holds ((v0 "\/" v1) "\/" (v0 "\/" v65)) = (v65 "\/" (v0 "\/" v1))

      proof

        let v65, v1, v0;

        (((v0 "\/" v1) "\/" v65) "/\" ((v65 "\/" v0) "\/" (v0 "\/" v1))) = (v65 "\/" (v0 "\/" v1)) by A180;

        hence thesis by A184;

      end;

      

       A190: for v65, v66, v64 holds ((v64 "\/" v66) "\/" (v65 "\/" v64)) = (v66 "\/" (v64 "\/" v65))

      proof

        let v65, v66, v64;

        ((v64 "\/" v65) "\/" (v64 "\/" v66)) = ((v64 "\/" v66) "\/" (v65 "\/" v64)) by A176;

        hence thesis by A186;

      end;

      

       A194: for v66, v65, v64 holds ((v64 "\/" v65) "\/" (v66 "\/" v64)) = (v66 "\/" (v64 "\/" v65))

      proof

        let v66, v65, v64;

        ((v64 "\/" v65) "\/" (v64 "\/" v66)) = ((v64 "\/" v65) "\/" (v66 "\/" v64)) by A2, A3, JoinCom;

        hence thesis by A186;

      end;

      

       A196: for v65, v66, v64 holds (v65 "\/" (v64 "\/" v66)) = (v66 "\/" (v64 "\/" v65))

      proof

        let v65, v66, v64;

        ((v64 "\/" v65) "\/" (v66 "\/" v64)) = (v65 "\/" (v64 "\/" v66)) by A190;

        hence thesis by A194;

      end;

      let v0, v1, v2;

      (v0 "\/" (v1 "\/" v2)) = (v2 "\/" (v1 "\/" v0)) by A196

      .= ((v1 "\/" v0) "\/" v2) by A2, A3, JoinCom

      .= ((v0 "\/" v1) "\/" v2) by A2, A3, JoinCom;

      hence thesis;

    end;

    theorem :: ROBBINS5:9

    

     Seventh: L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0, v1, v2 holds (v0 "/\" (v1 "\/" v2)) = ((v0 "/\" v1) "\/" (v0 "/\" v2))

    proof

      assume

       A3: L is join-absorbing;

      assume

       A4: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A72: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v1 "/\" v0) "\/" (v2 "/\" v0))

      proof

        let v0, v2, v1;

        ((v2 "/\" v0) "\/" (v1 "/\" v0)) = (v0 "/\" (v1 "\/" v2)) by A4;

        hence thesis by A3, A4, JoinCom;

      end;

      

       A79: for v66, v64, v65 holds ((v65 "/\" v64) "\/" (v66 "/\" v65)) = (v65 "/\" (v64 "\/" v66))

      proof

        let v66, v64, v65;

        (v64 "/\" v65) = (v65 "/\" v64) by A3, A4, MeetCom;

        hence thesis by A72;

      end;

      let v0, v1, v2;

      (v0 "/\" (v1 "\/" v2)) = ((v0 "/\" v1) "\/" (v2 "/\" v0)) by A79

      .= ((v0 "/\" v1) "\/" (v0 "/\" v2)) by A3, A4, MeetCom;

      hence thesis;

    end;

    theorem :: ROBBINS5:10

    L is join-absorbing & (for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0))) implies for v0, v1, v2 holds (v0 "\/" (v1 "/\" v2)) = ((v0 "\/" v1) "/\" (v0 "\/" v2))

    proof

      assume

       A2: L is join-absorbing;

      assume

       A3: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      

       A7: for v65, v66 holds v65 = ((v66 "/\" v65) "\/" (v65 "/\" v65))

      proof

        let v65, v66;

        (v65 "/\" (v65 "\/" v66)) = v65 by A2;

        hence thesis by A3;

      end;

      

       A12: for v1, v64, v2 holds (((v2 "/\" v64) "\/" (v1 "/\" v64)) "\/" ((v1 "\/" v2) "/\" (v1 "\/" v2))) = (v1 "\/" v2)

      proof

        let v1, v64, v2;

        (v64 "/\" (v1 "\/" v2)) = ((v2 "/\" v64) "\/" (v1 "/\" v64)) by A3;

        hence thesis by A7;

      end;

      

       A15: for v1, v0 holds ((v0 "/\" v1) "/\" v1) = (v0 "/\" v1)

      proof

        let v1, v0;

        ((v0 "/\" v1) "/\" v1) = (v0 "/\" (v1 "/\" v1)) by A2, A3, MeetAssoc

        .= (v0 "/\" v1) by A2, A3, Lemma1;

        hence thesis;

      end;

      

       A22: for v65, v64, v0 holds ((v0 "/\" v64) "\/" (v65 "/\" v64)) = (v64 "/\" (v65 "\/" (v0 "/\" v64)))

      proof

        let v65, v64, v0;

        ((v0 "/\" v64) "/\" v64) = (v0 "/\" v64) by A15;

        hence thesis by A3;

      end;

      

       A26: for v66, v1, v65 holds ((v66 "/\" (v65 "\/" v1)) "\/" v65) = ((v65 "\/" v1) "/\" (v65 "\/" v66))

      proof

        let v66, v1, v65;

        (v65 "/\" (v65 "\/" v1)) = v65 by A2;

        hence thesis by A3;

      end;

      

       A29: for v0, v2, v1 holds ((v2 "/\" v0) "/\" (v0 "/\" (v1 "\/" v2))) = (v2 "/\" v0)

      proof

        let v0, v2, v1;

        ((v2 "/\" v0) "\/" (v1 "/\" v0)) = (v0 "/\" (v1 "\/" v2)) by A3;

        hence thesis by A2;

      end;

      

       A39: for v65, v64, v66 holds (v65 "/\" (v66 "\/" v64)) = (v65 "/\" (v66 "\/" (v64 "/\" v65)))

      proof

        let v65, v64, v66;

        ((v64 "/\" v65) "\/" (v66 "/\" v65)) = (v65 "/\" (v66 "\/" v64)) by A3;

        hence thesis by A22;

      end;

      

       A44: for v0, v65, v64 holds (((v64 "/\" v65) "\/" (v0 "/\" v65)) "\/" (((v0 "/\" v65) "\/" v64) "/\" ((v0 "/\" v65) "\/" v64))) = ((v0 "/\" v65) "\/" v64)

      proof

        let v0, v65, v64;

        ((v0 "/\" v65) "/\" v65) = (v0 "/\" v65) by A15;

        hence thesis by A12;

      end;

      

       A53: for v66, v1, v65, v2 holds ((v66 "/\" (v1 "\/" (v2 "/\" v65))) "\/" (v65 "/\" (v1 "\/" v2))) = ((v1 "\/" (v2 "/\" v65)) "/\" (v65 "\/" v66))

      proof

        let v66, v1, v65, v2;

        (v65 "/\" (v1 "\/" (v2 "/\" v65))) = (v65 "/\" (v1 "\/" v2)) by A39;

        hence thesis by A3;

      end;

      

       A89: for v2, v1, v0 holds (((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" ((v2 "/\" v1) "\/" v0)) = ((v2 "/\" v1) "\/" v0)

      proof

        let v2, v1, v0;

        (((v2 "/\" v1) "\/" v0) "/\" ((v2 "/\" v1) "\/" v0)) = ((v2 "/\" v1) "\/" v0) by A2, A3, Lemma1;

        hence thesis by A44;

      end;

      

       A94: for v0, v1 holds (v0 "\/" (v1 "\/" v0)) = (v1 "\/" v0)

      proof

        let v0, v1;

        (v0 "\/" (v1 "\/" v0)) = (v0 "\/" (v0 "\/" v1)) by JoinCom, A2, A3

        .= ((v0 "\/" v0) "\/" v1) by JoinAssoc, A2, A3

        .= (v0 "\/" v1) by JoinIdem, A2, A3

        .= (v1 "\/" v0) by JoinCom, A2, A3;

        hence thesis;

      end;

      

       A121: for v64, v65 holds (v64 "/\" (v65 "/\" v64)) = (v65 "/\" v64)

      proof

        let v64, v65;

        (v64 "/\" (v65 "/\" v64)) = (v64 "/\" (v64 "/\" v65)) by MeetCom, A2, A3

        .= ((v64 "/\" v64) "/\" v65) by MeetAssoc, A2, A3

        .= (v64 "/\" v65) by A2, A3, Lemma1;

        hence thesis by A2, A3, MeetCom;

      end;

      

       A137: for v0, v2, v1 holds (v0 "/\" (v1 "\/" v2)) = ((v1 "/\" v0) "\/" (v2 "/\" v0))

      proof

        let v0, v2, v1;

        ((v2 "/\" v0) "\/" (v1 "/\" v0)) = (v0 "/\" (v1 "\/" v2)) by A3;

        hence thesis by A2, A3, JoinCom;

      end;

      

       A140: for v1, v2, v0 holds ((v1 "/\" (v0 "\/" v2)) "\/" ((v2 "/\" v1) "\/" v0)) = ((v2 "/\" v1) "\/" v0)

      proof

        let v1, v2, v0;

        ((v0 "/\" v1) "\/" (v2 "/\" v1)) = (v1 "/\" (v0 "\/" v2)) by A137;

        hence thesis by A89;

      end;

      

       A150: for v1, v65 holds (v65 "/\" (v65 "/\" v1)) = (v65 "/\" v1)

      proof

        let v1, v65;

        (v65 "/\" (v65 "/\" v1)) = ((v65 "/\" v65) "/\" v1) by A2, A3, MeetAssoc

        .= (v65 "/\" v1) by A2, A3, Lemma1;

        hence thesis;

      end;

      

       A154: for v64, v2, v65 holds ((v64 "/\" (v65 "\/" v2)) "\/" v65) = ((v65 "\/" (v2 "/\" v64)) "/\" (v65 "\/" v64))

      proof

        let v64, v2, v65;

        (v64 "/\" (v65 "\/" (v2 "/\" v64))) = (v64 "/\" (v65 "\/" v2)) by A39;

        hence thesis by A26;

      end;

      

       A156: for v64, v2, v65 holds ((v65 "\/" v2) "/\" (v65 "\/" v64)) = ((v65 "\/" (v2 "/\" v64)) "/\" (v65 "\/" v64))

      proof

        let v64, v2, v65;

        ((v64 "/\" (v65 "\/" v2)) "\/" v65) = ((v65 "\/" v2) "/\" (v65 "\/" v64)) by A26;

        hence thesis by A154;

      end;

      

       A161: for v66, v64, v1 holds ((v1 "/\" v64) "/\" ((v1 "/\" v64) "/\" (v66 "\/" v64))) = (v64 "/\" (v1 "/\" v64))

      proof

        let v66, v64, v1;

        (v64 "/\" (v1 "/\" v64)) = (v1 "/\" v64) by A121;

        hence thesis by A29;

      end;

      

       A163: for v66, v64, v1 holds ((v1 "/\" v64) "/\" (v66 "\/" v64)) = (v64 "/\" (v1 "/\" v64))

      proof

        let v66, v64, v1;

        ((v1 "/\" v64) "/\" ((v1 "/\" v64) "/\" (v66 "\/" v64))) = ((v1 "/\" v64) "/\" (v66 "\/" v64)) by A150;

        hence thesis by A161;

      end;

      

       A165: for v66, v64, v1 holds ((v1 "/\" v64) "/\" (v66 "\/" v64)) = (v1 "/\" v64)

      proof

        let v66, v64, v1;

        (v64 "/\" (v1 "/\" v64)) = (v1 "/\" v64) by A121;

        hence thesis by A163;

      end;

      

       A169: for v65, v66, v0 holds ((v0 "/\" v66) "\/" v65) = ((v65 "\/" v66) "/\" (v65 "\/" (v0 "/\" v66)))

      proof

        let v65, v66, v0;

        ((v0 "/\" v66) "/\" (v65 "\/" v66)) = (v0 "/\" v66) by A165;

        hence thesis by A26;

      end;

      

       A173: for v64, v65, v67, v66 holds ((v67 "/\" (v65 "\/" v66)) "\/" (v64 "/\" (v65 "\/" (v66 "/\" v67)))) = ((v65 "\/" (v66 "/\" v67)) "/\" (v67 "\/" v64))

      proof

        let v64, v65, v67, v66;

        ((v64 "/\" (v65 "\/" (v66 "/\" v67))) "\/" (v67 "/\" (v65 "\/" v66))) = ((v67 "/\" (v65 "\/" v66)) "\/" (v64 "/\" (v65 "\/" (v66 "/\" v67)))) by A2, A3, JoinCom;

        hence thesis by A53;

      end;

      

       A177: for v64, v66, v65 holds ((v64 "/\" (v65 "\/" v66)) "\/" ((v65 "\/" v64) "/\" (v65 "\/" (v66 "/\" v64)))) = ((v66 "/\" v64) "\/" v65)

      proof

        let v64, v66, v65;

        ((v66 "/\" v64) "\/" v65) = ((v65 "\/" v64) "/\" (v65 "\/" (v66 "/\" v64))) by A169;

        hence thesis by A140;

      end;

      

       A179: for v65, v64, v66 holds ((v65 "\/" (v66 "/\" v64)) "/\" (v64 "\/" (v65 "\/" v64))) = ((v66 "/\" v64) "\/" v65)

      proof

        let v65, v64, v66;

        ((v64 "/\" (v65 "\/" v66)) "\/" ((v65 "\/" v64) "/\" (v65 "\/" (v66 "/\" v64)))) = ((v65 "\/" (v66 "/\" v64)) "/\" (v64 "\/" (v65 "\/" v64))) by A173;

        hence thesis by A177;

      end;

      

       A181: for v65, v64, v66 holds ((v65 "\/" (v66 "/\" v64)) "/\" (v65 "\/" v64)) = ((v66 "/\" v64) "\/" v65)

      proof

        let v65, v64, v66;

        (v64 "\/" (v65 "\/" v64)) = (v65 "\/" v64) by A94;

        hence thesis by A179;

      end;

      

       A183: for v64, v66, v65 holds ((v65 "\/" v66) "/\" (v65 "\/" v64)) = ((v66 "/\" v64) "\/" v65)

      proof

        let v64, v66, v65;

        ((v65 "\/" (v66 "/\" v64)) "/\" (v65 "\/" v64)) = ((v65 "\/" v66) "/\" (v65 "\/" v64)) by A156;

        hence thesis by A181;

      end;

      let v0, v1, v2;

      (v0 "\/" (v1 "/\" v2)) = ((v1 "/\" v2) "\/" v0) by A2, A3, JoinCom

      .= ((v0 "\/" v1) "/\" (v0 "\/" v2)) by A183;

      hence thesis;

    end;

    reserve L for distributive join-commutative meet-commutative non empty LattStr;

    reserve v0,v1,v2 for Element of L;

    theorem :: ROBBINS5:11

    

     LatToSho: for v0, v1, v2 holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0)) by LATTICES:def 11;

    theorem :: ROBBINS5:12

    

     Combined: for L be non empty LattStr holds L is distributive Lattice iff L is join-absorbing satisfying_Sholander_1

    proof

      let L be non empty LattStr;

      thus L is distributive Lattice implies L is join-absorbing satisfying_Sholander_1 by LatToSho;

      assume

       A1: L is join-absorbing satisfying_Sholander_1;

      then

       A2: for v0,v2,v1 be Element of L holds (v0 "/\" (v1 "\/" v2)) = ((v2 "/\" v0) "\/" (v1 "/\" v0));

      then

       A3: L is distributive by Seventh, A1;

      

       A4: L is meet-commutative join-commutative by A2, A1, MeetCom, JoinCom;

      

       A5: L is meet-associative join-associative by A2, A1, MeetAssoc, JoinAssoc;

      for v0,v1 be Element of L holds ((v0 "/\" v1) "\/" v1) = v1

      proof

        let v0,v1 be Element of L;

        ((v0 "/\" v1) "\/" v1) = (v1 "\/" (v0 "/\" v1)) by A4

        .= (v1 "\/" (v1 "/\" v0)) by A4

        .= v1 by MeetAbsor, A1, A2;

        hence thesis;

      end;

      then L is meet-absorbing;

      hence thesis by A3, A4, A5, A1;

    end;

    registration

      cluster join-absorbing satisfying_Sholander_1 -> distributive Lattice-like for non empty LattStr;

      coherence by Combined;

      cluster distributive join-commutative meet-commutative -> satisfying_Sholander_1 for non empty LattStr;

      coherence by LatToSho;

    end

    begin

    reserve L for non empty LattStr;

    reserve v103,v3,v102,v101,v100,v2,v1,v0 for Element of L;

    definition

      let L;

      :: ROBBINS5:def2

      attr L is satisfying_McKenzie_1 means for v1, v2, v0 holds (v0 "\/" (v1 "/\" (v0 "/\" v2))) = v0;

      :: ROBBINS5:def3

      attr L is satisfying_McKenzie_2 means for v1, v2, v0 holds (v0 "/\" (v1 "\/" (v0 "\/" v2))) = v0;

      :: ROBBINS5:def4

      attr L is satisfying_McKenzie_3 means for v2, v1, v0 holds (((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1) = v1;

      :: ROBBINS5:def5

      attr L is satisfying_McKenzie_4 means for v2, v1, v0 holds (((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1) = v1;

    end

    theorem :: ROBBINS5:13

    

     MainMcKenzie: (L is satisfying_McKenzie_1 satisfying_McKenzie_2 & (for v2, v1, v0 holds (((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1) = v1) & (for v2, v1, v0 holds (((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1) = v1)) implies ((for v1, v0 holds (v0 "/\" (v0 "\/" v1)) = v0) & (for v1, v0 holds (v0 "\/" (v0 "/\" v1)) = v0) & L is join-commutative meet-commutative meet-associative join-associative)

    proof

      assume

       A2: L is satisfying_McKenzie_1;

      assume

       A3: L is satisfying_McKenzie_2;

      assume

       A4: for v2, v1, v0 holds (((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1) = v1;

      assume

       A5: for v2, v1, v0 holds (((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1) = v1;

      

       A9: for v100, v101 holds (v100 "\/" (v101 "/\" v100)) = v100

      proof

        now

          let v101, v1, v2, v100;

          (v100 "/\" (v1 "\/" (v100 "\/" v2))) = v100 by A3;

          hence (v100 "\/" (v101 "/\" v100)) = v100 by A2;

        end;

        hence thesis;

      end;

      

       A13: for v100, v101 holds (v100 "/\" (v101 "\/" v100)) = v100

      proof

        now

          let v101, v1, v2, v100;

          (v100 "\/" (v1 "/\" (v100 "/\" v2))) = v100 by A2;

          hence (v100 "/\" (v101 "\/" v100)) = v100 by A3;

        end;

        hence thesis;

      end;

      

       A17: for v101, v100 holds ((v100 "/\" v101) "\/" v101) = v101

      proof

        now

          let v2, v101, v100;

          ((v100 "/\" v101) "\/" (v101 "/\" ((v100 "/\" v101) "/\" v2))) = (v100 "/\" v101) by A2;

          hence ((v100 "/\" v101) "\/" v101) = v101 by A4;

        end;

        hence thesis;

      end;

      

       A21: for v102, v100 holds (v100 "/\" (v100 "\/" v102)) = v100

      proof

        now

          let v2, v0, v102, v100;

          (((v0 "/\" (v100 "\/" v102)) "\/" ((v100 "\/" v102) "/\" v2)) "\/" (v100 "\/" v102)) = (v100 "\/" v102) by A4;

          hence (v100 "/\" (v100 "\/" v102)) = v100 by A3;

        end;

        hence thesis;

      end;

      

       A25: for v102, v1, v2, v100 holds ((v100 "\/" ((v1 "\/" (v100 "\/" v2)) "/\" v102)) "\/" (v1 "\/" (v100 "\/" v2))) = (v1 "\/" (v100 "\/" v2))

      proof

        let v102, v1, v2, v100;

        (v100 "/\" (v1 "\/" (v100 "\/" v2))) = v100 by A3;

        hence thesis by A4;

      end;

      

       A33: for v102, v100 holds (v100 "\/" (v100 "/\" v102)) = v100

      proof

        now

          let v2, v0, v102, v100;

          (((v0 "\/" (v100 "/\" v102)) "/\" ((v100 "/\" v102) "\/" v2)) "/\" (v100 "/\" v102)) = (v100 "/\" v102) by A5;

          hence (v100 "\/" (v100 "/\" v102)) = v100 by A2;

        end;

        hence thesis;

      end;

      

       A37: for v102, v1, v2, v100 holds ((v100 "/\" ((v1 "/\" (v100 "/\" v2)) "\/" v102)) "/\" (v1 "/\" (v100 "/\" v2))) = (v1 "/\" (v100 "/\" v2))

      proof

        let v102, v1, v2, v100;

        (v100 "\/" (v1 "/\" (v100 "/\" v2))) = v100 by A2;

        hence thesis by A5;

      end;

      

       A41: for v101, v100 holds ((v100 "\/" v101) "/\" v101) = v101

      proof

        now

          let v2, v101, v100;

          ((v100 "\/" v101) "/\" (v101 "\/" ((v100 "\/" v101) "\/" v2))) = (v100 "\/" v101) by A3;

          hence ((v100 "\/" v101) "/\" v101) = v101 by A5;

        end;

        hence thesis;

      end;

      

       A49: for v102, v100, v1 holds ((v100 "/\" ((v1 "/\" v100) "\/" v102)) "/\" (v1 "/\" v100)) = (v1 "/\" v100)

      proof

        let v102, v100, v1;

        (v100 "\/" (v1 "/\" v100)) = v100 by A9;

        hence thesis by A5;

      end;

      

       A53: for v102, v100, v1 holds ((v100 "\/" ((v1 "\/" v100) "/\" v102)) "\/" (v1 "\/" v100)) = (v1 "\/" v100)

      proof

        let v102, v100, v1;

        (v100 "/\" (v1 "\/" v100)) = v100 by A13;

        hence thesis by A4;

      end;

      

       A57: for v1, v2, v100 holds (v100 "\/" (v1 "\/" (v100 "\/" v2))) = (v1 "\/" (v100 "\/" v2))

      proof

        let v1, v2, v100;

        (v100 "/\" (v1 "\/" (v100 "\/" v2))) = v100 by A3;

        hence thesis by A17;

      end;

      

       A61: for v100, v1 holds (v100 "\/" (v1 "\/" v100)) = (v1 "\/" v100)

      proof

        let v100, v1;

        (v100 "/\" (v1 "\/" v100)) = v100 by A13;

        hence thesis by A17;

      end;

      

       A65: for v1, v101 holds ((v101 "\/" v1) "\/" v101) = (v101 "\/" v1)

      proof

        let v1, v101;

        (v101 "/\" (v101 "\/" v1)) = v101 by A21;

        hence thesis by A9;

      end;

      

       A69: for v1, v100 holds (v100 "\/" (v100 "\/" v1)) = (v100 "\/" v1)

      proof

        let v1, v100;

        (v100 "/\" (v100 "\/" v1)) = v100 by A21;

        hence thesis by A17;

      end;

      

       A73: for v1, v101 holds ((v101 "/\" v1) "/\" v101) = (v101 "/\" v1)

      proof

        let v1, v101;

        (v101 "\/" (v101 "/\" v1)) = v101 by A33;

        hence thesis by A13;

      end;

      

       A77: for v1, v2, v100 holds (v100 "/\" (v1 "/\" (v100 "/\" v2))) = (v1 "/\" (v100 "/\" v2))

      proof

        let v1, v2, v100;

        (v100 "\/" (v1 "/\" (v100 "/\" v2))) = v100 by A2;

        hence thesis by A41;

      end;

      

       A81: for v100, v1 holds (v100 "/\" (v1 "/\" v100)) = (v1 "/\" v100)

      proof

        let v100, v1;

        (v100 "\/" (v1 "/\" v100)) = v100 by A9;

        hence thesis by A41;

      end;

      

       A85: for v1, v2, v101 holds ((v1 "/\" (v101 "/\" v2)) "\/" v101) = (v101 "\/" (v1 "/\" (v101 "/\" v2)))

      proof

        let v1, v2, v101;

        (v101 "\/" (v1 "/\" (v101 "/\" v2))) = v101 by A2;

        hence thesis by A61;

      end;

      

       A88: for v0, v2, v1 holds ((v0 "/\" (v1 "/\" v2)) "\/" v1) = v1

      proof

        let v0, v2, v1;

        (v1 "\/" (v0 "/\" (v1 "/\" v2))) = v1 by A2;

        hence thesis by A85;

      end;

      

       A91: for v1, v101 holds ((v101 "/\" v1) "\/" v101) = (v101 "\/" (v101 "/\" v1))

      proof

        let v1, v101;

        (v101 "\/" (v101 "/\" v1)) = v101 by A33;

        hence thesis by A61;

      end;

      

       A94: for v1, v0 holds ((v0 "/\" v1) "\/" v0) = v0

      proof

        let v1, v0;

        (v0 "\/" (v0 "/\" v1)) = v0 by A33;

        hence thesis by A91;

      end;

      

       A97: for v1, v102, v100 holds (v100 "/\" ((v100 "\/" v102) "\/" v1)) = v100

      proof

        let v1, v102, v100;

        (((v100 "\/" v102) "\/" v1) "\/" (v100 "\/" v102)) = ((v100 "\/" v102) "\/" v1) by A65;

        hence thesis by A3;

      end;

      

       A101: for v1, v101 holds ((v101 "\/" v1) "/\" v101) = v101

      proof

        let v1, v101;

        ((v101 "\/" v1) "\/" v101) = (v101 "\/" v1) by A65;

        hence thesis by A41;

      end;

      

       A105: for v103, v102, v100 holds ((v100 "\/" v103) "\/" (v103 "\/" (v100 "\/" v102))) = (v103 "\/" (v100 "\/" v102))

      proof

        let v103, v102, v100;

        ((v103 "\/" (v100 "\/" v102)) "/\" v103) = v103 by A101;

        hence thesis by A25;

      end;

      

       A109: for v101, v100, v1 holds (v100 "\/" (v101 "/\" (v1 "/\" v100))) = v100

      proof

        let v101, v100, v1;

        (v100 "/\" (v1 "/\" v100)) = (v1 "/\" v100) by A81;

        hence thesis by A2;

      end;

      

       A113: for v103, v102, v100 holds ((v100 "/\" v103) "/\" (v103 "/\" (v100 "/\" v102))) = (v103 "/\" (v100 "/\" v102))

      proof

        let v103, v102, v100;

        ((v103 "/\" (v100 "/\" v102)) "\/" v103) = v103 by A94;

        hence thesis by A37;

      end;

      

       A117: for v1, v102, v101 holds (((v101 "/\" v102) "/\" v1) "\/" v101) = v101

      proof

        let v1, v102, v101;

        (((v101 "/\" v102) "/\" v1) "/\" (v101 "/\" v102)) = ((v101 "/\" v102) "/\" v1) by A73;

        hence thesis by A88;

      end;

      

       A121: for v2, v1, v101 holds (((v101 "\/" v1) "\/" v2) "/\" v101) = (v101 "/\" ((v101 "\/" v1) "\/" v2))

      proof

        let v2, v1, v101;

        (v101 "/\" ((v101 "\/" v1) "\/" v2)) = v101 by A97;

        hence thesis by A81;

      end;

      

       A124: for v2, v1, v0 holds (((v0 "\/" v1) "\/" v2) "/\" v0) = v0

      proof

        let v2, v1, v0;

        (v0 "/\" ((v0 "\/" v1) "\/" v2)) = v0 by A97;

        hence thesis by A121;

      end;

      

       A127: for v1, v100, v2 holds (v100 "/\" (v1 "/\" (v2 "/\" v100))) = (v1 "/\" (v2 "/\" v100))

      proof

        let v1, v100, v2;

        (v100 "\/" (v1 "/\" (v2 "/\" v100))) = v100 by A109;

        hence thesis by A41;

      end;

      

       A131: for v0, v102, v101 holds ((v101 "/\" v102) "\/" (v0 "\/" v101)) = (v0 "\/" v101)

      proof

        let v0, v102, v101;

        ((v0 "\/" v101) "/\" v101) = v101 by A41;

        hence thesis by A117;

      end;

      

       A135: for v1, v102, v101 holds ((v101 "/\" v102) "\/" (v101 "\/" v1)) = (v101 "\/" v1)

      proof

        let v1, v102, v101;

        ((v101 "\/" v1) "/\" v101) = v101 by A101;

        hence thesis by A117;

      end;

      

       A139: for v0, v102, v101 holds ((v101 "\/" v102) "/\" (v0 "/\" v101)) = (v0 "/\" v101)

      proof

        let v0, v102, v101;

        ((v0 "/\" v101) "\/" v101) = v101 by A17;

        hence thesis by A124;

      end;

      

       A143: for v102, v100 holds ((v100 "/\" v102) "/\" (v102 "/\" v100)) = (v102 "/\" v100)

      proof

        let v102, v100;

        ((v102 "/\" v100) "\/" v102) = v102 by A94;

        hence thesis by A49;

      end;

      

       A147: for v100, v1, v102 holds ((v100 "/\" v102) "/\" ((v102 "/\" v1) "/\" v100)) = ((v102 "/\" v1) "/\" v100)

      proof

        let v100, v1, v102;

        (((v102 "/\" v1) "/\" v100) "\/" v102) = v102 by A117;

        hence thesis by A49;

      end;

      

       A151: for v102, v100 holds ((v100 "\/" v102) "\/" (v102 "\/" v100)) = (v102 "\/" v100)

      proof

        let v102, v100;

        ((v102 "\/" v100) "/\" v102) = v102 by A101;

        hence thesis by A53;

      end;

      

       A155: for v100, v101, v2 holds ((v100 "/\" (v2 "\/" v101)) "/\" (v101 "/\" v100)) = (v101 "/\" v100)

      proof

        let v100, v101, v2;

        ((v101 "/\" v100) "\/" (v2 "\/" v101)) = (v2 "\/" v101) by A131;

        hence thesis by A49;

      end;

      

       A159: for v100, v2, v101 holds ((v100 "/\" (v101 "\/" v2)) "/\" (v101 "/\" v100)) = (v101 "/\" v100)

      proof

        let v100, v2, v101;

        ((v101 "/\" v100) "\/" (v101 "\/" v2)) = (v101 "\/" v2) by A135;

        hence thesis by A49;

      end;

      

       A163: for v100, v101, v2 holds ((v100 "\/" (v2 "/\" v101)) "\/" (v101 "\/" v100)) = (v101 "\/" v100)

      proof

        let v100, v101, v2;

        ((v101 "\/" v100) "/\" (v2 "/\" v101)) = (v2 "/\" v101) by A139;

        hence thesis by A53;

      end;

      

       A167: for v1, v0 holds ((v0 "/\" v1) "\/" (v1 "/\" v0)) = (v0 "/\" v1)

      proof

        let v1, v0;

        ((v0 "/\" v1) "/\" (v1 "/\" v0)) = (v1 "/\" v0) by A143;

        hence thesis by A33;

      end;

      

       A170: for v0, v1 holds ((v1 "/\" v0) "\/" (v0 "/\" v1)) = (v0 "/\" v1)

      proof

        let v0, v1;

        ((v0 "/\" v1) "/\" (v1 "/\" v0)) = (v1 "/\" v0) by A143;

        hence thesis by A94;

      end;

      

       A173: for v1, v0 holds (v0 "/\" v1) = (v1 "/\" v0)

      proof

        let v1, v0;

        ((v0 "/\" v1) "\/" (v1 "/\" v0)) = (v0 "/\" v1) by A167;

        hence thesis by A170;

      end;

      

       A182: for v1, v0 holds ((v0 "\/" v1) "/\" (v1 "\/" v0)) = (v0 "\/" v1)

      proof

        let v1, v0;

        ((v0 "\/" v1) "\/" (v1 "\/" v0)) = (v1 "\/" v0) by A151;

        hence thesis by A21;

      end;

      

       A185: for v0, v1 holds ((v1 "\/" v0) "\/" (v0 "\/" v1)) = ((v0 "\/" v1) "\/" (v1 "\/" v0))

      proof

        let v0, v1;

        ((v0 "\/" v1) "\/" (v1 "\/" v0)) = (v1 "\/" v0) by A151;

        hence thesis by A65;

      end;

      

       A188: for v0, v1 holds (v1 "\/" v0) = ((v1 "\/" v0) "\/" (v0 "\/" v1))

      proof

        let v0, v1;

        ((v0 "\/" v1) "\/" (v1 "\/" v0)) = (v1 "\/" v0) by A151;

        hence thesis by A185;

      end;

      

       A191: for v1, v0 holds (v0 "\/" v1) = (v1 "\/" v0)

      proof

        let v1, v0;

        ((v0 "\/" v1) "\/" (v1 "\/" v0)) = (v1 "\/" v0) by A151;

        hence thesis by A188;

      end;

      

       A200: for v100, v2, v101 holds ((v100 "\/" v101) "\/" (v100 "\/" (v101 "\/" v2))) = (v101 "\/" (v100 "\/" (v101 "\/" v2)))

      proof

        let v100, v2, v101;

        (v101 "\/" (v100 "\/" (v101 "\/" v2))) = (v100 "\/" (v101 "\/" v2)) by A57;

        hence thesis by A105;

      end;

      

       A203: for v0, v2, v1 holds ((v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" v2))) = (v0 "\/" (v1 "\/" v2))

      proof

        let v0, v2, v1;

        (v1 "\/" (v0 "\/" (v1 "\/" v2))) = (v0 "\/" (v1 "\/" v2)) by A57;

        hence thesis by A200;

      end;

      

       A205: for v1, v2, v0 holds ((v0 "\/" v1) "\/" ((v0 "\/" v2) "\/" v1)) = (v1 "\/" (v0 "\/" v2))

      proof

        let v1, v2, v0;

        (v1 "\/" (v0 "\/" v2)) = ((v0 "\/" v2) "\/" v1) by A191;

        hence thesis by A105;

      end;

      

       A208: for v102, v100, v1 holds ((v100 "\/" (v102 "\/" (v1 "/\" v100))) "\/" (v100 "\/" v102)) = ((v102 "\/" (v1 "/\" v100)) "\/" (v100 "\/" v102))

      proof

        let v102, v100, v1;

        ((v102 "\/" (v1 "/\" v100)) "\/" (v100 "\/" v102)) = (v100 "\/" v102) by A163;

        hence thesis by A105;

      end;

      

       A211: for v1, v0, v2 holds ((v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" (v2 "/\" v0)))) = ((v1 "\/" (v2 "/\" v0)) "\/" (v0 "\/" v1))

      proof

        let v1, v0, v2;

        ((v0 "\/" (v1 "\/" (v2 "/\" v0))) "\/" (v0 "\/" v1)) = ((v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" (v2 "/\" v0)))) by A191;

        hence thesis by A208;

      end;

      

       A213: for v1, v0, v2 holds (v0 "\/" (v1 "\/" (v2 "/\" v0))) = ((v1 "\/" (v2 "/\" v0)) "\/" (v0 "\/" v1))

      proof

        let v1, v0, v2;

        ((v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" (v2 "/\" v0)))) = (v0 "\/" (v1 "\/" (v2 "/\" v0))) by A203;

        hence thesis by A211;

      end;

      

       A215: for v1, v0, v2 holds (v0 "\/" (v1 "\/" (v2 "/\" v0))) = (v0 "\/" v1)

      proof

        let v1, v0, v2;

        ((v1 "\/" (v2 "/\" v0)) "\/" (v0 "\/" v1)) = (v0 "\/" v1) by A163;

        hence thesis by A213;

      end;

      

       A218: for v101, v102, v1 holds ((v1 "\/" v102) "\/" (v101 "\/" v102)) = ((v1 "\/" v102) "\/" v101)

      proof

        let v101, v102, v1;

        (v102 "/\" (v1 "\/" v102)) = v102 by A13;

        hence thesis by A215;

      end;

      

       A221: for v1, v0, v2 holds (v0 "\/" ((v2 "/\" v0) "\/" v1)) = (v0 "\/" v1)

      proof

        let v1, v0, v2;

        (v1 "\/" (v2 "/\" v0)) = ((v2 "/\" v0) "\/" v1) by A191;

        hence thesis by A215;

      end;

      

       A224: for v2, v1, v0 holds ((v0 "\/" v1) "\/" (v0 "\/" v2)) = (v1 "\/" (v0 "\/" v2))

      proof

        let v2, v1, v0;

        ((v0 "\/" v1) "\/" ((v0 "\/" v2) "\/" v1)) = ((v0 "\/" v1) "\/" (v0 "\/" v2)) by A218;

        hence thesis by A205;

      end;

      

       A227: for v102, v1, v101 holds ((v101 "\/" v1) "\/" (v101 "\/" v102)) = ((v101 "\/" v1) "\/" v102)

      proof

        let v102, v1, v101;

        (v101 "/\" (v101 "\/" v1)) = v101 by A21;

        hence thesis by A221;

      end;

      

       A230: for v1, v2, v0 holds (v1 "\/" (v0 "\/" v2)) = ((v0 "\/" v1) "\/" v2)

      proof

        let v1, v2, v0;

        ((v0 "\/" v1) "\/" (v0 "\/" v2)) = (v1 "\/" (v0 "\/" v2)) by A224;

        hence thesis by A227;

      end;

      

       A236: for v102, v1, v0 holds ((v1 "\/" v0) "\/" ((v0 "\/" v1) "\/" v102)) = ((v1 "\/" v0) "\/" v102)

      proof

        let v102, v1, v0;

        ((v0 "\/" v1) "/\" (v1 "\/" v0)) = (v0 "\/" v1) by A182;

        hence thesis by A221;

      end;

      

       A239: for v0, v2, v1 holds ((v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" v2))) = ((v0 "\/" v1) "\/" v2)

      proof

        let v0, v2, v1;

        ((v1 "\/" v0) "\/" v2) = (v0 "\/" (v1 "\/" v2)) by A230;

        hence thesis by A236;

      end;

      

       A241: for v0, v2, v1 holds (v1 "\/" (v0 "\/" (v0 "\/" (v1 "\/" v2)))) = ((v0 "\/" v1) "\/" v2)

      proof

        let v0, v2, v1;

        ((v0 "\/" v1) "\/" (v0 "\/" (v1 "\/" v2))) = (v1 "\/" (v0 "\/" (v0 "\/" (v1 "\/" v2)))) by A230;

        hence thesis by A239;

      end;

      

       A244: for v1, v2, v0 holds (v0 "\/" (v1 "\/" (v0 "\/" v2))) = ((v1 "\/" v0) "\/" v2)

      proof

        let v1, v2, v0;

        (v1 "\/" (v1 "\/" (v0 "\/" v2))) = (v1 "\/" (v0 "\/" v2)) by A69;

        hence thesis by A241;

      end;

      

       A246: for v1, v2, v0 holds (v1 "\/" (v0 "\/" v2)) = ((v1 "\/" v0) "\/" v2)

      proof

        let v1, v2, v0;

        (v0 "\/" (v1 "\/" (v0 "\/" v2))) = (v1 "\/" (v0 "\/" v2)) by A57;

        hence thesis by A244;

      end;

      

       A257: for v1, v2, v0 holds ((v1 "/\" v0) "/\" (v1 "/\" (v0 "/\" v2))) = (v1 "/\" (v0 "/\" v2))

      proof

        let v1, v2, v0;

        (v0 "/\" v1) = (v1 "/\" v0) by A173;

        hence thesis by A113;

      end;

      

       A261: for v102, v100, v1 holds ((v100 "/\" (v102 "/\" (v1 "\/" v100))) "/\" (v100 "/\" v102)) = ((v102 "/\" (v1 "\/" v100)) "/\" (v100 "/\" v102))

      proof

        let v102, v100, v1;

        ((v102 "/\" (v1 "\/" v100)) "/\" (v100 "/\" v102)) = (v100 "/\" v102) by A155;

        hence thesis by A113;

      end;

      

       A264: for v1, v0, v2 holds ((v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v2 "\/" v0)))) = ((v1 "/\" (v2 "\/" v0)) "/\" (v0 "/\" v1))

      proof

        let v1, v0, v2;

        ((v0 "/\" (v1 "/\" (v2 "\/" v0))) "/\" (v0 "/\" v1)) = ((v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v2 "\/" v0)))) by A173;

        hence thesis by A261;

      end;

      

       A266: for v1, v0, v2 holds (v0 "/\" (v1 "/\" (v2 "\/" v0))) = ((v1 "/\" (v2 "\/" v0)) "/\" (v0 "/\" v1))

      proof

        let v1, v0, v2;

        ((v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v2 "\/" v0)))) = (v0 "/\" (v1 "/\" (v2 "\/" v0))) by A257;

        hence thesis by A264;

      end;

      

       A268: for v1, v0, v2 holds (v0 "/\" (v1 "/\" (v2 "\/" v0))) = (v0 "/\" v1)

      proof

        let v1, v0, v2;

        ((v1 "/\" (v2 "\/" v0)) "/\" (v0 "/\" v1)) = (v0 "/\" v1) by A155;

        hence thesis by A266;

      end;

      

       A271: for v101, v0, v2, v1 holds (((v0 "/\" (v1 "\/" v2)) "/\" v101) "/\" (v101 "/\" (v1 "/\" v0))) = (v101 "/\" ((v0 "/\" (v1 "\/" v2)) "/\" (v1 "/\" v0)))

      proof

        let v101, v0, v2, v1;

        ((v0 "/\" (v1 "\/" v2)) "/\" (v1 "/\" v0)) = (v1 "/\" v0) by A159;

        hence thesis by A113;

      end;

      

       A274: for v3, v0, v2, v1 holds (((v0 "/\" (v1 "\/" v2)) "/\" v3) "/\" (v3 "/\" (v1 "/\" v0))) = (v3 "/\" (v1 "/\" v0))

      proof

        let v3, v0, v2, v1;

        ((v0 "/\" (v1 "\/" v2)) "/\" (v1 "/\" v0)) = (v1 "/\" v0) by A159;

        hence thesis by A271;

      end;

      

       A277: for v102, v2, v100 holds ((v100 "/\" (v102 "/\" (v100 "\/" v2))) "/\" (v100 "/\" v102)) = ((v102 "/\" (v100 "\/" v2)) "/\" (v100 "/\" v102))

      proof

        let v102, v2, v100;

        ((v102 "/\" (v100 "\/" v2)) "/\" (v100 "/\" v102)) = (v100 "/\" v102) by A159;

        hence thesis by A113;

      end;

      

       A280: for v1, v2, v0 holds ((v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v0 "\/" v2)))) = ((v1 "/\" (v0 "\/" v2)) "/\" (v0 "/\" v1))

      proof

        let v1, v2, v0;

        ((v0 "/\" (v1 "/\" (v0 "\/" v2))) "/\" (v0 "/\" v1)) = ((v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v0 "\/" v2)))) by A173;

        hence thesis by A277;

      end;

      

       A282: for v1, v2, v0 holds (v0 "/\" (v1 "/\" (v0 "\/" v2))) = ((v1 "/\" (v0 "\/" v2)) "/\" (v0 "/\" v1))

      proof

        let v1, v2, v0;

        ((v0 "/\" v1) "/\" (v0 "/\" (v1 "/\" (v0 "\/" v2)))) = (v0 "/\" (v1 "/\" (v0 "\/" v2))) by A257;

        hence thesis by A280;

      end;

      

       A284: for v1, v2, v0 holds (v0 "/\" (v1 "/\" (v0 "\/" v2))) = (v0 "/\" v1)

      proof

        let v1, v2, v0;

        ((v1 "/\" (v0 "\/" v2)) "/\" (v0 "/\" v1)) = (v0 "/\" v1) by A159;

        hence thesis by A282;

      end;

      

       A287: for v101, v1, v102 holds ((v102 "/\" v1) "/\" (v101 "/\" v102)) = ((v102 "/\" v1) "/\" v101)

      proof

        let v101, v1, v102;

        (v102 "\/" (v102 "/\" v1)) = v102 by A33;

        hence thesis by A268;

      end;

      

       A290: for v1, v0, v2 holds (v0 "/\" ((v2 "\/" v0) "/\" v1)) = (v0 "/\" v1)

      proof

        let v1, v0, v2;

        (v1 "/\" (v2 "\/" v0)) = ((v2 "\/" v0) "/\" v1) by A173;

        hence thesis by A268;

      end;

      

       A293: for v2, v1, v0 holds ((v0 "/\" v1) "/\" (v1 "/\" v2)) = ((v1 "/\" v2) "/\" v0)

      proof

        let v2, v1, v0;

        ((v0 "/\" v1) "/\" ((v1 "/\" v2) "/\" v0)) = ((v0 "/\" v1) "/\" (v1 "/\" v2)) by A287;

        hence thesis by A147;

      end;

      

       A295: for v1, v2, v0 holds (v0 "/\" ((v0 "\/" v2) "/\" v1)) = (v0 "/\" v1)

      proof

        let v1, v2, v0;

        (v1 "/\" (v0 "\/" v2)) = ((v0 "\/" v2) "/\" v1) by A173;

        hence thesis by A284;

      end;

      

       A299: for v102, v101, v1 holds ((v1 "/\" v101) "/\" (v101 "/\" v102)) = ((v1 "/\" v101) "/\" v102)

      proof

        let v102, v101, v1;

        (v101 "\/" (v1 "/\" v101)) = v101 by A9;

        hence thesis by A290;

      end;

      

       A303: for v102, v1, v101 holds ((v101 "/\" v1) "/\" (v101 "/\" v102)) = ((v101 "/\" v1) "/\" v102)

      proof

        let v102, v1, v101;

        (v101 "\/" (v101 "/\" v1)) = v101 by A33;

        hence thesis by A290;

      end;

      

       A307: for v101, v2, v100, v1 holds ((v100 "/\" v101) "/\" (v101 "/\" (v100 "/\" v2))) = (v101 "/\" (v100 "/\" ((v1 "\/" v100) "/\" v2)))

      proof

        let v101, v2, v100, v1;

        (v100 "/\" ((v1 "\/" v100) "/\" v2)) = (v100 "/\" v2) by A290;

        hence thesis by A113;

      end;

      

       A310: for v1, v2, v0, v3 holds ((v0 "/\" v1) "/\" (v0 "/\" v2)) = (v1 "/\" (v0 "/\" ((v3 "\/" v0) "/\" v2)))

      proof

        let v1, v2, v0, v3;

        ((v0 "/\" v1) "/\" (v1 "/\" (v0 "/\" v2))) = ((v0 "/\" v1) "/\" (v0 "/\" v2)) by A299;

        hence thesis by A307;

      end;

      

       A312: for v1, v2, v0, v3 holds ((v0 "/\" v1) "/\" v2) = (v1 "/\" (v0 "/\" ((v3 "\/" v0) "/\" v2)))

      proof

        let v1, v2, v0, v3;

        ((v0 "/\" v1) "/\" (v0 "/\" v2)) = ((v0 "/\" v1) "/\" v2) by A303;

        hence thesis by A310;

      end;

      

       A314: for v2, v1, v0 holds ((v0 "/\" v1) "/\" v2) = (v1 "/\" (v0 "/\" v2))

      proof

        now

          let v1, v2, v0, v3;

          (v0 "/\" ((v3 "\/" v0) "/\" v2)) = (v0 "/\" v2) by A290;

          hence ((v0 "/\" v1) "/\" v2) = (v1 "/\" (v0 "/\" v2)) by A312;

        end;

        hence thesis;

      end;

      

       A316: for v0, v2, v1 holds (v1 "/\" (v0 "/\" (v1 "/\" v2))) = ((v1 "/\" v2) "/\" v0)

      proof

        let v0, v2, v1;

        ((v0 "/\" v1) "/\" (v1 "/\" v2)) = (v1 "/\" (v0 "/\" (v1 "/\" v2))) by A314;

        hence thesis by A293;

      end;

      

       A319: for v1, v2, v0 holds (v1 "/\" (v0 "/\" v2)) = ((v0 "/\" v2) "/\" v1)

      proof

        let v1, v2, v0;

        (v0 "/\" (v1 "/\" (v0 "/\" v2))) = (v1 "/\" (v0 "/\" v2)) by A77;

        hence thesis by A316;

      end;

      

       A322: for v0, v2, v1 holds (v0 "/\" (v1 "/\" v2)) = (v2 "/\" (v1 "/\" v0))

      proof

        let v0, v2, v1;

        ((v1 "/\" v2) "/\" v0) = (v2 "/\" (v1 "/\" v0)) by A314;

        hence thesis by A319;

      end;

      

       A324: for v0, v3, v2, v1 holds (((v1 "\/" v2) "/\" (v0 "/\" v3)) "/\" (v3 "/\" (v1 "/\" v0))) = (v3 "/\" (v1 "/\" v0))

      proof

        let v0, v3, v2, v1;

        ((v0 "/\" (v1 "\/" v2)) "/\" v3) = ((v1 "\/" v2) "/\" (v0 "/\" v3)) by A314;

        hence thesis by A274;

      end;

      

       A327: for v2, v3, v1, v0 holds ((v0 "/\" v2) "/\" (v3 "/\" ((v0 "\/" v1) "/\" (v2 "/\" v3)))) = (v3 "/\" (v0 "/\" v2))

      proof

        let v2, v3, v1, v0;

        (((v0 "\/" v1) "/\" (v2 "/\" v3)) "/\" (v3 "/\" (v0 "/\" v2))) = ((v0 "/\" v2) "/\" (v3 "/\" ((v0 "\/" v1) "/\" (v2 "/\" v3)))) by A322;

        hence thesis by A324;

      end;

      

       A330: for v1, v2, v3, v0 holds ((v0 "/\" v1) "/\" ((v0 "\/" v3) "/\" (v1 "/\" v2))) = (v2 "/\" (v0 "/\" v1))

      proof

        let v1, v2, v3, v0;

        (v2 "/\" ((v0 "\/" v3) "/\" (v1 "/\" v2))) = ((v0 "\/" v3) "/\" (v1 "/\" v2)) by A127;

        hence thesis by A327;

      end;

      

       A333: for v1, v3, v2, v0 holds (v1 "/\" (v0 "/\" ((v0 "\/" v2) "/\" (v1 "/\" v3)))) = (v3 "/\" (v0 "/\" v1))

      proof

        let v1, v3, v2, v0;

        ((v0 "/\" v1) "/\" ((v0 "\/" v2) "/\" (v1 "/\" v3))) = (v1 "/\" (v0 "/\" ((v0 "\/" v2) "/\" (v1 "/\" v3)))) by A314;

        hence thesis by A330;

      end;

      

       A336: for v1, v3, v0 holds (v0 "/\" (v1 "/\" (v0 "/\" v3))) = (v3 "/\" (v1 "/\" v0))

      proof

        now

          let v0, v3, v2, v1;

          (v1 "/\" ((v1 "\/" v2) "/\" (v0 "/\" v3))) = (v1 "/\" (v0 "/\" v3)) by A295;

          hence (v0 "/\" (v1 "/\" (v0 "/\" v3))) = (v3 "/\" (v1 "/\" v0)) by A333;

        end;

        hence thesis;

      end;

      

       A339: for v1, v2, v0 holds (v1 "/\" (v0 "/\" v2)) = (v2 "/\" (v1 "/\" v0))

      proof

        let v1, v2, v0;

        (v0 "/\" (v1 "/\" (v0 "/\" v2))) = (v1 "/\" (v0 "/\" v2)) by A77;

        hence thesis by A336;

      end;

      for v0, v2, v1 holds (v0 "/\" (v1 "/\" v2)) = ((v0 "/\" v1) "/\" v2)

      proof

        let v0, v2, v1;

        (v0 "/\" (v1 "/\" v2)) = (v2 "/\" (v0 "/\" v1)) by A339

        .= ((v0 "/\" v1) "/\" v2) by A173;

        hence thesis;

      end;

      hence thesis by A173, A191, A21, A33, A246;

    end;

    theorem :: ROBBINS5:14

    

     AuxiliaryMcKenzie: L is join-commutative join-associative meet-commutative meet-associative & (for v1, v0 holds (v0 "/\" (v0 "\/" v1)) = v0) & (for v1, v0 holds (v0 "\/" (v0 "/\" v1)) = v0) implies (for v1, v2, v0 holds (v0 "\/" (v1 "/\" (v0 "/\" v2))) = v0) & (for v1, v2, v0 holds (v0 "/\" (v1 "\/" (v0 "\/" v2))) = v0) & (for v2, v1, v0 holds (((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1) = v1) & (for v2, v1, v0 holds (((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1) = v1)

    proof

      assume

       A2: L is join-commutative;

      assume

       A3: L is join-associative;

      assume

       A4: L is meet-commutative;

      assume

       A5: L is meet-associative;

      assume

       A6: for v1, v0 holds (v0 "/\" (v0 "\/" v1)) = v0;

      assume

       A7: for v1, v0 holds (v0 "\/" (v0 "/\" v1)) = v0;

      thus for v1, v2, v0 holds (v0 "\/" (v1 "/\" (v0 "/\" v2))) = v0

      proof

        let v1, v2, v0;

        (v0 "\/" (v1 "/\" (v0 "/\" v2))) = (v0 "\/" ((v1 "/\" v0) "/\" v2)) by A5

        .= (v0 "\/" ((v0 "/\" v1) "/\" v2)) by A4

        .= (v0 "\/" (v0 "/\" (v1 "/\" v2))) by A5

        .= v0 by A7;

        hence thesis;

      end;

      thus for v1, v2, v0 holds (v0 "/\" (v1 "\/" (v0 "\/" v2))) = v0

      proof

        let v1, v2, v0;

        (v0 "/\" (v1 "\/" (v0 "\/" v2))) = (v0 "/\" ((v1 "\/" v0) "\/" v2)) by A3

        .= (v0 "/\" ((v0 "\/" v1) "\/" v2)) by A2

        .= (v0 "/\" (v0 "\/" (v1 "\/" v2))) by A3

        .= v0 by A6;

        hence thesis;

      end;

      thus for v2, v1, v0 holds (((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1) = v1

      proof

        let v2, v1, v0;

        (((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1) = ((v0 "/\" v1) "\/" ((v1 "/\" v2) "\/" v1)) by A3

        .= ((v0 "/\" v1) "\/" (v1 "\/" (v1 "/\" v2))) by A2

        .= ((v0 "/\" v1) "\/" v1) by A7

        .= (v1 "\/" (v0 "/\" v1)) by A2

        .= (v1 "\/" (v1 "/\" v0)) by A4

        .= v1 by A7;

        hence thesis;

      end;

      let v2, v1, v0;

      (((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1) = ((v0 "\/" v1) "/\" ((v1 "\/" v2) "/\" v1)) by A5

      .= ((v0 "\/" v1) "/\" (v1 "/\" (v1 "\/" v2))) by A4

      .= ((v0 "\/" v1) "/\" v1) by A6

      .= (v1 "/\" (v0 "\/" v1)) by A4

      .= (v1 "/\" (v1 "\/" v0)) by A2

      .= v1 by A6;

      hence thesis;

    end;

    definition

      let L be non empty LattStr;

      :: ROBBINS5:def6

      attr L is satisfying_4_McKenzie_axioms means L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4;

    end

    registration

      cluster satisfying_4_McKenzie_axioms -> satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3 satisfying_McKenzie_4 for non empty LattStr;

      coherence ;

      cluster satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3 satisfying_McKenzie_4 -> satisfying_4_McKenzie_axioms for non empty LattStr;

      coherence ;

    end

    reserve L for non empty LattStr;

    theorem :: ROBBINS5:15

    

     CombinedMcKenzie: L is Lattice iff L is satisfying_4_McKenzie_axioms

    proof

      thus L is Lattice implies L is satisfying_4_McKenzie_axioms

      proof

        assume

         A1: L is Lattice;

        

         C1: for v1, v0 holds (v0 "/\" (v0 "\/" v1)) = v0 by A1, LATTICES:def 9;

        for v1, v0 holds (v0 "\/" (v0 "/\" v1)) = v0

        proof

          let v1, v0;

          

           A2: L is join-commutative meet-commutative meet-absorbing by A1;

          

          then (v0 "\/" (v0 "/\" v1)) = ((v0 "/\" v1) "\/" v0)

          .= ((v1 "/\" v0) "\/" v0) by A2

          .= v0 by A2;

          hence thesis;

        end;

        then L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4 by AuxiliaryMcKenzie, A1, C1;

        hence thesis;

      end;

      assume L is satisfying_4_McKenzie_axioms;

      then

       b1: L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4;

      then

       B1: (for v1,v0 be Element of L holds (v0 "/\" (v0 "\/" v1)) = v0) & (for v1,v0 be Element of L holds (v0 "\/" (v0 "/\" v1)) = v0) & L is join-commutative meet-commutative meet-associative join-associative by MainMcKenzie;

      

       B2: for v0,v1 be Element of L holds ((v1 "/\" v0) "\/" v0) = v0

      proof

        let v0, v1;

        ((v1 "/\" v0) "\/" v0) = (v0 "\/" (v1 "/\" v0)) by B1

        .= (v0 "\/" (v0 "/\" v1)) by B1

        .= v0 by b1, MainMcKenzie;

        hence thesis;

      end;

      L is meet-absorbing join-absorbing by b1, B2, MainMcKenzie;

      hence thesis by B1;

    end;

    registration

      cluster Lattice-like -> satisfying_4_McKenzie_axioms for non empty LattStr;

      coherence by CombinedMcKenzie;

      cluster satisfying_4_McKenzie_axioms -> Lattice-like for non empty LattStr;

      coherence by CombinedMcKenzie;

    end