Nuprl Definition : euclid5

euclid5(e) ==
  ∀P,Q,R,S,T,U:Point.  (P-T-Q ⇒ R-T-S ⇒ Q-U-R ⇒ P # QS ⇒ PT ≅ QT ⇒ RT ≅ ST ⇒ (∃I:Point. (S-Q-I ∧ P-U-I)))


Definitions occuring in Statement :  geo-lsep: a # bc,  geo-strict-between: a-b-c,  geo-congruent: ab ≅ cd,  geo-point: Point,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  geo-lsep: a # bc,  implies: P ⇒ Q,  geo-congruent: ab ≅ cd,  exists: ∃x:A. B[x],  geo-point: Point,  and: P ∧ Q,  geo-strict-between: a-b-c
FDL editor aliases :  euclid5 euclid5 euclid5
Latex:
euclid5(e)  ==
    \mforall{}P,Q,R,S,T,U:Point.
        (P-T-Q  {}\mRightarrow{}  R-T-S  {}\mRightarrow{}  Q-U-R  {}\mRightarrow{}  P  \#  QS  {}\mRightarrow{}  PT  \mcong{}  QT  {}\mRightarrow{}  RT  \mcong{}  ST  {}\mRightarrow{}  (\mexists{}I:Point.  (S-Q-I  \mwedge{}  P-U-I)))


Date html generated: 2018_05_22-PM-00_12_45
Last ObjectModification: 2018_01_10-PM-03_25_28

Theory : euclidean!plane!geometry


Home Index