theorem :: FLANG_2:5

for E, x being set
for A, B being Subset of (E ^omega) st ( x in A or x in B ) & x <> <%> E holds
A ^^ B <> {(<%> E)}