theorem
for
C1,
C2 being
Coherence_Space for
X being
Subset of
[:C1,(union C2):] st ( for
x being
set st
x in X holds
x `1 is
finite ) & ( for
a,
b being
finite Element of
C1 st
a c= b holds
for
y being
set st
[a,y] in X holds
[b,y] in X ) & ( for
a being
finite Element of
C1 for
y1,
y2 being
set st
[a,y1] in X &
[a,y2] in X holds
{y1,y2} in C2 ) holds
ex
f being
U-continuous Function of
C1,
C2 st
X = graph f