Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### On the Two Short Axiomatizations of Ortholattices

by
Wioletta Truszkowska, and

MML identifier: ROBBINS2
[ Mizar article, MML identifier index ]

```environ

vocabulary LATTICES, SUBSET_1, ARYTM_3, ROBBINS1, ROBBINS2;
notation STRUCT_0, LATTICES, ROBBINS1;
constructors REALSET1, ROBBINS1;
clusters ROBBINS1;

begin :: One Axiom for Boolean Algebra

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

definition
cluster TrivComplLat -> satisfying_DN_1;
cluster TrivOrtLat -> satisfying_DN_1;
end;

definition
cluster join-commutative join-associative satisfying_DN_1
(non empty ComplLattStr);
end;

reserve L for satisfying_DN_1 (non empty ComplLattStr);
reserve x, y, z, u, v for Element of L;

theorem :: ROBBINS2:1  :: A61
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z, u, v being Element of L holds
((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)` = y;

theorem :: ROBBINS2:2  :: A62
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z, u being Element of L holds
((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y;

theorem :: ROBBINS2:3  :: A63
for L being satisfying_DN_1 (non empty ComplLattStr),
x being Element of L holds
((x + x`)` + x)` = x`;

theorem :: ROBBINS2:4  :: A64
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z, u being Element of L holds
((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)`)`)` = y;

theorem :: ROBBINS2:5  :: A65
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
((x + y)` + ((z + x)` + y)`)` = y;

theorem :: ROBBINS2:6  :: A66
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
((x + y)` + (x` + y)`)` = y;

theorem :: ROBBINS2:7  :: A67
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(((x + y)` + x)` + (x + y)`)` = x;

theorem :: ROBBINS2:8  :: A68
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + ((x + y)` + x)`)` = (x + y)`;

theorem :: ROBBINS2:9  :: A69
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(((x + y)` + z)` + (x + z)`)` = z;

theorem :: ROBBINS2:10  :: A70
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(x + ((y + z)` + (y + x)`)`)` = (y + x)`;

theorem :: ROBBINS2:11  :: A71
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)`;

theorem :: ROBBINS2:12  :: A72
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(x + ((y + z)` + (z + x)`)`)` = (z + x)`;

theorem :: ROBBINS2:13  :: A73
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z, u being Element of L holds
((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y;

theorem :: ROBBINS2:14  :: A74
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + y)` = (y + x)`;

theorem :: ROBBINS2:15  :: A75
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(((x + y)` + (y + z)`)` + z)` = (y + z)`;

theorem :: ROBBINS2:16  :: A76
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)`;

theorem :: ROBBINS2:17  :: A77
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(((x + y)` + x)` + y)` = (y + y)`;

theorem :: ROBBINS2:18  :: A78
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x` + (y + x)`)` = x;

theorem :: ROBBINS2:19  :: A79
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
((x + y)` + y`)` = y;

theorem :: ROBBINS2:20  :: A80
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + (y + x`)`)` = x`;

theorem :: ROBBINS2:21  :: A81
for L being satisfying_DN_1 (non empty ComplLattStr),
x being Element of L holds
(x + x)` = x`;

theorem :: ROBBINS2:22  :: A83
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(((x + y)` + x)` + y)` = y`;

theorem :: ROBBINS2:23  :: A85
for L being satisfying_DN_1 (non empty ComplLattStr),
x being Element of L holds
x`` = x;

theorem :: ROBBINS2:24  :: A86
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
((x + y)` + x)`+ y = y``;

theorem :: ROBBINS2:25  :: A87
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + y)`` = y + x;

theorem :: ROBBINS2:26  :: A88
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
x + ((y + z)` + (y + x)`)` = (y + x )``;

theorem :: ROBBINS2:27  :: A89
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
x + y = y + x;

definition
cluster satisfying_DN_1 -> join-commutative (non empty ComplLattStr);
end;

theorem :: ROBBINS2:28  :: A90
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
((x + y)` + x)` + y = y;

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

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

theorem :: ROBBINS2:31  :: A93
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + y`)` + (y` + y)` = (x + y`)`;

theorem :: ROBBINS2:32  :: A94
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + y)` + (y + y`)` = (x + y)`;

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

theorem :: ROBBINS2:34  :: A96
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
((x + y`)`` + y)` = (y` + y)`;

theorem :: ROBBINS2:35  :: A97
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
((x + y`) + y)` = (y` + y)`;

theorem :: ROBBINS2:36  :: A98
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
((((x + y`) + z)` + y)` + (y` + y)`)` = y;

theorem :: ROBBINS2:37  :: A99
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
x + ((y + z)` + (y + x)`)` = y + x;

theorem :: ROBBINS2:38  :: A100
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
x + (y + ((z + y)` + x)`)` = (z + y)` + x;

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

theorem :: ROBBINS2:40  :: A102
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
((x + y)` + ((x + y)` + (x + z)`)`)` + y = y;

theorem :: ROBBINS2:41  :: A103
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(((x + y`) + z)` + y)`` = y;

theorem :: ROBBINS2:42  :: A104
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
x + ((y + x`) + z)` = x;

theorem :: ROBBINS2:43  :: A105
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
x` + ((y + x) + z)` = x`;

theorem :: ROBBINS2:44  :: A107
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + y)` + x = x + y`;

theorem :: ROBBINS2:45  :: A108
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y being Element of L holds
(x + (x + y`)`)` = (x + y)`;

theorem :: ROBBINS2:46  :: A109
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
((x + y)` + (x + z))` + y = y;

theorem :: ROBBINS2:47  :: A110
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(((x + y)` + z)` + (x` + y)`)` + y = (x` + y)``;

theorem :: ROBBINS2:48  :: A111
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(((x + y)` + z)` + (x` + y)`)` + y = x` + y;

theorem :: ROBBINS2:49  :: A112
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+ (y + z);

theorem :: ROBBINS2:50  :: A113
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (y + z);

theorem :: ROBBINS2:51  :: A114
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y + z);

theorem :: ROBBINS2:52  :: A115
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
x`` + (y + z) = (y + x) + (y + z);

theorem :: ROBBINS2:53  :: A117
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
(x + y) + (x + z) = y + (x + z);

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

theorem :: ROBBINS2:55  :: A119
for L being satisfying_DN_1 (non empty ComplLattStr),
x, y, z being Element of L holds
x + (y + z) = z + (y + x);

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

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

definition
cluster satisfying_DN_1 -> join-associative (non empty ComplLattStr);
cluster satisfying_DN_1 -> Robbins (non empty ComplLattStr);
end;

theorem :: ROBBINS2:58
for L being non empty ComplLattStr,
x, z being Element of L st
L is join-commutative join-associative Huntington holds
(z + x) *' (z + x`) = z;

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

definition
cluster join-commutative join-associative Robbins -> satisfying_DN_1
(non empty ComplLattStr);
end;

definition
cluster satisfying_DN_1 de_Morgan preOrthoLattice;
end;

definition
cluster satisfying_DN_1 de_Morgan -> Boolean preOrthoLattice;
cluster Boolean -> satisfying_DN_1 (well-complemented preOrthoLattice);
end;

begin :: Meredith Two Axioms for Boolean Algebras

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

definition
cluster satisfying_MD_1 satisfying_MD_2 ->
join-commutative join-associative Huntington (non empty ComplLattStr);
cluster join-commutative join-associative Huntington ->
satisfying_MD_1 satisfying_MD_2 (non empty ComplLattStr);
end;

definition
cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan
preOrthoLattice;
end;

definition
cluster satisfying_MD_1 satisfying_MD_2 de_Morgan ->
Boolean preOrthoLattice;
cluster Boolean -> satisfying_MD_1 satisfying_MD_2 (well-complemented
preOrthoLattice);
end;
```