theorem :: NAT_6:26

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