theorem :: CLASSES2:69

for U being Universe holds
( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U )