for G being Group
for B, A being Subgroup of G
for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)