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