:: deftheorem defines FlatCoh COHSP_1:def 2 :
for X being set holds FlatCoh X = CohSp (id X);