let G be Group; :: 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 = (1_ G) * H by GROUP_1:def 5
.= carr H by Th37 ;
(a * (a ")) * H = (1_ G) * H by GROUP_1:def 5
.= carr H by Th37 ;
hence ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) by A1, Th116; :: thesis: verum