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

assume A1: ( <%x%> in A * & not <%x%> in A ) ; :: thesis: contradiction
defpred S₁[ Nat] means <%x%> in A |^ $1;
consider n being Nat such that
A2: S₁[n] by A1, Th42;
A3: ex i being Nat st S₁[i] by A2;
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

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

now

assume A9: ( a = <%x%> & b = <%> E ) ; :: thesis: contradiction
reconsider n2 = n2 as Element of NAT by ORDINAL1:def 13;
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 A7, A8, A9, NAT_1:13; :: thesis: verum

end;

hence contradiction by A5; :: thesis: verum

end;

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

end;

A10: ( n1 = 1 implies <%x%> in A ) by A4, Th26;

now

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

end;

hence contradiction by A1, A6, A10, NAT_1:26; :: thesis: verum

end;

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