Description: Lemma for poimir stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | poimir.0 | |
|
poimirlem22.s | |
||
poimirlem22.1 | |
||
poimirlem22.2 | |
||
poimirlem22.3 | |
||
poimirlem21.4 | |
||
Assertion | poimirlem21 | |