theorem :: CLASSES3:22

for X being epsilon-transitive set holds Tarski-Class X = GrothendieckUniverse X