Description: Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tglng.p | |
|
tglng.l | |
||
tglng.i | |
||
tglnpt.g | |
||
tglnpt.a | |
||
tglnpt.x | |
||
Assertion | tglnpt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tglng.p | |
|
2 | tglng.l | |
|
3 | tglng.i | |
|
4 | tglnpt.g | |
|
5 | tglnpt.a | |
|
6 | tglnpt.x | |
|
7 | 1 2 3 | tglnunirn | |
8 | 4 7 | syl | |
9 | elssuni | |
|
10 | 5 9 | syl | |
11 | 10 6 | sseldd | |
12 | 8 11 | sseldd | |