theorem Th20: :: MSUALG_7:20
for r1, r2 being Real st r1 <= r2 holds
RealSubLatt (r1,r2) is complete