set C = 1Cat (U,U);
not 1Cat (U,U) is U -small

proof

assume 1Cat (U,U) is U -small ; :: thesis: contradiction
then {U} is Element of U by COMMACAT:3;
then U in U by Th18;
hence contradiction ; :: thesis: verum

end;

hence not for b₁ being Category holds b₁ is U -small ; :: thesis: verum