theorem Th6: :: JORDAN1H:6

RealOrd linearly_orders REAL