let G be Group; :: thesis: for A being Subset of G
for a being Element of G holds
( a in A " iff a " in A )
let A be Subset of G; :: thesis: for a being Element of G holds
( a in A " iff a " in A )
let a be Element of G; :: thesis: ( a in A " iff a " in A )
( (a ") " = a & (A ") " = A ) ;
hence ( a in A " iff a " in A ) ; :: thesis: verum