theorem Th3: :: CLASSES1:3

for X, Y, Z being set st Y in Tarski-Class X & Z c= Y holds
Z in Tarski-Class X