Metamath Proof Explorer


Syntax definition csubs

Description: Declare the syntax for surreal subtraction.

Ref Expression
Assertion csubs class -s