theorem Th7: :: GROUP_6:7

for G being strict Group
for B being strict Subgroup of G holds
( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )