let C1, C2 be Subset of (E ^omega); :: thesis: ( ( for x being set holds
( x in C1 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds
( x in C2 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) implies C1 = C2 )
assume that
A2: for x being set holds
( x in C1 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) and
A3: for x being set holds
( x in C2 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ; :: thesis: C1 = C2

now :: thesis: for x being set holds
( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) )

let x be set ; :: thesis: ( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) )
thus ( x in C1 implies x in C2 ) :: thesis: ( x in C2 implies x in C1 )

proof

assume x in C1 ; :: thesis: x in C2
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by A2;
hence x in C2 by A3; :: thesis: verum

end;

assume x in C2 ; :: thesis: x in C1
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by A3;
hence x in C1 by A2; :: thesis: verum

end;

hence C1 = C2 by TARSKI:1; :: thesis: verum