Metamath Proof Explorer


Syntax definition carchi

Description: Class notation for the Archimedean property.

Ref Expression
Assertion carchi class Archi