theorem :: NAT_6:26

for p being natural number holds Leg (p,p) = 0 by Def3;