let G be Group; :: 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} "

assume x in {(g "),(h ")} ; :: thesis: x in {g,h} "

then A3: ( x = g " or x = h " ) by TARSKI:def 2;

( g in {g,h} & h in {g,h} ) by TARSKI:def 2;

hence x in {g,h} " by A3; :: thesis: verum

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} " )
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 a being Element of G such that

A1: x = a " and

A2: a in {g,h} ;

( a = g or a = h ) by A2, TARSKI:def 2;

hence x in {(g "),(h ")} by A1, TARSKI:def 2; :: thesis: verum

end;assume x in {g,h} " ; :: thesis: x in {(g "),(h ")}

then consider a being Element of G such that

A1: x = a " and

A2: a in {g,h} ;

( a = g or a = h ) by A2, TARSKI:def 2;

hence x in {(g "),(h ")} by A1, TARSKI:def 2; :: thesis: verum

assume x in {(g "),(h ")} ; :: thesis: x in {g,h} "

then A3: ( x = g " or x = h " ) by TARSKI:def 2;

( g in {g,h} & h in {g,h} ) by TARSKI:def 2;

hence x in {g,h} " by A3; :: thesis: verum