set G = the Grothendieck of {} ;
{} in the Grothendieck of {} by CLASSES3:def 4;
hence not for b₁ being Grothendieck holds b₁ is empty ; :: thesis: verum