let n be Ordinal; :: thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min b1,b2,T = min b2,b1,T & max b1,b2,T = max b2,b1,T )
let T be connected TermOrder of n; :: thesis: for b1, b2 being bag of n holds
( min b1,b2,T = min b2,b1,T & max b1,b2,T = max b2,b1,T )
let b1, b2 be bag of n; :: thesis: ( min b1,b2,T = min b2,b1,T & max b1,b2,T = max b2,b1,T )
now
per cases ( min b1,b2,T = b1 or min b1,b2,T <> b1 ) ;
case A1: min b1,b2,T = b1 ; :: thesis: min b1,b2,T = min b2,b1,T
now
per cases ( b1 <= b2,T or b1 = b2 ) by A1, Def4;
case A2: b1 <= b2,T ; :: thesis: min b1,b2,T = min b2,b1,T
now
per cases ( b1 = b2 or b1 <> b2 ) ;
case b1 = b2 ; :: thesis: min b2,b1,T = min b1,b2,T
hence min b2,b1,T = min b1,b2,T ; :: thesis: verum
end;
case b1 <> b2 ; :: thesis: min b2,b1,T = min b1,b2,T
then not b2 <= b1,T by A2, Lm3;
hence min b2,b1,T = min b1,b2,T by A1, Def4; :: thesis: verum
end;
end;
end;
hence min b1,b2,T = min b2,b1,T ; :: thesis: verum
end;
case b1 = b2 ; :: thesis: min b2,b1,T = min b1,b2,T
hence min b2,b1,T = min b1,b2,T ; :: thesis: verum
end;
end;
end;
hence min b1,b2,T = min b2,b1,T ; :: thesis: verum
end;
case A3: min b1,b2,T <> b1 ; :: thesis: min b1,b2,T = min b2,b1,T
A4: now
assume not b2 <= b1,T ; :: thesis: contradiction
then b1 <= b2,T by Lm5;
hence contradiction by A3, Def4; :: thesis: verum
end;
thus min b1,b2,T = b2 by A3, Th11
.= min b2,b1,T by A4, Def4 ; :: thesis: verum
end;
end;
end;
hence min b1,b2,T = min b2,b1,T ; :: thesis: max b1,b2,T = max b2,b1,T
now
per cases ( max b1,b2,T = b1 or max b1,b2,T <> b1 ) ;
case A5: max b1,b2,T = b1 ; :: thesis: max b1,b2,T = max b2,b1,T
now
per cases ( b2 <= b1,T or b1 = b2 ) by A5, Def5;
case A6: b2 <= b1,T ; :: thesis: max b1,b2,T = max b2,b1,T
now
per cases ( b1 = b2 or b1 <> b2 ) ;
case b1 = b2 ; :: thesis: max b2,b1,T = max b1,b2,T
hence max b2,b1,T = max b1,b2,T ; :: thesis: verum
end;
case b1 <> b2 ; :: thesis: max b2,b1,T = max b1,b2,T
then not b1 <= b2,T by A6, Lm3;
hence max b2,b1,T = max b1,b2,T by A5, Def5; :: thesis: verum
end;
end;
end;
hence max b1,b2,T = max b2,b1,T ; :: thesis: verum
end;
case b1 = b2 ; :: thesis: max b2,b1,T = max b1,b2,T
hence max b2,b1,T = max b1,b2,T ; :: thesis: verum
end;
end;
end;
hence max b1,b2,T = max b2,b1,T ; :: thesis: verum
end;
case A7: max b1,b2,T <> b1 ; :: thesis: max b2,b1,T = max b1,b2,T
now
per cases ( b1 <= b2,T or b2 <= b1,T ) by Lm5;
case b1 <= b2,T ; :: thesis: max b2,b1,T = max b1,b2,T
hence max b2,b1,T = b2 by Def5
.= max b1,b2,T by A7, Th12 ;
:: thesis: verum
end;
case b2 <= b1,T ; :: thesis: max b2,b1,T = max b1,b2,T
hence max b2,b1,T = max b1,b2,T by A7, Def5; :: thesis: verum
end;
end;
end;
hence max b2,b1,T = max b1,b2,T ; :: thesis: verum
end;
end;
end;
hence max b1,b2,T = max b2,b1,T ; :: thesis: verum