Nuprl Lemma : oriented-colinear-trans
∀e:OrientedPlane
∀[A,C,B,D:Point]. (Colinear(A;B;C) ⇒ Colinear(B;C;D) ⇒ B ≠ C ⇒ {Colinear(A;C;D) ∧ Colinear(A;B;D)})
Proof
Definitions occuring in Statement :
oriented-plane: OrientedPlane,
geo-colinear: Colinear(a;b;c),
geo-sep: a ≠ b,
geo-point: Point,
uall: ∀[x:A]. B[x],
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
euclidean-plane: EuclideanPlane,
oriented-plane: OrientedPlane
Lemmas referenced :
geo-colinear-transitivity
Rules used in proof :
hypothesis,
sqequalSubstitution,
sqequalReflexivity,
sqequalRule,
extract_by_obid,
introduction,
cut,
computationStep,
sqequalTransitivity
Latex:
\mforall{}e:OrientedPlane
\mforall{}[A,C,B,D:Point].
(Colinear(A;B;C) {}\mRightarrow{} Colinear(B;C;D) {}\mRightarrow{} B \mneq{} C {}\mRightarrow{} \{Colinear(A;C;D) \mwedge{} Colinear(A;B;D)\})
Date html generated:
2017_10_02-PM-04_46_32
Last ObjectModification:
2017_08_07-AM-10_57_23
Theory : euclidean!plane!geometry
Home
Index