let X1, X2 be set ; :: thesis: ( ( for x being set holds
( x in X1 iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) & ( for x being set holds
( x in X2 iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) implies X1 = X2 )
assume A1: ( ( for x being set holds
( x in X1 iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) & ( for x being set holds
( x in X2 iff ex f being U-stable Function of C1,C2 st x = Trace f ) ) & not X1 = X2 ) ; :: thesis: contradiction
then consider x being object such that
A2: ( ( x in X1 & not x in X2 ) or ( x in X2 & not x in X1 ) ) by TARSKI:2;
( x in X2 iff for f being U-stable Function of C1,C2 holds not x = Trace f ) by A1, A2;
hence contradiction by A1; :: thesis: verum