---

Step * of Lemma geo-perp-all-symmetry

∀e:BasicGeometry. ∀[a,b,c,d:Point].  (ab ⊥ cd ⇒ {ba ⊥ cd ∧ ab ⊥ dc ∧ ba ⊥ dc ∧ cd ⊥ ab ∧ dc ⊥ ab ∧ cd ⊥ ba ∧ dc ⊥ ba})
BY
{ (Intros
   THEN D 0
   THEN SplitAndConcl
   THEN RepeatFor 2 (ParallelLast)
   THEN FLemma `geo-perp-in-symmetry` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry
    \mforall{}[a,b,c,d:Point].
        (ab  \mbot{}  cd  {}\mRightarrow{}  \{ba  \mbot{}  cd  \mwedge{}  ab  \mbot{}  dc  \mwedge{}  ba  \mbot{}  dc  \mwedge{}  cd  \mbot{}  ab  \mwedge{}  dc  \mbot{}  ab  \mwedge{}  cd  \mbot{}  ba  \mwedge{}  dc  \mbot{}  ba\})


By

---

Latex:
(Intros
  THEN  D  0
  THEN  SplitAndConcl
  THEN  RepeatFor  2  (ParallelLast)
  THEN  FLemma  `geo-perp-in-symmetry`  [-1]
  THEN  Auto)

---

Home Index