Step
*
2
1
of Lemma
canonical-parallel2
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
3. a : Point
4. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
⊢ f a c ∈ ∃l:{l:LINE| a I l}  [(l = c ∈ (l,m:Line//l || m))]
BY
{ Assert ⌜f a c ∈ {l:LINE| a I l} ⌝⋅ }
1
.....assertion..... 
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
3. a : Point
4. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
⊢ f a c ∈ {l:LINE| a I l} 
2
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
3. a : Point
4. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
5. f a c ∈ {l:LINE| a I l} 
⊢ f a c ∈ ∃l:{l:LINE| a I l}  [(l = c ∈ (l,m:Line//l || m))]
Latex:
Latex:
1.  e  :  EuclideanParPlane
2.  c  :  l,m:Line//l  ||  m
3.  a  :  Point
4.  f  :  \mforall{}p:Point.  \mforall{}l:Line.    (\mexists{}m:Line  [(l  ||  m  \mwedge{}  p  I  m)])
\mvdash{}  f  a  c  \mmember{}  \mexists{}l:\{l:LINE|  a  I  l\}    [(l  =  c)]
By
Latex:
Assert  \mkleeneopen{}f  a  c  \mmember{}  \{l:LINE|  a  I  l\}  \mkleeneclose{}\mcdot{}
Home
Index