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) and
A2: m in dom (SgmX RealOrd ,A) and
A3: n < m ; :: thesis: not (SgmX RealOrd ,A) . m <= (SgmX RealOrd ,A) . n
A4: RealOrd linearly_orders A by Th11, ORDERS_1:134;
SgmX RealOrd ,A is one-to-one by Th11, ORDERS_1:134, TRIANG_1:8;
then A5: (SgmX RealOrd ,A) . n <> (SgmX RealOrd ,A) . m by A1, A2, A3, FUNCT_1:def 8;
( (SgmX RealOrd ,A) /. n = (SgmX RealOrd ,A) . n & (SgmX RealOrd ,A) /. m = (SgmX RealOrd ,A) . m ) by A1, A2, PARTFUN1:def 8;
then [((SgmX RealOrd ,A) . n),((SgmX RealOrd ,A) . m)] in RealOrd by A1, A2, A3, A4, TRIANG_1:def 2;
then (SgmX RealOrd ,A) . n <= (SgmX RealOrd ,A) . m by Th9;
hence not (SgmX RealOrd ,A) . m <= (SgmX RealOrd ,A) . n by A5, XXREAL_0:1; :: thesis: verum