let H be non empty multMagma ; :: thesis: for P, Q being Subset of H
for h being Element of H st P c= Q holds
P * h c= Q * h
let P, Q be Subset of H; :: thesis: for h being Element of H st P c= Q holds
P * h c= Q * h
let h be Element of H; :: thesis: ( P c= Q implies P * h c= Q * h )
assume A1: P c= Q ; :: thesis: P * h c= Q * h
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P * h or x in Q * h )
assume x in P * h ; :: thesis: x in Q * h
then consider g being Element of H such that
A2: ( x = g * h & g in P ) by GROUP_2:34;
thus x in Q * h by A1, A2, GROUP_2:34; :: thesis: verum