theorem Th21: :: CAT_6:21

for C being discrete CategoryStr
for f1, f2 being morphism of C st f1 |> f2 holds
( f1 = f2 & f1 (*) f2 = f2 )