let n be Ordinal; :: thesis: for T being TermOrder of n
for b1, b2 being bag of n holds
( max b1,b2,T = b1 or max b1,b2,T = b2 )
let T be TermOrder of n; :: thesis: for b1, b2 being bag of n holds
( max b1,b2,T = b1 or max b1,b2,T = b2 )
let b1, b2 be bag of n; :: thesis: ( max b1,b2,T = b1 or max b1,b2,T = b2 )
assume A1: max b1,b2,T <> b1 ; :: thesis: max b1,b2,T = b2

now

per cases ( not b2 <= b1,T or b1 = b2 ) by A1, Def5;

case not b2 <= b1,T ; :: thesis: max b1,b2,T = b2

hence max b1,b2,T = b2 by Def5; :: thesis: verum

end;

case b1 = b2 ; :: thesis: contradiction

then b2 <= b1,T by Lm2;
hence contradiction by A1, Def5; :: thesis: verum

end;

end;

end;

hence max b1,b2,T = b2 ; :: thesis: verum