Nuprl Lemma : eu-bisect-angle
∀e:EuclideanPlane. ∀a,b,c:Point.
  ((¬(a = b ∈ Point)) 
⇒ (¬(b = c ∈ Point)) 
⇒ (∃d:Point. ((¬(d = a ∈ Point)) ∧ (¬(d = c ∈ Point)) ∧ abd = dbc)))
Error : references
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.
    ((\mneg{}(a  =  b))  {}\mRightarrow{}  (\mneg{}(b  =  c))  {}\mRightarrow{}  (\mexists{}d:Point.  ((\mneg{}(d  =  a))  \mwedge{}  (\mneg{}(d  =  c))  \mwedge{}  abd  =  dbc)))
Date html generated:
2017_02_21-AM-10_18_48
Last ObjectModification:
2016_06_09-PM-03_04_35
Theory : euclidean!geometry
Home
Index