let G be finite Group; :: thesis: for H being Subgroup of G holds card H <= card G
let H be Subgroup of G; :: thesis: card H <= card G
the carrier of H c= the carrier of G by Def5;
hence card H <= card G by NAT_1:44; :: thesis: verum