let n be Ordinal; :: thesis: for a, b being bag of n st a < b holds

ex o being Ordinal st

( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) )

let a, b be bag of n; :: thesis: ( a < b implies ex o being Ordinal st

( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) ) )

assume a < b ; :: thesis: ex o being Ordinal st

( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) )

then consider o being Ordinal such that

A1: a . o < b . o and

A2: for l being Ordinal st l in o holds

a . l = b . l by PRE_POLY:def 9;

take o ; :: thesis: ( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) )

a . l = b . l ) )

thus a . o < b . o by A1; :: thesis: for l being Ordinal st l in o holds

a . l = b . l

thus for l being Ordinal st l in o holds

a . l = b . l by A2; :: thesis: verum

ex o being Ordinal st

( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) )

let a, b be bag of n; :: thesis: ( a < b implies ex o being Ordinal st

( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) ) )

assume a < b ; :: thesis: ex o being Ordinal st

( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) )

then consider o being Ordinal such that

A1: a . o < b . o and

A2: for l being Ordinal st l in o holds

a . l = b . l by PRE_POLY:def 9;

take o ; :: thesis: ( o in n & a . o < b . o & ( for l being Ordinal st l in o holds

a . l = b . l ) )

now :: thesis: o in n

hence
o in n
; :: thesis: ( a . o < b . o & ( for l being Ordinal st l in o holds assume A3:
not o in n
; :: thesis: contradiction

then A4: not o in dom b by PARTFUN1:def 2;

n = dom a by PARTFUN1:def 2;

then a . o = 0 by A3, FUNCT_1:def 2;

hence contradiction by A1, A4, FUNCT_1:def 2; :: thesis: verum

end;then A4: not o in dom b by PARTFUN1:def 2;

n = dom a by PARTFUN1:def 2;

then a . o = 0 by A3, FUNCT_1:def 2;

hence contradiction by A1, A4, FUNCT_1:def 2; :: thesis: verum

a . l = b . l ) )

thus a . o < b . o by A1; :: thesis: for l being Ordinal st l in o holds

a . l = b . l

thus for l being Ordinal st l in o holds

a . l = b . l by A2; :: thesis: verum