let G be Group; :: thesis: for A, B being Subset of G holds
( A c= B iff A " c= B " )
let A, B be Subset of G; :: thesis: ( A c= B iff A " c= B " )
A1: A " = { (g " ) where g is Element of G : g in A } by GROUP_2:def 1;
A2: B " = { (g " ) where g is Element of G : g in B } by GROUP_2:def 1;
thus ( A c= B implies A " c= B " ) :: thesis: ( A " c= B " implies A c= B )

proof

assume A3: A c= B ; :: thesis: A " c= B "
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A " or a in B " )
assume a in A " ; :: thesis: a in B "
then consider g being Element of G such that
A4: ( a = g " & g in A ) by A1;
thus a in B " by A2, A3, A4; :: thesis: verum

end;

assume A5: A " c= B " ; :: thesis: A c= B
A6: ( A = (A " ) " & B = (B " ) " ) by Th8;
A7: (A " ) " = { (g " ) where g is Element of G : g in A " } by GROUP_2:def 1;
A8: (B " ) " = { (g " ) where g is Element of G : g in B " } by GROUP_2:def 1;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in B )
assume a in A ; :: thesis: a in B
then consider g being Element of G such that
A9: ( a = g " & g in A " ) by A6, A7;
thus a in B by A5, A6, A8, A9; :: thesis: verum