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 object ; :: 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 and
A2: a in A " and
A3: b in B ;
consider c being Element of G such that
A4: ( a = c " & c in A ) by A2;
( x = (c |^ b) " & c |^ b in A |^ B ) by A1, A3, A4, Th26;
hence x in (A |^ B) " ; :: thesis: verum
end;
let x be object ; :: 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
A5: x = a " and
A6: a in A |^ B ;
consider b, c being Element of G such that
A7: a = b |^ c and
A8: b in A and
A9: c in B by A6;
A10: b " in A " by A8;
x = (b ") |^ c by A5, A7, Th26;
hence x in (A ") |^ B by A9, A10; :: thesis: verum