for A being Ordinal
for W being set st A in Tarski-Class W holds
( succ A in Tarski-Class W & A c= Tarski-Class W ) by Th5;