for n being Nat holds Segm n c= Segm (n + 1) by Th11, Th27;