Metamath Proof Explorer


Syntax definition cge-real

Description: Extend wff notation to include the 'greater than or equal to' relation, see df-gte .

Ref Expression
Assertion cge-real class