let U be Universe; :: thesis: not for C being U -petit Category holds C is U -element
assume A1: for C being U -petit Category holds C is U -element ; :: thesis: contradiction
consider C being U -petit Category such that
the carrier of C is Element of U and
A2: the carrier' of C is not Element of U by Th64;
not C is U -element by A2;
hence contradiction by A1; :: thesis: verum