Step
*
of Lemma
geo-line-sep-or-lemma
∀g:EuclideanParPlane. ∀l,m,p:Line.
(((∀L,M,N:Line. (L \/ M
⇒ (L \/ N ∨ M \/ N))) ∧ l \/ m)
⇒ (geo-line-sep(g;p;l) ∨ geo-line-sep(g;p;m)))
BY
{ ((Auto THEN InstHyp [⌜l⌝;⌜m⌝;⌜p⌝] (5)⋅ THEN Auto) THEN D -1) }
1
1. g : EuclideanParPlane
2. l : Line
3. m : Line
4. p : Line
5. ∀L,M,N:Line. (L \/ M
⇒ (L \/ N ∨ M \/ N))
6. l \/ m
7. l \/ p
⊢ geo-line-sep(g;p;l) ∨ geo-line-sep(g;p;m)
2
1. g : EuclideanParPlane
2. l : Line
3. m : Line
4. p : Line
5. ∀L,M,N:Line. (L \/ M
⇒ (L \/ N ∨ M \/ N))
6. l \/ m
7. m \/ p
⊢ geo-line-sep(g;p;l) ∨ geo-line-sep(g;p;m)
Latex:
Latex:
\mforall{}g:EuclideanParPlane. \mforall{}l,m,p:Line.
(((\mforall{}L,M,N:Line. (L \mbackslash{}/ M {}\mRightarrow{} (L \mbackslash{}/ N \mvee{} M \mbackslash{}/ N))) \mwedge{} l \mbackslash{}/ m)
{}\mRightarrow{} (geo-line-sep(g;p;l) \mvee{} geo-line-sep(g;p;m)))
By
Latex:
((Auto THEN InstHyp [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}] (5)\mcdot{} THEN Auto) THEN D -1)
Home
Index