Metamath Proof Explorer


Syntax definition cnn0s

Description: Declare the syntax for surreal non-negative integers.

Ref Expression
Assertion cnn0s
class NN0_s