for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for s, t being finite binary DecoratedTree of IndexedREAL st s is one-to-one & t is one-to-one & t in X & s in X & (rng s) /\ (rng t) = {} & ( for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ) holds
MakeTree (t,s,((MaxVl X) + 1)) is one-to-one