let C1, C2 be Coherence_Space; for x1, y1, x2, y2 being set holds
( [[x1,x2],[y1,y2]] in Web (C1 [*] C2) iff ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) )
let x1, y1, x2, y2 be set ; ( [[x1,x2],[y1,y2]] in Web (C1 [*] C2) iff ( [x1,y1] in Web C1 & [x2,y2] in Web C2 ) )
A1:
{[x1,x2],[y1,y2]} c= [:{x1,y1},{x2,y2}:]
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in {[x1,x2],[y1,y2]} or [x,y] in [:{x1,y1},{x2,y2}:] )
assume
[x,y] in {[x1,x2],[y1,y2]}
;
[x,y] in [:{x1,y1},{x2,y2}:]
then
( (
[x,y] = [x1,x2] &
x1 in {x1,y1} &
x2 in {x2,y2} ) or (
[x,y] = [y1,y2] &
y1 in {x1,y1} &
y2 in {x2,y2} ) )
by TARSKI:def 2;
hence
[x,y] in [:{x1,y1},{x2,y2}:]
by ZFMISC_1:87;
verum
end;
A2:
( proj1 {[x1,x2],[y1,y2]} = {x1,y1} & proj2 {[x1,x2],[y1,y2]} = {x2,y2} )
by FUNCT_5:13;
hereby ( [x1,y1] in Web C1 & [x2,y2] in Web C2 implies [[x1,x2],[y1,y2]] in Web (C1 [*] C2) )
assume
[[x1,x2],[y1,y2]] in Web (C1 [*] C2)
;
( [x1,y1] in Web C1 & [x2,y2] in Web C2 )then
{[x1,x2],[y1,y2]} in C1 [*] C2
by COH_SP:5;
then
(
{x1,y1} in C1 &
{x2,y2} in C2 )
by A2, Th97;
hence
(
[x1,y1] in Web C1 &
[x2,y2] in Web C2 )
by COH_SP:5;
verum
end;
assume
( [x1,y1] in Web C1 & [x2,y2] in Web C2 )
; [[x1,x2],[y1,y2]] in Web (C1 [*] C2)
then
( {x1,y1} in C1 & {x2,y2} in C2 )
by COH_SP:5;
then
{[x1,x2],[y1,y2]} in C1 [*] C2
by A1, Th96;
hence
[[x1,x2],[y1,y2]] in Web (C1 [*] C2)
by COH_SP:5; verum