---

Step * of Lemma stable__geo-perp-in

∀e:BasicGeometry. ∀x:Point.  ∀[a,b,c,d:Point].  Stable{ab  ⊥x cd}
BY
{ (Auto
   THEN (Unfold `geo-perp-in` 0 THEN Unfold `implies` 0 THEN Fold `all` 0)
   THEN RepeatFor 2 ((BLemma `stable__and` THEN Auto))
   THEN RepeatFor 4 ((BLemma `stable__all` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}x:Point.    \mforall{}[a,b,c,d:Point].    Stable\{ab    \mbot{}x  cd\}


By

---

Latex:
(Auto
  THEN  (Unfold  `geo-perp-in`  0  THEN  Unfold  `implies`  0  THEN  Fold  `all`  0)
  THEN  RepeatFor  2  ((BLemma  `stable\_\_and`  THEN  Auto))
  THEN  RepeatFor  4  ((BLemma  `stable\_\_all`  THEN  Auto)))

---

Home Index