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