let A be finite Subset of REAL ; :: thesis: SgmX RealOrd ,A is increasing
set IT = SgmX RealOrd ,A;
let n, m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: ( not n in proj1 (SgmX RealOrd ,A) or not m in proj1 (SgmX RealOrd ,A) or m <= n or not (SgmX RealOrd ,A) . m <= (SgmX RealOrd ,A) . n )
assume that
A1: ( n in dom (SgmX RealOrd ,A) & m in dom (SgmX RealOrd ,A) ) and
A2: n < m ; :: thesis: not (SgmX RealOrd ,A) . m <= (SgmX RealOrd ,A) . n
A3: RealOrd linearly_orders A by Th11, ORDERS_1:134;
( (SgmX RealOrd ,A) /. n = (SgmX RealOrd ,A) . n & (SgmX RealOrd ,A) /. m = (SgmX RealOrd ,A) . m ) by A1, PARTFUN1:def 8;
then [((SgmX RealOrd ,A) . n),((SgmX RealOrd ,A) . m)] in RealOrd by A1, A2, A3, PRE_POLY:def 2;
then A4: (SgmX RealOrd ,A) . n <= (SgmX RealOrd ,A) . m by Th9;
SgmX RealOrd ,A is one-to-one by Th11, ORDERS_1:134, PRE_POLY:10;
then (SgmX RealOrd ,A) . n <> (SgmX RealOrd ,A) . m by A1, A2, FUNCT_1:def 8;
hence not (SgmX RealOrd ,A) . m <= (SgmX RealOrd ,A) . n by A4, XXREAL_0:1; :: thesis: verum