let E be set ; :: thesis: for A, B being Subset of (E ^omega ) holds
( A ^^ B = {} iff ( A = {} or B = {} ) )
let A, B be Subset of (E ^omega ); :: thesis: ( A ^^ B = {} iff ( A = {} or B = {} ) )
thus ( not A ^^ B = {} or A = {} or B = {} ) :: thesis: ( ( A = {} or B = {} ) implies A ^^ B = {} )

proof

assume that
A1: A ^^ B = {} and
A2: ( A <> {} & B <> {} ) ; :: thesis: contradiction
consider a being Element of E ^omega such that
A3: a in A by A2, SUBSET_1:10;
consider b being Element of E ^omega such that
A4: b in B by A2, SUBSET_1:10;
a ^ b in A ^^ B by A3, A4, Def1;
hence contradiction by A1; :: thesis: verum

end;

assume A5: ( A = {} or B = {} ) ; :: thesis: A ^^ B = {}
for x being set holds not x in A ^^ B

proof

given x being set such that A6: x in A ^^ B ; :: thesis: contradiction
ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by A6, Def1;
hence contradiction by A5; :: thesis: verum

end;

hence A ^^ B = {} by XBOOLE_0:def 1; :: thesis: verum