Metamath Proof Explorer


Syntax definition ccl

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

Ref Expression
Assertion ccl class cls