:: On the Two Short Axiomatizations of Ortholattices
:: by Wioletta Truszkowska and Adam Grabowski
::
:: Received June 28, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


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
proofend;
cluster TrivOrtLat  ->  satisfying_DN_1 ;
coherence
 TrivOrtLat is satisfying_DN_1
proofend;
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 )
proofend;
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
proofend;

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
proofend;

theorem Th3: :: ROBBINS2:3
for L being non empty satisfying_DN_1 ComplLLattStr
for x being Element of L holds (((x + (x `)) `) + x) ` = x `
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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) `
proofend;

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
proofend;

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) `
proofend;

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) `
proofend;

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) `
proofend;

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
proofend;

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) `
proofend;

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) `
proofend;

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) `
proofend;

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) `
proofend;

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
proofend;

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
proofend;

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 `
proofend;

theorem Th21: :: ROBBINS2:21
for L being non empty satisfying_DN_1 ComplLLattStr
for x being Element of L holds (x + x) ` = x `
proofend;

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 `
proofend;

theorem Th23: :: ROBBINS2:23
for L being non empty satisfying_DN_1 ComplLLattStr
for x being Element of L holds (x `) ` = x
proofend;

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 `) `
proofend;

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
proofend;

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) `) `
proofend;

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
proofend;

Lm1:  for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-commutative
proofend;

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
proofend;

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 `)) `
proofend;

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) `
proofend;

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) `
proofend;

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) `
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 `
proofend;

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 `)
proofend;

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) `
proofend;

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
proofend;

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) `) `
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

Lm3:  for L being non empty satisfying_DN_1 ComplLLattStr holds L is Robbins
proofend;

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
proofend;

theorem Th59: :: ROBBINS2:59
for L being non empty join-commutative join-associative ComplLLattStr st L is Robbins holds
L is satisfying_DN_1
proofend;

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 )
proofend;
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 )
proofend;
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 )
proofend;
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;