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 6
.= carr H by Th43 ;
((a " ) * a) * H = (1_ G) * H by GROUP_1:def 6
.= carr H by Th43 ;
hence ( carr H c= (a * H) * ((a " ) * H) & carr H c= ((a " ) * H) * (a * H) ) by A1, Th139; :: thesis: verum