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 Element of U )
reconsider m = {} as Element of U by CLASSES2:56;
consider o being set such that
A1: not o in U by CLASSES4:83;
set C = 1Cat (o,m);

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

thus 1Cat (o,m) is U -petit by Th61; :: thesis: ( the carrier of (1Cat (o,m)) is not Element of U & the carrier' of (1Cat (o,m)) is Element of U )
1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) by CAT_1:def 11;
hence ( the carrier of (1Cat (o,m)) is not Element of U & the carrier' of (1Cat (o,m)) is 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 Element of U ) ; :: thesis: verum