let G be Group; :: thesis: for H being Subgroup of G holds card H c= card G
let H be Subgroup of G; :: thesis: card H c= card G
the carrier of H c= the carrier of G by Def5;
hence card H c= card G by CARD_1:11; :: thesis: verum