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 = (index E) * (index B) by A1, A3, A4, GROUP_2:149;

then A6: (index E) * (index B) = (index D) * (index A) by A1, A2, A4, GROUP_2:149;

then index B divides (index A) * (index D) by INT_1:def 3;

then A7: index B divides index D by A5, INT_2:25;

ex n being Element of NAT st index D = (index B) * n

A10: index (C,B) >= index (A,D) by A1, A2, Th19;

A11: index B = index D

then A13: index A divides index E by A5, INT_2:25;

ex n being Element of NAT st index E = (index A) * n

A16: index A >= index E by A1, A3, Th19;

index A = index E

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 = (index E) * (index B) by A1, A3, A4, GROUP_2:149;

then A6: (index E) * (index B) = (index D) * (index A) by A1, A2, A4, GROUP_2:149;

then index B divides (index A) * (index D) by INT_1:def 3;

then A7: index B divides index D by A5, INT_2:25;

ex n being Element of NAT st index D = (index B) * n

proof

then A9:
index B divides index D
by NAT_D:def 3;
consider i being Integer such that

A8: index D = (index B) * i by A7, INT_1:def 3;

0 <= i by A1, A8, Th20;

then reconsider i = i as Element of NAT by INT_1:3;

take i ; :: thesis: index D = (index B) * i

thus index D = (index B) * i by A8; :: thesis: verum

end;A8: index D = (index B) * i by A7, INT_1:def 3;

0 <= i by A1, A8, Th20;

then reconsider i = i as Element of NAT by INT_1:3;

take i ; :: thesis: index D = (index B) * i

thus index D = (index B) * i by A8; :: thesis: verum

A10: index (C,B) >= index (A,D) by A1, A2, Th19;

A11: index B = index D

proof

index A divides (index B) * (index E)
by A6, INT_1:def 3;
assume A12:
index B <> index D
; :: thesis: contradiction

index D > 0 by A1, Th20;

then index B <= index D by A9, NAT_D:7;

hence contradiction by A10, A12, XXREAL_0:1; :: thesis: verum

end;index D > 0 by A1, Th20;

then index B <= index D by A9, NAT_D:7;

hence contradiction by A10, A12, XXREAL_0:1; :: thesis: verum

then A13: index A divides index E by A5, INT_2:25;

ex n being Element of NAT st index E = (index A) * n

proof

then A15:
index A divides index E
by NAT_D:def 3;
consider i being Integer such that

A14: index E = (index A) * i by A13, INT_1:def 3;

0 <= i by A1, A14, Th20;

then reconsider i = i as Element of NAT by INT_1:3;

take i ; :: thesis: index E = (index A) * i

thus index E = (index A) * i by A14; :: thesis: verum

end;A14: index E = (index A) * i by A13, INT_1:def 3;

0 <= i by A1, A14, Th20;

then reconsider i = i as Element of NAT by INT_1:3;

take i ; :: thesis: index E = (index A) * i

thus index E = (index A) * i by A14; :: thesis: verum

A16: index A >= index E by A1, A3, Th19;

index A = index E

proof

hence
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
by A11; :: thesis: verum
assume A17:
index A <> index E
; :: thesis: contradiction

index E > 0 by A1, Th20;

then index A <= index E by A15, NAT_D:7;

hence contradiction by A16, A17, XXREAL_0:1; :: thesis: verum

end;index E > 0 by A1, Th20;

then index A <= index E by A15, NAT_D:7;

hence contradiction by A16, A17, XXREAL_0:1; :: thesis: verum