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

Tarski-Class X is Grothendieck of X by Def4, CLASSES1:2;

hence Tarski-Class X = GrothendieckUniverse X by GDef, Th18; :: thesis: verum