---

Step * 1 1 of Lemma ross_pnp


1. P:. EquivRel(P;p1,p2.True)
2. P : @i'
3. x : P  (P) //True@i
 P //True  P //True
BY
{ UseWitness x }

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



1.  \mforall{}P:\mBbbP{}.  EquivRel(P;p1,p2.True)
2.  P  :  \mBbbP{}@i'
3.  x  :  P  \mvee{}  (\mneg{}P)  //True@i
\mvdash{}  P  //True  \mvee{}  \mneg{}P  //True


By

UseWitness  \mkleeneopen{}x\mkleeneclose{}\mcdot{}



Home Index