:: deftheorem Def5 defines UNIVERSE CLASSES2:def 5 :
for A being Ordinal
for b₂ being set holds
( b₂ = UNIVERSE A iff ex L being Sequence st
( b₂ = last L & dom L = succ A & L . 0 = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) );