theorem :: BAGORDER:2

for n, k being Element of NAT holds
( k in Seg n iff ( k - 1 is Element of NAT & k - 1 < n ) )