let G be finite addGroup; :: thesis: for H being Subgroup of G holds card H divides card G
let H be Subgroup of G; :: thesis: card H divides card G
card G = (card H) * (index H) by Th147;
hence card H divides card G by NAT_D:def 3; :: thesis: verum