let E, x be set ; :: thesis: for A being Subset of (E ^omega) holds
( <%x%> in A * iff <%x%> in A )
let A be Subset of (E ^omega); :: thesis: ( <%x%> in A * iff <%x%> in A )
thus ( <%x%> in A * implies <%x%> in A ) :: thesis: ( <%x%> in A implies <%x%> in A * )

proof

defpred S₁[ Nat] means <%x%> in A |^ $1;
assume that
A1: <%x%> in A * and
A2: not <%x%> in A ; :: thesis: contradiction
A3: ex i being Nat st S₁[i] by A1, Th41;
ex n1 being Nat st
( S₁[n1] & ( for n2 being Nat st S₁[n2] holds
n1 <= n2 ) ) from NAT_1:sch 5(A3);
then consider n1 being Nat such that
A4: S₁[n1] and
A5: for n2 being Nat st S₁[n2] holds
n1 <= n2 ;

A6: now :: thesis: not n1 = 0

assume n1 = 0 ; :: thesis: contradiction
then <%x%> in {(<%> E)} by A4, Th24;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

A7: now :: thesis: ( n1 > 1 implies <%x%> in A )

assume n1 > 1 ; :: thesis: <%x%> in A
then consider n2 being Nat such that
A8: n2 + 1 = n1 by NAT_1:6;
<%x%> in (A |^ n2) ^^ A by A4, A8, Th23;
then consider a, b being Element of E ^omega such that
A9: a in A |^ n2 and
A10: ( b in A & <%x%> = a ^ b ) by Def1;

now :: thesis: ( a = <%x%> implies not b = <%> E )

reconsider n2 = n2 as Element of NAT by ORDINAL1:def 12;
assume that
A11: a = <%x%> and
b = <%> E ; :: thesis: contradiction
ex i being Element of NAT st
( S₁[i] & n1 > i )

proof

take n2 ; :: thesis: ( S₁[n2] & n1 > n2 )
thus ( S₁[n2] & n1 > n2 ) by A8, A9, A11, NAT_1:13; :: thesis: verum

end;

hence contradiction by A5; :: thesis: verum

end;

hence <%x%> in A by A10, Th4; :: thesis: verum

end;

( n1 = 1 implies <%x%> in A ) by A4, Th25;
hence contradiction by A2, A7, A6, NAT_1:25; :: thesis: verum

end;

assume <%x%> in A ; :: thesis: <%x%> in A *
then <%x%> in A |^ 1 by Th25;
hence <%x%> in A * by Th41; :: thesis: verum