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

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