theorem Th5: :: JORDAN1H:5

field RealOrd = REAL