let X be set ; :: thesis: for G being Grothendieck of X holds Tarski-Class X c= G
let G be Grothendieck of X; :: thesis: Tarski-Class X c= G
G is_Tarski-Class_of X by Def4;
hence Tarski-Class X c= G by CLASSES1:def 4; :: thesis: verum