let G be Group; :: thesis: for A, B being Subset of G holds (A " ) |^ B = (A |^ B) "
let A, B be Subset of G; :: thesis: (A " ) |^ B = (A |^ B) "
thus (A " ) |^ B c= (A |^ B) " :: according to XBOOLE_0:def 10 :: thesis: (A |^ B) " c= (A " ) |^ B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A " ) |^ B or x in (A |^ B) " )
assume x in (A " ) |^ B ; :: thesis: x in (A |^ B) "
then consider a, b being Element of G such that
A1: ( x = a |^ b & a in A " & b in B ) ;
consider c being Element of G such that
A2: ( a = c " & c in A ) by A1;
( x = (c |^ b) " & c |^ b in A |^ B ) by A1, A2, Th32;
hence x in (A |^ B) " ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ B) " or x in (A " ) |^ B )
assume x in (A |^ B) " ; :: thesis: x in (A " ) |^ B
then consider a being Element of G such that
A3: ( x = a " & a in A |^ B ) ;
consider b, c being Element of G such that
A4: ( a = b |^ c & b in A & c in B ) by A3;
( x = (b " ) |^ c & b " in A " ) by A3, A4, Th32;
hence x in (A " ) |^ B by A4; :: thesis: verum