### Nuprl Lemma : test-prove-distinct

`∀e:EuclideanPlane. ∀A,B,C,X,Y,Z,W,U,V:Point.`
`  ((Colinear(A;B;X) ∨ A-X-B ∨ B-X-A)`
`  `` (A_B_C ∨ C_B_A)`
`  `` (Y_C_A ∨ A_C_Y)`
`  `` (ZW=AY ∨ ZW=YA)`
`  `` ZW=UV`
`  `` (¬(U = V ∈ Point)))`

Proof

Definitions occuring in Statement :  euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-colinear: `Colinear(a;b;c)` eu-between: `a-b-c` eu-congruent: `ab=cd` eu-point: `Point` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` not: `¬A` false: `False` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` or: `P ∨ Q` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q`
Lemmas referenced :  equal_wf eu-point_wf eu-congruent_wf or_wf eu-between-eq_wf eu-colinear_wf eu-between_wf euclidean-plane_wf eu-congruence-identity eu-congruence-identity-sym eu-between-eq-same eu-colinear-def eu-between-same2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination introduction extract_by_obid isectElimination setElimination rename hypothesisEquality because_Cache unionElimination equalitySymmetry hyp_replacement Error :applyLambdaEquality,  sqequalRule independent_isectElimination dependent_functionElimination productElimination

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C,X,Y,Z,W,U,V:Point.
((Colinear(A;B;X)  \mvee{}  A-X-B  \mvee{}  B-X-A)
{}\mRightarrow{}  (A\_B\_C  \mvee{}  C\_B\_A)
{}\mRightarrow{}  (Y\_C\_A  \mvee{}  A\_C\_Y)
{}\mRightarrow{}  (ZW=AY  \mvee{}  ZW=YA)
{}\mRightarrow{}  ZW=UV
{}\mRightarrow{}  (\mneg{}(U  =  V)))

Date html generated: 2016_10_26-AM-07_44_07
Last ObjectModification: 2016_07_12-AM-08_11_51

Theory : euclidean!geometry

Home Index