let G be addGroup; :: thesis: for a, b being Element of G
for H being Subgroup of G holds H + a,H + b are_equipotent
let a, b be Element of G; :: thesis: for H being Subgroup of G holds H + a,H + b are_equipotent
let H be Subgroup of G; :: thesis: H + a,H + b are_equipotent
( H + a,b + H are_equipotent & b + H,H + b are_equipotent ) by Th129;
hence H + a,H + b are_equipotent by WELLORD2:15; :: thesis: verum