---

Step * of Lemma sp-join-meet-distrib

∀[x,y,z:Sierpinski].  (x ∧ y ∨ z = x ∨ z ∧ y ∨ z ∈ Sierpinski)
BY
{ (Auto
   THEN (BLemma `Sierpinski-equal` THENA Auto)
   THEN (RWO "sp-join-is-bottom" 0 THENA Auto)
   THEN (RWO "Sierpinski-equal2" 0 THENA Auto)
   THEN (RWO "sp-meet-is-top" 0 THENA Auto)) }

1
1. x : Sierpinski
2. y : Sierpinski
3. z : Sierpinski
⊢ ((x = ⊤ ∈ Sierpinski) ∧ (y = ⊤ ∈ Sierpinski) ⇐⇒ ⊥ = ⊤ ∈ Sierpinski) ∧ (z = ⊤ ∈ Sierpinski ⇐⇒ ⊥ = ⊤ ∈ Sierpinski)
⇐⇒ (x ∨ z = ⊤ ∈ Sierpinski) ∧ (y ∨ z = ⊤ ∈ Sierpinski) ⇐⇒ ⊥ = ⊤ ∈ Sierpinski

---

Latex:

---

Latex:
\mforall{}[x,y,z:Sierpinski].    (x  \mwedge{}  y  \mvee{}  z  =  x  \mvee{}  z  \mwedge{}  y  \mvee{}  z)


By

---

Latex:
(Auto
  THEN  (BLemma  `Sierpinski-equal`  THENA  Auto)
  THEN  (RWO  "sp-join-is-bottom"  0  THENA  Auto)
  THEN  (RWO  "Sierpinski-equal2"  0  THENA  Auto)
  THEN  (RWO  "sp-meet-is-top"  0  THENA  Auto))

---

Home Index