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