for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for p being Element of BinFinTrees IndexedREAL st p in X holds
Vrootl p <= MaxVl X