let C1, C2 be Coherence_Space; :: thesis: 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 = {} ) )
let x be set ; :: thesis: ( x in C1 "\/" C2 implies ex a being Element of C1 ex b being Element of C2 st
( x = a U+ b & ( a = {} or b = {} ) ) )
assume x in C1 "\/" C2 ; :: thesis: ex a being Element of C1 ex b being Element of C2 st
( x = a U+ b & ( a = {} or b = {} ) )
then ( x in { (a U+ {}) where a is Element of C1 : verum } or x in { ({} U+ b) where b is Element of C2 : verum } ) by XBOOLE_0:def 3;
then ( ( {} in C2 & ex a being Element of C1 st x = a U+ {} ) or ( {} in C1 & ex b being Element of C2 st x = {} U+ b ) ) by COH_SP:1;
hence ex a being Element of C1 ex b being Element of C2 st
( x = a U+ b & ( a = {} or b = {} ) ) ; :: thesis: verum