Step * 1 1 1 1 of Lemma real-weak-Markov


1. : ℝ
2. : ℝ
3. ∀z:ℝ((¬(z x)) ∨ (z y)))
4. : ℝ
5. ¬((z y) x)
6. ¬((z x) x)
⊢ (|x y| z)) ∨ (z r0))
BY
((OrRight THEN Auto) THEN ParallelLast⋅}


Latex:


Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  \mforall{}z:\mBbbR{}.  ((\mneg{}(z  =  x))  \mvee{}  (\mneg{}(z  =  y)))
4.  z  :  \mBbbR{}
5.  \mneg{}((z  +  y)  =  x)
6.  \mneg{}((z  +  x)  =  x)
\mvdash{}  (\mneg{}(|x  -  y|  =  z))  \mvee{}  (\mneg{}(z  =  r0))


By


Latex:
((OrRight  THEN  Auto)  THEN  ParallelLast\mcdot{})




Home Index