theorem Th53: :: NUMBER17:53

for n being Nat
for e being object holds (Segm (n + 1)) --> e = <%e%> ^ ((Segm n) --> e)