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 that
A1: x in A and
A2: x <> <%> E ; :: thesis: A * <> {(<%> E)}
A <> {(<%> E)} by A1, A2, TARSKI:def 1;
hence A * <> {(<%> E)} by A1, FLANG_1:47; :: thesis: verum