:: deftheorem defines -CatProduct-like ALTCAT_5:def 9 :
for C being category
for I being set
for A being ObjectsFamily of I,C
for B being Object of C holds
( B is A -CatProduct-like iff ex P being MorphismsFamily of B,A st
( P is feasible & P is projection-morphisms ) );