Description: Reverse closure for a terminal object: If a class has a terminal object, the class is a category. (Contributed by AV, 4-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | termorcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-termo | |
|
2 | 1 | mptrcl | |