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
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in H * h or 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 and
A3: g in H by GROUP_2:104;
g * h in H by A1, A3, GROUP_2:50;
hence a in the carrier of H by A2; :: thesis: verum