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

definition

let L be non empty ComplLattStr ;
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 ComplLattStr 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 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 b₁ being non empty ComplLattStr st
( b₁ is join-commutative & b₁ is join-associative & b₁ is satisfying_DN_1 )

proof end;

end;

theorem Th1: :: ROBBINS2:1

for L being non empty satisfying_DN_1 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
for x being Element of L holds (x + x) ` = x `

proof end;

theorem Th22: :: ROBBINS2:22

for L being non empty satisfying_DN_1 ComplLattStr
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 ComplLattStr
for x being Element of L holds (x ` ) ` = x

proof end;

theorem Th24: :: ROBBINS2:24

for L being non empty satisfying_DN_1 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
for x, y being Element of L holds x + y = y + x

proof end;

Lm1: for L being non empty satisfying_DN_1 ComplLattStr holds L is join-commutative

proof end;

registration

cluster non empty satisfying_DN_1 -> non empty join-commutative ComplLattStr ;
coherence
for b₁ being non empty ComplLattStr st b₁ is satisfying_DN_1 holds
b₁ is join-commutative by Lm1;

end;

theorem Th28: :: ROBBINS2:28

for L being non empty satisfying_DN_1 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr
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 ComplLattStr holds L is join-associative

proof end;

Lm3: for L being non empty satisfying_DN_1 ComplLattStr holds L is Robbins

proof end;

registration

cluster non empty satisfying_DN_1 -> non empty join-associative ComplLattStr ;
coherence
for b₁ being non empty ComplLattStr st b₁ is satisfying_DN_1 holds
b₁ is join-associative by Lm2;
cluster non empty satisfying_DN_1 -> non empty Robbins ComplLattStr ;
coherence
for b₁ being non empty ComplLattStr st b₁ is satisfying_DN_1 holds
b₁ is Robbins by Lm3;

end;

theorem Th58: :: ROBBINS2:58

for L being non empty ComplLattStr
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 ComplLattStr st L is join-commutative & L is join-associative & L is Robbins holds
L is satisfying_DN_1

proof end;

registration

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

end;

registration

cluster de_Morgan satisfying_DN_1 OrthoLattStr ;
existence
ex b₁ being preOrthoLattice st
( b₁ is satisfying_DN_1 & b₁ is de_Morgan )

proof end;

end;

registration

cluster de_Morgan satisfying_DN_1 -> Boolean OrthoLattStr ;
coherence
for b₁ being preOrthoLattice st b₁ is satisfying_DN_1 & b₁ is de_Morgan holds
b₁ is Boolean ;
cluster Boolean well-complemented -> well-complemented satisfying_DN_1 OrthoLattStr ;
coherence
for b₁ being well-complemented preOrthoLattice st b₁ is Boolean holds
b₁ is satisfying_DN_1 ;

end;

definition

let L be non empty ComplLattStr ;
attr L is satisfying_MD_1 means :Def2: :: ROBBINS2:def 2
for x, y being Element of L holds (((x ` ) + y) ` ) + x = x;
attr L 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 ComplLattStr 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 ComplLattStr 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

let L be non empty ComplLattStr ; :: 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, 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;

A4: 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;

A5: 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;

A6: 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;
A7: (((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, A7, Def2 ;
hence (((x ` ) + y) ` ) + y = y + x ; :: thesis: verum

end;

A8: 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;

A9: 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 A3
.= (y ` ) + x by A1, Def2 ;
hence x + ((y ` ) + x) = (y ` ) + x ; :: thesis: verum

end;

A10: 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 A6
.= x by A1, Def2 ;
hence x + x = x ; :: thesis: verum

end;

A11: 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 A10
.= x + y by A6 ;
hence x + (x + y) = x + y ; :: thesis: verum

end;

A12: 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 A6
.= (((y ` ) + (x + y)) ` ) + (x + (x + y)) by A11
.= (x + y) + (x + y) by A1, Def3
.= x + y by A10 ;
hence (x + y) + y = x + y ; :: 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 by A1, Def2;
hence ((x ` ) ` ) + x = x by A10; :: thesis: verum

end;

A14: 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 A11
.= y + x by A8 ;
hence x + (y + x) = y + x ; :: thesis: verum

end;

A15: 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 A13
.= x + y by A6 ;
hence x + (((x ` ) ` ) + y) = x + y ; :: thesis: verum

end;

A16: 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 A6
.= (((y ` ) + x) ` ) + x by A12
.= x + y by A6 ;
hence (x + y) + x = x + y ; :: thesis: verum

end;

A17: 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 A6
.= (((z ` ) + (x + y)) ` ) + (y + (x + y)) by A14
.= (x + y) + (y + z) by A1, Def3 ;
hence (x + y) + (y + z) = (x + y) + z ; :: thesis: verum

end;

A18: 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 A14
.= y by A1, Def2 ;
hence ((x + (y ` )) ` ) + y = y ; :: thesis: verum

end;

A19: 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 A13
.= ((x ` ) ` ) + x by A16
.= x by A13 ;
hence x + ((x ` ) ` ) = x ; :: thesis: verum

end;

A20: 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 A16
.= x by A1, Def2 ;
hence x + (((x ` ) + y) ` ) = x ; :: thesis: verum

end;

A21: 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 A18
.= ((y + (x ` )) ` ) + x by A16
.= x by A18 ;
hence x + ((y + (x ` )) ` ) = x ; :: thesis: verum

end;

A22: 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 A6
.= (((x ` ) + (((((y ` ) + x) ` ) + x) ` )) ` ) + ((y ` ) + (((((y ` ) + x) ` ) + x) ` )) by A6
.= (y ` ) + x by A5 ;
hence (((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) = (y ` ) + x ; :: thesis: verum

end;

A23: 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 A9
.= (((((y ` ) + x) ` ) + x) ` ) + x by A6
.= ((x + y) ` ) + x by A6 ;
hence ((x + y) ` ) + x = (y ` ) + x ; :: thesis: verum

end;

A24: 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 A6
.= (x ` ) + (((y ` ) + x) ` ) by A23 ;
hence ((x + y) ` ) + (((y ` ) + x) ` ) = (x ` ) + (((y ` ) + x) ` ) ; :: thesis: verum

end;

A25: 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 A15
.= x + ((x ` ) ` ) by A19
.= x by A19 ;
hence x + ((((x ` ) ` ) ` ) ` ) = x ; :: thesis: verum

end;

A26: for x being Element of L holds ((x ` ) ` ) ` = x `

proof

let x be Element of L; :: thesis: ((x ` ) ` ) ` = x `
((x ` ) ` ) ` = ((x + ((((x ` ) ` ) ` ) ` )) ` ) + (((x ` ) ` ) ` ) by A18
.= (x ` ) + (((x ` ) ` ) ` ) by A25
.= x ` by A19 ;
hence ((x ` ) ` ) ` = x ` ; :: thesis: verum

end;

A27: 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 A4
.= (((y ` ) + x) ` ) + ((((((y ` ) ` ) ` ) + x) ` ) + x) by A26
.= (((((y ` ) ` ) ` ) + x) ` ) + ((((((y ` ) ` ) ` ) + x) ` ) + x) by A26
.= x + ((y ` ) ` ) by A4 ;
hence x + ((y ` ) ` ) = x + y ; :: thesis: verum

end;

A28: 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 A26
.= (((x ` ) + ((x ` ) ` )) ` ) + x by A27
.= x by A1, Def2 ;
hence (x ` ) ` = x ; :: thesis: verum

end;

A29: 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 A21
.= (x ` ) + ((y + x) ` ) by A28 ;
hence (x ` ) + ((y + x) ` ) = x ` ; :: thesis: verum

end;

A30: 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 A20
.= (x ` ) + ((x + y) ` ) by A28 ;
hence (x ` ) + ((x + y) ` ) = x ` ; :: thesis: verum

end;

A31: 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 A22
.= ((x ` ) ` ) + ((y ` ) + ((x + y) ` )) by A30
.= ((x ` ) ` ) + (y ` ) by A29
.= x + (y ` ) by A28 ;
hence x + (y ` ) = (y ` ) + x ; :: thesis: verum

end;

A32: 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 A28;
hence x + y = y + x by A31; :: thesis: verum

end;

hence L is join-commutative by LATTICES:def 4; :: thesis: ( L is Huntington & L is join-associative )
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 A32
.= (((x ` ) + y) ` ) + (((y ` ) + (x ` )) ` ) by A32
.= ((x ` ) ` ) + (((y ` ) + (x ` )) ` ) by A24
.= x + (((y ` ) + (x ` )) ` ) by A28
.= x by A21 ;
hence (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x ; :: thesis: verum

end;

hence L is Huntington by ROBBINS1:def 6; :: thesis: L is join-associative
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 A32
.= (z + x) + y by A17
.= (x + z) + y by A32
.= y + (x + z) by A32 ;
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 A32;
(x + y) + z = (x + y) + (y + z) by A17
.= x + (y + z) by A32, 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 ComplLattStr ;
coherence
for b₁ being non empty ComplLattStr st b₁ is satisfying_MD_1 & b₁ is satisfying_MD_2 holds
( b₁ is join-commutative & b₁ is join-associative & b₁ is Huntington ) by Lm4;
cluster non empty join-commutative join-associative Huntington -> non empty satisfying_MD_1 satisfying_MD_2 ComplLattStr ;
coherence
for b₁ being non empty ComplLattStr st b₁ is join-commutative & b₁ is join-associative & b₁ is Huntington holds
( b₁ is satisfying_MD_1 & b₁ is satisfying_MD_2 )

proof end;

end;

registration

cluster de_Morgan satisfying_DN_1 satisfying_MD_1 satisfying_MD_2 OrthoLattStr ;
existence
ex b₁ being preOrthoLattice st
( b₁ is satisfying_MD_1 & b₁ is satisfying_MD_2 & b₁ is satisfying_DN_1 & b₁ is de_Morgan )

proof end;

end;

registration

cluster de_Morgan satisfying_MD_1 satisfying_MD_2 -> Boolean OrthoLattStr ;
coherence
for b₁ being preOrthoLattice st b₁ is satisfying_MD_1 & b₁ is satisfying_MD_2 & b₁ is de_Morgan holds
b₁ is Boolean ;
cluster Boolean well-complemented -> well-complemented satisfying_MD_1 satisfying_MD_2 OrthoLattStr ;
coherence
for b₁ being well-complemented preOrthoLattice st b₁ is Boolean holds
( b₁ is satisfying_MD_1 & b₁ is satisfying_MD_2 ) ;

end;