Step * 1 of Lemma int_lt_to_int_upper


∀i:ℤ. ∀[A:{i + 1...} ⟶ ℙ]. (∀j:ℤ. A[j] supposing i < j ⇐⇒ ∀j:{i + 1...}. A[j])
BY
{ Auto }


Latex:


Latex:

\mforall{}i:\mBbbZ{}.  \mforall{}[A:\{i  +  1...\}  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}j:\mBbbZ{}.  A[j]  supposing  i  <  j  \mLeftarrow{}{}\mRightarrow{}  \mforall{}j:\{i  +  1...\}.  A[j])


By


Latex:
Auto




Home Index