Step
*
of Lemma
less_than_transitivity
∀[x,y,z:ℤ]. (x < z) supposing (y < z and x < y)
BY
{ TACTIC:((UnivCD THENA Auto) THEN TACTIC:(All (Unfold `less_than`) THEN D -2 THEN ParallelLast THEN Auto)) }
1
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. less_than'(x;y)
5. x ∈ ℤ
6. y ∈ ℤ
7. less_than'(y;z)
8. y ∈ ℤ
9. z ∈ ℤ
⊢ less_than'(x;z)
Latex:
Latex:
\mforall{}[x,y,z:\mBbbZ{}]. (x < z) supposing (y < z and x < y)
By
Latex:
TACTIC:((UnivCD THENA Auto)
THEN TACTIC:(All (Unfold `less\_than`) THEN D -2 THEN ParallelLast THEN Auto)
)
Home
Index