theorem ThA54: :: GROUP_1A:100

for G being addGroup holds G is Subgroup of G