Предствлен новый метод доказательства инвариантности системы линейных неравенств для интерактивных циклов, определенных над полем рациональных чисел с линейным оператором в теле цикла. Метод учитывает предусловие цикла в виде системы линейных неравенств. Рассмотрения ограничены случеам, когда все собственные значения линейного оператора вещественны.
