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 :: thesis: ( max (b1,b2,T) = b2 implies min (b1,b2,T) = b1 )
assume A2: max (b1,b2,T) = b2 ; :: thesis: min (b1,b2,T) = b1
now :: thesis: ( ( not b2 <= b1,T & min (b1,b2,T) = b1 ) or ( b1 = b2 & min (b1,b2,T) = b1 ) )
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 :: thesis: ( min (b1,b2,T) = b1 implies max (b1,b2,T) = b2 )
assume A3: min (b1,b2,T) = b1 ; :: thesis: max (b1,b2,T) = b2
now :: thesis: ( ( b1 <= b2,T & max (b1,b2,T) = b2 ) or ( b1 = b2 & max (b1,b2,T) = b2 ) )
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