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] & [{y},z] in Trace f ) by Def20;
( dom f = C1 & rng f c= C2 ) by FUNCT_2:def 1, RELAT_1:def 19;
then ( {y} in C1 & y in {y} ) by A1, Th32, TARSKI:def 1;
then ( y in union C1 & z in union C2 ) by A1, TARSKI:def 4, ZFMISC_1:106;
hence x in [:(union C1),(union C2):] by A1, ZFMISC_1:106; :: thesis: verum

end;

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