theorem Th2: :: HUFFMAN1:2

for X, Y, Z being non empty finite Subset of (BinFinTrees IndexedREAL) st Z = X \/ Y holds
MaxVl Z = max ((MaxVl X),(MaxVl Y))