---

Step * of Lemma geo-ge-symmetry

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab ≥ cd ⇒ {ba ≥ cd ∧ ab ≥ dc ∧ ba ≥ dc})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN Try ((RepeatFor 2 (ParallelOp -2)
              THEN RepeatFor 2 (ParallelLast)
              THEN Auto
              THEN FLemma `geo-congruent-full-symmetry` [-2]
              THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab ≥ cd
⊢ ba ≥ cd

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab ≥ cd
7. ba ≥ cd
⊢ ab ≥ dc

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab ≥ cd
7. ba ≥ cd
8. ab ≥ dc
⊢ ba ≥ dc

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab  \mgeq{}  cd  {}\mRightarrow{}  \{ba  \mgeq{}  cd  \mwedge{}  ab  \mgeq{}  dc  \mwedge{}  ba  \mgeq{}  dc\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  Try  ((RepeatFor  2  (ParallelOp  -2)
                        THEN  RepeatFor  2  (ParallelLast)
                        THEN  Auto
                        THEN  FLemma  `geo-congruent-full-symmetry`  [-2]
                        THEN  Auto)))

---

Home Index