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