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 and
A2: 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
A3: y = bool [:a,b:] by A2;
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, A3; :: thesis: verum

end;

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