let E, x 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 |^ (0,1) by Th79;
hence A ? <> {(<%> E)} by A1, Th30; :: thesis: verum