P. 12 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 1101-1200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lem4.6.6i4j2 1101	Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 4, and j is set to 2. (Contributed by Roy F. Longton, 2-Jul-2005.)
((a →4 b) ∪ (a →2 b)) = (a →0 b)
Theorem	com3iia 1102	The dual of com3ii 457. (Contributed by Roy F. Longton, 2-Jul-2005.)
a C b    ⇒   (a ∪ (a⊥ ∩ b)) = (a ∪ b)
Theorem	lem4.6.7 1103	Equation 4.15 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-2005.)
a⊥ ≤ b    ⇒   b ≤ (a →1 b)
0.8  Weakly distributive ortholattices (WDOL)
0.8.1  WDOL law
Axiom	ax-wdol 1104	The WDOL (weakly distributive ortholattice) axiom. (Contributed by NM, 4-Mar-2006.)
((a ≡ b) ∪ (a ≡ b⊥ )) = 1
Theorem	wdcom 1105	Any two variables (weakly) commute in a WDOL. (Contributed by NM, 4-Mar-2006.)
C (a, b) = 1
Theorem	wdwom 1106	Prove 2-variable WOML rule in WDOL. This will make all WOML theorems available to us. The proof does not use ax-r3 439 or ax-wom 361. Since this is the same as ax-wom 361, from here on we will freely use those theorems invoking ax-wom 361. (Contributed by NM, 4-Mar-2006.)
(a⊥ ∪ (a ∩ b)) = 1    ⇒   (b ∪ (a⊥ ∩ b⊥ )) = 1
Theorem	wddi1 1107	Prove the weak distributive law in WDOL. This is our first WDOL theorem making use of ax-wom 361, which is justified by wdwom 1106. (Contributed by NM, 4-Mar-2006.)
((a ∩ (b ∪ c)) ≡ ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi2 1108	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
(((a ∪ b) ∩ c) ≡ ((a ∩ c) ∪ (b ∩ c))) = 1
Theorem	wddi3 1109	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∪ (b ∩ c)) ≡ ((a ∪ b) ∩ (a ∪ c))) = 1
Theorem	wddi4 1110	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
(((a ∩ b) ∪ c) ≡ ((a ∪ c) ∩ (b ∪ c))) = 1
Theorem	wdid0id5 1111	Show that quantum identity follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a ≡0 b) = 1    ⇒   (a ≡ b) = 1
Theorem	wdid0id1 1112	Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a ≡0 b) = 1    ⇒   (a ≡1 b) = 1
Theorem	wdid0id2 1113	Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a ≡0 b) = 1    ⇒   (a ≡2 b) = 1
Theorem	wdid0id3 1114	Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a ≡0 b) = 1    ⇒   (a ≡3 b) = 1
Theorem	wdid0id4 1115	Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a ≡0 b) = 1    ⇒   (a ≡4 b) = 1
Theorem	wdka4o 1116	Show WDOL analog of WOM law. (Contributed by NM, 5-Mar-2006.)
(a ≡0 b) = 1    ⇒   ((a ∪ c) ≡0 (b ∪ c)) = 1
Theorem	wddi-0 1117	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (b ∪ c)) ≡0 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-1 1118	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (b ∪ c)) ≡1 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-2 1119	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (b ∪ c)) ≡2 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-3 1120	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (b ∪ c)) ≡3 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-4 1121	The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (b ∪ c)) ≡4 ((a ∩ b) ∪ (a ∩ c))) = 1
0.9  Modular ortholattices (MOL)
0.9.1  Modular law
Axiom	ax-ml 1122	The modular law axiom. (Contributed by NM, 15-Mar-2010.)
((a ∪ b) ∩ (a ∪ c)) ≤ (a ∪ (b ∩ (a ∪ c)))
Theorem	ml 1123	Modular law in equational form. (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(a ∪ (b ∩ (a ∪ c))) = ((a ∪ b) ∩ (a ∪ c))
Theorem	mldual 1124	Dual of modular law. (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(a ∩ (b ∪ (a ∩ c))) = ((a ∩ b) ∪ (a ∩ c))
Theorem	ml2i 1125	Inference version of modular law. (Contributed by NM, 1-Apr-2012.)
c ≤ a    ⇒   (c ∪ (b ∩ a)) = ((c ∪ b) ∩ a)
Theorem	mli 1126	Inference version of modular law. (Contributed by NM, 1-Apr-2012.)
c ≤ a    ⇒   ((a ∩ b) ∪ c) = (a ∩ (b ∪ c))
Theorem	mldual2i 1127	Inference version of dual of modular law. (Contributed by NM, 1-Apr-2012.)
a ≤ c    ⇒   (c ∩ (b ∪ a)) = ((c ∩ b) ∪ a)
Theorem	mlduali 1128	Inference version of dual of modular law. (Contributed by NM, 1-Apr-2012.)
a ≤ c    ⇒   ((a ∪ b) ∩ c) = (a ∪ (b ∩ c))
Theorem	ml3le 1129	Form of modular law that swaps two terms. (Contributed by NM, 1-Apr-2012.)
(a ∪ (b ∩ (c ∪ a))) ≤ (a ∪ (c ∩ (b ∪ a)))
Theorem	ml3 1130	Form of modular law that swaps two terms. (Contributed by NM, 1-Apr-2012.)
(a ∪ (b ∩ (c ∪ a))) = (a ∪ (c ∩ (b ∪ a)))
Theorem	vneulem1 1131	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(((x ∪ y) ∪ u) ∩ w) = (((x ∪ y) ∪ u) ∩ ((u ∪ w) ∩ w))
Theorem	vneulem2 1132	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(((x ∪ y) ∪ u) ∩ ((u ∪ w) ∩ w)) = ((((x ∪ y) ∩ (u ∪ w)) ∪ u) ∩ w)
Theorem	vneulem3 1133	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
((x ∪ y) ∩ (u ∪ w)) = 0    ⇒   ((((x ∪ y) ∩ (u ∪ w)) ∪ u) ∩ w) = (u ∩ w)
Theorem	vneulem4 1134	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
((x ∪ y) ∩ (u ∪ w)) = 0    ⇒   (((x ∪ y) ∪ u) ∩ w) = (u ∩ w)
Theorem	vneulem5 1135	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(((x ∪ y) ∪ u) ∩ ((x ∪ y) ∪ w)) = ((x ∪ y) ∪ (((x ∪ y) ∪ u) ∩ w))
Theorem	vneulem6 1136	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = ((c ∩ a) ∪ (b ∪ d))
Theorem	vneulem7 1137	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((c ∩ a) ∪ (b ∪ d)) = (b ∪ d)
Theorem	vneulem8 1138	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = (b ∪ d)
Theorem	vneulem9 1139	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) = ((c ∩ d) ∪ (a ∪ b))
Theorem	vneulem10 1140	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) = (a ∪ c)
Theorem	vneulem11 1141	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)) = ((c ∪ d) ∪ (a ∩ b))
Theorem	vneulem12 1142	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
(((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b))))
Theorem	vneulem13 1143	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b)))) = ((c ∩ d) ∪ (a ∩ b))
Theorem	vneulem14 1144	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((c ∩ d) ∪ (a ∩ b))
Theorem	vneulem15 1145	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)))
Theorem	vneulem16 1146	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) = ((a ∩ b) ∪ (c ∩ d))
Theorem	vneulem 1147	von Neumann's modular law lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Theorem	vneulemexp 1148	Expanded version of vneulem 1147. (Contributed by NM, 31-Mar-2011.)
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Theorem	l42modlem1 1149	Lemma for l42mod 1151.. (Contributed by NM, 8-Apr-2012.)
(((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e)) = ((a ∪ b) ∪ ((a ∪ d) ∩ (b ∪ e)))
Theorem	l42modlem2 1150	Lemma for l42mod 1151.. (Contributed by NM, 8-Apr-2012.)
((((a ∪ b) ∩ c) ∪ d) ∩ e) ≤ (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e))
Theorem	l42mod 1151	An equation that fails in OML L42 when converted to a Hilbert space equation. (Contributed by NM, 8-Apr-2012.)
((((a ∪ b) ∩ c) ∪ d) ∩ e) ≤ ((a ∪ b) ∪ ((a ∪ d) ∩ (b ∪ e)))
Theorem	modexp 1152	Expansion by modular law. (Contributed by NM, 10-Apr-2012.)
(a ∩ (b ∪ c)) = (a ∩ (b ∪ (c ∩ (a ∪ b))))
0.9.2  Arguesian law
Axiom	ax-arg 1153	The Arguesian law as an axiom. (Contributed by NM, 1-Apr-2012.)
((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2)    ⇒   ((a0 ∪ a1) ∩ (b0 ∪ b1)) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))
Theorem	dp15lema 1154	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    ⇒   ((a0 ∪ e) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
Theorem	dp15lemb 1155	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    ⇒   ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
Theorem	dp15lemc 1156	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 10-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)))
Theorem	dp15lemd 1157	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    ⇒   (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))) = (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)))
Theorem	dp15leme 1158	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    ⇒   (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)))
Theorem	dp15lemf 1159	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    ⇒   (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))) ≤ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
Theorem	dp15lemg 1160	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    ⇒   (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	dp15lemh 1161	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	dp15 1162	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (1)=>(5) (Contributed by NM, 1-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	dp53lema 1163	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
Theorem	dp53lemb 1164	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
Theorem	dp53lemc 1165	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
Theorem	dp53lemd 1166	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
Theorem	dp53leme 1167	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (a0 ∪ p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp53lemf 1168	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (a0 ∪ p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp53lemg 1169	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp53 1170	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (5)=>(3) (Contributed by NM, 2-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp35lemg 1171	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp35lemf 1172	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (a0 ∪ p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp35leme 1173	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (a0 ∪ p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp35lemd 1174	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
Theorem	dp35lemc 1175	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
Theorem	dp35lemb 1176	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
Theorem	dp35lembb 1177	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
Theorem	dp35lema 1178	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
Theorem	dp35lem0 1179	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	dp35 1180	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(5) (Contributed by NM, 12-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	dp34 1181	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(4) (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))
Theorem	dp41lema 1182	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   ((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))
Theorem	dp41lemb 1183	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   c2 = ((c2 ∩ ((a0 ∪ b0) ∪ b1)) ∩ ((a0 ∪ a1) ∪ b1))
Theorem	dp41lemc0 1184	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 4-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = ((a0 ∪ b1) ∪ ((a0 ∪ b0) ∩ (a1 ∪ b1)))
Theorem	dp41lemc 1185	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   ((c2 ∩ ((a0 ∪ b0) ∪ b1)) ∩ ((a0 ∪ a1) ∪ b1)) ≤ (c2 ∩ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
Theorem	dp41lemd 1186	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   (c2 ∩ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1))))
Theorem	dp41leme 1187	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1)))) ≤ ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
Theorem	dp41lemf 1188	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1)))))
Theorem	dp41lemg 1189	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1))))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0)))))
Theorem	dp41lemh 1190	Part of proof (4)=>(1) in Day/Pickering 1982. "By CP(a,b)". (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0))))) ≤ (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2)))))
Theorem	dp41lemj 1191	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2))))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2)))))
Theorem	dp41lemk 1192	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2))))) = ((c0 ∪ (b2 ∩ (a0 ∪ a2))) ∪ (c1 ∪ (a2 ∩ (b1 ∪ b2))))
Theorem	dp41leml 1193	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   ((c0 ∪ (b2 ∩ (a0 ∪ a2))) ∪ (c1 ∪ (a2 ∩ (b1 ∪ b2)))) = (c0 ∪ c1)
Theorem	dp41lemm 1194	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   c2 ≤ (c0 ∪ c1)
Theorem	dp41 1195	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (4)=>(1) (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   c2 ≤ (c0 ∪ c1)
Theorem	dp32 1196	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(2) (Contributed by NM, 4-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ ((a0 ∩ (a1 ∪ (c2 ∩ (c0 ∪ c1)))) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	dp23 1197	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (2)=>(3) (Contributed by NM, 4-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	xdp41 1198	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    &   p2 ≤ (a2 ∪ b2)    ⇒   c2 ≤ (c0 ∪ c1)
Theorem	xdp15 1199	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	xdp53 1200	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))