Metamath Proof Explorer


Syntax definition cslt

Description: Declare the less than relationship over surreal numbers (see df-slt ).

Ref Expression
Assertion cslt class < s