let G be addGroup; :: 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: (0_ G) + a = a by Def4;
( 0_ G in H & a + (0_ G) = a ) by Th46, Def4;
hence ( a in a + H & a in H + a ) by A1, Th103, Th104; :: thesis: verum