### Nuprl Lemma : eu-out-refl

`∀e:EuclideanPlane. ∀a,b,c:Point.  (out(a bc) `` out(a cb))`

Proof

Definitions occuring in Statement :  eu-out: `out(p ab)` euclidean-plane: `EuclideanPlane` eu-point: `Point` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` eu-out: `out(p ab)` and: `P ∧ Q` cand: `A c∧ B` not: `¬A` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane`
Lemmas referenced :  and_wf not_wf eu-between-eq_wf eu-out_wf eu-point_wf euclidean-plane_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut hypothesis independent_pairFormation independent_functionElimination lemma_by_obid isectElimination setElimination rename hypothesisEquality because_Cache

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (out(a  bc)  {}\mRightarrow{}  out(a  cb))

Date html generated: 2016_05_18-AM-06_42_03
Last ObjectModification: 2015_12_28-AM-09_23_32

Theory : euclidean!geometry

Home Index