let G be non empty multMagma ; :: 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