let X be non empty finite Subset of (BinFinTrees IndexedREAL); for s, t being finite binary DecoratedTree of IndexedREAL holds not MakeTree (t,s,((MaxVl X) + 1)) in X
let s, t be finite binary DecoratedTree of IndexedREAL ; not MakeTree (t,s,((MaxVl X) + 1)) in X
assume A1:
MakeTree (t,s,((MaxVl X) + 1)) in X
; contradiction
set px = MakeTree (t,s,((MaxVl X) + 1));
consider L being non empty finite Subset of NAT such that
A2:
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & MaxVl X = max L )
by Def9;
( dom (MakeTree (t,s,((MaxVl X) + 1))) is finite & dom (MakeTree (t,s,((MaxVl X) + 1))) is binary )
by BINTREE1:def 3;
then reconsider px = MakeTree (t,s,((MaxVl X) + 1)) as Element of BinFinTrees IndexedREAL by Def2;
Vrootl px in L
by A1, A2;
then A3:
Vrootl px <= MaxVl X
by A2, XXREAL_2:def 8;
px . {} = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))]
by TREES_4:def 4;
hence
contradiction
by NAT_1:13, A3; verum