theorem :: GROUP_2:72

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