let G be Group; :: thesis: for H being Subgroup of G
for h being Element of G st h in H holds
H * h c= the carrier of H
let H be Subgroup of G; :: thesis: for h being Element of G st h in H holds
H * h c= the carrier of H
let h be Element of G; :: thesis: ( h in H implies H * h c= the carrier of H )
assume A1: h in H ; :: thesis: H * h c= the carrier of H
for a being set st a in H * h holds
a in the carrier of H

proof

let a be set ; :: thesis: ( a in H * h implies a in the carrier of H )
assume a in H * h ; :: thesis: a in the carrier of H
then consider g being Element of G such that
A2: ( a = g * h & g in H ) by GROUP_2:126;
g * h in H by A1, A2, GROUP_2:59;
hence a in the carrier of H by A2, STRUCT_0:def 5; :: thesis: verum

end;

hence H * h c= the carrier of H by TARSKI:def 3; :: thesis: verum