let n be Ordinal; :: thesis: for T being TermOrder of n
for b being bag of n holds
( min b,b,T = b & max b,b,T = b )
let T be TermOrder of n; :: thesis: for b being bag of n holds
( min b,b,T = b & max b,b,T = b )
let b be bag of n; :: thesis: ( min b,b,T = b & max b,b,T = b )
thus min b,b,T = b by Def4; :: thesis: max b,b,T = b
thus max b,b,T = b by Def5; :: thesis: verum