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

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