Nuprl Definition : triangle-axiom1

triangle-axiom1(g) ==  ∀p,q,r:Point. ∀s:p ≠ q. ∀s1:q ≠ r.  (r ≠ p ∨ q ⇒ p ≠ q ∨ r)


Definitions occuring in Statement :  pgeo-join: p ∨ q,  pgeo-psep: a ≠ b,  pgeo-plsep: a ≠ b,  pgeo-point: Point,  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  pgeo-point: Point,  all: ∀x:A. B[x],  pgeo-psep: a ≠ b,  implies: P ⇒ Q,  pgeo-plsep: a ≠ b,  pgeo-join: p ∨ q
FDL editor aliases :  triangle-axiom1
Latex:
triangle-axiom1(g)  ==    \mforall{}p,q,r:Point.  \mforall{}s:p  \mneq{}  q.  \mforall{}s1:q  \mneq{}  r.    (r  \mneq{}  p  \mvee{}  q  {}\mRightarrow{}  p  \mneq{}  q  \mvee{}  r)


Date html generated: 2018_05_22-PM-00_40_08
Last ObjectModification: 2017_11_03-PM-01_44_01

Theory : euclidean!plane!geometry


Home Index