Metamath Proof Explorer


Syntax definition clts

Description: Declare the less-than relation over surreal numbers (see df-lts ).

Ref Expression
Assertion clts class < s