set L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } ;
A1: X is finite ;
A2: { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } is finite from FRAENKEL:sch 21(A1);
consider q being object such that
A3: q in X by XBOOLE_0:def 1;
reconsider q = q as Element of BinFinTrees IndexedREAL by A3;
A4: Vrootl q in { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } by A3;

now :: thesis: for x being object st x in { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } holds
x in NAT

let x be object ; :: thesis: ( x in { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } implies x in NAT )
assume x in { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } ; :: thesis: x in NAT
then consider p being Element of BinFinTrees IndexedREAL such that
A5: ( x = Vrootl p & p in X ) ;
reconsider p = p as DecoratedTree of IndexedREAL ;
( dom p is finite & p is binary ) by Def2;
then reconsider p = p as finite binary DecoratedTree of IndexedREAL by FINSET_1:10;
thus x in NAT by A5, ORDINAL1:def 12; :: thesis: verum

end;

then reconsider L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } as non empty finite Subset of NAT by A2, A4, TARSKI:def 3;
take max L ; :: thesis: ( max L is Nat & ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & max L = max L ) )
thus ( max L is Nat & ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & max L = max L ) ) by TARSKI:1; :: thesis: verum