theorem Th4: :: ALTCAT_5:4

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