let G be addGroup; :: 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_1A:def 41 :: thesis: (N1 /\ N2) * a = addMagma(# the carrier of (N1 /\ N2), the addF of (N1 /\ N2) #)
thus (N1 /\ N2) * a = (N1 * a) /\ (N2 * a) by Th63
.= N1 /\ (N2 * a) by Def13
.= addMagma(# the carrier of (N1 /\ N2), the addF of (N1 /\ N2) #) by Def13 ; :: thesis: verum