theorem Th4: :: ALTCAT_6:4

for I being set
for A being ObjectsFamily of I,(EnsCat {{}})
for o being Object of (EnsCat {{}})
for P being MorphismsFamily of A,o st P = I --> {} holds
( P is feasible & P is coprojection-morphisms )