let C1, C2 be Coherence_Space; :: thesis: for x, y being set holds
( x U+ y in C1 "\/" C2 iff ( ( x in C1 & y = {} ) or ( x = {} & y in C2 ) ) )
let x, y be set ; :: thesis: ( x U+ y in C1 "\/" C2 iff ( ( x in C1 & y = {} ) or ( x = {} & y in C2 ) ) )
A1: now :: thesis: ( ex a being Element of C1 st x U+ y = a U+ {} implies ( x in C1 & y = {} ) )
given a being Element of C1 such that A2: x U+ y = a U+ {} ; :: thesis: ( x in C1 & y = {} )
x = a by A2, Th80;
hence ( x in C1 & y = {} ) by A2, Th80; :: thesis: verum
end;
A3: now :: thesis: ( ex a being Element of C2 st x U+ y = {} U+ a implies ( y in C2 & x = {} ) )
given a being Element of C2 such that A4: x U+ y = {} U+ a ; :: thesis: ( y in C2 & x = {} )
y = a by A4, Th80;
hence ( y in C2 & x = {} ) by A4, Th80; :: thesis: verum
end;
( x U+ y in C1 "\/" C2 iff ( x U+ y in { (a U+ {}) where a is Element of C1 : verum } or x U+ y in { ({} U+ b) where b is Element of C2 : verum } ) ) by XBOOLE_0:def 3;
hence ( x U+ y in C1 "\/" C2 iff ( ( x in C1 & y = {} ) or ( x = {} & y in C2 ) ) ) by A1, A3; :: thesis: verum