:: deftheorem defines "\/" COHSP_1:def 24 :
for C1, C2 being Coherence_Space holds C1 "\/" C2 = { (a U+ {}) where a is Element of C1 : verum } \/ { ({} U+ b) where b is Element of C2 : verum } ;