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

proof

defpred S₁[ Nat] means <%x%> in A |^ $1;
assume that
A1: <%x%> in A * and
A2: not <%x%> in A ; :: thesis:
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:

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

end;

A7: now :: thesis:

assume n1 > 1 ; :: thesis:
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:

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

proof

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

end;

hence contradiction by A5; :: thesis:

end;

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

end;

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

end;

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