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 " )
( (A ") " = A & (B ") " = B ) ;
hence ( A c= B iff A " c= B " ) by Lm1; :: thesis: verum