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