let H be non empty addMagma ; :: thesis: for P, Q, P1, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P + Q c= P1 + Q1
let P, Q, P1, Q1 be Subset of H; :: thesis: ( P c= P1 & Q c= Q1 implies P + Q c= P1 + Q1 )
assume A1: ( P c= P1 & Q c= Q1 ) ; :: thesis: P + Q c= P1 + Q1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P + Q or x in P1 + Q1 )
assume x in P + Q ; :: thesis: x in P1 + Q1
then ex g, t being Element of H st
( x = g + t & g in P & t in Q ) ;
hence x in P1 + Q1 by A1; :: thesis: verum