---

Step * of Lemma not-equal-implies-less

∀[T:Type]. ∀x,y:T.  ((¬(x = y ∈ T)) ⇒ (x < y ∨ y < x)) supposing T ⊆r ℤ
BY
{ (Auto
   THEN (Assert ¬(x = y ∈ ℤ) BY
               RepeatFor 2 (ParallelLast))
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜x = a ∈ ℤ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜y = b ∈ ℤ⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. a : ℤ
2. b : ℤ
⊢ (¬(a = b ∈ ℤ)) ⇒ (a < b ∨ b < a)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x,y:T.    ((\mneg{}(x  =  y))  {}\mRightarrow{}  (x  <  y  \mvee{}  y  <  x))  supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(Auto
  THEN  (Assert  \mneg{}(x  =  y)  BY
                          RepeatFor  2  (ParallelLast))
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}x  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}y  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index