for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for w being finite binary DecoratedTree of IndexedREAL st X = {w} holds
MaxVl X = Vrootl w