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 & card H = card the carrier of H & card G = card the carrier of G ) by Def5;
hence card H c= card G by CARD_1:27; :: thesis: verum