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