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 object ; :: 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 and
A2: a in A and
A3: b in B ;
b " in B " by A3;
then (b ") * a in (B ") * A by A2;
hence x in ((B ") * A) * B by A1, A3; :: thesis: verum