Step * 1 1 of Lemma left-convex3


1. OrientedPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. leftof pb
8. Colinear(p;b;z)
9. z_q_x
10. p ≠ b
⊢ leftof pb
BY
((InstLemma `geo-sep-or` [⌜e⌝; ⌜p⌝;⌜b⌝;⌜z⌝]⋅ THENA Auto) THEN -1) }

1
1. OrientedPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. leftof pb
8. Colinear(p;b;z)
9. z_q_x
10. p ≠ b
11. p ≠ z
⊢ leftof pb

2
1. OrientedPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. leftof pb
8. Colinear(p;b;z)
9. z_q_x
10. p ≠ b
11. b ≠ z
⊢ leftof pb


Latex:


Latex:

1.  e  :  OrientedPlane
2.  b  :  Point
3.  p  :  Point
4.  q  :  Point
5.  x  :  Point
6.  z  :  Point
7.  q  leftof  pb
8.  Colinear(p;b;z)
9.  z\_q\_x
10.  p  \mneq{}  b
\mvdash{}  x  leftof  pb


By


Latex:
((InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)




Home Index