let G be Group; :: thesis: for A, B being Subset of G holds (A * B) " = (B ") * (A ")
let A, B be Subset of G; :: thesis: (A * B) " = (B ") * (A ")
thus (A * B) " c= (B ") * (A ") :: according to XBOOLE_0:def 10 :: thesis: (B ") * (A ") c= (A * B) "
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A * B) " or x in (B ") * (A ") )
assume x in (A * B) " ; :: thesis: x in (B ") * (A ")
then consider g being Element of G such that
A1: x = g " and
A2: g in A * B ;
consider g1, g2 being Element of G such that
A3: g = g1 * g2 and
A4: ( g1 in A & g2 in B ) by A2;
A5: ( g1 " in A " & g2 " in B " ) by A4;
x = (g2 ") * (g1 ") by A1, A3, GROUP_1:17;
hence x in (B ") * (A ") by A5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B ") * (A ") or x in (A * B) " )
assume x in (B ") * (A ") ; :: thesis: x in (A * B) "
then consider g1, g2 being Element of G such that
A6: x = g1 * g2 and
A7: g1 in B " and
A8: g2 in A " ;
consider b being Element of G such that
A9: g2 = b " and
A10: b in A by A8;
consider a being Element of G such that
A11: g1 = a " and
A12: a in B by A7;
A13: b * a in A * B by A12, A10;
x = (b * a) " by A6, A11, A9, GROUP_1:17;
hence x in (A * B) " by A13; :: thesis: verum