let G be Group; :: thesis: for a, b, c being Element of G holds {a} |^ {b,c} = {(a |^ b),(a |^ c)}
let a, b, c be Element of G; :: thesis: {a} |^ {b,c} = {(a |^ b),(a |^ c)}
thus {a} |^ {b,c} c= {(a |^ b),(a |^ c)} :: according to XBOOLE_0:def 10 :: thesis: {(a |^ b),(a |^ c)} c= {a} |^ {b,c}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} |^ {b,c} or x in {(a |^ b),(a |^ c)} )
assume x in {a} |^ {b,c} ; :: thesis: x in {(a |^ b),(a |^ c)}
then consider g, h being Element of G such that
A1: ( x = g |^ h & g in {a} & h in {b,c} ) ;
( g = a & ( h = b or h = c ) ) by A1, TARSKI:def 1, TARSKI:def 2;
hence x in {(a |^ b),(a |^ c)} by A1, TARSKI:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(a |^ b),(a |^ c)} or x in {a} |^ {b,c} )
assume x in {(a |^ b),(a |^ c)} ; :: thesis: x in {a} |^ {b,c}
then ( ( x = a |^ b or x = a |^ c ) & a in {a} & b in {b,c} & c in {b,c} ) by TARSKI:def 1, TARSKI:def 2;
hence x in {a} |^ {b,c} ; :: thesis: verum