theorem Th27: :: NAT_1:39

for m, n being Nat holds
( n <= m iff Segm n c= Segm m )