:: deftheorem defines 1Cat CAT_1:def 11 :
for o, m being object holds 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);