let b3, b4 be bag of X; :: thesis: ( ( for k being object holds b3 . k =max ((b1 . k),(b2 . k)) ) & ( for k being object holds b4 . k =max ((b1 . k),(b2 . k)) ) implies b3 = b4 ) assume A13:
for k being object holds b3 . k =max ((b1 . k),(b2 . k))
; :: thesis: ( ex k being object st not b4 . k =max ((b1 . k),(b2 . k)) or b3 = b4 ) assume A14:
for k being object holds b4 . k =max ((b1 . k),(b2 . k))
; :: thesis: b3 = b4