let G be addGroup; :: thesis: for H being Subgroup of G holds
( carr H in Left_Cosets H & carr H in Right_Cosets H )
let H be Subgroup of G; :: thesis: ( carr H in Left_Cosets H & carr H in Right_Cosets H )
( carr H = (0_ G) + H & carr H = H + (0_ G) ) by Th37;
hence ( carr H in Left_Cosets H & carr H in Right_Cosets H ) by Def15, Def16; :: thesis: verum