let n, m be Ordinal; :: thesis: for b1, b2 being bag of n st support b1 = {m} & support b2 = {m} holds
( b1 <=' b2 iff b1 . m <= b2 . m )
let b1, b2 be bag of n; :: thesis: ( support b1 = {m} & support b2 = {m} implies ( b1 <=' b2 iff b1 . m <= b2 . m ) )
assume H0: ( support b1 = {m} & support b2 = {m} ) ; :: thesis: ( b1 <=' b2 iff b1 . m <= b2 . m )

H1: now :: thesis: for l being Ordinal st l <> m holds
( b1 . l = 0 & b2 . l = 0 )

let l be Ordinal; :: thesis: ( l <> m implies ( b1 . l = 0 & b2 . l = 0 ) )
assume l <> m ; :: thesis: ( b1 . l = 0 & b2 . l = 0 )
then H2: ( not l in support b1 & not l in support b2 ) by H0, TARSKI:def 1;
hence b1 . l = 0 by PRE_POLY:def 7; :: thesis: b2 . l = 0
thus b2 . l = 0 by H2, PRE_POLY:def 7; :: thesis: verum

end;

A: now :: thesis: ( b1 <=' b2 implies b1 . m <= b2 . m )

assume A1: b1 <=' b2 ; :: thesis: b1 . m <= b2 . m

per cases ( b1 = b2 or b1 <> b2 ) ;

suppose b1 = b2 ; :: thesis: b1 . m <= b2 . m

hence b1 . m <= b2 . m ; :: thesis: verum

end;

suppose b1 <> b2 ; :: thesis: b1 . m <= b2 . m

then consider k being Ordinal such that
A3: ( b1 . k < b2 . k & ( for l being Ordinal st l in k holds
b1 . l = b2 . l ) ) by A1, PRE_POLY:def 10, PRE_POLY:def 9;
k = m by H1, A3;
hence b1 . m <= b2 . m by A3; :: thesis: verum

end;

end;

end;

now :: thesis: ( b1 . m <= b2 . m implies b1 <=' b2 )

assume A1: b1 . m <= b2 . m ; :: thesis: b1 <=' b2

per cases ( b1 = b2 or b1 <> b2 ) ;

suppose b1 = b2 ; :: thesis: b1 <=' b2

hence b1 <=' b2 ; :: thesis: verum

end;

suppose A4: b1 <> b2 ; :: thesis: b1 <=' b2

A2: now :: thesis: not b1 . m = b2 . m

assume A5: b1 . m = b2 . m ; :: thesis: contradiction

now :: thesis: for o being object st o in n holds
b1 . o = b2 . o

let o be object ; :: thesis: ( o in n implies b1 . b₁ = b2 . b₁ )
assume A6: o in n ; :: thesis: b1 . b₁ = b2 . b₁

per cases ( o = m or o <> m ) ;

suppose o = m ; :: thesis: b1 . b₁ = b2 . b₁

hence b1 . o = b2 . o by A5; :: thesis: verum

end;

suppose A7: o <> m ; :: thesis: b1 . b₁ = b2 . b₁

hence b1 . o = 0 by H1, A6
.= b2 . o by A6, A7, H1 ;
:: thesis: verum

end;

end;

end;

hence contradiction by A4, PBOOLE:def 10; :: thesis: verum

end;

ex k being Ordinal st
( b1 . k < b2 . k & ( for l being Ordinal st l in k holds
b1 . l = b2 . l ) )

proof

take k = m; :: thesis: ( b1 . k < b2 . k & ( for l being Ordinal st l in k holds
b1 . l = b2 . l ) )
thus b1 . k < b2 . k by A2, A1, XXREAL_0:1; :: thesis: for l being Ordinal st l in k holds
b1 . l = b2 . l

now :: thesis: for l being Ordinal st l in k holds
b1 . l = b2 . l

let l be Ordinal; :: thesis: ( l in k implies b1 . l = b2 . l )
assume l in k ; :: thesis: b1 . l = b2 . l
then A3: l <> m ;
hence b1 . l = 0 by H1
.= b2 . l by A3, H1 ;
:: thesis: verum

end;

hence for l being Ordinal st l in k holds
b1 . l = b2 . l ; :: thesis: verum

end;

hence b1 <=' b2 by PRE_POLY:def 9, PRE_POLY:def 10; :: thesis: verum

end;

end;

end;

hence ( b1 <=' b2 iff b1 . m <= b2 . m ) by A; :: thesis: verum