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

A1: now

assume A2: max b1,b2,T = b2 ; :: thesis: min b1,b2,T = b1

now

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

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

then b1 <= b2,T by Lm5;
hence min b1,b2,T = b1 by Def4; :: thesis: verum

end;

case b1 = b2 ; :: thesis: min b1,b2,T = b1

hence min b1,b2,T = b1 by Th11; :: thesis: verum

end;

end;

end;

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

end;

now

assume A3: min b1,b2,T = b1 ; :: thesis: max b1,b2,T = b2

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

hence ( min b1,b2,T = b1 iff max b1,b2,T = b2 ) by A1; :: thesis: verum