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
h + P c= h + Q
let P, Q be Subset of H; :: thesis: for h being Element of H st P c= Q holds
h + P c= h + Q
let h be Element of H; :: thesis: ( P c= Q implies h + P c= h + Q )
assume A1: P c= Q ; :: thesis: h + P c= h + Q
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in h + P or x in h + Q )
assume x in h + P ; :: thesis: x in h + Q
then ex g being Element of H st
( x = h + g & g in P ) by Th27;
hence x in h + Q by A1, Th27; :: thesis: verum