let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: for p being Element of BinFinTrees IndexedREAL st p in X holds
Vrootl p <= MaxVl X
let p be Element of BinFinTrees IndexedREAL; :: thesis: ( p in X implies Vrootl p <= MaxVl X )
assume A1: p in X ; :: thesis: Vrootl p <= MaxVl X
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;
Vrootl p in L by A2, A1;
hence Vrootl p <= MaxVl X by XXREAL_2:def 8, A2; :: thesis: verum