let H be non empty addMagma ; :: 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 object ; :: 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 ex g being Element of H st
( x = g + h & g in P ) by Th28;
hence x in Q + h by A1, Th28; :: thesis: verum