Step
*
of Lemma
member-int_seg
∀[i,j,x:ℤ].  (x ∈ {i..j-}) supposing ((i ≤ x) and x < j)
BY
{ Auto }
Latex:
Latex:
\mforall{}[i,j,x:\mBbbZ{}].    (x  \mmember{}  \{i..j\msupminus{}\})  supposing  ((i  \mleq{}  x)  and  x  <  j)
By
Latex:
Auto
Home
Index