let E be set ; :: thesis: for A being Subset of (E ^omega ) holds
( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
let A be Subset of (E ^omega ); :: thesis: ( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
thus ( not A * = {(<%> E)} or A = {} or A = {(<%> E)} ) :: thesis: ( ( A = {} or A = {(<%> E)} ) implies A * = {(<%> E)} )

proof

assume that
A1: A * = {(<%> E)} and
A2: ( A <> {} & A <> {(<%> E)} ) ; :: thesis: contradiction
consider x being set such that
A3: ( x in A & x <> <%> E ) by A2, ZFMISC_1:41;
A c= A * by Th44;
hence contradiction by A1, A3, TARSKI:def 1; :: thesis: verum

end;

A4: now

assume A5: A = {} ; :: thesis: A * = {(<%> E)}

A6: now

let x be set ; :: thesis: ( x in A * implies x in {(<%> E)} )
assume x in A * ; :: thesis: x in {(<%> E)}
then consider n being Nat such that
A7: x in A |^ n by Th42;
A8: ( n = 0 implies x in {(<%> E)} ) by A7, Th25;
not n > 0 by A5, A7, Th28;
hence x in {(<%> E)} by A8; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in {(<%> E)} implies x in A * )
assume x in {(<%> E)} ; :: thesis: x in A *
then x in A |^ 0 by Th25;
hence x in A * by Th42; :: thesis: verum

end;

hence A * = {(<%> E)} by A6, TARSKI:2; :: thesis: verum

end;

now

assume A9: A = {(<%> E)} ; :: thesis: A * = {(<%> E)}
A10: A * c= {(<%> E)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A * or x in {(<%> E)} )
assume x in A * ; :: thesis: x in {(<%> E)}
then consider n being Nat such that
A11: x in A |^ n by Th42;
thus x in {(<%> E)} by A9, A11, Th29; :: thesis: verum

end;

{(<%> E)} c= A *

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(<%> E)} or x in A * )
assume x in {(<%> E)} ; :: thesis: x in A *
then x in A |^ 0 by Th25;
hence x in A * by Th42; :: thesis: verum

end;

hence A * = {(<%> E)} by A10, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( ( A = {} or A = {(<%> E)} ) implies A * = {(<%> E)} ) by A4; :: thesis: verum