Step * 1 of Lemma lsep-inner-pasch-strict


1. OrientedPlane
2. Point
3. Point
4. {c:Point| ab} 
5. {p:Point| a-p-c} 
6. {q:Point| b-q-c} 
7. ∃x:{Point| (b_x_p ∧ a_x_q)}
8. ab
9. a-p-c
10. b-q-c
11. aq
12. aq
13. pb
14. pb
⊢ ∃x:{Point| (b-x-p ∧ a-x-q)}
BY
ExRepD }

1
1. OrientedPlane
2. Point
3. Point
4. {c:Point| ab} 
5. {p:Point| a-p-c} 
6. {q:Point| b-q-c} 
7. Point
8. b_x_p
9. a_x_q
10. ab
11. a-p-c
12. b-q-c
13. aq
14. aq
15. pb
16. pb
⊢ ∃x:{Point| (b-x-p ∧ a-x-q)}


Latex:


Latex:

1.  e  :  OrientedPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  \{c:Point|  c  \#  ab\} 
5.  p  :  \{p:Point|  a-p-c\} 
6.  q  :  \{q:Point|  b-q-c\} 
7.  \mexists{}x:\{Point|  (b\_x\_p  \mwedge{}  a\_x\_q)\}
8.  c  \#  ab
9.  a-p-c
10.  b-q-c
11.  c  \#  aq
12.  b  \#  aq
13.  c  \#  pb
14.  a  \#  pb
\mvdash{}  \mexists{}x:\{Point|  (b-x-p  \mwedge{}  a-x-q)\}


By


Latex:
ExRepD




Home Index