let x, E be set ; :: thesis: for A being Subset of (E ^omega ) st x in A & x <> <%> E holds
A + <> {(<%> E)}
let A be Subset of (E ^omega ); :: thesis: ( x in A & x <> <%> E implies A + <> {(<%> E)} )
assume A1: ( x in A & x <> <%> E ) ; :: thesis: A + <> {(<%> E)}
A + = A |^.. 1 by Th50;
hence A + <> {(<%> E)} by A1, Th14; :: thesis: verum