let n be Element of NAT ; :: thesis: 1 is Nat of n
1 in Seg (n + 1) by Th22;
hence 1 is Nat of n by Th8; :: thesis: verum