Metamath Proof Explorer


Syntax definition cnt

Description: Extend class notation with interior of a subset of a topology base set.

Ref Expression
Assertion cnt class int