let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: 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 ; :: thesis: not MakeTree (t,s,((MaxVl X) + 1)) in X
assume A1: MakeTree (t,s,((MaxVl X) + 1)) in X ; :: thesis: 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; :: thesis: verum