let G be addGroup; :: 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 <> {} ) )
set x = the Element of A;
set y = the Element of B;
thus ( A * B <> {} implies ( A <> {} & B <> {} ) ) :: thesis: ( A <> {} & B <> {} implies A * B <> {} )

proof

set x = the Element of A * B;
assume A * B <> {} ; :: thesis: ( A <> {} & B <> {} )
then ex a, b being Element of G st
( the Element of A * B = a * b & a in A & b in B ) by Th31;
hence ( A <> {} & B <> {} ) ; :: thesis: verum

end;

assume A1: A <> {} ; :: thesis: ( not B <> {} or A * B <> {} )
assume A2: B <> {} ; :: thesis: A * B <> {}
then reconsider x = the Element of A, y = the Element of B as Element of G by A1, TARSKI:def 3;
x * y in A * B by A1, A2;
hence A * B <> {} ; :: thesis: verum