let G be Group; :: thesis: for A, B being Subset of G holds
( A |^ B <> {} iff ( A <> {} & B <> {} ) )
let A, B be Subset of G; :: thesis: ( A |^ B <> {} iff ( A <> {} & B <> {} ) )
thus ( A |^ B <> {} implies ( A <> {} & B <> {} ) ) :: thesis: ( A <> {} & B <> {} implies A |^ B <> {} )

proof

assume A1: A |^ B <> {} ; :: thesis: ( A <> {} & B <> {} )
consider x being Element of A |^ B;
ex a, b being Element of G st
( x = a |^ b & a in A & b in B ) by A1, Th38;
hence ( A <> {} & B <> {} ) ; :: thesis: verum

end;

assume A2: A <> {} ; :: thesis: ( not B <> {} or A |^ B <> {} )
consider x being Element of A;
assume A3: B <> {} ; :: thesis: A |^ B <> {}
consider y being Element of B;
reconsider x = x, y = y as Element of G by A2, A3, TARSKI:def 3;
x |^ y in A |^ B by A2, A3;
hence A |^ B <> {} ; :: thesis: verum