:: On the Two Short Axiomatizations of Ortholattices
:: by Wioletta Truszkowska and Adam Grabowski
::
:: Copyright (c) 2003-2019 Association of Mizar Users

definition
let L be non empty ComplLLattStr ;
attr L 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 end;

registration
existence
ex b1 being non empty ComplLLattStr st
( b1 is join-commutative & b1 is join-associative & b1 is satisfying_DN_1 )
proof 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 end;

theorem Th23: :: ROBBINS2:23
for L being non empty satisfying_DN_1 ComplLLattStr
for x being Element of L holds (x )  = x
proof 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 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 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 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 end;

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

registration
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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 end;

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

registration
coherence
for b1 being non empty ComplLLattStr st b1 is satisfying_DN_1 holds
b1 is join-associative
by Lm2;
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 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 end;

registration
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
existence
ex b1 being preOrthoLattice st
( b1 is satisfying_DN_1 & b1 is de_Morgan )
proof end;
end;

registration
coherence
for b1 being preOrthoLattice st b1 is satisfying_DN_1 & b1 is de_Morgan holds
b1 is Boolean
;
coherence
for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
b1 is satisfying_DN_1
;
end;

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

:: deftheorem 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 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;
hence (x ) + ((x ) + y) = (x ) + y by A1; :: 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;
(((x ) + y) ) + y = (((x ) + y) ) + ((((x ) + y) ) + y) by A2
.= y + x by A1, A4 ;
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 ;
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
.= (((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
.= 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
.= y + x by A1 ;
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 ;
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;
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
.= (((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
.= y + x by A1 ;
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
.= (((x ) + ((x ) )) ) + ((x ) ) by A16
.= (((x ) + ((x ) )) ) + x by A18
.= x by A1 ;
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
.= y + x by A1 ;
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
.= (((x ) + y) ) + x by A8
.= x by A1 ;
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
.= 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 ;
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:
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 ;
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 ;
hence (x + y) + z = x + (y + z) ; :: thesis: verum
end;
hence L is join-associative by LATTICES:def 5; :: thesis: verum
end;

registration
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;
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 end;
end;

registration
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 end;
end;

registration
coherence
for b1 being preOrthoLattice st b1 is satisfying_MD_1 & b1 is satisfying_MD_2 & b1 is de_Morgan holds
b1 is Boolean
;
coherence
for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 )
;
end;