let X be epsilon-transitive set ; :: thesis: Tarski-Class X = GrothendieckUniverse X
Tarski-Class X is Grothendieck of X by Def4, CLASSES1:2;
hence Tarski-Class X = GrothendieckUniverse X by GDef, Th18; :: thesis: verum