theorem :: CLASSES1:28
for X, Y, Z being set st Y c= Tarski-Class X & Z c= Tarski-Class X holds
[:Y,Z:] c= Tarski-Class X