defpred S₂[ Nat] means for X being non empty finite Subset of (BinFinTrees IndexedREAL) st card X = $1 holds
ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r];
A1: S₂[ 0 ] ;
A2: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A3: S₂[n] ; :: thesis:
let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis:
assume A4: card X = n + 1 ; :: thesis:
consider p being object such that
A5: p in X by XBOOLE_0:def 1;
reconsider p = p as DecoratedTree of IndexedREAL by A5;
A6: ( dom p is finite & p is binary ) by A5, Def2;
reconsider p = p as finite binary DecoratedTree of IndexedREAL by A6, FINSET_1:10;

per cases ;

suppose n = 0 ; :: thesis:

then consider d being object such that
A7: X = {d} by CARD_2:42, A4;
X = {p} by A5, A7, TARSKI:def 1;
then S₁[X,p] by TARSKI:def 1;
hence ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r] ; :: thesis:

end;

suppose A8: n <> 0 ; :: thesis:

set Y = X \ {p};
A9: card {p} = 1 by CARD_2:42;
A10: card (X \ {p}) = (card X) - (card {p}) by ZFMISC_1:31, A5, CARD_2:44
.= n by A9, A4 ;
A11: X \ {p} c= X by XBOOLE_1:36;
reconsider Y = X \ {p} as non empty finite Subset of (BinFinTrees IndexedREAL) by A10, A8;
A12: X = Y \/ {p} by XBOOLE_1:45, ZFMISC_1:31, A5;
consider q being finite binary DecoratedTree of IndexedREAL such that
A13: S₁[Y,q] by A10, A3;

per cases ;

suppose A14: Vrootr p <= Vrootr q ; :: thesis:

take r = p; :: thesis:
for t being finite binary DecoratedTree of IndexedREAL st t in X holds
Vrootr r <= Vrootr t

proof

let t be finite binary DecoratedTree of IndexedREAL ; :: thesis:
assume t in X ; :: thesis:
then A15: ( t in Y or t in {p} ) by XBOOLE_0:def 3, A12;

per cases by A15, TARSKI:def 1;

suppose t in Y ; :: thesis:

then Vrootr q <= Vrootr t by A13;
hence Vrootr r <= Vrootr t by A14, XXREAL_0:2; :: thesis:

end;

suppose t = p ; :: thesis:

hence Vrootr r <= Vrootr t ; :: thesis:

end;

end;

end;

hence S₁[X,r] by A5; :: thesis:

end;

suppose A16: not Vrootr p <= Vrootr q ; :: thesis:

take r = q; :: thesis:
for t being finite binary DecoratedTree of IndexedREAL st t in X holds
Vrootr r <= Vrootr t

proof

let t be finite binary DecoratedTree of IndexedREAL ; :: thesis:
assume A17: t in X ; :: thesis:

per cases by A17, A12, XBOOLE_0:def 3;

suppose t in Y ; :: thesis:

hence Vrootr r <= Vrootr t by A13; :: thesis:

end;

suppose t in {p} ; :: thesis:

hence Vrootr r <= Vrootr t by A16, TARSKI:def 1; :: thesis:

end;

end;

end;

hence S₁[X,r] by A11, A13; :: thesis:

end;

end;

end;

end;

end;

A18: for n being Nat holds S₂[n] from NAT_1:sch 2(A1, A2);
card X is Nat ;
hence ex b₁ being finite binary DecoratedTree of IndexedREAL st
( b₁ in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds
Vrootr b₁ <= Vrootr q ) ) by A18; :: thesis: