let E be set ; :: thesis: for A being Subset of (E ^omega) holds
( A ? = A iff <%> E in A )
let A be Subset of (E ^omega); :: thesis: ( A ? = A iff <%> E in A )
thus ( A ? = A implies <%> E in A ) :: thesis: ( <%> E in A implies A ? = A )
proof
assume A ? = A ; :: thesis: <%> E in A
then A = {(<%> E)} \/ A by Th76;
hence <%> E in A by ZFMISC_1:39; :: thesis: verum
end;
assume <%> E in A ; :: thesis: A ? = A
then A = {(<%> E)} \/ A by ZFMISC_1:40;
hence A ? = A by Th76; :: thesis: verum