---

Step * of Lemma Dtri-cycle

∀e:EuclideanPlane. ∀a,b,c:Point.
  (Dtri(e;a;b;c) ⇒ {(Dtri(e;a;c;b) ∧ Dtri(e;c;a;b)) ∧ (Dtri(e;c;b;a) ∧ Dtri(e;b;a;c)) ∧ Dtri(e;b;c;a)})
BY
{ (Auto
   THEN (FLemma `Dtri-iff-lsep` [-1] THEN Auto)
   THEN (FLemma `lsep-all-sym` [-1] THEN Auto)
   THEN D 0
   THEN GenRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Dtri(e;a;b;c)
6. a # bc
7. b # ca
8. c # ab
9. a # cb
10. b # ac
11. c # ba
⊢ Dtri(e;a;c;b)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Dtri(e;a;b;c)
6. a # bc
7. b # ca
8. c # ab
9. a # cb
10. b # ac
11. c # ba
⊢ Dtri(e;c;a;b)

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Dtri(e;a;b;c)
6. a # bc
7. b # ca
8. c # ab
9. a # cb
10. b # ac
11. c # ba
⊢ Dtri(e;c;b;a)

4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Dtri(e;a;b;c)
6. a # bc
7. b # ca
8. c # ab
9. a # cb
10. b # ac
11. c # ba
⊢ Dtri(e;b;a;c)

5
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Dtri(e;a;b;c)
6. a # bc
7. b # ca
8. c # ab
9. a # cb
10. b # ac
11. c # ba
⊢ Dtri(e;b;c;a)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.
    (Dtri(e;a;b;c)
    {}\mRightarrow{}  \{(Dtri(e;a;c;b)  \mwedge{}  Dtri(e;c;a;b))  \mwedge{}  (Dtri(e;c;b;a)  \mwedge{}  Dtri(e;b;a;c))  \mwedge{}  Dtri(e;b;c;a)\})


By

---

Latex:
(Auto
  THEN  (FLemma  `Dtri-iff-lsep`  [-1]  THEN  Auto)
  THEN  (FLemma  `lsep-all-sym`  [-1]  THEN  Auto)
  THEN  D  0
  THEN  GenRepD)

---

Home Index