:: deftheorem Def5 defines Tarski-Class CLASSES1:def 5 :
for X being set
for A being Ordinal
for b₃ being set holds
( b₃ = Tarski-Class (X,A) iff ex L being Sequence st
( b₃ = last L & dom L = succ A & L . 0 = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ( { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in L . C } ) \/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) ) );