take 1Cat (U,U) ; :: thesis: 1Cat (U,U) is U -petit
thus 1Cat (U,U) is U -petit by Th61; :: thesis: verum