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.7 1101	Equation 4.15 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)
a⊥ ≤ b    ⇒   b ≤ (a →1 b)
0.8  Weakly distributive ortholattices (WDOL)
0.8.1  WDOL law
Axiom	ax-wdol 1102	The WDOL (weakly distributive ortholattice) axiom.
((a ≡ b) ∪ (a ≡ b⊥ )) = 1
Theorem	wdcom 1103	Any two variables (weakly) commute in a WDOL.
C (a, b) = 1
Theorem	wdwom 1104	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.
(a⊥ ∪ (a ∩ b)) = 1    ⇒   (b ∪ (a⊥ ∩ b⊥ )) = 1
Theorem	wddi1 1105	Prove the weak distributive law in WDOL. This is our first WDOL theorem making use of ax-wom 361, which is justified by wdwom 1104.
((a ∩ (b ∪ c)) ≡ ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi2 1106	The weak distributive law in WDOL.
(((a ∪ b) ∩ c) ≡ ((a ∩ c) ∪ (b ∩ c))) = 1
Theorem	wddi3 1107	The weak distributive law in WDOL.
((a ∪ (b ∩ c)) ≡ ((a ∪ b) ∩ (a ∪ c))) = 1
Theorem	wddi4 1108	The weak distributive law in WDOL.
(((a ∩ b) ∪ c) ≡ ((a ∪ c) ∩ (b ∪ c))) = 1
Theorem	wdid0id5 1109	Show that quantum identity follows from classical identity in a WDOL.
(a ≡0 b) = 1    ⇒   (a ≡ b) = 1
Theorem	wdid0id1 1110	Show a quantum identity that follows from classical identity in a WDOL.
(a ≡0 b) = 1    ⇒   (a ≡1 b) = 1
Theorem	wdid0id2 1111	Show a quantum identity that follows from classical identity in a WDOL.
(a ≡0 b) = 1    ⇒   (a ≡2 b) = 1
Theorem	wdid0id3 1112	Show a quantum identity that follows from classical identity in a WDOL.
(a ≡0 b) = 1    ⇒   (a ≡3 b) = 1
Theorem	wdid0id4 1113	Show a quantum identity that follows from classical identity in a WDOL.
(a ≡0 b) = 1    ⇒   (a ≡4 b) = 1
Theorem	wdka4o 1114	Show WDOL analog of WOM law.
(a ≡0 b) = 1    ⇒   ((a ∪ c) ≡0 (b ∪ c)) = 1
Theorem	wddi-0 1115	The weak distributive law in WDOL.
((a ∩ (b ∪ c)) ≡0 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-1 1116	The weak distributive law in WDOL.
((a ∩ (b ∪ c)) ≡1 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-2 1117	The weak distributive law in WDOL.
((a ∩ (b ∪ c)) ≡2 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-3 1118	The weak distributive law in WDOL.
((a ∩ (b ∪ c)) ≡3 ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wddi-4 1119	The weak distributive law in WDOL.
((a ∩ (b ∪ c)) ≡4 ((a ∩ b) ∪ (a ∩ c))) = 1
0.9  Modular ortholattices (MOL)
0.9.1  Modular law
Axiom	ax-ml 1120	The modular law axiom.
((a ∪ b) ∩ (a ∪ c)) ≤ (a ∪ (b ∩ (a ∪ c)))
Theorem	ml 1121	Modular law in equational form.
(a ∪ (b ∩ (a ∪ c))) = ((a ∪ b) ∩ (a ∪ c))
Theorem	mldual 1122	Dual of modular law.
(a ∩ (b ∪ (a ∩ c))) = ((a ∩ b) ∪ (a ∩ c))
Theorem	ml2i 1123	Inference version of modular law.
c ≤ a    ⇒   (c ∪ (b ∩ a)) = ((c ∪ b) ∩ a)
Theorem	mli 1124	Inference version of modular law.
c ≤ a    ⇒   ((a ∩ b) ∪ c) = (a ∩ (b ∪ c))
Theorem	mldual2i 1125	Inference version of dual of modular law.
a ≤ c    ⇒   (c ∩ (b ∪ a)) = ((c ∩ b) ∪ a)
Theorem	mlduali 1126	Inference version of dual of modular law.
a ≤ c    ⇒   ((a ∪ b) ∩ c) = (a ∪ (b ∩ c))
Theorem	ml3le 1127	Form of modular law that swaps two terms.
(a ∪ (b ∩ (c ∪ a))) ≤ (a ∪ (c ∩ (b ∪ a)))
Theorem	ml3 1128	Form of modular law that swaps two terms.
(a ∪ (b ∩ (c ∪ a))) = (a ∪ (c ∩ (b ∪ a)))
Theorem	vneulem1 1129	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((x ∪ y) ∪ u) ∩ w) = (((x ∪ y) ∪ u) ∩ ((u ∪ w) ∩ w))
Theorem	vneulem2 1130	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((x ∪ y) ∪ u) ∩ ((u ∪ w) ∩ w)) = ((((x ∪ y) ∩ (u ∪ w)) ∪ u) ∩ w)
Theorem	vneulem3 1131	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((x ∪ y) ∩ (u ∪ w)) = 0    ⇒   ((((x ∪ y) ∩ (u ∪ w)) ∪ u) ∩ w) = (u ∩ w)
Theorem	vneulem4 1132	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((x ∪ y) ∩ (u ∪ w)) = 0    ⇒   (((x ∪ y) ∪ u) ∩ w) = (u ∩ w)
Theorem	vneulem5 1133	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((x ∪ y) ∪ u) ∩ ((x ∪ y) ∪ w)) = ((x ∪ y) ∪ (((x ∪ y) ∪ u) ∩ w))
Theorem	vneulem6 1134	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = ((c ∩ a) ∪ (b ∪ d))
Theorem	vneulem7 1135	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((c ∩ a) ∪ (b ∪ d)) = (b ∪ d)
Theorem	vneulem8 1136	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = (b ∪ d)
Theorem	vneulem9 1137	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) = ((c ∩ d) ∪ (a ∪ b))
Theorem	vneulem10 1138	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) = (a ∪ c)
Theorem	vneulem11 1139	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)) = ((c ∪ d) ∪ (a ∩ b))
Theorem	vneulem12 1140	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b))))
Theorem	vneulem13 1141	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b)))) = ((c ∩ d) ∪ (a ∩ b))
Theorem	vneulem14 1142	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((c ∩ d) ∪ (a ∩ b))
Theorem	vneulem15 1143	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)))
Theorem	vneulem16 1144	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) = ((a ∩ b) ∪ (c ∩ d))
Theorem	vneulem 1145	von Neumann's modular law lemma. Lemma 9, Kalmbach p. 96
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Theorem	vneulemexp 1146	Expanded version of vneulem 1145.
((a ∪ b) ∩ (c ∪ d)) = 0    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Theorem	l42modlem1 1147	Lemma for l42mod 1149..
(((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e)) = ((a ∪ b) ∪ ((a ∪ d) ∩ (b ∪ e)))
Theorem	l42modlem2 1148	Lemma for l42mod 1149..
((((a ∪ b) ∩ c) ∪ d) ∩ e) ≤ (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ e))
Theorem	l42mod 1149	An equation that fails in OML L42 when converted to a Hilbert space equation.
((((a ∪ b) ∩ c) ∪ d) ∩ e) ≤ ((a ∪ b) ∪ ((a ∪ d) ∩ (b ∪ e)))
Theorem	modexp 1150	Expansion by modular law.
(a ∩ (b ∪ c)) = (a ∩ (b ∪ (c ∩ (a ∪ b))))
0.9.2  Arguesian law
Axiom	ax-arg 1151	The Arguesian law as an axiom.
((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2)    ⇒   ((a0 ∪ a1) ∩ (b0 ∪ b1)) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))
Theorem	dp15lema 1152	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   e = (b0 ∩ (a0 ∪ p0))    ⇒   ((a0 ∪ e) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
Theorem	dp15lemb 1153	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1154	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1155	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1156	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1157	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1158	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1159	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1160	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)
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 1161	Part of proof (5)=>(3) in Day/Pickering 1982.
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 1162	Part of proof (5)=>(3) in Day/Pickering 1982.
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 1163	Part of proof (5)=>(3) in Day/Pickering 1982.
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 1164	Part of proof (5)=>(3) in Day/Pickering 1982.
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 1165	Part of proof (5)=>(3) in Day/Pickering 1982.
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 1166	Part of proof (5)=>(3) in Day/Pickering 1982.
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 1167	Part of proof (5)=>(3) in Day/Pickering 1982.
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 1168	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)
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 1169	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1170	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1171	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1172	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1173	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1174	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1175	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1176	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1177	Part of proof (3)=>(5) in Day/Pickering 1982.
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 1178	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)
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 1179	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)
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 1180	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1181	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1182	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1183	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1184	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1185	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1186	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1187	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1188	Part of proof (4)=>(1) in Day/Pickering 1982. "By CP(a,b)".
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 1189	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1190	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1191	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1192	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1193	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)
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 1194	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)
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 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). (2)=>(3)
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 1196	Part of proof (4)=>(1) in Day/Pickering 1982.
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 1197	Part of proof (1)=>(5) in Day/Pickering 1982.
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 1198	Part of proof (5)=>(3) in Day/Pickering 1982.
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	xxdp41 1199	Part of proof (4)=>(1) in Day/Pickering 1982.
p2 ≤ (a2 ∪ b2)    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   c2 ≤ (c0 ∪ c1)
Theorem	xxdp15 1200	Part of proof (1)=>(5) in Day/Pickering 1982.
p2 ≤ (a2 ∪ b2)    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))