theorem Th83: :: COHSP_1:83

for C1, C2 being Coherence_Space
for x being object holds
( x in C1 "/\" C2 iff ex a being Element of C1 ex b being Element of C2 st x = a U+ b ) ;