let C1, C2 be Coherence_Space; :: thesis: for x being set holds
( x in C1 [*] C2 iff ex a being Element of C1 ex b being Element of C2 st x c= [:a,b:] )
let x be set ; :: thesis: ( x in C1 [*] C2 iff ex a being Element of C1 ex b being Element of C2 st x c= [:a,b:] )

hereby :: thesis: ( ex a being Element of C1 ex b being Element of C2 st x c= [:a,b:] implies x in C1 [*] C2 )

assume x in C1 [*] C2 ; :: thesis: ex a being Element of C1 ex b being Element of C2 st x c= [:a,b:]
then consider y being set such that
A1: ( x in y & y in { (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum } ) by TARSKI:def 4;
consider a being Element of C1, b being Element of C2 such that
A2: y = bool [:a,b:] by A1;
take a = a; :: thesis: ex b being Element of C2 st x c= [:a,b:]
take b = b; :: thesis: x c= [:a,b:]
thus x c= [:a,b:] by A1, A2; :: thesis: verum

end;

given a' being Element of C1, b' being Element of C2 such that A3: x c= [:a',b':] ; :: thesis: x in C1 [*] C2
( x in bool [:a',b':] & bool [:a',b':] in { (bool [:a,b:]) where a is Element of C1, b is Element of C2 : verum } ) by A3;
hence x in C1 [*] C2 by TARSKI:def 4; :: thesis: verum