for r1, r2 being Real st r1 <= r2 holds
RealSubLatt (r1,r2) is complete