theorem :: ALTCAT_5:5

for C being category
for A being ObjectsFamily of {},C
for B being Object of C st B is terminal holds
B is A -CatProduct-like