theorem Th4: :: ALTCAT_4:4

for C being non empty with_units AltCatStr
for o being Object of C holds
( idm o is epi & idm o is mono )