let U be Universe; :: thesis: for o, m being object holds 1Cat (o,m) is U -petit
let o, m be object ; :: thesis: 1Cat (o,m) is U -petit
reconsider o2 = {} , m2 = {} as Element of U by CLASSES2:56;
1Cat (o2,m2) is U -element by Th55;
hence 1Cat (o,m) is U -petit by Th60; :: thesis: verum