Step
*
of Lemma
classical-excluded-middle
∀P:ℙ. {P ∨ (¬P)}
BY
{ Auto }
1
1. P : ℙ@i'
⊢ {P ∨ (¬P)}
Latex:
Latex:
\mforall{}P:\mBbbP{}.  \{P  \mvee{}  (\mneg{}P)\}
By
Latex:
Auto
Home
Index