Trace f c= [:C1,(union C2):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Trace f or x in [:C1,(union C2):] )
assume x in Trace f ; :: thesis: x in [:C1,(union C2):]
then consider a, y being set such that
A1: ( x = [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;
A2: ( dom f = C1 & rng f c= C2 ) by FUNCT_2:def 1, RELAT_1:def 19;
f . a in rng f by A1, FUNCT_1:def 5;
then y in union C2 by A1, A2, TARSKI:def 4;
hence x in [:C1,(union C2):] by A1, A2, ZFMISC_1:106; :: thesis: verum

end;

hence Trace f is Subset of [:C1,(union C2):] ; :: thesis: verum