Metamath Proof Explorer


Syntax definition cfin3

Description: Extend class notation to include the class of III-finite sets.

Ref Expression
Assertion cfin3 class FinIII