let G be Group; :: thesis: ( G is finite implies 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) ) )

assume A1: G is finite ; :: thesis: 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) )

let C be Subgroup of G; :: thesis: 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) )

let A, B be Subgroup of C; :: thesis: 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) )

let D be Subgroup of A; :: thesis: ( D = A /\ B implies 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) ) )

assume A2: D = A /\ B ; :: thesis: 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) )

let E be Subgroup of B; :: thesis: ( E = A /\ B implies 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) ) )

assume A3: E = A /\ B ; :: thesis: 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) )

let F be Subgroup of C; :: thesis: ( F = A /\ B & index (C,A), index (C,B) are_coprime implies ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A4: F = A /\ B ; :: thesis: ( not index (C,A), index (C,B) are_coprime or ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A5: index A, index B are_coprime ; :: thesis: ( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
index F = () * () by ;
then A6: (index E) * () = () * () by ;
then index B divides () * () by INT_1:def 3;
then A7: index B divides index D by ;
ex n being Element of NAT st index D = () * n
proof
consider i being Integer such that
A8: index D = () * i by ;
0 <= i by A1, A8, Th20;
then reconsider i = i as Element of NAT by INT_1:3;
take i ; :: thesis: index D = () * i
thus index D = () * i by A8; :: thesis: verum
end;
then A9: index B divides index D by NAT_D:def 3;
A10: index (C,B) >= index (A,D) by A1, A2, Th19;
A11: index B = index D
proof
assume A12: index B <> index D ; :: thesis: contradiction
index D > 0 by ;
then index B <= index D by ;
hence contradiction by A10, A12, XXREAL_0:1; :: thesis: verum
end;
index A divides () * () by ;
then A13: index A divides index E by ;
ex n being Element of NAT st index E = () * n
proof
consider i being Integer such that
A14: index E = () * i by ;
0 <= i by ;
then reconsider i = i as Element of NAT by INT_1:3;
take i ; :: thesis: index E = () * i
thus index E = () * i by A14; :: thesis: verum
end;
then A15: index A divides index E by NAT_D:def 3;
A16: index A >= index E by A1, A3, Th19;
index A = index E
proof
assume A17: index A <> index E ; :: thesis: contradiction
index E > 0 by ;
then index A <= index E by ;
hence contradiction by A16, A17, XXREAL_0:1; :: thesis: verum
end;
hence ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) by A11; :: thesis: verum