let C1, C2 be Coherence_Space; :: thesis: for f being U-stable Function of C1,C2
for a being Element of C1
for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )
let f be U-stable Function of C1,C2; :: thesis: for a being Element of C1
for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )
A1: dom f = C1 by FUNCT_2:def 1;
let a be Element of C1; :: thesis: for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )
let y be set ; :: thesis: ( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )

hereby :: thesis: ( ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) implies y in f . a )

assume y in f . a ; :: thesis: ex b being Element of C1 st
( [b,y] in Trace f & b c= a )
then consider b being set such that
A2: ( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) by A1, Th23;
reconsider b = b as Element of C1 by A2, CLASSES1:def 1;
take b = b; :: thesis: ( [b,y] in Trace f & b c= a )

now

let c be set ; :: thesis: ( c in dom f & c c= b & y in f . c implies b = c )
assume A3: ( c in dom f & c c= b & y in f . c ) ; :: thesis: b = c
then c c= a by A2, XBOOLE_1:1;
then b c= c by A2, A3;
hence b = c by A3, XBOOLE_0:def 10; :: thesis: verum

end;

hence [b,y] in Trace f by A1, A2, Th32; :: thesis: b c= a
thus b c= a by A2; :: thesis: verum

end;

given b being Element of C1 such that A4: ( [b,y] in Trace f & b c= a ) ; :: thesis: y in f . a
( f . b c= f . a & y in f . b ) by A1, A4, Def12, Th32;
hence y in f . a ; :: thesis: verum