let n, m be Nat; :: thesis: for O being Ordinal
for A being finite Subset of (Bags O) st n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m holds
(SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m
let O be Ordinal; :: thesis: for A being finite Subset of (Bags O) st n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m holds
(SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m
let A be finite Subset of (Bags O); :: thesis: ( n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m implies (SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m )
set S = SgmX ((BagOrder O),A);
assume A1: ( n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m ) ; :: thesis: (SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m
BagOrder O linearly_orders field (BagOrder O) by ORDERS_1:37;
then BagOrder O linearly_orders Bags O by ORDERS_1:12;
then BagOrder O linearly_orders A by ORDERS_1:38;
then A2: ( (SgmX ((BagOrder O),A)) /. n <> (SgmX ((BagOrder O),A)) /. m & [((SgmX ((BagOrder O),A)) /. n),((SgmX ((BagOrder O),A)) /. m)] in BagOrder O ) by PRE_POLY:def 2, A1;
then (SgmX ((BagOrder O),A)) /. n <=' (SgmX ((BagOrder O),A)) /. m by PRE_POLY:def 14;
hence (SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m by A2, PRE_POLY:def 10; :: thesis: verum