let E, x be set ; :: thesis: for A being Subset of (E ^omega) holds
( x in A ? iff ( x = <%> E or x in A ) )
let A be Subset of (E ^omega); :: thesis: ( x in A ? iff ( x = <%> E or x in A ) )
( x in A ? iff x in {(<%> E)} \/ A ) by Th76;
then ( x in A ? iff ( x in {(<%> E)} or x in A ) ) by XBOOLE_0:def 3;
hence ( x in A ? iff ( x = <%> E or x in A ) ) by TARSKI:def 1; :: thesis: verum