Nuprl Lemma : geo-midpoint-id3

e:BasicGeometry. ∀a,b:Point.  (b=a=a  a ≡ b)


Proof




Definitions occuring in Statement :  geo-midpoint: a=m=b basic-geometry: BasicGeometry geo-eq: a ≡ b geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  uimplies: supposing a guard: {T} subtype_rel: A ⊆B uall: [x:A]. B[x] prop: member: t ∈ T implies:  Q all: x:A. B[x] geo-midpoint: a=m=b and: P ∧ Q
Lemmas referenced :  Error :basic-geo-primitives_wf,  Error :basic-geo-structure_wf,  basic-geometry_wf subtype_rel_transitivity basic-geometry-subtype geo-point_wf geo-midpoint_wf geo-congruence-identity-sym geo-eq_inversion
Rules used in proof :  because_Cache sqequalRule independent_isectElimination instantiate applyEquality hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productElimination

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b:Point.    (b=a=a  {}\mRightarrow{}  a  \mequiv{}  b)



Date html generated: 2017_10_02-PM-04_45_57
Last ObjectModification: 2017_08_05-AM-11_45_58

Theory : euclidean!plane!geometry


Home Index