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:177;
then index H <> 0 by GROUP_1:90;
hence index G,H > 0 ; :: thesis: verum