:: deftheorem Def7 defines @ YELLOW21:def 7 :
for C being lattice-wise category
for a, b being Object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds @ f = f;