let G be addGroup; :: thesis: for a being Element of G
for H being Subgroup of G holds H + (2 * a) c= (H + a) + (H + a)
let a be Element of G; :: thesis: for H being Subgroup of G holds H + (2 * a) c= (H + a) + (H + a)
let H be Subgroup of G; :: thesis: H + (2 * a) c= (H + a) + (H + a)
( 2 * a = a + a & (H + a) + a = H + (a + a) ) by ThB34, Th26;
hence H + (2 * a) c= (H + a) + (H + a) by Th122; :: thesis: verum