:: ROBBINS2 semantic presentation

definition
let c1 be non empty ComplLattStr ;
attr a1 is satisfying_DN_1 means :Def1: :: ROBBINS2:def 1
for b1, b2, b3, b4 being Element of a1 holds (((((b1 + b2) ` ) + b3) ` ) + ((b1 + (((b3 ` ) + ((b3 + b4) ` )) ` )) ` )) ` = b3;
end;

:: deftheorem Def1 defines satisfying_DN_1 ROBBINS2:def 1 :
for b1 being non empty ComplLattStr holds
( b1 is satisfying_DN_1 iff for b2, b3, b4, b5 being Element of b1 holds (((((b2 + b3) ` ) + b4) ` ) + ((b2 + (((b4 ` ) + ((b4 + b5) ` )) ` )) ` )) ` = b4 );

registration
cluster TrivComplLat -> satisfying_DN_1 ;
coherence
TrivComplLat is satisfying_DN_1
proof end;
cluster TrivOrtLat -> satisfying_DN_1 ;
coherence
TrivOrtLat is satisfying_DN_1
proof end;
end;

registration
cluster non empty join-commutative join-associative satisfying_DN_1 ComplLattStr ;
existence
ex b1 being non empty ComplLattStr st
( b1 is join-commutative & b1 is join-associative & b1 is satisfying_DN_1 )
proof end;
end;

theorem Th1: :: ROBBINS2:1
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4, b5, b6 being Element of b1 holds (((b2 + b3) ` ) + ((((((b4 + b5) ` ) + b2) ` ) + (((b3 ` ) + ((b3 + b6) ` )) ` )) ` )) ` = b3
proof end;

theorem Th2: :: ROBBINS2:2
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4, b5 being Element of b1 holds (((b2 + b3) ` ) + ((((b4 + b2) ` ) + (((b3 ` ) + ((b3 + b5) ` )) ` )) ` )) ` = b3
proof end;

theorem Th3: :: ROBBINS2:3
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2 being Element of b1 holds (((b2 + (b2 ` )) ` ) + b2) ` = b2 `
proof end;

theorem Th4: :: ROBBINS2:4
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4, b5 being Element of b1 holds (((b2 + b3) ` ) + ((((b4 + b2) ` ) + ((((((b3 + (b3 ` )) ` ) + b3) ` ) + ((b3 + b5) ` )) ` )) ` )) ` = b3
proof end;

theorem Th5: :: ROBBINS2:5
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((b2 + b3) ` ) + ((((b4 + b2) ` ) + b3) ` )) ` = b3
proof end;

theorem Th6: :: ROBBINS2:6
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (((b2 + b3) ` ) + (((b2 ` ) + b3) ` )) ` = b3
proof end;

theorem Th7: :: ROBBINS2:7
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (((((b2 + b3) ` ) + b2) ` ) + ((b2 + b3) ` )) ` = b2
proof end;

theorem Th8: :: ROBBINS2:8
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (b2 + ((((b2 + b3) ` ) + b2) ` )) ` = (b2 + b3) `
proof end;

theorem Th9: :: ROBBINS2:9
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((((b2 + b3) ` ) + b4) ` ) + ((b2 + b4) ` )) ` = b4
proof end;

theorem Th10: :: ROBBINS2:10
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (b2 + ((((b3 + b4) ` ) + ((b3 + b2) ` )) ` )) ` = (b3 + b2) `
proof end;

theorem Th11: :: ROBBINS2:11
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((((((b2 + b3) ` ) + b4) ` ) + (((b2 ` ) + b3) ` )) ` ) + b3) ` = ((b2 ` ) + b3) `
proof end;

theorem Th12: :: ROBBINS2:12
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (b2 + ((((b3 + b4) ` ) + ((b4 + b2) ` )) ` )) ` = (b4 + b2) `
proof end;

theorem Th13: :: ROBBINS2:13
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4, b5 being Element of b1 holds (((b2 + b3) ` ) + ((((b4 + b2) ` ) + (((b3 ` ) + ((b5 + b3) ` )) ` )) ` )) ` = b3
proof end;

theorem Th14: :: ROBBINS2:14
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (b2 + b3) ` = (b3 + b2) `
proof end;

theorem Th15: :: ROBBINS2:15
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((((b2 + b3) ` ) + ((b3 + b4) ` )) ` ) + b4) ` = (b3 + b4) `
proof end;

theorem Th16: :: ROBBINS2:16
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((b2 + ((((b2 + b3) ` ) + b4) ` )) ` ) + b4) ` = (((b2 + b3) ` ) + b4) `
proof end;

theorem Th17: :: ROBBINS2:17
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (((((b2 + b3) ` ) + b2) ` ) + b3) ` = (b3 + b3) `
proof end;

theorem Th18: :: ROBBINS2:18
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((b2 ` ) + ((b3 + b2) ` )) ` = b2
proof end;

theorem Th19: :: ROBBINS2:19
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (((b2 + b3) ` ) + (b3 ` )) ` = b3
proof end;

theorem Th20: :: ROBBINS2:20
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (b2 + ((b3 + (b2 ` )) ` )) ` = b2 `
proof end;

theorem Th21: :: ROBBINS2:21
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2 being Element of b1 holds (b2 + b2) ` = b2 `
proof end;

theorem Th22: :: ROBBINS2:22
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (((((b2 + b3) ` ) + b2) ` ) + b3) ` = b3 `
proof end;

theorem Th23: :: ROBBINS2:23
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2 being Element of b1 holds (b2 ` ) ` = b2
proof end;

theorem Th24: :: ROBBINS2:24
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((((b2 + b3) ` ) + b2) ` ) + b3 = (b3 ` ) `
proof end;

theorem Th25: :: ROBBINS2:25
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((b2 + b3) ` ) ` = b3 + b2
proof end;

theorem Th26: :: ROBBINS2:26
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds b2 + ((((b3 + b4) ` ) + ((b3 + b2) ` )) ` ) = ((b3 + b2) ` ) `
proof end;

theorem Th27: :: ROBBINS2:27
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds b2 + b3 = b3 + b2
proof end;

Lemma29: for b1 being non empty satisfying_DN_1 ComplLattStr holds b1 is join-commutative
proof end;

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

theorem Th28: :: ROBBINS2:28
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((((b2 + b3) ` ) + b2) ` ) + b3 = b3
proof end;

theorem Th29: :: ROBBINS2:29
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((((b2 + b3) ` ) + b3) ` ) + b2 = b2 by Th28;

theorem Th30: :: ROBBINS2:30
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds b2 + ((((b3 + b2) ` ) + b3) ` ) = b2 by Th28;

theorem Th31: :: ROBBINS2:31
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((b2 + (b3 ` )) ` ) + (((b3 ` ) + b3) ` ) = (b2 + (b3 ` )) `
proof end;

theorem Th32: :: ROBBINS2:32
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((b2 + b3) ` ) + ((b3 + (b3 ` )) ` ) = (b2 + b3) `
proof end;

theorem Th33: :: ROBBINS2:33
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((b2 + b3) ` ) + (((b3 ` ) + b3) ` ) = (b2 + b3) ` by Th32;

theorem Th34: :: ROBBINS2:34
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((((b2 + (b3 ` )) ` ) ` ) + b3) ` = ((b3 ` ) + b3) `
proof end;

theorem Th35: :: ROBBINS2:35
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((b2 + (b3 ` )) + b3) ` = ((b3 ` ) + b3) `
proof end;

theorem Th36: :: ROBBINS2:36
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds ((((((b2 + (b3 ` )) + b4) ` ) + b3) ` ) + (((b3 ` ) + b3) ` )) ` = b3
proof end;

theorem Th37: :: ROBBINS2:37
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds b2 + ((((b3 + b4) ` ) + ((b3 + b2) ` )) ` ) = b3 + b2
proof end;

theorem Th38: :: ROBBINS2:38
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds b2 + ((b3 + ((((b4 + b3) ` ) + b2) ` )) ` ) = ((b4 + b3) ` ) + b2
proof end;

theorem Th39: :: ROBBINS2:39
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds b2 + ((((b3 + b2) ` ) + ((b3 + b4) ` )) ` ) = b3 + b2 by Th37;

theorem Th40: :: ROBBINS2:40
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds ((((b2 + b3) ` ) + ((((b2 + b3) ` ) + ((b2 + b4) ` )) ` )) ` ) + b3 = b3
proof end;

theorem Th41: :: ROBBINS2:41
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((((b2 + (b3 ` )) + b4) ` ) + b3) ` ) ` = b3
proof end;

theorem Th42: :: ROBBINS2:42
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds b2 + (((b3 + (b2 ` )) + b4) ` ) = b2
proof end;

theorem Th43: :: ROBBINS2:43
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (b2 ` ) + (((b3 + b2) + b4) ` ) = b2 `
proof end;

theorem Th44: :: ROBBINS2:44
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds ((b2 + b3) ` ) + b2 = b2 + (b3 ` )
proof end;

theorem Th45: :: ROBBINS2:45
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3 being Element of b1 holds (b2 + ((b2 + (b3 ` )) ` )) ` = (b2 + b3) `
proof end;

theorem Th46: :: ROBBINS2:46
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds ((((b2 + b3) ` ) + (b2 + b4)) ` ) + b3 = b3
proof end;

theorem Th47: :: ROBBINS2:47
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds ((((((b2 + b3) ` ) + b4) ` ) + (((b2 ` ) + b3) ` )) ` ) + b3 = (((b2 ` ) + b3) ` ) `
proof end;

theorem Th48: :: ROBBINS2:48
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds ((((((b2 + b3) ` ) + b4) ` ) + (((b2 ` ) + b3) ` )) ` ) + b3 = (b2 ` ) + b3
proof end;

theorem Th49: :: ROBBINS2:49
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((b2 ` ) + (((((b3 + b2) ` ) ` ) + (b3 + b4)) ` )) ` ) + (b3 + b4) = (((b3 + b2) ` ) ` ) + (b3 + b4)
proof end;

theorem Th50: :: ROBBINS2:50
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((b2 ` ) + (((b3 + b2) + (b3 + b4)) ` )) ` ) + (b3 + b4) = (((b3 + b2) ` ) ` ) + (b3 + b4)
proof end;

theorem Th51: :: ROBBINS2:51
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (((b2 ` ) + (((b3 + b2) + (b3 + b4)) ` )) ` ) + (b3 + b4) = (b3 + b2) + (b3 + b4)
proof end;

theorem Th52: :: ROBBINS2:52
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds ((b2 ` ) ` ) + (b3 + b4) = (b3 + b2) + (b3 + b4)
proof end;

theorem Th53: :: ROBBINS2:53
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (b2 + b3) + (b2 + b4) = b3 + (b2 + b4)
proof end;

theorem Th54: :: ROBBINS2:54
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (b2 + b3) + (b2 + b4) = b4 + (b2 + b3) by Th53;

theorem Th55: :: ROBBINS2:55
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds b2 + (b3 + b4) = b4 + (b3 + b2)
proof end;

theorem Th56: :: ROBBINS2:56
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds b2 + (b3 + b4) = b3 + (b4 + b2) by Th55;

theorem Th57: :: ROBBINS2:57
for b1 being non empty satisfying_DN_1 ComplLattStr
for b2, b3, b4 being Element of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4) by Th55;

Lemma53: for b1 being non empty satisfying_DN_1 ComplLattStr holds b1 is join-associative
proof end;

Lemma54: for b1 being non empty satisfying_DN_1 ComplLattStr holds b1 is Robbins
proof end;

registration
cluster non empty satisfying_DN_1 -> non empty join-associative ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is satisfying_DN_1 holds
b1 is join-associative by Lemma53;
cluster non empty satisfying_DN_1 -> non empty Robbins ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is satisfying_DN_1 holds
b1 is Robbins by Lemma54;
end;

theorem Th58: :: ROBBINS2:58
for b1 being non empty ComplLattStr
for b2, b3 being Element of b1 st b1 is join-commutative & b1 is join-associative & b1 is Huntington holds
(b3 + b2) *' (b3 + (b2 ` )) = b3
proof end;

theorem Th59: :: ROBBINS2:59
for b1 being non empty ComplLattStr st b1 is join-commutative & b1 is join-associative & b1 is Robbins holds
b1 is satisfying_DN_1
proof end;

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

registration
cluster join-commutative join-associative Robbins de_Morgan satisfying_DN_1 OrthoLattStr ;
existence
ex b1 being preOrthoLattice st
( b1 is satisfying_DN_1 & b1 is de_Morgan )
proof end;
end;

registration
cluster de_Morgan satisfying_DN_1 -> Boolean OrthoLattStr ;
coherence
for b1 being preOrthoLattice st b1 is satisfying_DN_1 & b1 is de_Morgan holds
b1 is Boolean
proof end;
cluster Boolean well-complemented -> join-commutative join-associative Robbins well-complemented satisfying_DN_1 OrthoLattStr ;
coherence
for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
b1 is satisfying_DN_1
proof end;
end;

definition
let c1 be non empty ComplLattStr ;
attr a1 is satisfying_MD_1 means :Def2: :: ROBBINS2:def 2
for b1, b2 being Element of a1 holds (((b1 ` ) + b2) ` ) + b1 = b1;
attr a1 is satisfying_MD_2 means :Def3: :: ROBBINS2:def 3
for b1, b2, b3 being Element of a1 holds (((b1 ` ) + b2) ` ) + (b3 + b2) = b2 + (b3 + b1);
end;

:: deftheorem Def2 defines satisfying_MD_1 ROBBINS2:def 2 :
for b1 being non empty ComplLattStr holds
( b1 is satisfying_MD_1 iff for b2, b3 being Element of b1 holds (((b2 ` ) + b3) ` ) + b2 = b2 );

:: deftheorem Def3 defines satisfying_MD_2 ROBBINS2:def 3 :
for b1 being non empty ComplLattStr holds
( b1 is satisfying_MD_2 iff for b2, b3, b4 being Element of b1 holds (((b2 ` ) + b3) ` ) + (b4 + b3) = b3 + (b4 + b2) );

E59: now
let c1 be non empty ComplLattStr ;
assume E60: ( c1 is satisfying_MD_1 & c1 is satisfying_MD_2 ) ;
E61: for b1, b2 being Element of c1 holds (b1 ` ) + ((b1 ` ) + b2) = (b1 ` ) + b2
proof
let c2, c3 be Element of c1;
set c4 = (c2 ` ) + c3;
(((c2 ` ) + c3) ` ) + c2 = c2 by E60, Def2;
hence (c2 ` ) + ((c2 ` ) + c3) = (c2 ` ) + c3 by E60, Def2;
end;
E62: for b1, b2, b3 being Element of c1 holds (((((b1 ` ) + b2) ` ) + b3) ` ) + ((b1 ` ) + b3) = b3 + ((b1 ` ) + b2)
proof
let c2, c3, c4 be Element of c1;
(((((c2 ` ) + c3) ` ) + c4) ` ) + ((c2 ` ) + c4) = c4 + ((c2 ` ) + ((c2 ` ) + c3)) by E60, Def3
.= c4 + ((c2 ` ) + c3) by E61 ;
hence (((((c2 ` ) + c3) ` ) + c4) ` ) + ((c2 ` ) + c4) = c4 + ((c2 ` ) + c3) ;
end;
E63: for b1, b2, b3 being Element of c1 holds (((b1 ` ) + b2) ` ) + ((((b1 ` ) + b3) ` ) + b2) = b2 + b1
proof
let c2, c3, c4 be Element of c1;
(((c2 ` ) + c3) ` ) + ((((c2 ` ) + c4) ` ) + c3) = c3 + ((((c2 ` ) + c4) ` ) + c2) by E60, Def3
.= c3 + c2 by E60, Def2 ;
hence (((c2 ` ) + c3) ` ) + ((((c2 ` ) + c4) ` ) + c3) = c3 + c2 ;
end;
E64: for b1, b2, b3 being Element of c1 holds (((b1 ` ) + ((((b2 + b1) ` ) + b3) ` )) ` ) + (b2 + ((((b2 + b1) ` ) + b3) ` )) = b2 + b1
proof
let c2, c3, c4 be Element of c1;
set c5 = (((c3 + c2) ` ) + c4) ` ;
(((c2 ` ) + ((((c3 + c2) ` ) + c4) ` )) ` ) + (c3 + ((((c3 + c2) ` ) + c4) ` )) = ((((c3 + c2) ` ) + c4) ` ) + (c3 + c2) by E60, Def3
.= c3 + c2 by E60, Def2 ;
hence (((c2 ` ) + ((((c3 + c2) ` ) + c4) ` )) ` ) + (c3 + ((((c3 + c2) ` ) + c4) ` )) = c3 + c2 ;
end;
E65: for b1, b2 being Element of c1 holds (((b1 ` ) + b2) ` ) + b2 = b2 + b1
proof
let c2, c3 be Element of c1;
set c4 = (c2 ` ) + c3;
E66: (((c2 ` ) + c3) ` ) + ((((c2 ` ) + c3) ` ) + c3) = c3 + ((((c2 ` ) + c3) ` ) + c2) by E60, Def3;
(((c2 ` ) + c3) ` ) + c3 = (((c2 ` ) + c3) ` ) + ((((c2 ` ) + c3) ` ) + c3) by E61
.= c3 + c2 by E60, E66, Def2 ;
hence (((c2 ` ) + c3) ` ) + c3 = c3 + c2 ;
end;
E66: for b1, b2 being Element of c1 holds b1 + (b2 + (b2 + b1)) = b2 + b1
proof
let c2, c3 be Element of c1;
set c4 = c3 + c2;
c2 + (c3 + (c3 + c2)) = ((((c3 + c2) ` ) + c2) ` ) + (c3 + c2) by E60, Def3
.= c3 + c2 by E60, Def2 ;
hence c2 + (c3 + (c3 + c2)) = c3 + c2 ;
end;
E67: for b1, b2 being Element of c1 holds b1 + ((b2 ` ) + b1) = (b2 ` ) + b1
proof
let c2, c3 be Element of c1;
c2 + ((c3 ` ) + c2) = (((((c3 ` ) + c2) ` ) + c2) ` ) + ((c3 ` ) + c2) by E62
.= (c3 ` ) + c2 by E60, Def2 ;
hence c2 + ((c3 ` ) + c2) = (c3 ` ) + c2 ;
end;
E68: for b1 being Element of c1 holds b1 + b1 = b1
proof
let c2 be Element of c1;
c2 + c2 = (((c2 ` ) + c2) ` ) + c2 by E65
.= c2 by E60, Def2 ;
hence c2 + c2 = c2 ;
end;
E69: for b1, b2 being Element of c1 holds b1 + (b1 + b2) = b1 + b2
proof
let c2, c3 be Element of c1;
c2 + (c2 + c3) = (((c3 ` ) + c2) ` ) + (c2 + c2) by E60, Def3
.= (((c3 ` ) + c2) ` ) + c2 by E68
.= c2 + c3 by E65 ;
hence c2 + (c2 + c3) = c2 + c3 ;
end;
E70: for b1, b2 being Element of c1 holds (b1 + b2) + b2 = b1 + b2
proof
let c2, c3 be Element of c1;
set c4 = c2 + c3;
(c2 + c3) + c3 = (((c3 ` ) + (c2 + c3)) ` ) + (c2 + c3) by E65
.= (((c3 ` ) + (c2 + c3)) ` ) + (c2 + (c2 + c3)) by E69
.= (c2 + c3) + (c2 + c3) by E60, Def3
.= c2 + c3 by E68 ;
hence (c2 + c3) + c3 = c2 + c3 ;
end;
E71: for b1 being Element of c1 holds ((b1 ` ) ` ) + b1 = b1
proof
let c2 be Element of c1;
(((c2 ` ) + (c2 ` )) ` ) + c2 = c2 by E60, Def2;
hence ((c2 ` ) ` ) + c2 = c2 by E68;
end;
E72: for b1, b2 being Element of c1 holds b1 + (b2 + b1) = b2 + b1
proof
let c2, c3 be Element of c1;
c2 + (c3 + c2) = c2 + (c3 + (c3 + c2)) by E69
.= c3 + c2 by E66 ;
hence c2 + (c3 + c2) = c3 + c2 ;
end;
E73: for b1, b2 being Element of c1 holds b1 + (((b1 ` ) ` ) + b2) = b1 + b2
proof
let c2, c3 be Element of c1;
c2 + (((c2 ` ) ` ) + c3) = (((c3 ` ) + c2) ` ) + (((c2 ` ) ` ) + c2) by E60, Def3
.= (((c3 ` ) + c2) ` ) + c2 by E71
.= c2 + c3 by E65 ;
hence c2 + (((c2 ` ) ` ) + c3) = c2 + c3 ;
end;
E74: for b1, b2 being Element of c1 holds (b1 + b2) + b1 = b1 + b2
proof
let c2, c3 be Element of c1;
(c2 + c3) + c2 = ((((c3 ` ) + c2) ` ) + c2) + c2 by E65
.= (((c3 ` ) + c2) ` ) + c2 by E70
.= c2 + c3 by E65 ;
hence (c2 + c3) + c2 = c2 + c3 ;
end;
E75: for b1, b2, b3 being Element of c1 holds (b1 + b2) + (b2 + b3) = (b1 + b2) + b3
proof
let c2, c3, c4 be Element of c1;
set c5 = c2 + c3;
(c2 + c3) + c4 = (((c4 ` ) + (c2 + c3)) ` ) + (c2 + c3) by E65
.= (((c4 ` ) + (c2 + c3)) ` ) + (c3 + (c2 + c3)) by E72
.= (c2 + c3) + (c3 + c4) by E60, Def3 ;
hence (c2 + c3) + (c3 + c4) = (c2 + c3) + c4 ;
end;
E76: for b1, b2 being Element of c1 holds ((b1 + (b2 ` )) ` ) + b2 = b2
proof
let c2, c3 be Element of c1;
((c2 + (c3 ` )) ` ) + c3 = (((c3 ` ) + (c2 + (c3 ` ))) ` ) + c3 by E72
.= c3 by E60, Def2 ;
hence ((c2 + (c3 ` )) ` ) + c3 = c3 ;
end;
E77: for b1 being Element of c1 holds b1 + ((b1 ` ) ` ) = b1
proof
let c2 be Element of c1;
c2 + ((c2 ` ) ` ) = (((c2 ` ) ` ) + c2) + ((c2 ` ) ` ) by E71
.= ((c2 ` ) ` ) + c2 by E74
.= c2 by E71 ;
hence c2 + ((c2 ` ) ` ) = c2 ;
end;
E78: for b1, b2 being Element of c1 holds b1 + (((b1 ` ) + b2) ` ) = b1
proof
let c2, c3 be Element of c1;
c2 + (((c2 ` ) + c3) ` ) = ((((c2 ` ) + c3) ` ) + c2) + (((c2 ` ) + c3) ` ) by E60, Def2
.= (((c2 ` ) + c3) ` ) + c2 by E74
.= c2 by E60, Def2 ;
hence c2 + (((c2 ` ) + c3) ` ) = c2 ;
end;
E79: for b1, b2 being Element of c1 holds b1 + ((b2 + (b1 ` )) ` ) = b1
proof
let c2, c3 be Element of c1;
c2 + ((c3 + (c2 ` )) ` ) = (((c3 + (c2 ` )) ` ) + c2) + ((c3 + (c2 ` )) ` ) by E76
.= ((c3 + (c2 ` )) ` ) + c2 by E74
.= c2 by E76 ;
hence c2 + ((c3 + (c2 ` )) ` ) = c2 ;
end;
E80: for b1, b2 being Element of c1 holds (((b1 ` ) + ((b1 + b2) ` )) ` ) + ((b2 ` ) + ((b1 + b2) ` )) = (b2 ` ) + b1
proof
let c2, c3 be Element of c1;
(((c2 ` ) + ((c2 + c3) ` )) ` ) + ((c3 ` ) + ((c2 + c3) ` )) = (((c2 ` ) + ((c2 + c3) ` )) ` ) + ((c3 ` ) + (((((c3 ` ) + c2) ` ) + c2) ` )) by E65
.= (((c2 ` ) + (((((c3 ` ) + c2) ` ) + c2) ` )) ` ) + ((c3 ` ) + (((((c3 ` ) + c2) ` ) + c2) ` )) by E65
.= (c3 ` ) + c2 by E64 ;
hence (((c2 ` ) + ((c2 + c3) ` )) ` ) + ((c3 ` ) + ((c2 + c3) ` )) = (c3 ` ) + c2 ;
end;
E81: for b1, b2 being Element of c1 holds ((b1 + b2) ` ) + b1 = (b2 ` ) + b1
proof
let c2, c3 be Element of c1;
set c4 = (c3 ` ) + c2;
(c3 ` ) + c2 = c2 + ((c3 ` ) + c2) by E67
.= (((((c3 ` ) + c2) ` ) + c2) ` ) + c2 by E65
.= ((c2 + c3) ` ) + c2 by E65 ;
hence ((c2 + c3) ` ) + c2 = (c3 ` ) + c2 ;
end;
E82: for b1, b2 being Element of c1 holds ((b1 + b2) ` ) + (((b2 ` ) + b1) ` ) = (b1 ` ) + (((b2 ` ) + b1) ` )
proof
let c2, c3 be Element of c1;
((c2 + c3) ` ) + (((c3 ` ) + c2) ` ) = (((((c3 ` ) + c2) ` ) + c2) ` ) + (((c3 ` ) + c2) ` ) by E65
.= (c2 ` ) + (((c3 ` ) + c2) ` ) by E81 ;
hence ((c2 + c3) ` ) + (((c3 ` ) + c2) ` ) = (c2 ` ) + (((c3 ` ) + c2) ` ) ;
end;
E83: for b1 being Element of c1 holds b1 + ((((b1 ` ) ` ) ` ) ` ) = b1
proof
let c2 be Element of c1;
c2 + ((((c2 ` ) ` ) ` ) ` ) = c2 + (((c2 ` ) ` ) + ((((c2 ` ) ` ) ` ) ` )) by E73
.= c2 + ((c2 ` ) ` ) by E77
.= c2 by E77 ;
hence c2 + ((((c2 ` ) ` ) ` ) ` ) = c2 ;
end;
E84: for b1 being Element of c1 holds ((b1 ` ) ` ) ` = b1 `
proof
let c2 be Element of c1;
((c2 ` ) ` ) ` = ((c2 + ((((c2 ` ) ` ) ` ) ` )) ` ) + (((c2 ` ) ` ) ` ) by E76
.= (c2 ` ) + (((c2 ` ) ` ) ` ) by E83
.= c2 ` by E77 ;
hence ((c2 ` ) ` ) ` = c2 ` ;
end;
E85: for b1, b2 being Element of c1 holds b1 + ((b2 ` ) ` ) = b1 + b2
proof
let c2, c3 be Element of c1;
c2 + c3 = (((c3 ` ) + c2) ` ) + ((((c3 ` ) + c2) ` ) + c2) by E63
.= (((c3 ` ) + c2) ` ) + ((((((c3 ` ) ` ) ` ) + c2) ` ) + c2) by E84
.= (((((c3 ` ) ` ) ` ) + c2) ` ) + ((((((c3 ` ) ` ) ` ) + c2) ` ) + c2) by E84
.= c2 + ((c3 ` ) ` ) by E63 ;
hence c2 + ((c3 ` ) ` ) = c2 + c3 ;
end;
E86: for b1 being Element of c1 holds (b1 ` ) ` = b1
proof
let c2 be Element of c1;
(c2 ` ) ` = (((((c2 ` ) ` ) ` ) + ((c2 ` ) ` )) ` ) + ((c2 ` ) ` ) by E60, Def2
.= (((c2 ` ) + ((c2 ` ) ` )) ` ) + ((c2 ` ) ` ) by E84
.= (((c2 ` ) + ((c2 ` ) ` )) ` ) + c2 by E85
.= c2 by E60, Def2 ;
hence (c2 ` ) ` = c2 ;
end;
E87: for b1, b2 being Element of c1 holds (b1 ` ) + ((b2 + b1) ` ) = b1 `
proof
let c2, c3 be Element of c1;
c2 ` = (c2 ` ) + ((c3 + ((c2 ` ) ` )) ` ) by E79
.= (c2 ` ) + ((c3 + c2) ` ) by E86 ;
hence (c2 ` ) + ((c3 + c2) ` ) = c2 ` ;
end;
E88: for b1, b2 being Element of c1 holds (b1 ` ) + ((b1 + b2) ` ) = b1 `
proof
let c2, c3 be Element of c1;
c2 ` = (c2 ` ) + ((((c2 ` ) ` ) + c3) ` ) by E78
.= (c2 ` ) + ((c2 + c3) ` ) by E86 ;
hence (c2 ` ) + ((c2 + c3) ` ) = c2 ` ;
end;
E89: for b1, b2 being Element of c1 holds b1 + (b2 ` ) = (b2 ` ) + b1
proof
let c2, c3 be Element of c1;
(c3 ` ) + c2 = (((c2 ` ) + ((c2 + c3) ` )) ` ) + ((c3 ` ) + ((c2 + c3) ` )) by E80
.= ((c2 ` ) ` ) + ((c3 ` ) + ((c2 + c3) ` )) by E88
.= ((c2 ` ) ` ) + (c3 ` ) by E87
.= c2 + (c3 ` ) by E86 ;
hence c2 + (c3 ` ) = (c3 ` ) + c2 ;
end;
E90: for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1
proof
let c2, c3 be Element of c1;
(c3 ` ) ` = c3 by E86;
hence c2 + c3 = c3 + c2 by E89;
end;
hence c1 is join-commutative by LATTICES:def 4;
for b1, b2 being Element of c1 holds (((b1 ` ) + (b2 ` )) ` ) + (((b1 ` ) + b2) ` ) = b1
proof
let c2, c3 be Element of c1;
(((c2 ` ) + (c3 ` )) ` ) + (((c2 ` ) + c3) ` ) = (((c3 ` ) + (c2 ` )) ` ) + (((c2 ` ) + c3) ` ) by E90
.= (((c2 ` ) + c3) ` ) + (((c3 ` ) + (c2 ` )) ` ) by E90
.= ((c2 ` ) ` ) + (((c3 ` ) + (c2 ` )) ` ) by E82
.= c2 + (((c3 ` ) + (c2 ` )) ` ) by E86
.= c2 by E79 ;
hence (((c2 ` ) + (c3 ` )) ` ) + (((c2 ` ) + c3) ` ) = c2 ;
end;
hence c1 is Huntington by ROBBINS1:def 6;
for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3)
proof
let c2, c3, c4 be Element of c1;
for b1, b2, b3 being Element of c1 holds (b1 + b2) + (b3 + b1) = b2 + (b1 + b3)
proof
let c5, c6, c7 be Element of c1;
(c5 + c6) + (c7 + c5) = (c7 + c5) + (c5 + c6) by E90
.= (c7 + c5) + c6 by E75
.= (c5 + c7) + c6 by E90
.= c6 + (c5 + c7) by E90 ;
hence (c5 + c6) + (c7 + c5) = c6 + (c5 + c7) ;
end;
then (c3 + c2) + (c4 + c3) = c2 + (c3 + c4) ;
then E91: (c2 + c3) + (c4 + c3) = c2 + (c3 + c4) by E90;
(c2 + c3) + c4 = (c2 + c3) + (c3 + c4) by E75
.= c2 + (c3 + c4) by E90, E91 ;
hence (c2 + c3) + c4 = c2 + (c3 + c4) ;
end;
hence c1 is join-associative by LATTICES:def 5;
end;

registration
cluster non empty satisfying_MD_1 satisfying_MD_2 -> non empty join-commutative join-associative Huntington ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is satisfying_MD_1 & b1 is satisfying_MD_2 holds
( b1 is join-commutative & b1 is join-associative & b1 is Huntington ) by Lemma59;
cluster non empty join-commutative join-associative Huntington -> non empty satisfying_MD_1 satisfying_MD_2 ComplLattStr ;
coherence
for b1 being non empty ComplLattStr 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
cluster join-commutative join-associative Boolean Robbins Huntington de_Morgan satisfying_DN_1 satisfying_MD_1 satisfying_MD_2 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 end;
end;

registration
cluster de_Morgan satisfying_MD_1 satisfying_MD_2 -> Boolean 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
proof end;
cluster Boolean well-complemented -> join-commutative join-associative Huntington well-complemented satisfying_MD_1 satisfying_MD_2 OrthoLattStr ;
coherence
for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 )
proof end;
end;