[mizar] Mizar theorem GROUP_6:93

[Victor Makarov <viktmak@gmail.com>]

Dear Forum:

I am trying to understand the statement of the theorem GROUP_6:93:

https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=:B:JVk/NDA9PyNzODcrNSNsYTg1ND81NCN2bGJrZHFwd2A4PWM1MzJjZDRjNmBmNzQ0ZmA9NmRkNzM0M2RkPWBjYDFmYGE3ZmcxNCNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=http%3a%2f%2fmizar.org%2fJFM%2fVol3%2fgroup_6.abs.html%23K2 

theorem :: GROUP_6:93
   for N being strict normal Subgroup of G holds
 (B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic;

What does mean (B "\/" N)" and (B "\/" N,N)`*` ?

How is the theorem  GROUP_6:93 related to the Second Isomorphism Theorem?

Second Isomorphism Theorem:
(Theorem B in Wikipedia):
https://mx10.uwb.edu.pl/fmlurlsvc/?fewReq=:B:JVk/NDA9PyNzODcrNSNsYTg1ND81NCN2bGJrZHFwd2A4MWEwYTYyMTZkMz02NzIzZDdmM2Y0ZmBkPDAxPGQ0N2AyNjI3NTIxMSNxODQyNTc1MTYwPDEjdGxhODZHPUF3QFBdNTc2MDY2KDZHPUF3QFBcNTc2MDY2I3dmdXE4aGx/ZHcoY2p3cGhFaGx/ZHcrcHJnK2BhcCt1aSNmODY8I21haTg1&url=https%3a%2f%2fen.wikipedia.org%2fwiki%2fIsomorphism_theorems 

Theorem B (groups)

Let G be a group. Let S be a subgroup of G, and let N be a normal subgroup of G.
 Then the following hold:

The product SN is a subgroup of G,
The subgroup N is a normal subgroup of SN},
The intersection S/\N is a normal subgroup of S, and
The quotient groups (SN)/N and S/(S/\N)} are isomorphic.
(Wikipedia uses another symbol(\cap) for the intersection).

Thanks in advance,

Victor Makarov