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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LinTrace f or x in [:(union C1),(union C2):] )
assume x in LinTrace f ; :: thesis: x in [:(union C1),(union C2):]
then consider y, z being set such that
A1: x = [y,z] and
A2: [{y},z] in Trace f by Def20;
A3: y in {y} by TARSKI:def 1;
dom f = C1 by FUNCT_2:def 1;
then {y} in C1 by A2, Th32;
then A4: y in union C1 by A3, TARSKI:def 4;
z in union C2 by A2, ZFMISC_1:106;
hence x in [:(union C1),(union C2):] by A1, A4, ZFMISC_1:106; :: thesis: verum

end;

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