theorem Th7: :: TOPGRP_1:7

for G being Group
for A being Subset of G
for a being Element of G holds
( a in A " iff a " in A )