### Nuprl Lemma : eu-between-eq-seg-eq

e:EuclideanPlane. ∀a,b,c,a',b',c':Point.  (a_b_c  a'_b'_c'  ab=a'b'  ac=a'c'  bc=b'c')

Proof

Definitions occuring in Statement :  euclidean-plane: EuclideanPlane eu-between-eq: a_b_c eu-congruent: ab=cd eu-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] euclidean-plane: EuclideanPlane uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q squash: T true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis independent_isectElimination because_Cache dependent_functionElimination productElimination equalityTransitivity equalitySymmetry equalityEquality setEquality applyEquality lambdaEquality imageElimination natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,a',b',c':Point.    (a\_b\_c  {}\mRightarrow{}  a'\_b'\_c'  {}\mRightarrow{}  ab=a'b'  {}\mRightarrow{}  ac=a'c'  {}\mRightarrow{}  bc=b'c')

Date html generated: 2016_05_18-AM-06_43_49
Last ObjectModification: 2016_01_16-PM-10_29_04

Theory : euclidean!geometry

Home Index