let C1, C2 be Subset of (E ^omega); ( ( 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%> ) )
; C1 = C2
now for x being object holds
( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) )let x be
object ;
( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) )thus
(
x in C1 implies
x in C2 )
( x in C2 implies x in C1 )assume
x in C2
;
x in C1then
ex
e being
Element of
E st
(
e in E &
x = <%e%> )
by A5;
hence
x in C1
by A4;
verum end;
hence
C1 = C2
by TARSKI:2; verum