Metamath Proof Explorer


Syntax definition cresub

Description: Real number subtraction.

Ref Expression
Assertion cresub
class -R