theorem :: CLASSES4:48

for n being Element of FinSETS holds GrothendieckUniverse n = FinSETS