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