Metamath Proof Explorer


Syntax definition cupword

Description: Extend class notation to include the set of strictly increasing sequences.

Ref Expression
Assertion cupword
class UpWord S