let A be finite Subset of REAL; :: thesis: SgmX (RealOrd,A) is increasing
set IT = SgmX (RealOrd,A);
let n, m be Nat; :: according to SEQM_3:def 1 :: thesis: ( not n in dom (SgmX (RealOrd,A)) or not m in dom (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 Th6, ORDERS_1:38;
( (SgmX (RealOrd,A)) /. n = (SgmX (RealOrd,A)) . n & (SgmX (RealOrd,A)) /. m = (SgmX (RealOrd,A)) . m ) by A1, PARTFUN1:def 6;
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 Th4;
SgmX (RealOrd,A) is one-to-one by Th6, ORDERS_1:38, PRE_POLY:10;
then (SgmX (RealOrd,A)) . n <> (SgmX (RealOrd,A)) . m by A1, A2, FUNCT_1:def 4;
hence not (SgmX (RealOrd,A)) . m <= (SgmX (RealOrd,A)) . n by A4, XXREAL_0:1; :: thesis: verum