---

Step * 1 of Lemma geo-opp-side_functionality


1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. A' : Point
7. B' : Point
8. P' : Point
9. Q' : Point
10. A ≡ A'
11. B ≡ B'
12. P ≡ P'
13. Q ≡ Q'
14. (¬(∀T:Point. (P_T_Q ⇒ (¬Colinear(A;B;T))))) ∧ (¬Colinear(A;B;P)) ∧ (¬Colinear(A;B;Q))
⊢ (¬(∀T:Point. (P'_T_Q' ⇒ (¬Colinear(A';B';T))))) ∧ (¬Colinear(A';B';P')) ∧ (¬Colinear(A';B';Q'))
BY
{ (RWO "10 11 12 13" 14 THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  P  :  Point
5.  Q  :  Point
6.  A'  :  Point
7.  B'  :  Point
8.  P'  :  Point
9.  Q'  :  Point
10.  A  \mequiv{}  A'
11.  B  \mequiv{}  B'
12.  P  \mequiv{}  P'
13.  Q  \mequiv{}  Q'
14.  (\mneg{}(\mforall{}T:Point.  (P\_T\_Q  {}\mRightarrow{}  (\mneg{}Colinear(A;B;T)))))  \mwedge{}  (\mneg{}Colinear(A;B;P))  \mwedge{}  (\mneg{}Colinear(A;B;Q))
\mvdash{}  (\mneg{}(\mforall{}T:Point.  (P'\_T\_Q'  {}\mRightarrow{}  (\mneg{}Colinear(A';B';T)))))  \mwedge{}  (\mneg{}Colinear(A';B';P'))  \mwedge{}  (\mneg{}Colinear(A';B';Q'))


By

---

Latex:
(RWO  "10  11  12  13"  14  THEN  Auto)

---

Home Index