let n be Nat; :: thesis: 1 is Nat of n
1 in Seg (n + 1) by Th20;
hence 1 is Nat of n by Th7; :: thesis: verum