theorem :: CLASSES2:8
for X, W being set st X is epsilon-transitive & X in Tarski-Class W holds
X c= Tarski-Class W by Th7;