set GX = the Grothendieck of NAT ;
NAT in the Grothendieck of NAT by CLASSES3:def 4;
hence not for b₁ being Universe holds b₁ is denumerable by Th20; :: thesis: verum