reconsider o = {} , m = {} as Element of U by CLASSES2:56;
take 1Cat (o,m) ; :: thesis: 1Cat (o,m) is U -element
thus 1Cat (o,m) is U -element by Th55; :: thesis: verum