---

Step * of Lemma geo-out_functionality

∀e:BasicGeometry. ∀p,a,b,p',a',b':Point.  (p ≡ p' ⇒ a ≡ a' ⇒ b ≡ b' ⇒ {out(p ab) ⇐⇒ out(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 ∧ p ≠ b ∧ (¬((¬p_a_b) ∧ (¬p_b_a)))
⊢ p' ≠ a' ∧ p' ≠ b' ∧ (¬((¬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' ∧ p' ≠ b' ∧ (¬((¬p'_a'_b') ∧ (¬p'_b'_a')))
⊢ p ≠ a ∧ p ≠ b ∧ (¬((¬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{}  \{out(p  ab)  \mLeftarrow{}{}\mRightarrow{}  out(p'  a'b')\})


By

---

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

---

Home Index