:: deftheorem defines feasible ALTCAT_5:def 4 :
for C being non empty AltCatStr
for I being set
for A being ObjectsFamily of I,C
for B being Object of C
for P being MorphismsFamily of B,A holds
( P is feasible iff for i being set st i in I holds
ex o being Object of C st
( o = A . i & P . i in <^B,o^> ) );