theorem Th1: :: NEWTON:1

for n being Nat st n >= 1 holds
Seg n = ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n}