---

Step * of Lemma lt-angle-irrefl

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (abc < xyz ⇒ (¬xyz < abc))
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN (gSeparatedCasesLSep ⌜a⌝⌜b⌝⌜c⌝⋅ THENA Auto)
   THEN (gSeparatedCasesLSep ⌜x⌝⌜y⌝⌜z⌝⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. a # bc
11. x # yz
⊢ False

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. a # bc
11. ¬x # yz
12. Colinear(x;y;z)
⊢ False

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. x # yz
⊢ False

4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (abc  <  xyz  {}\mRightarrow{}  (\mneg{}xyz  <  abc))


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  (gSeparatedCasesLSep  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gSeparatedCasesLSep  \mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index