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 <> {} and
A3: B <> {} ; :: thesis: contradiction
consider a being Element of E ^omega such that
A4: a in A by A2, SUBSET_1:4;
consider b being Element of E ^omega such that
A5: b in B by A3, SUBSET_1:4;
a ^ b in A ^^ B by A4, A5, Def1;
hence contradiction by A1; :: thesis: verum
end;
assume A6: ( A = {} or B = {} ) ; :: thesis: A ^^ B = {}
for x being object holds not x in A ^^ B
proof
given x being object such that A7: 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 A7, Def1;
hence contradiction by A6; :: thesis: verum
end;
hence A ^^ B = {} by XBOOLE_0:def 1; :: thesis: verum