let G be non empty addMagma ; :: thesis: for g, h being Element of G holds {g} + {h} = {(g + h)}
let g, h be Element of G; :: thesis: {g} + {h} = {(g + h)}
thus {g} + {h} c= {(g + h)} :: according to XBOOLE_0:def 10 :: thesis: {(g + h)} c= {g} + {h}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {g} + {h} or x in {(g + h)} )
assume x in {g} + {h} ; :: thesis: x in {(g + h)}
then consider g1, g2 being Element of G such that
A1: x = g1 + g2 and
A2: ( g1 in {g} & g2 in {h} ) ;
( g1 = g & g2 = h ) by A2, TARSKI:def 1;
hence x in {(g + h)} by A1, TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g + h)} or x in {g} + {h} )
assume x in {(g + h)} ; :: thesis: x in {g} + {h}
then A3: x = g + h by TARSKI:def 1;
( g in {g} & h in {h} ) by TARSKI:def 1;
hence x in {g} + {h} by A3; :: thesis: verum