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