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 ) )

now :: thesis: o in n

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;

hence o in n ; :: thesis: ( a . o < b . o & ( for l being Ordinal st l in o holds
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