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