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
A1: A c= A * by Th43;
assume that
A2: A * = {(<%> E)} and
A3: ( A <> {} & A <> {(<%> E)} ) ; :: thesis: contradiction
ex x being object st
( x in A & x <> <%> E ) by A3, ZFMISC_1:35;
hence contradiction by A2, A1, TARSKI:def 1; :: thesis: verum
end;
A4: now :: thesis: ( A = {} implies A * = {(<%> E)} )
assume A5: A = {} ; :: thesis: A * = {(<%> E)}
A6: now :: thesis: for x being object st x in A * holds
x in {(<%> E)}
let x be object ; :: 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 Th41;
( n = 0 implies x in {(<%> E)} ) by A7, Th24;
hence x in {(<%> E)} by A5, A7, Th27; :: thesis: verum
end;
now :: thesis: for x being object st x in {(<%> E)} holds
x in A *
let x be object ; :: thesis: ( x in {(<%> E)} implies x in A * )
assume x in {(<%> E)} ; :: thesis: x in A *
then x in A |^ 0 by Th24;
hence x in A * by Th41; :: thesis: verum
end;
hence A * = {(<%> E)} by A6, TARSKI:2; :: thesis: verum
end;
now :: thesis: ( A = {(<%> E)} implies A * = {(<%> E)} )
assume A8: A = {(<%> E)} ; :: thesis: A * = {(<%> E)}
A9: A * c= {(<%> E)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * or x in {(<%> E)} )
assume x in A * ; :: thesis: x in {(<%> E)}
then ex n being Nat st x in A |^ n by Th41;
hence x in {(<%> E)} by A8, Th28; :: thesis: verum
end;
{(<%> E)} c= A *
proof
let x be object ; :: 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 Th24;
hence x in A * by Th41; :: thesis: verum
end;
hence A * = {(<%> E)} by A9, XBOOLE_0:def 10; :: thesis: verum
end;
hence ( ( A = {} or A = {(<%> E)} ) implies A * = {(<%> E)} ) by A4; :: thesis: verum