theorem :: CAT_4:54

for C being Cocartesian_category holds EmptyMS C is initial by Def26;