Nuprl Lemma : p9-tarski-aux

∀e:HeytingGeometry. ∀a,b,c:Point.  (a # bc ⇒ ab ≅ cb ⇒ (∃x:Point. a=x=c))


Proof



Definitions occuring in Statement :  geo-triangle: a # bc,  heyting-geometry: HeytingGeometry,  geo-midpoint: a=m=b,  geo-congruent: ab ≅ cd,  geo-point: Point,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q
Lemmas referenced :  isosceles-mid-exists
Rules used in proof :  cut,  introduction,  extract_by_obid,  hypothesis
Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  ab  \mcong{}  cb  {}\mRightarrow{}  (\mexists{}x:Point.  a=x=c))


Date html generated: 2018_05_22-PM-00_21_01
Last ObjectModification: 2018_05_12-AM-10_02_49

Theory : euclidean!plane!geometry


Home Index