Step * of Lemma eu-construction-unicity

`∀e:EuclideanPlane. ∀[Q,A,X,Y:Point].  (X = Y ∈ Point) supposing (AY=AX and Q_A_X and Q_A_Y and (¬(Q = A ∈ Point)))`
BY
`{ (Auto`
`   THEN (InstLemma `eu-five-segment` [⌜e⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜Y⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜X⌝]⋅`
`   THENM (FLemma `eu-congruence-identity` [-1] THEN Auto)`
`   )`
`   THEN Auto) }`

1
`.....antecedent..... `
`1. e : EuclideanPlane@i'`
`2. Q : Point`
`3. A : Point`
`4. X : Point`
`5. Y : Point`
`6. ¬(Q = A ∈ Point)`
`7. Q_A_Y`
`8. Q_A_X`
`9. AY=AX`
`⊢ QY=QX`

Latex:

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[Q,A,X,Y:Point].    (X  =  Y)  supposing  (AY=AX  and  Q\_A\_X  and  Q\_A\_Y  and  (\mneg{}(Q  =  A)))

By

Latex:
(Auto
THEN  (InstLemma  `eu-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
THENM  (FLemma  `eu-congruence-identity`  [-1]  THEN  Auto)
)
THEN  Auto)

Home Index