theorem :: CLASSES5:26

for x being object holds
( x is Set of FinSETS iff x is FinSet )