let n, m be Nat; 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; 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); ( 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 )
; (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; verum