let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: for w being finite binary DecoratedTree of IndexedREAL st X = {w} holds
MaxVl X = Vrootl w
let w be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( X = {w} implies MaxVl X = Vrootl w )
assume A1: X = {w} ; :: thesis: MaxVl X = Vrootl w
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;
A3: for n being object st n in L holds
n = Vrootl w

proof

let n be object ; :: thesis: ( n in L implies n = Vrootl w )
assume n in L ; :: thesis: n = Vrootl w
then ex p being Element of BinFinTrees IndexedREAL st
( n = Vrootl p & p in X ) by A2;
hence n = Vrootl w by TARSKI:def 1, A1; :: thesis: verum

end;

for n being object st n = Vrootl w holds
n in L

proof

let n be object ; :: thesis: ( n = Vrootl w implies n in L )
assume A4: n = Vrootl w ; :: thesis: n in L
consider y being object such that
A5: y in L by XBOOLE_0:def 1;
ex p being Element of BinFinTrees IndexedREAL st
( y = Vrootl p & p in X ) by A2, A5;
hence n in L by A5, A4, TARSKI:def 1, A1; :: thesis: verum

end;

then L = {(Vrootl w)} by TARSKI:def 1, A3;
hence MaxVl X = Vrootl w by A2, XXREAL_2:11; :: thesis: verum