Metamath Proof Explorer


Syntax definition clthfstruct

Description: Extend class notation to include ordering on structures whose range is hereditarily finite.

Ref Expression
Assertion clthfstruct Could not format assertion : No typesetting found for class