Description: Lemma for poimir , establishing that away from the opposite vertex the walks in poimirlem9 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | poimir.0 | |
|
poimirlem22.s | |
||
poimirlem9.1 | |
||
poimirlem9.2 | |
||
poimirlem9.3 | |
||
Assertion | poimirlem8 | |