robbins2.miz



    begin

    definition

      let L be non empty ComplLLattStr;

      :: ROBBINS2:def1

      attr L is satisfying_DN_1 means

      : Def1: for x,y,z,u be Element of L holds ((((((x + y) ` ) + z) ` ) + ((x + (((z ` ) + ((z + u) ` )) ` )) ` )) ` ) = z;

    end

    registration

      cluster TrivComplLat -> satisfying_DN_1;

      coherence by STRUCT_0:def 10;

      cluster TrivOrtLat -> satisfying_DN_1;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster join-commutative join-associative satisfying_DN_1 for non empty ComplLLattStr;

      existence

      proof

        take TrivComplLat ;

        thus thesis;

      end;

    end

    reserve L for satisfying_DN_1 non empty ComplLLattStr;

    reserve x,y,z for Element of L;

    theorem :: ROBBINS2:1

    

     Th1: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z,u,v be Element of L holds ((((x + y) ` ) + ((((((z + u) ` ) + x) ` ) + (((y ` ) + ((y + v) ` )) ` )) ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z,u,v be Element of L;

      set X = ((((z + u) ` ) + x) ` ), Y = ((z + (((x ` ) + ((x + u) ` )) ` )) ` );

      set Z = y, U = v;

      ((((((X + Y) ` ) + Z) ` ) + ((X + (((Z ` ) + ((Z + U) ` )) ` )) ` )) ` ) = Z by Def1;

      hence thesis by Def1;

    end;

    theorem :: ROBBINS2:2

    

     Th2: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z,u be Element of L holds ((((x + y) ` ) + ((((z + x) ` ) + (((y ` ) + ((y + u) ` )) ` )) ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z,u be Element of L;

      set v = the Element of L;

      ((((x + z) ` ) + ((((((y + u) ` ) + x) ` ) + (((z ` ) + ((z + v) ` )) ` )) ` )) ` ) = z by Th1;

      hence thesis by Th1;

    end;

    theorem :: ROBBINS2:3

    

     Th3: for L be satisfying_DN_1 non empty ComplLLattStr, x be Element of L holds ((((x + (x ` )) ` ) + x) ` ) = (x ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x be Element of L;

      set y = the Element of L;

      set V = ((x + y) ` );

      ((((x + (x ` )) ` ) + ((((((((x ` ) ` ) + y) ` ) + x) ` ) + ((((x ` ) ` ) + (((x ` ) + V) ` )) ` )) ` )) ` ) = (x ` ) by Th1;

      hence thesis by Def1;

    end;

    theorem :: ROBBINS2:4

    

     Th4: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z,u be Element of L holds ((((x + y) ` ) + ((((z + x) ` ) + ((((((y + (y ` )) ` ) + y) ` ) + ((y + u) ` )) ` )) ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z,u be Element of L;

      ((((y + (y ` )) ` ) + y) ` ) = (y ` ) by Th3;

      hence thesis by Th2;

    end;

    theorem :: ROBBINS2:5

    

     Th5: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((x + y) ` ) + ((((z + x) ` ) + y) ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set u = the Element of L;

      set U = (((y ` ) + ((y + u) ` )) ` );

      ((((x + y) ` ) + ((((z + x) ` ) + ((((((y + (y ` )) ` ) + y) ` ) + ((y + U) ` )) ` )) ` )) ` ) = y by Th4;

      hence thesis by Def1;

    end;

    theorem :: ROBBINS2:6

    

     Th6: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((((x + y) ` ) + (((x ` ) + y) ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set Z = ((x + (x ` )) ` );

      ((((x + y) ` ) + ((((Z + x) ` ) + y) ` )) ` ) = y by Th5;

      hence thesis by Th3;

    end;

    theorem :: ROBBINS2:7

    

     Th7: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((((((x + y) ` ) + x) ` ) + ((x + y) ` )) ` ) = x

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set X = ((x + y) ` );

      ((((X + x) ` ) + ((((x + X) ` ) + ((((((x + (x ` )) ` ) + x) ` ) + ((x + y) ` )) ` )) ` )) ` ) = x by Th4;

      hence thesis by Th5;

    end;

    theorem :: ROBBINS2:8

    

     Th8: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((x + ((((x + y) ` ) + x) ` )) ` ) = ((x + y) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set X = ((x + y) ` ), Y = x;

      ((((((X + Y) ` ) + X) ` ) + ((X + Y) ` )) ` ) = X by Th7;

      hence thesis by Th7;

    end;

    theorem :: ROBBINS2:9

    

     Th9: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((((x + y) ` ) + z) ` ) + ((x + z) ` )) ` ) = z

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set X = ((x + y) ` ), Y = z, Z = ((((x + y) ` ) + x) ` );

      ((((X + Y) ` ) + ((((Z + X) ` ) + Y) ` )) ` ) = Y by Th5;

      hence thesis by Th7;

    end;

    theorem :: ROBBINS2:10

    

     Th10: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((x + ((((y + z) ` ) + ((y + x) ` )) ` )) ` ) = ((y + x) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set Z = ((y + x) ` ), X = ((y + z) ` ), Y = x;

      ((((((X + Y) ` ) + Z) ` ) + ((X + Z) ` )) ` ) = Z by Th9;

      hence thesis by Th9;

    end;

    theorem :: ROBBINS2:11

    

     Th11: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y) ` ) = (((x ` ) + y) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set X = ((x + y) ` ), Z = (((x ` ) + y) ` ), Y = z;

      ((((((X + Y) ` ) + Z) ` ) + ((X + Z) ` )) ` ) = Z by Th9;

      hence thesis by Th6;

    end;

    theorem :: ROBBINS2:12

    

     Th12: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((x + ((((y + z) ` ) + ((z + x) ` )) ` )) ` ) = ((z + x) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set Y = z, Z = ((((y + x) ` ) + ((y + z) ` )) ` );

      ((x + ((((Y + Z) ` ) + ((Y + x) ` )) ` )) ` ) = ((Y + x) ` ) by Th10;

      hence thesis by Th10;

    end;

    theorem :: ROBBINS2:13

    

     Th13: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z,u be Element of L holds ((((x + y) ` ) + ((((z + x) ` ) + (((y ` ) + ((u + y) ` )) ` )) ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z,u be Element of L;

      set U = ((((u + z) ` ) + ((u + y) ` )) ` );

      ((((x + y) ` ) + ((((z + x) ` ) + (((y ` ) + ((y + U) ` )) ` )) ` )) ` ) = y by Th2;

      hence thesis by Th10;

    end;

    theorem :: ROBBINS2:14

    

     Th14: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((x + y) ` ) = ((y + x) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set Z = y, X = x, Y = ((y + x) ` );

      ((((Y + Z) ` ) + ((Z + X) ` )) ` ) = y by Th7;

      hence thesis by Th12;

    end;

    theorem :: ROBBINS2:15

    

     Th15: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((((x + y) ` ) + ((y + z) ` )) ` ) + z) ` ) = ((y + z) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set Y = ((((x + y) ` ) + ((y + z) ` )) ` );

      ((z + Y) ` ) = ((Y + z) ` ) by Th14;

      hence thesis by Th12;

    end;

    theorem :: ROBBINS2:16

    

     Th16: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((x + ((((x + y) ` ) + z) ` )) ` ) + z) ` ) = ((((x + y) ` ) + z) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set X = ((((x + y) ` ) + x) ` ), Y = ((x + y) ` );

      ((X + Y) ` ) = x by Th7;

      hence thesis by Th15;

    end;

    theorem :: ROBBINS2:17

    

     Th17: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((((((x + y) ` ) + x) ` ) + y) ` ) = ((y + y) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set X = ((x + y) ` );

      ((X + ((((X + x) ` ) + y) ` )) ` ) = y by Th5;

      hence thesis by Th16;

    end;

    theorem :: ROBBINS2:18

    

     Th18: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((x ` ) + ((y + x) ` )) ` ) = x

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set X = ((y + x) ` );

      ((X + (((((x ` ) + y) ` ) + (((x ` ) + X) ` )) ` )) ` ) = x by Th13;

      hence thesis by Th10;

    end;

    theorem :: ROBBINS2:19

    

     Th19: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((((x + y) ` ) + (y ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      (((y ` ) + ((x + y) ` )) ` ) = y by Th18;

      hence thesis by Th14;

    end;

    theorem :: ROBBINS2:20

    

     Th20: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((x + ((y + (x ` )) ` )) ` ) = (x ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set Z = (x ` ), X = y, Y = x;

      ((((((X + Y) ` ) + Z) ` ) + ((X + Z) ` )) ` ) = Z by Th9;

      hence thesis by Th19;

    end;

    theorem :: ROBBINS2:21

    

     Th21: for L be satisfying_DN_1 non empty ComplLLattStr, x be Element of L holds ((x + x) ` ) = (x ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x be Element of L;

      set y = the Element of L;

      set Y = ((y + x) ` );

      ((x + ((Y + (x ` )) ` )) ` ) = (x ` ) by Th20;

      hence thesis by Th19;

    end;

    theorem :: ROBBINS2:22

    

     Th22: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((((((x + y) ` ) + x) ` ) + y) ` ) = (y ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      (y ` ) = ((y + y) ` ) by Th21

      .= ((((((x + y) ` ) + x) ` ) + y) ` ) by Th17;

      hence thesis;

    end;

    theorem :: ROBBINS2:23

    

     Th23: for L be satisfying_DN_1 non empty ComplLLattStr, x be Element of L holds ((x ` ) ` ) = x

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x be Element of L;

      ((x ` ) ` ) = ((((((x + (x ` )) ` ) + x) ` ) + (x ` )) ` ) by Th22

      .= x by Th19;

      hence thesis;

    end;

    theorem :: ROBBINS2:24

    

     Th24: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((((x + y) ` ) + x) ` ) + y) = ((y ` ) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      (((((((x + y) ` ) + x) ` ) + y) ` ) ` ) = ((y ` ) ` ) by Th22;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:25

    

     Th25: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((x + y) ` ) ` ) = (y + x)

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      (((x + y) ` ) ` ) = (((y + x) ` ) ` ) by Th14

      .= (y + x) by Th23;

      hence thesis;

    end;

    theorem :: ROBBINS2:26

    

     Th26: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (x + ((((y + z) ` ) + ((y + x) ` )) ` )) = (((y + x) ` ) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      (((x + ((((y + z) ` ) + ((y + x) ` )) ` )) ` ) ` ) = (((y + x) ` ) ` ) by Th10;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:27

    

     Th27: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (x + y) = (y + x)

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      (x + y) = (((x + y) ` ) ` ) by Th23

      .= (y + x) by Th25;

      hence thesis;

    end;

    

     Lm1: for L be satisfying_DN_1 non empty ComplLLattStr holds L is join-commutative

    proof

      let L;

      for x, y holds (x + y) = (y + x) by Th27;

      hence thesis by LATTICES:def 4;

    end;

    registration

      cluster satisfying_DN_1 -> join-commutative for non empty ComplLLattStr;

      coherence by Lm1;

    end

    theorem :: ROBBINS2:28

    

     Th28: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((((x + y) ` ) + x) ` ) + y) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      (((((x + y) ` ) + x) ` ) + y) = ((y ` ) ` ) by Th24;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:29

    for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((((x + y) ` ) + y) ` ) + x) = x by Th28;

    theorem :: ROBBINS2:30

    for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (x + ((((y + x) ` ) + y) ` )) = x by Th28;

    theorem :: ROBBINS2:31

    

     Th31: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((x + (y ` )) ` ) + (((y ` ) + y) ` )) = ((x + (y ` )) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set X = ((x + (y ` )) ` );

      (X + ((((y + X) ` ) + y) ` )) = X by Th28;

      hence thesis by Th20;

    end;

    theorem :: ROBBINS2:32

    

     Th32: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((x + y) ` ) + ((y + (y ` )) ` )) = ((x + y) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set X = ((x + y) ` ), Y = (y ` );

      (X + ((((Y + X) ` ) + Y) ` )) = X by Th28;

      hence thesis by Th18;

    end;

    theorem :: ROBBINS2:33

    for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((x + y) ` ) + (((y ` ) + y) ` )) = ((x + y) ` ) by Th32;

    theorem :: ROBBINS2:34

    

     Th34: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((((x + (y ` )) ` ) ` ) + y) ` ) = (((y ` ) + y) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set Y = (y ` ), Z = y;

      ((((((x + Y) ` ) + ((Y + Z) ` )) ` ) + Z) ` ) = ((Y + Z) ` ) by Th15;

      hence thesis by Th31;

    end;

    theorem :: ROBBINS2:35

    

     Th35: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((x + (y ` )) + y) ` ) = (((y ` ) + y) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      (((((x + (y ` )) ` ) ` ) + y) ` ) = (((y ` ) + y) ` ) by Th34;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:36

    

     Th36: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (((((((x + (y ` )) + z) ` ) + y) ` ) + (((y ` ) + y) ` )) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      (((x + (y ` )) + y) ` ) = (((y ` ) + y) ` ) by Th35;

      hence thesis by Th9;

    end;

    theorem :: ROBBINS2:37

    

     Th37: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (x + ((((y + z) ` ) + ((y + x) ` )) ` )) = (y + x)

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      (x + ((((y + z) ` ) + ((y + x) ` )) ` )) = (((y + x) ` ) ` ) by Th26;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:38

    

     Th38: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (x + ((y + ((((z + y) ` ) + x) ` )) ` )) = (((z + y) ` ) + x)

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set Y = ((z + y) ` ), Z = (y ` );

      (x + ((((Y + Z) ` ) + ((Y + x) ` )) ` )) = (Y + x) by Th37;

      hence thesis by Th19;

    end;

    theorem :: ROBBINS2:39

    for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (x + ((((y + x) ` ) + ((y + z) ` )) ` )) = (y + x) by Th37;

    theorem :: ROBBINS2:40

    

     Th40: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (((((x + y) ` ) + ((((x + y) ` ) + ((x + z) ` )) ` )) ` ) + y) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set Y = ((((x + y) ` ) + ((x + z) ` )) ` );

      (((((y + Y) ` ) + Y) ` ) + y) = y by Th28;

      hence thesis by Th37;

    end;

    theorem :: ROBBINS2:41

    

     Th41: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((((x + (y ` )) + z) ` ) + y) ` ) ` ) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      ((((((x + (y ` )) + z) ` ) + y) ` ) + (((y ` ) + y) ` )) = (((((x + (y ` )) + z) ` ) + y) ` ) by Th32;

      hence thesis by Th36;

    end;

    theorem :: ROBBINS2:42

    

     Th42: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (x + (((y + (x ` )) + z) ` )) = x

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      ((((((y + (x ` )) + z) ` ) + x) ` ) ` ) = x by Th41;

      hence thesis by Th25;

    end;

    theorem :: ROBBINS2:43

    

     Th43: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((x ` ) + (((y + x) + z) ` )) = (x ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set X = (x ` );

      (X + (((y + (X ` )) + z) ` )) = X by Th42;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:44

    

     Th44: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds (((x + y) ` ) + x) = (x + (y ` ))

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      set Z = x;

      (x + ((y + ((((Z + y) ` ) + x) ` )) ` )) = (((Z + y) ` ) + x) by Th38;

      hence thesis by Th28;

    end;

    theorem :: ROBBINS2:45

    

     Th45: for L be satisfying_DN_1 non empty ComplLLattStr, x,y be Element of L holds ((x + ((x + (y ` )) ` )) ` ) = ((x + y) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y be Element of L;

      ((x + ((((x + y) ` ) + x) ` )) ` ) = ((x + y) ` ) by Th8;

      hence thesis by Th44;

    end;

    theorem :: ROBBINS2:46

    

     Th46: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (((((x + y) ` ) + (x + z)) ` ) + y) = y

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      ((((x + y) ` ) + ((((x + y) ` ) + ((x + z) ` )) ` )) ` ) = ((((x + y) ` ) + (x + z)) ` ) by Th45;

      hence thesis by Th40;

    end;

    theorem :: ROBBINS2:47

    

     Th47: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y) = ((((x ` ) + y) ` ) ` )

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      (((((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y) ` ) ` ) = ((((x ` ) + y) ` ) ` ) by Th11;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:48

    

     Th48: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y) = ((x ` ) + y)

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      (((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y) = ((((x ` ) + y) ` ) ` ) by Th47;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:49

    

     Th49: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((x ` ) + (((((y + x) ` ) ` ) + (y + z)) ` )) ` ) + (y + z)) = ((((y + x) ` ) ` ) + (y + z))

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set X = ((y + x) ` ), Y = (y + z), Z = x;

      (((((((X + Y) ` ) + Z) ` ) + (((X ` ) + Y) ` )) ` ) + Y) = ((X ` ) + Y) by Th48;

      hence thesis by Th46;

    end;

    theorem :: ROBBINS2:50

    

     Th50: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((x ` ) + (((y + x) + (y + z)) ` )) ` ) + (y + z)) = ((((y + x) ` ) ` ) + (y + z))

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      ((((x ` ) + (((((y + x) ` ) ` ) + (y + z)) ` )) ` ) + (y + z)) = ((((y + x) ` ) ` ) + (y + z)) by Th49;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:51

    

     Th51: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((((x ` ) + (((y + x) + (y + z)) ` )) ` ) + (y + z)) = ((y + x) + (y + z))

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      ((((x ` ) + (((y + x) + (y + z)) ` )) ` ) + (y + z)) = ((((y + x) ` ) ` ) + (y + z)) by Th50;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:52

    

     Th52: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (((x ` ) ` ) + (y + z)) = ((y + x) + (y + z))

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      ((x ` ) + (((y + x) + (y + z)) ` )) = (x ` ) by Th43;

      hence thesis by Th51;

    end;

    theorem :: ROBBINS2:53

    

     Th53: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((x + y) + (x + z)) = (y + (x + z))

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      set Y = x, X = y;

      (((X ` ) ` ) + (Y + z)) = ((Y + X) + (Y + z)) by Th52;

      hence thesis by Th23;

    end;

    theorem :: ROBBINS2:54

    for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((x + y) + (x + z)) = (z + (x + y)) by Th53;

    theorem :: ROBBINS2:55

    

     Th55: for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (x + (y + z)) = (z + (y + x))

    proof

      let L be satisfying_DN_1 non empty ComplLLattStr;

      let x,y,z be Element of L;

      ((y + x) + (y + z)) = (z + (y + x)) by Th53;

      hence thesis by Th53;

    end;

    theorem :: ROBBINS2:56

    for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds (x + (y + z)) = (y + (z + x)) by Th55;

    theorem :: ROBBINS2:57

    for L be satisfying_DN_1 non empty ComplLLattStr, x,y,z be Element of L holds ((x + y) + z) = (x + (y + z)) by Th55;

    

     Lm2: for L be satisfying_DN_1 non empty ComplLLattStr holds L is join-associative

    proof

      let L;

      for x, y, z holds ((x + y) + z) = (x + (y + z)) by Th55;

      hence thesis by LATTICES:def 5;

    end;

    

     Lm3: L is Robbins

    proof

      for x, y holds ((((x + y) ` ) + ((x + (y ` )) ` )) ` ) = x by Th6;

      hence thesis by ROBBINS1:def 5;

    end;

    registration

      cluster satisfying_DN_1 -> join-associative for non empty ComplLLattStr;

      coherence by Lm2;

      cluster satisfying_DN_1 -> Robbins for non empty ComplLLattStr;

      coherence by Lm3;

    end

    theorem :: ROBBINS2:58

    

     Th58: for L be non empty ComplLLattStr, x,z be Element of L st L is join-commutative join-associative Huntington holds ((z + x) *' (z + (x ` ))) = z

    proof

      let L be non empty ComplLLattStr;

      let x,z be Element of L;

      assume L is join-commutative join-associative Huntington;

      then

      reconsider L9 = L as join-commutative join-associative Huntington non empty ComplLLattStr;

      reconsider z9 = z, x9 = x as Element of L9;

      ((z9 + x9) *' (z9 + (x9 ` ))) = (z9 + (x9 *' (x9 ` ))) by ROBBINS1: 31

      .= (z9 + ( Bot L9)) by ROBBINS1: 15

      .= z9 by ROBBINS1: 13;

      hence thesis;

    end;

    theorem :: ROBBINS2:59

    

     Th59: for L be join-commutative join-associative non empty ComplLLattStr st L is Robbins holds L is satisfying_DN_1

    proof

      let L be join-commutative join-associative non empty ComplLLattStr;

      assume L is Robbins;

      then

      reconsider L9 = L as join-commutative join-associative Robbins non empty ComplLLattStr;

      let x,y,z,u be Element of L;

      

       A1: L9 is Huntington;

      then

       A2: ((z + x) *' (z + (x ` ))) = z by Th58;

      

       A3: ((((x + y) ` ) + z) *' z) = ((z + ((x + y) ` )) *' z)

      .= (z *' (z + ((x + y) ` )))

      .= z by A1, ROBBINS1: 21;

      

       A4: (((((x + y) ` ) + z) *' x) + z) = (z + ((((x + y) ` ) + z) *' x))

      .= ((z + (((x + y) ` ) + z)) *' (z + x)) by A1, ROBBINS1: 31

      .= (((((x + y) ` ) + z) + z) *' (z + x))

      .= ((((x + y) ` ) + (z + z)) *' (z + x)) by LATTICES:def 5

      .= ((((x + y) ` ) + z) *' (z + x)) by A1, ROBBINS1: 12

      .= ((((((x ` ) *' (y ` )) ` ) ` ) + z) *' (z + x)) by A1, ROBBINS1: 17

      .= ((((x ` ) *' (y ` )) + z) *' (z + x)) by A1, ROBBINS1: 3

      .= ((z + ((x ` ) *' (y ` ))) *' (z + x))

      .= (((z + (x ` )) *' (z + (y ` ))) *' (z + x)) by A1, ROBBINS1: 31

      .= ((z + x) *' ((z + (x ` )) *' (z + (y ` ))))

      .= ((z + x) *' (((x ` ) + z) *' (z + (y ` ))))

      .= ((z + x) *' (((x ` ) + z) *' ((y ` ) + z)))

      .= (((z + x) *' ((x ` ) + z)) *' ((y ` ) + z)) by A1, ROBBINS1: 16

      .= (((z + x) *' (z + (x ` ))) *' ((y ` ) + z))

      .= (z *' (z + (y ` ))) by A2

      .= z by A1, ROBBINS1: 21;

      ((((((x + y) ` ) + z) ` ) + ((x + (((z ` ) + ((z + u) ` )) ` )) ` )) ` ) = ((((((((x + y) ` ) + z) ` ) ` ) *' (((x + (((z ` ) + ((z + u) ` )) ` )) ` ) ` )) ` ) ` ) by A1, ROBBINS1: 17

      .= ((((((x + y) ` ) + z) ` ) ` ) *' (((x + (((z ` ) + ((z + u) ` )) ` )) ` ) ` )) by A1, ROBBINS1: 3

      .= ((((((x + y) ` ) + z) ` ) ` ) *' (x + (((z ` ) + ((z + u) ` )) ` ))) by A1, ROBBINS1: 3

      .= ((((x + y) ` ) + z) *' (x + (((z ` ) + ((z + u) ` )) ` ))) by A1, ROBBINS1: 3

      .= ((((((x + y) ` ) ` ) *' (z ` )) ` ) *' (x + (((z ` ) + ((z + u) ` )) ` ))) by A1, ROBBINS1: 17

      .= ((((x + y) *' (z ` )) ` ) *' (x + (((z ` ) + ((z + u) ` )) ` ))) by A1, ROBBINS1: 3

      .= ((((x + y) *' (z ` )) ` ) *' (x + (((((z ` ) ` ) *' (((z + u) ` ) ` )) ` ) ` ))) by A1, ROBBINS1: 17

      .= ((((x + y) *' (z ` )) ` ) *' (x + (((z *' (((z + u) ` ) ` )) ` ) ` ))) by A1, ROBBINS1: 3

      .= ((((x + y) *' (z ` )) ` ) *' (x + (z *' (((z + u) ` ) ` )))) by A1, ROBBINS1: 3

      .= ((((x + y) *' (z ` )) ` ) *' (x + (z *' (z + u)))) by A1, ROBBINS1: 3

      .= ((((x + y) *' (z ` )) ` ) *' (x + z)) by A1, ROBBINS1: 21

      .= (((((x + y) *' (z ` )) ` ) *' x) + ((((x + y) *' (z ` )) ` ) *' z)) by A1, ROBBINS1: 30

      .= (((((((x + y) ` ) ` ) *' (z ` )) ` ) *' x) + ((((x + y) *' (z ` )) ` ) *' z)) by A1, ROBBINS1: 3

      .= (((((x + y) ` ) + z) *' x) + ((((x + y) *' (z ` )) ` ) *' z)) by A1, ROBBINS1: 17

      .= (((((x + y) ` ) + z) *' x) + ((((((x + y) ` ) ` ) *' (z ` )) ` ) *' z)) by A1, ROBBINS1: 3

      .= z by A1, A3, A4, ROBBINS1: 17;

      hence thesis;

    end;

    registration

      cluster join-commutative join-associative Robbins -> satisfying_DN_1 for non empty ComplLLattStr;

      coherence by Th59;

    end

    registration

      cluster satisfying_DN_1 de_Morgan for preOrthoLattice;

      existence

      proof

        take TrivOrtLat ;

        thus thesis;

      end;

    end

    registration

      cluster satisfying_DN_1 de_Morgan -> Boolean for preOrthoLattice;

      coherence ;

      cluster Boolean -> satisfying_DN_1 for well-complemented preOrthoLattice;

      coherence ;

    end

    begin

    definition

      let L be non empty ComplLLattStr;

      :: ROBBINS2:def2

      attr L is satisfying_MD_1 means for x,y be Element of L holds ((((x ` ) + y) ` ) + x) = x;

      :: ROBBINS2:def3

      attr L is satisfying_MD_2 means for x,y,z be Element of L holds ((((x ` ) + y) ` ) + (z + y)) = (y + (z + x));

    end

     Lm4:

    now

      let L be non empty ComplLLattStr;

      assume

       A1: L is satisfying_MD_1 satisfying_MD_2;

      

       A2: for x,y be Element of L holds ((x ` ) + ((x ` ) + y)) = ((x ` ) + y)

      proof

        let x,y be Element of L;

        set X = ((x ` ) + y);

        ((X ` ) + x) = x by A1;

        hence thesis by A1;

      end;

      

       A3: for x,y be Element of L holds ((((x ` ) + y) ` ) + y) = (y + x)

      proof

        let x,y be Element of L;

        set X = ((x ` ) + y);

        

         A4: ((X ` ) + ((X ` ) + y)) = (y + ((X ` ) + x)) by A1;

        ((((x ` ) + y) ` ) + y) = ((X ` ) + ((X ` ) + y)) by A2

        .= (y + x) by A1, A4;

        hence thesis;

      end;

      

       A5: for x be Element of L holds (x + x) = x

      proof

        let x be Element of L;

        (x + x) = ((((x ` ) + x) ` ) + x) by A3

        .= x by A1;

        hence thesis;

      end;

      

       A6: for x,y be Element of L holds (x + (x + y)) = (x + y)

      proof

        let x,y be Element of L;

        (x + (x + y)) = ((((y ` ) + x) ` ) + (x + x)) by A1

        .= ((((y ` ) + x) ` ) + x) by A5

        .= (x + y) by A3;

        hence thesis;

      end;

      

       A7: for x,y be Element of L holds ((x + y) + y) = (x + y)

      proof

        let x,y be Element of L;

        set Y = (x + y);

        ((x + y) + y) = ((((y ` ) + (x + y)) ` ) + (x + y)) by A3

        .= ((((y ` ) + (x + y)) ` ) + (x + (x + y))) by A6

        .= (Y + (x + y)) by A1

        .= (x + y) by A5;

        hence thesis;

      end;

      

       A8: for x,y be Element of L holds ((x + y) + x) = (x + y)

      proof

        let x,y be Element of L;

        ((x + y) + x) = (((((y ` ) + x) ` ) + x) + x) by A3

        .= ((((y ` ) + x) ` ) + x) by A7

        .= (x + y) by A3;

        hence thesis;

      end;

      

       A9: for x,y be Element of L holds (x + (y + (y + x))) = (y + x)

      proof

        let x,y be Element of L;

        set Z = (y + x);

        (x + (y + (y + x))) = ((((Z ` ) + x) ` ) + (y + x)) by A1

        .= (y + x) by A1;

        hence thesis;

      end;

      

       A10: for x,y be Element of L holds (x + (y + x)) = (y + x)

      proof

        let x,y be Element of L;

        (x + (y + x)) = (x + (y + (y + x))) by A6

        .= (y + x) by A9;

        hence thesis;

      end;

      

       A11: for x,y be Element of L holds (((x + (y ` )) ` ) + y) = y

      proof

        let x,y be Element of L;

        (((x + (y ` )) ` ) + y) = ((((y ` ) + (x + (y ` ))) ` ) + y) by A10

        .= y by A1;

        hence thesis;

      end;

      

       A12: for x be Element of L holds (((x ` ) ` ) + x) = x

      proof

        let x be Element of L;

        ((((x ` ) + (x ` )) ` ) + x) = x by A1;

        hence thesis by A5;

      end;

      

       A13: for x be Element of L holds (x + ((x ` ) ` )) = x

      proof

        let x be Element of L;

        (x + ((x ` ) ` )) = ((((x ` ) ` ) + x) + ((x ` ) ` )) by A12

        .= (((x ` ) ` ) + x) by A8

        .= x by A12;

        hence thesis;

      end;

      

       A14: for x,y be Element of L holds (x + (((x ` ) ` ) + y)) = (x + y)

      proof

        let x,y be Element of L;

        (x + (((x ` ) ` ) + y)) = ((((y ` ) + x) ` ) + (((x ` ) ` ) + x)) by A1

        .= ((((y ` ) + x) ` ) + x) by A12

        .= (x + y) by A3;

        hence thesis;

      end;

      

       A15: for x be Element of L holds (x + ((((x ` ) ` ) ` ) ` )) = x

      proof

        let x be Element of L;

        (x + ((((x ` ) ` ) ` ) ` )) = (x + (((x ` ) ` ) + ((((x ` ) ` ) ` ) ` ))) by A14

        .= (x + ((x ` ) ` )) by A13

        .= x by A13;

        hence thesis;

      end;

      

       A16: for x be Element of L holds (((x ` ) ` ) ` ) = (x ` )

      proof

        let x be Element of L;

        (((x ` ) ` ) ` ) = (((x + ((((x ` ) ` ) ` ) ` )) ` ) + (((x ` ) ` ) ` )) by A11

        .= ((x ` ) + (((x ` ) ` ) ` )) by A15

        .= (x ` ) by A13;

        hence thesis;

      end;

      

       A17: for x,y,z be Element of L holds ((((x ` ) + y) ` ) + ((((x ` ) + z) ` ) + y)) = (y + x)

      proof

        let x,y,z be Element of L;

        ((((x ` ) + y) ` ) + ((((x ` ) + z) ` ) + y)) = (y + ((((x ` ) + z) ` ) + x)) by A1

        .= (y + x) by A1;

        hence thesis;

      end;

      

       A18: for x,y be Element of L holds (x + ((y ` ) ` )) = (x + y)

      proof

        let x,y be Element of L;

        (x + y) = ((((y ` ) + x) ` ) + ((((y ` ) + x) ` ) + x)) by A17

        .= ((((y ` ) + x) ` ) + ((((((y ` ) ` ) ` ) + x) ` ) + x)) by A16

        .= ((((((y ` ) ` ) ` ) + x) ` ) + ((((((y ` ) ` ) ` ) + x) ` ) + x)) by A16

        .= (x + ((y ` ) ` )) by A17;

        hence thesis;

      end;

      

       A19: for x be Element of L holds ((x ` ) ` ) = x

      proof

        let x be Element of L;

        ((x ` ) ` ) = ((((((x ` ) ` ) ` ) + ((x ` ) ` )) ` ) + ((x ` ) ` )) by A1

        .= ((((x ` ) + ((x ` ) ` )) ` ) + ((x ` ) ` )) by A16

        .= ((((x ` ) + ((x ` ) ` )) ` ) + x) by A18

        .= x by A1;

        hence thesis;

      end;

      

       A20: for x,y,z be Element of L holds ((((x ` ) + ((((y + x) ` ) + z) ` )) ` ) + (y + ((((y + x) ` ) + z) ` ))) = (y + x)

      proof

        let x,y,z be Element of L;

        set P = ((((y + x) ` ) + z) ` );

        ((((x ` ) + P) ` ) + (y + P)) = (P + (y + x)) by A1

        .= (y + x) by A1;

        hence thesis;

      end;

      

       A21: for x,y be Element of L holds ((((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` ))) = ((y ` ) + x)

      proof

        let x,y be Element of L;

        ((((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` ))) = ((((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + (((((y ` ) + x) ` ) + x) ` ))) by A3

        .= ((((x ` ) + (((((y ` ) + x) ` ) + x) ` )) ` ) + ((y ` ) + (((((y ` ) + x) ` ) + x) ` ))) by A3

        .= ((y ` ) + x) by A20;

        hence thesis;

      end;

      

       A22: for x,y be Element of L holds (x + (((x ` ) + y) ` )) = x

      proof

        let x,y be Element of L;

        (x + (((x ` ) + y) ` )) = (((((x ` ) + y) ` ) + x) + (((x ` ) + y) ` )) by A1

        .= ((((x ` ) + y) ` ) + x) by A8

        .= x by A1;

        hence thesis;

      end;

      

       A23: for x,y be Element of L holds ((x ` ) + ((x + y) ` )) = (x ` )

      proof

        let x,y be Element of L;

        (x ` ) = ((x ` ) + ((((x ` ) ` ) + y) ` )) by A22

        .= ((x ` ) + ((x + y) ` )) by A19;

        hence thesis;

      end;

      

       A24: for x,y be Element of L holds (x + ((y + (x ` )) ` )) = x

      proof

        let x,y be Element of L;

        (x + ((y + (x ` )) ` )) = ((((y + (x ` )) ` ) + x) + ((y + (x ` )) ` )) by A11

        .= (((y + (x ` )) ` ) + x) by A8

        .= x by A11;

        hence thesis;

      end;

      

       A25: for x,y be Element of L holds ((x ` ) + ((y + x) ` )) = (x ` )

      proof

        let x,y be Element of L;

        (x ` ) = ((x ` ) + ((y + ((x ` ) ` )) ` )) by A24

        .= ((x ` ) + ((y + x) ` )) by A19;

        hence thesis;

      end;

      

       A26: for x,y be Element of L holds (x + (y ` )) = ((y ` ) + x)

      proof

        let x,y be Element of L;

        ((y ` ) + x) = ((((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` ))) by A21

        .= (((x ` ) ` ) + ((y ` ) + ((x + y) ` ))) by A23

        .= (((x ` ) ` ) + (y ` )) by A25

        .= (x + (y ` )) by A19;

        hence thesis;

      end;

      

       A27: for x,y be Element of L holds (x + y) = (y + x)

      proof

        let x,y be Element of L;

        ((y ` ) ` ) = y by A19;

        hence thesis by A26;

      end;

      hence L is join-commutative by LATTICES:def 4;

      

       A28: for x,y,z be Element of L holds ((((((x ` ) + y) ` ) + z) ` ) + ((x ` ) + z)) = (z + ((x ` ) + y))

      proof

        let x,y,z be Element of L;

        ((((((x ` ) + y) ` ) + z) ` ) + ((x ` ) + z)) = (z + ((x ` ) + ((x ` ) + y))) by A1

        .= (z + ((x ` ) + y)) by A2;

        hence thesis;

      end;

      

       A29: for x,y be Element of L holds (x + ((y ` ) + x)) = ((y ` ) + x)

      proof

        let x,y be Element of L;

        (x + ((y ` ) + x)) = ((((((y ` ) + x) ` ) + x) ` ) + ((y ` ) + x)) by A28

        .= ((y ` ) + x) by A1;

        hence thesis;

      end;

      

       A30: for x,y be Element of L holds (((x + y) ` ) + x) = ((y ` ) + x)

      proof

        let x,y be Element of L;

        set Y = ((y ` ) + x);

        ((y ` ) + x) = (x + ((y ` ) + x)) by A29

        .= ((((Y ` ) + x) ` ) + x) by A3

        .= (((x + y) ` ) + x) by A3;

        hence thesis;

      end;

      

       A31: for x,y be Element of L holds (((x + y) ` ) + (((y ` ) + x) ` )) = ((x ` ) + (((y ` ) + x) ` ))

      proof

        let x,y be Element of L;

        (((x + y) ` ) + (((y ` ) + x) ` )) = ((((((y ` ) + x) ` ) + x) ` ) + (((y ` ) + x) ` )) by A3

        .= ((x ` ) + (((y ` ) + x) ` )) by A30;

        hence thesis;

      end;

      for x,y be Element of L holds ((((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` )) = x

      proof

        let x,y be Element of L;

        ((((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` )) = ((((y ` ) + (x ` )) ` ) + (((x ` ) + y) ` )) by A27

        .= ((((x ` ) + y) ` ) + (((y ` ) + (x ` )) ` )) by A27

        .= (((x ` ) ` ) + (((y ` ) + (x ` )) ` )) by A31

        .= (x + (((y ` ) + (x ` )) ` )) by A19

        .= x by A24;

        hence thesis;

      end;

      hence L is Huntington by ROBBINS1:def 6;

      

       A32: for x,y,z be Element of L holds ((x + y) + (y + z)) = ((x + y) + z)

      proof

        let x,y,z be Element of L;

        set Y = (x + y);

        ((x + y) + z) = ((((z ` ) + Y) ` ) + Y) by A3

        .= ((((z ` ) + Y) ` ) + (y + Y)) by A10

        .= (Y + (y + z)) by A1;

        hence thesis;

      end;

      for x,y,z be Element of L holds ((x + y) + z) = (x + (y + z))

      proof

        let x,y,z be Element of L;

        for x,y,z be Element of L holds ((x + y) + (z + x)) = (y + (x + z))

        proof

          let x,y,z be Element of L;

          ((x + y) + (z + x)) = ((z + x) + (x + y)) by A27

          .= ((z + x) + y) by A32

          .= ((x + z) + y) by A27

          .= (y + (x + z)) by A27;

          hence thesis;

        end;

        then ((y + x) + (z + y)) = (x + (y + z));

        then

         A33: ((x + y) + (z + y)) = (x + (y + z)) by A27;

        ((x + y) + z) = ((x + y) + (y + z)) by A32

        .= (x + (y + z)) by A27, A33;

        hence thesis;

      end;

      hence L is join-associative by LATTICES:def 5;

    end;

    registration

      cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative Huntington for non empty ComplLLattStr;

      coherence by Lm4;

      cluster join-commutative join-associative Huntington -> satisfying_MD_1 satisfying_MD_2 for non empty ComplLLattStr;

      coherence

      proof

        let L be non empty ComplLLattStr;

        assume L is join-commutative join-associative Huntington;

        then

        reconsider L9 = L as join-commutative join-associative Huntington non empty ComplLLattStr;

        

         A1: L9 is satisfying_MD_2

        proof

          let x,y,z be Element of L9;

          set Z = (z + y);

          

           A2: (Z + (y ` )) = (z + (y + (y ` ))) by LATTICES:def 5

          .= (z + ( Top L9)) by ROBBINS1:def 8

          .= ( Top L9) by ROBBINS1: 19;

          ((((x ` ) + y) ` ) + (z + y)) = ((((x ` ) + ((y ` ) ` )) ` ) + (z + y)) by ROBBINS1: 3

          .= ((x *' (y ` )) + (z + y)) by ROBBINS1:def 4

          .= ((Z + x) *' (Z + (y ` ))) by ROBBINS1: 31

          .= (Z + x) by A2, ROBBINS1: 14

          .= (y + (z + x)) by LATTICES:def 5;

          hence thesis;

        end;

        L9 is satisfying_MD_1

        proof

          let x,y be Element of L9;

          ((((x ` ) + y) ` ) + x) = ((((x ` ) + ((y ` ) ` )) ` ) + x) by ROBBINS1: 3

          .= ((x *' (y ` )) + x) by ROBBINS1:def 4

          .= x by ROBBINS1: 20;

          hence thesis;

        end;

        hence thesis by A1;

      end;

    end

    registration

      cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan for preOrthoLattice;

      existence

      proof

        take TrivOrtLat ;

        thus thesis;

      end;

    end

    registration

      cluster satisfying_MD_1 satisfying_MD_2 de_Morgan -> Boolean for preOrthoLattice;

      coherence ;

      cluster Boolean -> satisfying_MD_1 satisfying_MD_2 for well-complemented preOrthoLattice;

      coherence ;

    end