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