let U be Universe; :: thesis: ex C being U -petit Category st
( the carrier of C is not Element of U & the carrier' of C is not Element of U )
consider o being set such that
A1: not o in U by CLASSES4:83;
set C = 1Cat (o,o);

now :: thesis: ( 1Cat (o,o) is U -petit & the carrier of (1Cat (o,o)) is not Element of U & the carrier' of (1Cat (o,o)) is not Element of U )

thus 1Cat (o,o) is U -petit by Th61; :: thesis: ( the carrier of (1Cat (o,o)) is not Element of U & the carrier' of (1Cat (o,o)) is not Element of U )
1Cat (o,o) = CatStr(# {o},{o},(o :-> o),(o :-> o),((o,o) :-> o) #) by CAT_1:def 11;
hence ( the carrier of (1Cat (o,o)) is not Element of U & the carrier' of (1Cat (o,o)) is not Element of U ) by A1, Th18; :: thesis: verum

end;

hence ex C being U -petit Category st
( the carrier of C is not Element of U & the carrier' of C is not Element of U ) ; :: thesis: verum