let n be Ordinal; :: thesis: for T being TermOrder of n
for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 )
let T be TermOrder of n; :: thesis: for b1, b2 being bag of n holds
( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 )
let b1, b2 be bag of n; :: thesis: ( min (b1,b2,T) = b1 or min (b1,b2,T) = b2 )
assume A1: min (b1,b2,T) <> b1 ; :: thesis: min (b1,b2,T) = b2
now :: thesis: ( ( not b1 <= b2,T & min (b1,b2,T) = b2 ) or ( b1 = b2 & contradiction ) )
per cases ( not b1 <= b2,T or b1 = b2 ) by A1, Def4;
case not b1 <= b2,T ; :: thesis: min (b1,b2,T) = b2
hence min (b1,b2,T) = b2 by Def4; :: thesis: verum
end;
case b1 = b2 ; :: thesis: contradiction
then b1 <= b2,T by Lm2;
hence contradiction by A1, Def4; :: thesis: verum
end;
end;
end;
hence min (b1,b2,T) = b2 ; :: thesis: verum