theorem Th2: :: ALTCAT_5:2
for C being category
for A being ObjectsFamily of {},C
for B being Object of C st B is terminal holds
ex P being MorphismsFamily of B,A st
( P is empty & P is projection-morphisms )