let G be finite Group; :: thesis: for H being Subgroup of G holds index (G,H) > 0
let H be Subgroup of G; :: thesis: index (G,H) > 0
card G = (card H) * (index H) by GROUP_2:147;
hence index (G,H) > 0 ; :: thesis: verum