Nuprl Lemma : geo-left-transitivity
∀g:OrientedPlane. ∀t,s,p,q,r:Point.
(p leftof ts ⇒ q leftof ts ⇒ r leftof ts ⇒ q leftof tp ⇒ r leftof tq ⇒ (¬r leftof pt))
Proof
Definitions occuring in Statement :
oriented-plane: OrientedPlane,
geo-left: a leftof bc,
geo-point: Point,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q
Lemmas referenced :
left-transitivity
Rules used in proof :
hypothesis,
extract_by_obid,
introduction,
cut
Latex:
\mforall{}g:OrientedPlane. \mforall{}t,s,p,q,r:Point.
(p leftof ts {}\mRightarrow{} q leftof ts {}\mRightarrow{} r leftof ts {}\mRightarrow{} q leftof tp {}\mRightarrow{} r leftof tq {}\mRightarrow{} (\mneg{}r leftof pt))
Date html generated:
2017_10_02-PM-06_49_29
Last ObjectModification:
2017_08_06-PM-07_29_20
Theory : euclidean!plane!geometry
Home
Index