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