Metamath Proof Explorer


Syntax definition clsw

Description: Extend class notation with the Last Symbol of a word.

Ref Expression
Assertion clsw class lastS