let f be U-continuous Function; ( dom f is subset-closed implies Trace f c= graph f )
assume A1:
dom f is subset-closed
; Trace f c= graph f
let x, z be object ; RELAT_1:def 3 ( not [x,z] in Trace f or [x,z] in graph f )
assume
[x,z] in Trace f
; [x,z] in graph f
then consider a, y being set such that
A2:
[x,z] = [a,y]
and
A3:
a in dom f
and
A4:
y in f . a
and
A5:
for b being set st b in dom f & b c= a & y in f . b holds
a = b
by Def17;
consider b being set such that
A6:
b is finite
and
A7:
b c= a
and
A8:
y in f . b
by A1, A3, A4, Th21;
b in dom f
by A1, A3, A7;
then
a = b
by A5, A7, A8;
hence
[x,z] in graph f
by A2, A3, A4, A6, Th24; verum