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