let n be Ordinal; :: thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
let T be connected TermOrder of n; :: thesis: for b1, b2 being bag of n holds
( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )
let b1, b2 be bag of n; :: thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )

per cases ( b2 <= b1,T or b1 <= b2,T ) by Lm5;

suppose A1: b2 <= b1,T ; :: thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )

then max (b1,b2,T) = b1 by Def5;
hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A1, Lm2; :: thesis: verum

end;

suppose A2: b1 <= b2,T ; :: thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )

now :: thesis: ( ( b1 = b2 & b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) or ( b1 <> b2 & b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) )

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

case A3: b1 = b2 ; :: thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )

then max (b1,b2,T) = b1 by Lm6;
hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A3, Lm2; :: thesis: verum

end;

case b1 <> b2 ; :: thesis: ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )

then b1 < b2,T by A2;
then not b2 <= b1,T by Th5;
then max (b1,b2,T) = b2 by Def5;
hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) by A2, Lm2; :: thesis: verum

end;

end;

end;

hence ( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T ) ; :: thesis: verum

end;

end;