theorem :: CLASSES2:66

for A being Ordinal holds UNIVERSE (succ A) = Tarski-Class (UNIVERSE A) by Lm6;