let f be U-continuous Function; :: thesis: ( dom f is subset-closed implies for a, y being set st [a,y] in Trace f holds
a is finite )
assume A1: dom f is subset-closed ; :: thesis: for a, y being set st [a,y] in Trace f holds
a is finite
let a, y be set ; :: thesis: ( [a,y] in Trace f implies a is finite )
assume A2: [a,y] in Trace f ; :: thesis: a is finite
then A3: a in dom f by Th31;
y in f . a by A2, Th31;
then consider b being set such that
A4: b is finite and
A5: b c= a and
A6: y in f . b by A1, A3, Th21;
b in dom f by A1, A3, A5;
hence a is finite by A2, A4, A5, A6, Th31; :: thesis: verum