let G be Group; :: 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 = (1_ G) * H & carr H = H * (1_ G) ) by Th37;
hence ( carr H in Left_Cosets H & carr H in Right_Cosets H ) by Def15, Def16; :: thesis: verum