take 1Cat ({},U) ; :: thesis: not 1Cat ({},U) is U -locally_small
thus not 1Cat ({},U) is U -locally_small by Th97; :: thesis: verum