let U be Universe; :: thesis: for o, m being Element of U holds 1Cat (o,m) is U -element
let o, m be Element of U; :: thesis: 1Cat (o,m) is U -element
1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) by CAT_1:def 11;
hence 1Cat (o,m) is U -element ; :: thesis: verum