theorem Th30: :: NAT_6:30

for p, q being 2 _greater Prime st p <> q holds
(Leg (p,q)) * (Leg (q,p)) = (- 1) |^ (((p - 1) / 2) * ((q - 1) / 2))