theorem Th10: :: CLASSES1:10

for X, Y being set
for A being Ordinal holds
( Y in Tarski-Class (X,(succ A)) iff ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) )