let f be U-continuous Function; :: thesis: ( dom f is subset-closed implies Trace f c= graph f )
assume A1: dom f is subset-closed ; :: thesis: Trace f c= graph f
let x, z be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,z] in Trace f or [x,z] in graph f )
assume [x,z] in Trace f ; :: thesis: [x,z] in graph f
then consider a, y being set such that
A2: ( [x,z] = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) by Def18;
consider b being set such that
A3: ( b is finite & b c= a & y in f . b ) by A1, A2, Th22;
b in dom f by A1, A2, A3, CLASSES1:def 1;
then ( a = b & x = a & z = y ) by A2, A3, ZFMISC_1:33;
hence [x,z] in graph f by A2, A3, Th25; :: thesis: verum