---

Step * of Lemma ross_pnp

P:. (P  (P) //True  (P //True  P //True))
BY
{ ((Assert P:. EquivRel(P;p1,p2.True) BY RepeatFor 3 ((D 0 THEN Auto))) THEN Auto THEN Try (BackThruSomeHyp)) }

1
1. P:. EquivRel(P;p1,p2.True)
2. P : @i'
3. P  (P) //True@i
 P //True  P //True


\mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P)  //True  {}\mRightarrow{}  (P  //True  \mvee{}  \mneg{}P  //True))


By

((Assert  \mforall{}P:\mBbbP{}.  EquivRel(P;p1,p2.True)  BY
                RepeatFor  3  ((D  0  THEN  Auto)))
  THEN  Auto
  THEN  Try  (BackThruSomeHyp))



Home Index