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 )
( 1_ G in H & a * (1_ G) = a & (1_ G) * a = a ) by Th55, GROUP_1:def 5;
hence ( a in a * H & a in H * a ) by Th125, Th126; :: thesis: verum