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 ( x in A & x <> <%> E ) ; :: thesis: A * <> {(<%> E)}
then ( A <> {} & A <> {(<%> E)} ) by TARSKI:def 1;
hence A * <> {(<%> E)} by FLANG_1:48; :: thesis: verum