theorem :: CLASSES1:7

for X being set holds Tarski-Class (X,{}) = {X} by Lm1;