let G be Group; :: thesis: 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; :: thesis: [.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 ;
:: thesis: verum