---

Step * of Lemma geo-out-strict_functionality

∀e:BasicGeometry. ∀p,a,b,p',a',b':Point.
  (p ≡ p' ⇒ a ≡ a' ⇒ b ≡ b' ⇒ {geo-out-strict(e;p;a;b) ⇐⇒ geo-out-strict(e;p';a';b')})
BY
{ (Auto THEN (D 0 THEN Auto) THEN ParallelLast) }

1
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. p' : Point
6. a' : Point
7. b' : Point
8. p ≡ p'
9. a ≡ a'
10. b ≡ b'
11. ¬((¬p-a-b) ∧ (¬p-b-a))
⊢ ¬((¬p'-a'-b') ∧ (¬p'-b'-a'))

2
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. p' : Point
6. a' : Point
7. b' : Point
8. p ≡ p'
9. a ≡ a'
10. b ≡ b'
11. ¬((¬p'-a'-b') ∧ (¬p'-b'-a'))
⊢ ¬((¬p-a-b) ∧ (¬p-b-a))

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,a,b,p',a',b':Point.
    (p  \mequiv{}  p'  {}\mRightarrow{}  a  \mequiv{}  a'  {}\mRightarrow{}  b  \mequiv{}  b'  {}\mRightarrow{}  \{geo-out-strict(e;p;a;b)  \mLeftarrow{}{}\mRightarrow{}  geo-out-strict(e;p';a';b')\})


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  ParallelLast)

---

Home Index