---

Step * of Lemma member-less_than'

∀[a,b:ℤ].  Ax ∈ less_than'(a;b) supposing less_than'(a;b)
BY
{ TACTIC:((UnivCD THENA Auto) THEN All (Unfold `less_than\'`)⋅) }

1
1. a : ℤ
2. b : ℤ
3. if (a) < (b)  then True  else False
⊢ Ax ∈ if (a) < (b)  then True  else False

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].    Ax  \mmember{}  less\_than'(a;b)  supposing  less\_than'(a;b)


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  All  (Unfold  `less\_than\mbackslash{}'`)\mcdot{})

---

Home Index