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