let G be Group; for N1, N2, N3 being strict normal Subgroup of G holds [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]
let N1, N2, N3 be strict normal Subgroup of G; [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]
N2 "\/" N3 is normal Subgroup of G
by GROUP_4:54;
hence [.N1,(N2 "\/" N3).] =
[.(N2 "\/" N3),N1.]
by Th69
.=
[.N2,N1.] "\/" [.N3,N1.]
by Th70
.=
[.N1,N2.] "\/" [.N3,N1.]
by Th69
.=
[.N1,N2.] "\/" [.N1,N3.]
by Th69
;
verum