theorem Th161: :: MATGRP_0:141

for G being Group holds multMagma(# the carrier of G, the multF of G #) is Subgroup of G