let G be addGroup; :: thesis: for a being Element of G
for H being Subgroup of G holds
( carr H c= (a + H) + ((- a) + H) & carr H c= ((- a) + H) + (a + H) )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( carr H c= (a + H) + ((- a) + H) & carr H c= ((- a) + H) + (a + H) )
let H be Subgroup of G; :: thesis: ( carr H c= (a + H) + ((- a) + H) & carr H c= ((- a) + H) + (a + H) )
A1: ((- a) + a) + H = (0_ G) + H by Def5
.= carr H by Th37 ;
(a + (- a)) + H = (0_ G) + H by Def5
.= carr H by Th37 ;
hence ( carr H c= (a + H) + ((- a) + H) & carr H c= ((- a) + H) + (a + H) ) by A1, Th116; :: thesis: verum