theorem Th9: :: CLASSES1:9

for X being set
for A being Ordinal st A <> {} & A is limit_ordinal holds
Tarski-Class (X,A) = { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) }