let n be Nat; :: thesis: succ n = n + 1
thus succ n = succ (Segm n)
.= Segm (n + 1) by NAT_1:38
.= n + 1 ; :: thesis: verum