theorem Th13: :: CLASSES1:13

for X, x being set
for A being Ordinal st A <> {} & A is limit_ordinal holds
( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) )