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