Step
*
of Lemma
i-member_functionality
∀I:Interval. ∀a,b:ℝ.  a ∈ I 
⇐⇒ b ∈ I supposing a = b
BY
{ ((D 0 THENA Auto)
   THEN RepeatFor 2 (D 1)
   THEN D 2
   THEN RepUR ``i-member`` 0
   THEN Try (DVar `x')
   THEN Reduce 0
   THEN Try (DVar `x1')
   THEN Reduce 0
   THEN Auto) }
Latex:
Latex:
\mforall{}I:Interval.  \mforall{}a,b:\mBbbR{}.    a  \mmember{}  I  \mLeftarrow{}{}\mRightarrow{}  b  \mmember{}  I  supposing  a  =  b
By
Latex:
((D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  1)
  THEN  D  2
  THEN  RepUR  ``i-member``  0
  THEN  Try  (DVar  `x')
  THEN  Reduce  0
  THEN  Try  (DVar  `x1')
  THEN  Reduce  0
  THEN  Auto)
Home
Index