theorem :: CLASSES4:2

REAL * = { X where X is FinSequence of REAL : verum }