Step * of Lemma assert_of_band2

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

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

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

3
1. : 𝔹
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