---

Step * of Lemma assert_of_band

∀p:𝔹. ∀q:⋂:↑p. 𝔹.  uiff(↑(p ∧b q);(↑p) ∧ (↑q))
BY
{ ((D 0 THENA Auto) THEN BoolCase ⌜p⌝⋅) }

1
.....wf..... 
1. p : 𝔹
⊢ p ∈ 𝔹

2
1. p : 𝔹
2. ↑p
⊢ ∀q:⋂:True. 𝔹. uiff(↑q;True ∧ (↑q))

3
1. p : 𝔹
2. ¬↑p
⊢ ∀q:⋂:False. 𝔹. uiff(False;False ∧ (↑q))

---

Latex:

---

Latex:
\mforall{}p:\mBbbB{}.  \mforall{}q:\mcap{}:\muparrow{}p.  \mBbbB{}.    uiff(\muparrow{}(p  \mwedge{}\msubb{}  q);(\muparrow{}p)  \mwedge{}  (\muparrow{}q))


By

---

Latex:
((D  0  THENA  Auto)  THEN  BoolCase  \mkleeneopen{}p\mkleeneclose{}\mcdot{})

---

Home Index