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