let C1, C2 be Subset of (E ^omega); :: thesis: ( ( for x being set holds
( x in C1 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) & ( for x being set holds
( x in C2 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) implies C1 = C2 )
assume that
A4: for x being set holds
( x in C1 iff ex e being Element of E st
( e in E & x = <%e%> ) ) and
A5: for x being set holds
( x in C2 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ; :: thesis: C1 = C2

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

let x be object ; :: 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 e being Element of E st
( e in E & x = <%e%> ) by A4;
hence x in C2 by A5; :: thesis: verum

end;

assume x in C2 ; :: thesis: x in C1
then ex e being Element of E st
( e in E & x = <%e%> ) by A5;
hence x in C1 by A4; :: thesis: verum

end;

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