Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Posets and lattices as relations
ctsr
Next ⟩
df-ps
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
ctsr
Description:
Extend class notation with the class of all totally ordered sets.
Ref
Expression
Assertion
ctsr
class
TosetRel