let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G holds N1 /\ N2 is normal
let N1, N2 be strict normal Subgroup of G; :: thesis: N1 /\ N2 is normal
let a be Element of G; :: according to GROUP_3:def 13 :: thesis: (N1 /\ N2) |^ a = multMagma(# the carrier of (N1 /\ N2), the multF of (N1 /\ N2) #)
thus (N1 /\ N2) |^ a = (N1 |^ a) /\ (N2 |^ a) by Th63
.= N1 /\ (N2 |^ a) by Def13
.= multMagma(# the carrier of (N1 /\ N2), the multF of (N1 /\ N2) #) by Def13 ; :: thesis: verum