let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds
( a in a * H & a in H * a )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( a in a * H & a in H * a )
let H be Subgroup of G; :: thesis: ( a in a * H & a in H * a )
A1: (1_ G) * a = a by GROUP_1:def 4;
( 1_ G in H & a * (1_ G) = a ) by Th46, GROUP_1:def 4;
hence ( a in a * H & a in H * a ) by A1, Th103, Th104; :: thesis: verum