let X be set ; :: thesis: for G being Grothendieck of X holds FinSETS c= G
let G be Grothendieck of X; :: thesis: FinSETS c= G
( FinSETS c= Tarski-Class X & Tarski-Class X c= G ) by Th44, CLASSES3:18;
hence FinSETS c= G ; :: thesis: verum