defpred S₁[ object ] means ex f being U-stable Function of C1,C2 st $1 = Trace f;
consider X being set such that
A3: for x being object holds
( x in X iff ( x in bool [:C1,(union C2):] & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ex f being U-stable Function of C1,C2 st x = Trace f )
let x be set ; :: thesis: ( x in X iff ex f being U-stable Function of C1,C2 st x = Trace f )
thus ( x in X iff ex f being U-stable Function of C1,C2 st x = Trace f ) by A3; :: thesis: verum