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 :: thesis: ( ( min (b1,b2,T) = b1 & min (b1,b2,T) = min (b2,b1,T) ) or ( min (b1,b2,T) <> b1 & min (b1,b2,T) = min (b2,b1,T) ) )
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 :: thesis: ( ( b1 <= b2,T & min (b1,b2,T) = min (b2,b1,T) ) or ( b1 = b2 & min (b2,b1,T) = min (b1,b2,T) ) )
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 :: thesis: ( ( b1 = b2 & min (b2,b1,T) = min (b1,b2,T) ) or ( b1 <> b2 & min (b2,b1,T) = min (b1,b2,T) ) )
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 :: thesis: b2 <= b1,T
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 :: thesis: ( ( max (b1,b2,T) = b1 & max (b1,b2,T) = max (b2,b1,T) ) or ( max (b1,b2,T) <> b1 & max (b2,b1,T) = max (b1,b2,T) ) )
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 :: thesis: ( ( b2 <= b1,T & max (b1,b2,T) = max (b2,b1,T) ) or ( b1 = b2 & max (b2,b1,T) = max (b1,b2,T) ) )
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 :: thesis: ( ( b1 = b2 & max (b2,b1,T) = max (b1,b2,T) ) or ( b1 <> b2 & max (b2,b1,T) = max (b1,b2,T) ) )
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 :: thesis: ( ( b1 <= b2,T & max (b2,b1,T) = max (b1,b2,T) ) or ( b2 <= b1,T & max (b2,b1,T) = max (b1,b2,T) ) )
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