theorem :: CAT_6:1

for C being CategoryStr
for f1, f2 being morphism of C st C is empty holds
not f1 |> f2 ;