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

( 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