theorem :: GROUP_1A:118

for G being finite addGroup
for H being Subgroup of G holds card H <= card G by DefA5, NAT_1:43;