theorem Th87: :: COHSP_1:87

for C1, C2 being Coherence_Space
for x being set st x in C1 "\/" C2 holds
ex a being Element of C1 ex b being Element of C2 st
( x = a U+ b & ( a = {} or b = {} ) )