Nuprl Lemma : geo-CCL-left

g:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| c} . ∀d:Point.
  ((∃p,q:Point. ((ab ≅ ap ∧ cd>cp) ∧ cd ≅ cq ∧ ab>aq))  CCL(a;b;c;d) leftof ac)


Proof




Definitions occuring in Statement :  euclidean-plane: EuclideanPlane geo-CCL: CCL(a;b;c;d) geo-congruent: ab ≅ cd geo-left: leftof bc geo-sep: b geo-gt-prim: ab>cd geo-point: Point all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q set: {x:A| B[x]} 
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] euclidean-plane: EuclideanPlane uimplies: supposing a and: P ∧ Q sq_stable: SqStable(P) exists: x:A. B[x] squash: T subtype_rel: A ⊆B guard: {T} prop:

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a  \#  c\}  .  \mforall{}d:Point.
    ((\mexists{}p,q:Point.  ((ab  \mcong{}  ap  \mwedge{}  cd>cp)  \mwedge{}  cd  \mcong{}  cq  \mwedge{}  ab>aq))  {}\mRightarrow{}  CCL(a;b;c;d)  leftof  ac)



Date html generated: 2020_05_20-AM-09_44_53
Last ObjectModification: 2019_11_13-PM-02_04_12

Theory : euclidean!plane!geometry


Home Index