Description: The half-line relation commutes. Theorem 6.6 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ishlg.p | |
|
ishlg.i | |
||
ishlg.k | |
||
ishlg.a | |
||
ishlg.b | |
||
ishlg.c | |
||
ishlg.g | |
||
hlcomd.1 | |
||
Assertion | hlcomd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ishlg.p | |
|
2 | ishlg.i | |
|
3 | ishlg.k | |
|
4 | ishlg.a | |
|
5 | ishlg.b | |
|
6 | ishlg.c | |
|
7 | ishlg.g | |
|
8 | hlcomd.1 | |
|
9 | 1 2 3 4 5 6 7 | hlcomb | |
10 | 8 9 | mpbid | |