theorem :: GROUP_1A:117

for G being addGroup
for H being Subgroup of G holds card H c= card G by DefA5, CARD_1:11;