let C1, C2 be Coherence_Space; :: thesis: for x, y being set holds
( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) )
let x, y be set ; :: thesis: ( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) )
now :: thesis: ( ex a being Element of C1 ex b being Element of C2 st x U+ y = a U+ b implies ex a being Element of C1 ex b being Element of C2 st
( x = a & y = b ) )
given a being Element of C1, b being Element of C2 such that A1: x U+ y = a U+ b ; :: thesis: ex a being Element of C1 ex b being Element of C2 st
( x = a & y = b )
take a = a; :: thesis: ex b being Element of C2 st
( x = a & y = b )
take b = b; :: thesis: ( x = a & y = b )
thus ( x = a & y = b ) by A1, Th80; :: thesis: verum
end;
hence ( x U+ y in C1 "/\" C2 iff ( x in C1 & y in C2 ) ) ; :: thesis: verum