Step
*
of Lemma
geo-congruent-transitivity
No Annotations
∀e:EuclideanPlane. ∀[a,b,c,d,x,y:Point]. (ab ≅ xy) supposing (cd ≅ xy and ab ≅ cd)
BY
{ ((Auto THEN InstLemma `geo-congruent-symmetry` [⌜e⌝] ⋅ THEN Auto)
THEN D 1
THEN (Unhide THEN Auto)
THEN InstLemma `geo-axioms-imply` [⌜e⌝]⋅
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}e:EuclideanPlane. \mforall{}[a,b,c,d,x,y:Point]. (ab \mcong{} xy) supposing (cd \mcong{} xy and ab \mcong{} cd)
By
Latex:
((Auto THEN InstLemma `geo-congruent-symmetry` [\mkleeneopen{}e\mkleeneclose{}] \mcdot{} THEN Auto)
THEN D 1
THEN (Unhide THEN Auto)
THEN InstLemma `geo-axioms-imply` [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index