:: ROBBINS2 semantic presentation

begin

definition
let L be non empty ComplLLattStr ;
attrL is satisfying_DN_1  means :Def1: :: ROBBINS2:def 1
 for x, y, z, u being Element of L holds (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z;
end;

:: deftheorem Def1 defines satisfying_DN_1 ROBBINS2:def_1_:_
 for L being non empty ComplLLattStr holds
( L is satisfying_DN_1 iff for x, y, z, u being Element of L holds (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z );

registration
cluster TrivComplLat  ->  satisfying_DN_1 ;
coherence
 TrivComplLat is satisfying_DN_1
proof
let x, y, z, u be Element of TrivComplLat; :: according to ROBBINS2:def_1 ::_thesis: (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z
thus  (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z by STRUCT_0:def_10; ::_thesis: verum
end;
cluster TrivOrtLat  ->  satisfying_DN_1 ;
coherence
 TrivOrtLat is satisfying_DN_1
proof
let x, y, z, u be Element of TrivOrtLat; :: according to ROBBINS2:def_1 ::_thesis: (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z
thus  (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster non empty join-commutative join-associative satisfying_DN_1 for ComplLLattStr ;
existence
 ex b1 being non empty ComplLLattStr st
( b1 is join-commutative & b1 is join-associative & b1 is satisfying_DN_1 )
proof
take  TrivComplLat ; ::_thesis: ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is satisfying_DN_1 )
thus  ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is satisfying_DN_1 ) ; ::_thesis: verum
end;
end;


theorem Th1: :: ROBBINS2:1
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z, u, v being Element of L holds (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u, v being Element of L holds (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y
let x, y, z, u, v be Element of L; ::_thesis: (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y
set X = (((z + u) `) + x) ` ;
set Y = (z + (((x `) + ((x + u) `)) `)) ` ;
set Z = y;
set U = v;
 (((((((((z + u) `) + x) `) + ((z + (((x `) + ((x + u) `)) `)) `)) `) + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y by Def1;
hence  (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y by Def1; ::_thesis: verum
end;

theorem Th2: :: ROBBINS2:2
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + (((y `) + ((y + u) `)) `)) `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + (((y `) + ((y + u) `)) `)) `)) ` = y
let x, y, z, u be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + (((y `) + ((y + u) `)) `)) `)) ` = y
set v = the Element of L;
 (((x + z) `) + ((((((y + u) `) + x) `) + (((z `) + ((z + the Element of L) `)) `)) `)) ` = z by Th1;
hence  (((x + y) `) + ((((z + x) `) + (((y `) + ((y + u) `)) `)) `)) ` = y by Th1; ::_thesis: verum
end;

theorem Th3: :: ROBBINS2:3
for L being non empty satisfying_DN_1 ComplLLattStr
for x being Element of L holds (((x + (x `)) `) + x) ` = x `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x being Element of L holds (((x + (x `)) `) + x) ` = x `
let x be Element of L; ::_thesis: (((x + (x `)) `) + x) ` = x `
set y = the Element of L;
set V = (x + the Element of L) ` ;
 (((x + (x `)) `) + ((((((((x `) `) + the Element of L) `) + x) `) + ((((x `) `) + (((x `) + ((x + the Element of L) `)) `)) `)) `)) ` = x ` by Th1;
hence  (((x + (x `)) `) + x) ` = x ` by Def1; ::_thesis: verum
end;

theorem Th4: :: ROBBINS2:4
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + u) `)) `)) `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + u) `)) `)) `)) ` = y
let x, y, z, u be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + u) `)) `)) `)) ` = y
 (((y + (y `)) `) + y) ` = y ` by Th3;
hence  (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + u) `)) `)) `)) ` = y by Th2; ::_thesis: verum
end;

theorem Th5: :: ROBBINS2:5
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((x + y) `) + ((((z + x) `) + y) `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x + y) `) + ((((z + x) `) + y) `)) ` = y
let x, y, z be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + y) `)) ` = y
set u = the Element of L;
set U = ((y `) + ((y + the Element of L) `)) ` ;
 (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + (((y `) + ((y + the Element of L) `)) `)) `)) `)) `)) ` = y by Th4;
hence  (((x + y) `) + ((((z + x) `) + y) `)) ` = y by Def1; ::_thesis: verum
end;

theorem Th6: :: ROBBINS2:6
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (((x + y) `) + (((x `) + y) `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((x + y) `) + (((x `) + y) `)) ` = y
let x, y be Element of L; ::_thesis: (((x + y) `) + (((x `) + y) `)) ` = y
set Z = (x + (x `)) ` ;
 (((x + y) `) + ((((((x + (x `)) `) + x) `) + y) `)) ` = y by Th5;
hence  (((x + y) `) + (((x `) + y) `)) ` = y by Th3; ::_thesis: verum
end;

theorem Th7: :: ROBBINS2:7
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (((((x + y) `) + x) `) + ((x + y) `)) ` = x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((((x + y) `) + x) `) + ((x + y) `)) ` = x
let x, y be Element of L; ::_thesis: (((((x + y) `) + x) `) + ((x + y) `)) ` = x
set X = (x + y) ` ;
 (((((x + y) `) + x) `) + ((((x + ((x + y) `)) `) + ((((((x + (x `)) `) + x) `) + ((x + y) `)) `)) `)) ` = x by Th4;
hence  (((((x + y) `) + x) `) + ((x + y) `)) ` = x by Th5; ::_thesis: verum
end;

theorem Th8: :: ROBBINS2:8
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (x + ((((x + y) `) + x) `)) ` = (x + y) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + ((((x + y) `) + x) `)) ` = (x + y) `
let x, y be Element of L; ::_thesis: (x + ((((x + y) `) + x) `)) ` = (x + y) `
set X = (x + y) ` ;
set Y = x;
 (((((((x + y) `) + x) `) + ((x + y) `)) `) + ((((x + y) `) + x) `)) ` = (x + y) ` by Th7;
hence  (x + ((((x + y) `) + x) `)) ` = (x + y) ` by Th7; ::_thesis: verum
end;

theorem Th9: :: ROBBINS2:9
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((((x + y) `) + z) `) + ((x + z) `)) ` = z
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((x + y) `) + z) `) + ((x + z) `)) ` = z
let x, y, z be Element of L; ::_thesis: (((((x + y) `) + z) `) + ((x + z) `)) ` = z
set X = (x + y) ` ;
set Y = z;
set Z = (((x + y) `) + x) ` ;
 (((((x + y) `) + z) `) + ((((((((x + y) `) + x) `) + ((x + y) `)) `) + z) `)) ` = z by Th5;
hence  (((((x + y) `) + z) `) + ((x + z) `)) ` = z by Th7; ::_thesis: verum
end;

theorem Th10: :: ROBBINS2:10
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (x + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) `
let x, y, z be Element of L; ::_thesis: (x + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) `
set Z = (y + x) ` ;
set X = (y + z) ` ;
set Y = x;
 (((((((y + z) `) + x) `) + ((y + x) `)) `) + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) ` by Th9;
hence  (x + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) ` by Th9; ::_thesis: verum
end;

theorem Th11: :: ROBBINS2:11
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) ` = ((x `) + y) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) ` = ((x `) + y) `
let x, y, z be Element of L; ::_thesis: (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) ` = ((x `) + y) `
set X = (x + y) ` ;
set Z = ((x `) + y) ` ;
set Y = z;
 (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + ((((x + y) `) + (((x `) + y) `)) `)) ` = ((x `) + y) ` by Th9;
hence  (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) ` = ((x `) + y) ` by Th6; ::_thesis: verum
end;

theorem Th12: :: ROBBINS2:12
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (x + ((((y + z) `) + ((z + x) `)) `)) ` = (z + x) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x + ((((y + z) `) + ((z + x) `)) `)) ` = (z + x) `
let x, y, z be Element of L; ::_thesis: (x + ((((y + z) `) + ((z + x) `)) `)) ` = (z + x) `
set Y = z;
set Z = (((y + x) `) + ((y + z) `)) ` ;
 (x + ((((z + ((((y + x) `) + ((y + z) `)) `)) `) + ((z + x) `)) `)) ` = (z + x) ` by Th10;
hence  (x + ((((y + z) `) + ((z + x) `)) `)) ` = (z + x) ` by Th10; ::_thesis: verum
end;

theorem Th13: :: ROBBINS2:13
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + (((y `) + ((u + y) `)) `)) `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + (((y `) + ((u + y) `)) `)) `)) ` = y
let x, y, z, u be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + (((y `) + ((u + y) `)) `)) `)) ` = y
set U = (((u + z) `) + ((u + y) `)) ` ;
 (((x + y) `) + ((((z + x) `) + (((y `) + ((y + ((((u + z) `) + ((u + y) `)) `)) `)) `)) `)) ` = y by Th2;
hence  (((x + y) `) + ((((z + x) `) + (((y `) + ((u + y) `)) `)) `)) ` = y by Th10; ::_thesis: verum
end;

theorem Th14: :: ROBBINS2:14
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (x + y) ` = (y + x) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + y) ` = (y + x) `
let x, y be Element of L; ::_thesis: (x + y) ` = (y + x) `
set Z = y;
set X = x;
set Y = (y + x) ` ;
 (((((y + x) `) + y) `) + ((y + x) `)) ` = y by Th7;
hence  (x + y) ` = (y + x) ` by Th12; ::_thesis: verum
end;

theorem Th15: :: ROBBINS2:15
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((((x + y) `) + ((y + z) `)) `) + z) ` = (y + z) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((x + y) `) + ((y + z) `)) `) + z) ` = (y + z) `
let x, y, z be Element of L; ::_thesis: (((((x + y) `) + ((y + z) `)) `) + z) ` = (y + z) `
set Y = (((x + y) `) + ((y + z) `)) ` ;
 (z + ((((x + y) `) + ((y + z) `)) `)) ` = (((((x + y) `) + ((y + z) `)) `) + z) ` by Th14;
hence  (((((x + y) `) + ((y + z) `)) `) + z) ` = (y + z) ` by Th12; ::_thesis: verum
end;

theorem Th16: :: ROBBINS2:16
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((x + ((((x + y) `) + z) `)) `) + z) ` = (((x + y) `) + z) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x + ((((x + y) `) + z) `)) `) + z) ` = (((x + y) `) + z) `
let x, y, z be Element of L; ::_thesis: (((x + ((((x + y) `) + z) `)) `) + z) ` = (((x + y) `) + z) `
set X = (((x + y) `) + x) ` ;
set Y = (x + y) ` ;
 (((((x + y) `) + x) `) + ((x + y) `)) ` = x by Th7;
hence  (((x + ((((x + y) `) + z) `)) `) + z) ` = (((x + y) `) + z) ` by Th15; ::_thesis: verum
end;

theorem Th17: :: ROBBINS2:17
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (((((x + y) `) + x) `) + y) ` = (y + y) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((((x + y) `) + x) `) + y) ` = (y + y) `
let x, y be Element of L; ::_thesis: (((((x + y) `) + x) `) + y) ` = (y + y) `
set X = (x + y) ` ;
 (((x + y) `) + ((((((x + y) `) + x) `) + y) `)) ` = y by Th5;
hence  (((((x + y) `) + x) `) + y) ` = (y + y) ` by Th16; ::_thesis: verum
end;

theorem Th18: :: ROBBINS2:18
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((x `) + ((y + x) `)) ` = x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x `) + ((y + x) `)) ` = x
let x, y be Element of L; ::_thesis: ((x `) + ((y + x) `)) ` = x
set X = (y + x) ` ;
 (((y + x) `) + (((((x `) + y) `) + (((x `) + ((y + x) `)) `)) `)) ` = x by Th13;
hence  ((x `) + ((y + x) `)) ` = x by Th10; ::_thesis: verum
end;

theorem Th19: :: ROBBINS2:19
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (((x + y) `) + (y `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((x + y) `) + (y `)) ` = y
let x, y be Element of L; ::_thesis: (((x + y) `) + (y `)) ` = y
 ((y `) + ((x + y) `)) ` = y by Th18;
hence  (((x + y) `) + (y `)) ` = y by Th14; ::_thesis: verum
end;

theorem Th20: :: ROBBINS2:20
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (x + ((y + (x `)) `)) ` = x `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + ((y + (x `)) `)) ` = x `
let x, y be Element of L; ::_thesis: (x + ((y + (x `)) `)) ` = x `
set Z = x ` ;
set X = y;
set Y = x;
 (((((y + x) `) + (x `)) `) + ((y + (x `)) `)) ` = x ` by Th9;
hence  (x + ((y + (x `)) `)) ` = x ` by Th19; ::_thesis: verum
end;

theorem Th21: :: ROBBINS2:21
for L being non empty satisfying_DN_1 ComplLLattStr
for x being Element of L holds (x + x) ` = x `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x being Element of L holds (x + x) ` = x `
let x be Element of L; ::_thesis: (x + x) ` = x `
set y = the Element of L;
set Y = ( the Element of L + x) ` ;
 (x + (((( the Element of L + x) `) + (x `)) `)) ` = x ` by Th20;
hence  (x + x) ` = x ` by Th19; ::_thesis: verum
end;

theorem Th22: :: ROBBINS2:22
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (((((x + y) `) + x) `) + y) ` = y `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((((x + y) `) + x) `) + y) ` = y `
let x, y be Element of L; ::_thesis: (((((x + y) `) + x) `) + y) ` = y `
y ` = (y + y) ` by Th21
.= (((((x + y) `) + x) `) + y) ` by Th17 ;
hence  (((((x + y) `) + x) `) + y) ` = y ` ; ::_thesis: verum
end;

theorem Th23: :: ROBBINS2:23
for L being non empty satisfying_DN_1 ComplLLattStr
for x being Element of L holds (x `) ` = x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x being Element of L holds (x `) ` = x
let x be Element of L; ::_thesis: (x `) ` = x
(x `) ` = (((((x + (x `)) `) + x) `) + (x `)) ` by Th22
.= x by Th19 ;
hence  (x `) ` = x ; ::_thesis: verum
end;

theorem Th24: :: ROBBINS2:24
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((((x + y) `) + x) `) + y = (y `) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((((x + y) `) + x) `) + y = (y `) `
let x, y be Element of L; ::_thesis: ((((x + y) `) + x) `) + y = (y `) `
 ((((((x + y) `) + x) `) + y) `) ` = (y `) ` by Th22;
hence  ((((x + y) `) + x) `) + y = (y `) ` by Th23; ::_thesis: verum
end;

theorem Th25: :: ROBBINS2:25
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((x + y) `) ` = y + x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + y) `) ` = y + x
let x, y be Element of L; ::_thesis: ((x + y) `) ` = y + x
((x + y) `) ` = ((y + x) `) ` by Th14
.= y + x by Th23 ;
hence  ((x + y) `) ` = y + x ; ::_thesis: verum
end;

theorem Th26: :: ROBBINS2:26
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) `
let x, y, z be Element of L; ::_thesis: x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) `
 ((x + ((((y + z) `) + ((y + x) `)) `)) `) ` = ((y + x) `) ` by Th10;
hence  x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) ` by Th23; ::_thesis: verum
end;

theorem Th27: :: ROBBINS2:27
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds x + y = y + x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds x + y = y + x
let x, y be Element of L; ::_thesis: x + y = y + x
x + y = ((x + y) `) ` by Th23
.= y + x by Th25 ;
hence  x + y = y + x ; ::_thesis: verum
end;

Lm1:  for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-commutative
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: L is join-commutative
 for x, y being Element of L holds x + y = y + x by Th27;
hence  L is join-commutative by LATTICES:def_4; ::_thesis: verum
end;

registration
cluster non empty satisfying_DN_1  ->  non empty join-commutative for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is satisfying_DN_1 holds
b1 is join-commutative by Lm1;
end;

theorem Th28: :: ROBBINS2:28
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((((x + y) `) + x) `) + y = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((((x + y) `) + x) `) + y = y
let x, y be Element of L; ::_thesis: ((((x + y) `) + x) `) + y = y
 ((((x + y) `) + x) `) + y = (y `) ` by Th24;
hence  ((((x + y) `) + x) `) + y = y by Th23; ::_thesis: verum
end;

theorem :: ROBBINS2:29
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((((x + y) `) + y) `) + x = x by Th28;

theorem :: ROBBINS2:30
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds x + ((((y + x) `) + y) `) = x by Th28;

theorem Th31: :: ROBBINS2:31
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((x + (y `)) `) + (((y `) + y) `) = (x + (y `)) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + (y `)) `) + (((y `) + y) `) = (x + (y `)) `
let x, y be Element of L; ::_thesis: ((x + (y `)) `) + (((y `) + y) `) = (x + (y `)) `
set X = (x + (y `)) ` ;
 ((x + (y `)) `) + ((((y + ((x + (y `)) `)) `) + y) `) = (x + (y `)) ` by Th28;
hence  ((x + (y `)) `) + (((y `) + y) `) = (x + (y `)) ` by Th20; ::_thesis: verum
end;

theorem Th32: :: ROBBINS2:32
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((x + y) `) + ((y + (y `)) `) = (x + y) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + y) `) + ((y + (y `)) `) = (x + y) `
let x, y be Element of L; ::_thesis: ((x + y) `) + ((y + (y `)) `) = (x + y) `
set X = (x + y) ` ;
set Y = y ` ;
 ((x + y) `) + (((((y `) + ((x + y) `)) `) + (y `)) `) = (x + y) ` by Th28;
hence  ((x + y) `) + ((y + (y `)) `) = (x + y) ` by Th18; ::_thesis: verum
end;

theorem :: ROBBINS2:33
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((x + y) `) + (((y `) + y) `) = (x + y) ` by Th32;

theorem Th34: :: ROBBINS2:34
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((((x + (y `)) `) `) + y) ` = ((y `) + y) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((((x + (y `)) `) `) + y) ` = ((y `) + y) `
let x, y be Element of L; ::_thesis: ((((x + (y `)) `) `) + y) ` = ((y `) + y) `
set Y = y ` ;
set Z = y;
 (((((x + (y `)) `) + (((y `) + y) `)) `) + y) ` = ((y `) + y) ` by Th15;
hence  ((((x + (y `)) `) `) + y) ` = ((y `) + y) ` by Th31; ::_thesis: verum
end;

theorem Th35: :: ROBBINS2:35
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((x + (y `)) + y) ` = ((y `) + y) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + (y `)) + y) ` = ((y `) + y) `
let x, y be Element of L; ::_thesis: ((x + (y `)) + y) ` = ((y `) + y) `
 ((((x + (y `)) `) `) + y) ` = ((y `) + y) ` by Th34;
hence  ((x + (y `)) + y) ` = ((y `) + y) ` by Th23; ::_thesis: verum
end;

theorem Th36: :: ROBBINS2:36
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds ((((((x + (y `)) + z) `) + y) `) + (((y `) + y) `)) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((((x + (y `)) + z) `) + y) `) + (((y `) + y) `)) ` = y
let x, y, z be Element of L; ::_thesis: ((((((x + (y `)) + z) `) + y) `) + (((y `) + y) `)) ` = y
 ((x + (y `)) + y) ` = ((y `) + y) ` by Th35;
hence  ((((((x + (y `)) + z) `) + y) `) + (((y `) + y) `)) ` = y by Th9; ::_thesis: verum
end;

theorem Th37: :: ROBBINS2:37
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds x + ((((y + z) `) + ((y + x) `)) `) = y + x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + ((((y + z) `) + ((y + x) `)) `) = y + x
let x, y, z be Element of L; ::_thesis: x + ((((y + z) `) + ((y + x) `)) `) = y + x
 x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) ` by Th26;
hence  x + ((((y + z) `) + ((y + x) `)) `) = y + x by Th23; ::_thesis: verum
end;

theorem Th38: :: ROBBINS2:38
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x
let x, y, z be Element of L; ::_thesis: x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x
set Y = (z + y) ` ;
set Z = y ` ;
 x + ((((((z + y) `) + (y `)) `) + ((((z + y) `) + x) `)) `) = ((z + y) `) + x by Th37;
hence  x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x by Th19; ::_thesis: verum
end;

theorem :: ROBBINS2:39
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds x + ((((y + x) `) + ((y + z) `)) `) = y + x by Th37;

theorem Th40: :: ROBBINS2:40
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds ((((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y
let x, y, z be Element of L; ::_thesis: ((((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y
set Y = (((x + y) `) + ((x + z) `)) ` ;
 ((((y + ((((x + y) `) + ((x + z) `)) `)) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y by Th28;
hence  ((((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y by Th37; ::_thesis: verum
end;

theorem Th41: :: ROBBINS2:41
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((((x + (y `)) + z) `) + y) `) ` = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((x + (y `)) + z) `) + y) `) ` = y
let x, y, z be Element of L; ::_thesis: (((((x + (y `)) + z) `) + y) `) ` = y
 (((((x + (y `)) + z) `) + y) `) + (((y `) + y) `) = ((((x + (y `)) + z) `) + y) ` by Th32;
hence  (((((x + (y `)) + z) `) + y) `) ` = y by Th36; ::_thesis: verum
end;

theorem Th42: :: ROBBINS2:42
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds x + (((y + (x `)) + z) `) = x
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + (((y + (x `)) + z) `) = x
let x, y, z be Element of L; ::_thesis: x + (((y + (x `)) + z) `) = x
 (((((y + (x `)) + z) `) + x) `) ` = x by Th41;
hence  x + (((y + (x `)) + z) `) = x by Th25; ::_thesis: verum
end;

theorem Th43: :: ROBBINS2:43
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (x `) + (((y + x) + z) `) = x `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x `) + (((y + x) + z) `) = x `
let x, y, z be Element of L; ::_thesis: (x `) + (((y + x) + z) `) = x `
set X = x ` ;
 (x `) + (((y + ((x `) `)) + z) `) = x ` by Th42;
hence  (x `) + (((y + x) + z) `) = x ` by Th23; ::_thesis: verum
end;

theorem Th44: :: ROBBINS2:44
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds ((x + y) `) + x = x + (y `)
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + y) `) + x = x + (y `)
let x, y be Element of L; ::_thesis: ((x + y) `) + x = x + (y `)
set Z = x;
 x + ((y + ((((x + y) `) + x) `)) `) = ((x + y) `) + x by Th38;
hence  ((x + y) `) + x = x + (y `) by Th28; ::_thesis: verum
end;

theorem Th45: :: ROBBINS2:45
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y being Element of L holds (x + ((x + (y `)) `)) ` = (x + y) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + ((x + (y `)) `)) ` = (x + y) `
let x, y be Element of L; ::_thesis: (x + ((x + (y `)) `)) ` = (x + y) `
 (x + ((((x + y) `) + x) `)) ` = (x + y) ` by Th8;
hence  (x + ((x + (y `)) `)) ` = (x + y) ` by Th44; ::_thesis: verum
end;

theorem Th46: :: ROBBINS2:46
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds ((((x + y) `) + (x + z)) `) + y = y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((x + y) `) + (x + z)) `) + y = y
let x, y, z be Element of L; ::_thesis: ((((x + y) `) + (x + z)) `) + y = y
 (((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) ` = (((x + y) `) + (x + z)) ` by Th45;
hence  ((((x + y) `) + (x + z)) `) + y = y by Th40; ::_thesis: verum
end;

theorem Th47: :: ROBBINS2:47
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) `
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) `
let x, y, z be Element of L; ::_thesis: ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) `
 ((((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) `) ` = (((x `) + y) `) ` by Th11;
hence  ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) ` by Th23; ::_thesis: verum
end;

theorem Th48: :: ROBBINS2:48
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (x `) + y
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (x `) + y
let x, y, z be Element of L; ::_thesis: ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (x `) + y
 ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) ` by Th47;
hence  ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (x `) + y by Th23; ::_thesis: verum
end;

theorem Th49: :: ROBBINS2:49
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z)
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z)
let x, y, z be Element of L; ::_thesis: (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z)
set X = (y + x) ` ;
set Y = y + z;
set Z = x;
 ((((((((y + x) `) + (y + z)) `) + x) `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th48;
hence  (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th46; ::_thesis: verum
end;

theorem Th50: :: ROBBINS2:50
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z)
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z)
let x, y, z be Element of L; ::_thesis: (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z)
 (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th49;
hence  (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th23; ::_thesis: verum
end;

theorem Th51: :: ROBBINS2:51
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (y + x) + (y + z)
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (y + x) + (y + z)
let x, y, z be Element of L; ::_thesis: (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (y + x) + (y + z)
 (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th50;
hence  (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (y + x) + (y + z) by Th23; ::_thesis: verum
end;

theorem Th52: :: ROBBINS2:52
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds ((x `) `) + (y + z) = (y + x) + (y + z)
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((x `) `) + (y + z) = (y + x) + (y + z)
let x, y, z be Element of L; ::_thesis: ((x `) `) + (y + z) = (y + x) + (y + z)
 (x `) + (((y + x) + (y + z)) `) = x ` by Th43;
hence  ((x `) `) + (y + z) = (y + x) + (y + z) by Th51; ::_thesis: verum
end;

theorem Th53: :: ROBBINS2:53
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z)
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z)
let x, y, z be Element of L; ::_thesis: (x + y) + (x + z) = y + (x + z)
set Y = x;
set X = y;
 ((y `) `) + (x + z) = (x + y) + (x + z) by Th52;
hence  (x + y) + (x + z) = y + (x + z) by Th23; ::_thesis: verum
end;

theorem :: ROBBINS2:54
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (x + y) + (x + z) = z + (x + y) by Th53;

theorem Th55: :: ROBBINS2:55
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds x + (y + z) = z + (y + x)
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + (y + z) = z + (y + x)
let x, y, z be Element of L; ::_thesis: x + (y + z) = z + (y + x)
 (y + x) + (y + z) = z + (y + x) by Th53;
hence  x + (y + z) = z + (y + x) by Th53; ::_thesis: verum
end;

theorem :: ROBBINS2:56
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds x + (y + z) = y + (z + x) by Th55;

theorem :: ROBBINS2:57
for L being non empty satisfying_DN_1 ComplLLattStr
for x, y, z being Element of L holds (x + y) + z = x + (y + z) by Th55;

Lm2:  for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-associative
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: L is join-associative
 for x, y, z being Element of L holds (x + y) + z = x + (y + z) by Th55;
hence  L is join-associative by LATTICES:def_5; ::_thesis: verum
end;

Lm3:  for L being non empty satisfying_DN_1 ComplLLattStr holds L is Robbins
proof
let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: L is Robbins
 for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x by Th6;
hence  L is Robbins by ROBBINS1:def_5; ::_thesis: verum
end;

registration
cluster non empty satisfying_DN_1  ->  non empty join-associative for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is satisfying_DN_1 holds
b1 is join-associative by Lm2;
cluster non empty satisfying_DN_1  ->  non empty Robbins for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is satisfying_DN_1 holds
b1 is Robbins by Lm3;
end;

theorem Th58: :: ROBBINS2:58
for L being non empty ComplLLattStr
for x, z being Element of L st L is join-commutative & L is join-associative & L is Huntington holds
(z + x) *' (z + (x `)) = z
proof
let L be non empty ComplLLattStr ; ::_thesis: for x, z being Element of L st L is join-commutative & L is join-associative & L is Huntington holds
(z + x) *' (z + (x `)) = z
let x, z be Element of L; ::_thesis: ( L is join-commutative & L is join-associative & L is Huntington implies (z + x) *' (z + (x `)) = z )
assume  ( L is join-commutative & L is join-associative & L is Huntington ) ; ::_thesis: (z + x) *' (z + (x `)) = z
then reconsider L9 = L as non empty join-commutative join-associative Huntington 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  (z + x) *' (z + (x `)) = z ; ::_thesis: verum
end;

theorem Th59: :: ROBBINS2:59
for L being non empty join-commutative join-associative ComplLLattStr st L is Robbins holds
L is satisfying_DN_1
proof
let L be non empty join-commutative join-associative ComplLLattStr ; ::_thesis: ( L is Robbins implies L is satisfying_DN_1 )
assume  L is Robbins ; ::_thesis: L is satisfying_DN_1
then reconsider L9 = L as non empty join-commutative join-associative Robbins ComplLLattStr ;
let x, y, z, u be Element of L; :: according to ROBBINS2:def_1 ::_thesis: (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z
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  (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z ; ::_thesis: verum
end;

registration
cluster non empty join-commutative join-associative Robbins  ->  non empty satisfying_DN_1 for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is Robbins holds
b1 is satisfying_DN_1 by Th59;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan satisfying_DN_1 for OrthoLattStr ;
existence
 ex b1 being preOrthoLattice st
( b1 is satisfying_DN_1 & b1 is de_Morgan )
proof
take  TrivOrtLat ; ::_thesis: ( TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan )
thus  ( TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan ) ; ::_thesis: verum
end;
end;

registration
cluster non empty Lattice-like de_Morgan satisfying_DN_1  ->  Boolean for OrthoLattStr ;
coherence
 for b1 being preOrthoLattice st b1 is satisfying_DN_1 & b1 is de_Morgan holds
b1 is Boolean ;
cluster non empty Lattice-like Boolean well-complemented  ->  well-complemented satisfying_DN_1 for OrthoLattStr ;
coherence
 for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
b1 is satisfying_DN_1 ;
end;

begin

definition
let L be non empty ComplLLattStr ;
attrL is satisfying_MD_1  means :Def2: :: ROBBINS2:def 2
 for x, y being Element of L holds (((x `) + y) `) + x = x;
attrL is satisfying_MD_2  means :Def3: :: ROBBINS2:def 3
 for x, y, z being Element of L holds (((x `) + y) `) + (z + y) = y + (z + x);
end;

:: deftheorem Def2 defines satisfying_MD_1 ROBBINS2:def_2_:_
 for L being non empty ComplLLattStr holds
( L is satisfying_MD_1 iff for x, y being Element of L holds (((x `) + y) `) + x = x );

:: deftheorem Def3 defines satisfying_MD_2 ROBBINS2:def_3_:_
 for L being non empty ComplLLattStr holds
( L is satisfying_MD_2 iff for x, y, z being Element of L holds (((x `) + y) `) + (z + y) = y + (z + x) );

Lm4: now__::_thesis:_for_L_being_non_empty_ComplLLattStr_st_L_is_satisfying_MD_1_&_L_is_satisfying_MD_2_holds_
(_L_is_join-commutative_&_L_is_Huntington_&_L_is_join-associative_)
let L be non empty ComplLLattStr ; ::_thesis: ( L is satisfying_MD_1 & L is satisfying_MD_2 implies ( L is join-commutative & L is Huntington & L is join-associative ) )
assume A1: ( L is satisfying_MD_1 & L is satisfying_MD_2 ) ; ::_thesis: ( L is join-commutative & L is Huntington & L is join-associative )
A2: for x, y being Element of L holds (x `) + ((x `) + y) = (x `) + y
proof
let x, y be Element of L; ::_thesis: (x `) + ((x `) + y) = (x `) + y
set X = (x `) + y;
 (((x `) + y) `) + x = x by A1, Def2;
hence  (x `) + ((x `) + y) = (x `) + y by A1, Def2; ::_thesis: verum
end;
A3: for x, y being Element of L holds (((x `) + y) `) + y = y + x
proof
let x, y be Element of L; ::_thesis: (((x `) + y) `) + y = y + x
set X = (x `) + y;
A4: (((x `) + y) `) + ((((x `) + y) `) + y) = y + ((((x `) + y) `) + x) by A1, Def3;
(((x `) + y) `) + y = (((x `) + y) `) + ((((x `) + y) `) + y) by A2
.= y + x by A1, A4, Def2 ;
hence  (((x `) + y) `) + y = y + x ; ::_thesis: verum
end;
A5: for x being Element of L holds x + x = x
proof
let x be Element of L; ::_thesis: x + x = x
x + x = (((x `) + x) `) + x by A3
.= x by A1, Def2 ;
hence  x + x = x ; ::_thesis: verum
end;
A6: for x, y being Element of L holds x + (x + y) = x + y
proof
let x, y be Element of L; ::_thesis: x + (x + y) = x + y
x + (x + y) = (((y `) + x) `) + (x + x) by A1, Def3
.= (((y `) + x) `) + x by A5
.= x + y by A3 ;
hence  x + (x + y) = x + y ; ::_thesis: verum
end;
A7: for x, y being Element of L holds (x + y) + y = x + y
proof
let x, y be Element of L; ::_thesis: (x + y) + y = x + y
set Y = x + y;
(x + y) + y = (((y `) + (x + y)) `) + (x + y) by A3
.= (((y `) + (x + y)) `) + (x + (x + y)) by A6
.= (x + y) + (x + y) by A1, Def3
.= x + y by A5 ;
hence  (x + y) + y = x + y ; ::_thesis: verum
end;
A8: for x, y being Element of L holds (x + y) + x = x + y
proof
let x, y be Element of L; ::_thesis: (x + y) + x = x + y
(x + y) + x = ((((y `) + x) `) + x) + x by A3
.= (((y `) + x) `) + x by A7
.= x + y by A3 ;
hence  (x + y) + x = x + y ; ::_thesis: verum
end;
A9: for x, y being Element of L holds x + (y + (y + x)) = y + x
proof
let x, y be Element of L; ::_thesis: x + (y + (y + x)) = y + x
set Z = y + x;
x + (y + (y + x)) = ((((y + x) `) + x) `) + (y + x) by A1, Def3
.= y + x by A1, Def2 ;
hence  x + (y + (y + x)) = y + x ; ::_thesis: verum
end;
A10: for x, y being Element of L holds x + (y + x) = y + x
proof
let x, y be Element of L; ::_thesis: x + (y + x) = y + x
x + (y + x) = x + (y + (y + x)) by A6
.= y + x by A9 ;
hence  x + (y + x) = y + x ; ::_thesis: verum
end;
A11: for x, y being Element of L holds ((x + (y `)) `) + y = y
proof
let x, y be Element of L; ::_thesis: ((x + (y `)) `) + y = y
((x + (y `)) `) + y = (((y `) + (x + (y `))) `) + y by A10
.= y by A1, Def2 ;
hence  ((x + (y `)) `) + y = y ; ::_thesis: verum
end;
A12: for x being Element of L holds ((x `) `) + x = x
proof
let x be Element of L; ::_thesis: ((x `) `) + x = x
 (((x `) + (x `)) `) + x = x by A1, Def2;
hence  ((x `) `) + x = x by A5; ::_thesis: verum
end;
A13: for x being Element of L holds x + ((x `) `) = x
proof
let x be Element of L; ::_thesis: x + ((x `) `) = x
x + ((x `) `) = (((x `) `) + x) + ((x `) `) by A12
.= ((x `) `) + x by A8
.= x by A12 ;
hence  x + ((x `) `) = x ; ::_thesis: verum
end;
A14: for x, y being Element of L holds x + (((x `) `) + y) = x + y
proof
let x, y be Element of L; ::_thesis: x + (((x `) `) + y) = x + y
x + (((x `) `) + y) = (((y `) + x) `) + (((x `) `) + x) by A1, Def3
.= (((y `) + x) `) + x by A12
.= x + y by A3 ;
hence  x + (((x `) `) + y) = x + y ; ::_thesis: verum
end;
A15: for x being Element of L holds x + ((((x `) `) `) `) = x
proof
let x be Element of L; ::_thesis: x + ((((x `) `) `) `) = x
x + ((((x `) `) `) `) = x + (((x `) `) + ((((x `) `) `) `)) by A14
.= x + ((x `) `) by A13
.= x by A13 ;
hence  x + ((((x `) `) `) `) = x ; ::_thesis: verum
end;
A16: for x being Element of L holds ((x `) `) ` = x `
proof
let x be Element of L; ::_thesis: ((x `) `) ` = x `
((x `) `) ` = ((x + ((((x `) `) `) `)) `) + (((x `) `) `) by A11
.= (x `) + (((x `) `) `) by A15
.= x ` by A13 ;
hence  ((x `) `) ` = x ` ; ::_thesis: verum
end;
A17: for x, y, z being Element of L holds (((x `) + y) `) + ((((x `) + z) `) + y) = y + x
proof
let x, y, z be Element of L; ::_thesis: (((x `) + y) `) + ((((x `) + z) `) + y) = y + x
(((x `) + y) `) + ((((x `) + z) `) + y) = y + ((((x `) + z) `) + x) by A1, Def3
.= y + x by A1, Def2 ;
hence  (((x `) + y) `) + ((((x `) + z) `) + y) = y + x ; ::_thesis: verum
end;
A18: for x, y being Element of L holds x + ((y `) `) = x + y
proof
let x, y be Element of L; ::_thesis: x + ((y `) `) = x + y
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  x + ((y `) `) = x + y ; ::_thesis: verum
end;
A19: for x being Element of L holds (x `) ` = x
proof
let x be Element of L; ::_thesis: (x `) ` = x
(x `) ` = (((((x `) `) `) + ((x `) `)) `) + ((x `) `) by A1, Def2
.= (((x `) + ((x `) `)) `) + ((x `) `) by A16
.= (((x `) + ((x `) `)) `) + x by A18
.= x by A1, Def2 ;
hence  (x `) ` = x ; ::_thesis: verum
end;
A20: for x, y, z being Element of L holds (((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x
proof
let x, y, z be Element of L; ::_thesis: (((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x
set P = (((y + x) `) + z) ` ;
(((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = ((((y + x) `) + z) `) + (y + x) by A1, Def3
.= y + x by A1, Def2 ;
hence  (((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x ; ::_thesis: verum
end;
A21: for x, y being Element of L holds (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x
proof
let x, y be Element of L; ::_thesis: (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x
(((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  (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x ; ::_thesis: verum
end;
A22: for x, y being Element of L holds x + (((x `) + y) `) = x
proof
let x, y be Element of L; ::_thesis: x + (((x `) + y) `) = x
x + (((x `) + y) `) = ((((x `) + y) `) + x) + (((x `) + y) `) by A1, Def2
.= (((x `) + y) `) + x by A8
.= x by A1, Def2 ;
hence  x + (((x `) + y) `) = x ; ::_thesis: verum
end;
A23: for x, y being Element of L holds (x `) + ((x + y) `) = x `
proof
let x, y be Element of L; ::_thesis: (x `) + ((x + y) `) = x `
x ` = (x `) + ((((x `) `) + y) `) by A22
.= (x `) + ((x + y) `) by A19 ;
hence  (x `) + ((x + y) `) = x ` ; ::_thesis: verum
end;
A24: for x, y being Element of L holds x + ((y + (x `)) `) = x
proof
let x, y be Element of L; ::_thesis: x + ((y + (x `)) `) = x
x + ((y + (x `)) `) = (((y + (x `)) `) + x) + ((y + (x `)) `) by A11
.= ((y + (x `)) `) + x by A8
.= x by A11 ;
hence  x + ((y + (x `)) `) = x ; ::_thesis: verum
end;
A25: for x, y being Element of L holds (x `) + ((y + x) `) = x `
proof
let x, y be Element of L; ::_thesis: (x `) + ((y + x) `) = x `
x ` = (x `) + ((y + ((x `) `)) `) by A24
.= (x `) + ((y + x) `) by A19 ;
hence  (x `) + ((y + x) `) = x ` ; ::_thesis: verum
end;
A26: for x, y being Element of L holds x + (y `) = (y `) + x
proof
let x, y be Element of L; ::_thesis: x + (y `) = (y `) + x
(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  x + (y `) = (y `) + x ; ::_thesis: verum
end;
A27: for x, y being Element of L holds x + y = y + x
proof
let x, y be Element of L; ::_thesis: x + y = y + x
 (y `) ` = y by A19;
hence  x + y = y + x by A26; ::_thesis: verum
end;
hence  L is join-commutative by LATTICES:def_4; ::_thesis: ( L is Huntington & L is join-associative )
A28: for x, y, z being Element of L holds (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y)
proof
let x, y, z be Element of L; ::_thesis: (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y)
(((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + ((x `) + y)) by A1, Def3
.= z + ((x `) + y) by A2 ;
hence  (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y) ; ::_thesis: verum
end;
A29: for x, y being Element of L holds x + ((y `) + x) = (y `) + x
proof
let x, y be Element of L; ::_thesis: x + ((y `) + x) = (y `) + x
x + ((y `) + x) = (((((y `) + x) `) + x) `) + ((y `) + x) by A28
.= (y `) + x by A1, Def2 ;
hence  x + ((y `) + x) = (y `) + x ; ::_thesis: verum
end;
A30: for x, y being Element of L holds ((x + y) `) + x = (y `) + x
proof
let x, y be Element of L; ::_thesis: ((x + y) `) + x = (y `) + x
set Y = (y `) + x;
(y `) + x = x + ((y `) + x) by A29
.= (((((y `) + x) `) + x) `) + x by A3
.= ((x + y) `) + x by A3 ;
hence  ((x + y) `) + x = (y `) + x ; ::_thesis: verum
end;
A31: for x, y being Element of L holds ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `)
proof
let x, y be Element of L; ::_thesis: ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `)
((x + y) `) + (((y `) + x) `) = (((((y `) + x) `) + x) `) + (((y `) + x) `) by A3
.= (x `) + (((y `) + x) `) by A30 ;
hence  ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `) ; ::_thesis: verum
end;
 for x, y being Element of L holds (((x `) + (y `)) `) + (((x `) + y) `) = x
proof
let x, y be Element of L; ::_thesis: (((x `) + (y `)) `) + (((x `) + y) `) = x
(((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  (((x `) + (y `)) `) + (((x `) + y) `) = x ; ::_thesis: verum
end;
hence  L is Huntington by ROBBINS1:def_6; ::_thesis: L is join-associative
A32: for x, y, z being Element of L holds (x + y) + (y + z) = (x + y) + z
proof
let x, y, z be Element of L; ::_thesis: (x + y) + (y + z) = (x + y) + z
set Y = x + y;
(x + y) + z = (((z `) + (x + y)) `) + (x + y) by A3
.= (((z `) + (x + y)) `) + (y + (x + y)) by A10
.= (x + y) + (y + z) by A1, Def3 ;
hence  (x + y) + (y + z) = (x + y) + z ; ::_thesis: verum
end;
 for x, y, z being Element of L holds (x + y) + z = x + (y + z)
proof
let x, y, z be Element of L; ::_thesis: (x + y) + z = x + (y + z)
 for x, y, z being Element of L holds (x + y) + (z + x) = y + (x + z)
proof
let x, y, z be Element of L; ::_thesis: (x + y) + (z + x) = y + (x + z)
(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  (x + y) + (z + x) = y + (x + z) ; ::_thesis: verum
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  (x + y) + z = x + (y + z) ; ::_thesis: verum
end;
hence  L is join-associative by LATTICES:def_5; ::_thesis: verum
end;

registration
cluster non empty satisfying_MD_1 satisfying_MD_2  ->  non empty join-commutative join-associative Huntington for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is satisfying_MD_1 & b1 is satisfying_MD_2 holds
( b1 is join-commutative & b1 is join-associative & b1 is Huntington ) by Lm4;
cluster non empty join-commutative join-associative Huntington  ->  non empty satisfying_MD_1 satisfying_MD_2 for ComplLLattStr ;
coherence
 for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is Huntington holds
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 )
proof
let L be non empty ComplLLattStr ; ::_thesis: ( L is join-commutative & L is join-associative & L is Huntington implies ( L is satisfying_MD_1 & L is satisfying_MD_2 ) )
assume  ( L is join-commutative & L is join-associative & L is Huntington ) ; ::_thesis: ( L is satisfying_MD_1 & L is satisfying_MD_2 )
then reconsider L9 = L as non empty join-commutative join-associative Huntington ComplLLattStr ;
A1: L9 is satisfying_MD_2
proof
let x, y, z be Element of L9; :: according to ROBBINS2:def_3 ::_thesis: (((x `) + y) `) + (z + y) = y + (z + x)
set Z = z + y;
A2: (z + y) + (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 + y) + x) *' ((z + y) + (y `)) by ROBBINS1:31
.= (z + y) + x by A2, ROBBINS1:14
.= y + (z + x) by LATTICES:def_5 ;
hence  (((x `) + y) `) + (z + y) = y + (z + x) ; ::_thesis: verum
end;
 L9 is satisfying_MD_1
proof
let x, y be Element of L9; :: according to ROBBINS2:def_2 ::_thesis: (((x `) + y) `) + x = x
(((x `) + y) `) + x = (((x `) + ((y `) `)) `) + x by ROBBINS1:3
.= (x *' (y `)) + x by ROBBINS1:def_4
.= x by ROBBINS1:20 ;
hence  (((x `) + y) `) + x = x ; ::_thesis: verum
end;
hence  ( L is satisfying_MD_1 & L is satisfying_MD_2 ) by A1; ::_thesis: verum
end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan satisfying_DN_1 satisfying_MD_1 satisfying_MD_2 for OrthoLattStr ;
existence
 ex b1 being preOrthoLattice st
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 & b1 is satisfying_DN_1 & b1 is de_Morgan )
proof
take  TrivOrtLat ; ::_thesis: ( TrivOrtLat is satisfying_MD_1 & TrivOrtLat is satisfying_MD_2 & TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan )
thus  ( TrivOrtLat is satisfying_MD_1 & TrivOrtLat is satisfying_MD_2 & TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan ) ; ::_thesis: verum
end;
end;

registration
cluster non empty Lattice-like de_Morgan satisfying_MD_1 satisfying_MD_2  ->  Boolean for OrthoLattStr ;
coherence
 for b1 being preOrthoLattice st b1 is satisfying_MD_1 & b1 is satisfying_MD_2 & b1 is de_Morgan holds
b1 is Boolean ;
cluster non empty Lattice-like Boolean well-complemented  ->  well-complemented satisfying_MD_1 satisfying_MD_2 for OrthoLattStr ;
coherence
 for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 ) ;
end;