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