let E, x be set ; :: thesis: for A, B being Subset of (E ^omega) st ( x in A or x in B ) & x <> <%> E holds
A ^^ B <> {(<%> E)}
let A, B be Subset of (E ^omega); :: thesis: ( ( x in A or x in B ) & x <> <%> E implies A ^^ B <> {(<%> E)} )
assume ( ( x in A or x in B ) & x <> <%> E ) ; :: thesis: A ^^ B <> {(<%> E)}
then ( A <> {(<%> E)} or B <> {(<%> E)} ) by TARSKI:def 1;
hence A ^^ B <> {(<%> E)} by FLANG_1:14; :: thesis: verum