Nuprl Lemma : opp-side-congruence-lemma

∀e:EuclideanPlane
  ∀[a,b,A,B,c,d,C,D:Point].
    (cd ≅ CD) supposing 
       (C leftof AB and 
       D leftof BA and 
       c leftof ab and 
       d leftof ba and 
       a # b and 
       bd ≅ BD and 
       ad ≅ AD and 
       bc ≅ BC and 
       ac ≅ AC and 
       ab ≅ AB)


Proof



Definitions occuring in Statement :  euclidean-plane: EuclideanPlane,  geo-congruent: ab ≅ cd,  geo-left: a leftof bc,  geo-sep: a # b,  geo-point: Point,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x]
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  and: P ∧ Q,  cand: A c∧ B,  implies: P ⇒ Q,  guard: {T},  basic-geometry: BasicGeometry,  subtype_rel: A ⊆r B,  prop: ℙ,  geo-congruent: ab ≅ cd,  not: ¬A,  false: False
Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,A,B,c,d,C,D:Point].
        (cd  \mcong{}  CD)  supposing 
              (C  leftof  AB  and 
              D  leftof  BA  and 
              c  leftof  ab  and 
              d  leftof  ba  and 
              a  \#  b  and 
              bd  \mcong{}  BD  and 
              ad  \mcong{}  AD  and 
              bc  \mcong{}  BC  and 
              ac  \mcong{}  AC  and 
              ab  \mcong{}  AB)


Date html generated: 2020_05_20-AM-10_07_57
Last ObjectModification: 2020_01_13-PM-04_05_43

Theory : euclidean!plane!geometry


Home Index