let n be Nat; :: thesis: for x being object st x in Seg n holds
not not x = 1 & ... & not x = n
let x be object ; :: thesis: ( x in Seg n implies not not x = 1 & ... & not x = n )
assume A1: x in Seg n ; :: thesis: 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 ; :: thesis: verum