theorem :: CLASSES1:8

for X being set
for A being Ordinal holds Tarski-Class (X,(succ A)) = ( { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A) } ) \/ ((bool (Tarski-Class (X,A))) /\ (Tarski-Class X)) by Lm1;