for x being set st x in FinSETS holds
x is finite