let n be Nat; :: thesis: for x being object st x in Segm (n + 1) holds
not not x = 0 & ... & not x = n
let x be object ; :: thesis: ( x in Segm (n + 1) implies not not x = 0 & ... & not x = n )
assume A1: x in Segm (n + 1) ; :: thesis: not not x = 0 & ... & not x = n
then reconsider k = x as Nat ;
k < n + 1 by A1, Th32;
then k <= n by Th13;
hence not not x = 0 & ... & not x = n ; :: thesis: verum