theorem Th7: :: JORDAN1H:7

for A being finite Subset of REAL holds SgmX (RealOrd,A) is increasing