Description: Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | oppgbas.1 | ||
oppgtset.2 | |||
Assertion | oppgtset |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oppgbas.1 | ||
2 | oppgtset.2 | ||
3 | df-tset | ||
4 | 9nn | ||
5 | 2re | ||
6 | 2lt9 | ||
7 | 5 6 | gtneii | |
8 | 1 3 4 7 | oppglem | |
9 | 2 8 | eqtri |