Step * of Lemma eu-congruent-iff-length

e:EuclideanPlane. ∀[a,b,c,d:Point].  uiff(ab=cd;|ab| |cd| ∈ {p:Point| O_X_p} )
BY
((Auto THEN Try ((FLemma `eu-seg-congruent-iff-length` [-1] THEN Auto)))
   THEN BLemma `eu-seg-congruent-iff-length`
   THEN Auto
   THEN RepUR ``eu-seg-congruent`` 0
   THEN Auto) }


Latex:


Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c,d:Point].    uiff(ab=cd;|ab|  =  |cd|)


By


Latex:
((Auto  THEN  Try  ((FLemma  `eu-seg-congruent-iff-length`  [-1]  THEN  Auto)))
  THEN  BLemma  `eu-seg-congruent-iff-length`
  THEN  Auto
  THEN  RepUR  ``eu-seg-congruent``  0
  THEN  Auto)




Home Index