let G be addGroup; :: thesis: for A, B being Subset of G holds A * B c= ((- B) + A) + B
let A, B be Subset of G; :: thesis: A * B c= ((- B) + A) + B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * B or x in ((- B) + A) + B )
assume x in A * B ; :: thesis: x in ((- B) + A) + B
then consider a, b being Element of G such that
A1: x = a * b and
A2: a in A and
A3: b in B ;
- b in - B by A3;
then (- b) + a in (- B) + A by A2;
hence x in ((- B) + A) + B by A1, A3; :: thesis: verum