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: ( S₂[n] implies S₂[n + 1] )
assume A3: S₂[n] ; :: thesis: S₂[n + 1]
let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: ( card X = n + 1 implies ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r] )
assume A4: card X = n + 1 ; :: thesis: ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r]
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 ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r]

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: verum

end;

suppose A8: n <> 0 ; :: thesis: ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r]

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 ( Vrootr p <= Vrootr q or not Vrootr p <= Vrootr q ) ;

suppose A14: Vrootr p <= Vrootr q ; :: thesis: ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r]

take r = p; :: thesis: S₁[X,r]
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: ( t in X implies Vrootr r <= Vrootr t )
assume t in X ; :: thesis: Vrootr r <= Vrootr t
then A15: ( t in Y or t in {p} ) by XBOOLE_0:def 3, A12;

per cases ( t in Y or t = p ) by A15, TARSKI:def 1;

suppose t in Y ; :: thesis: Vrootr r <= Vrootr t

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

end;

suppose t = p ; :: thesis: Vrootr r <= Vrootr t

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

end;

end;

end;

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

end;

suppose A16: not Vrootr p <= Vrootr q ; :: thesis: ex r being finite binary DecoratedTree of IndexedREAL st S₁[X,r]

take r = q; :: thesis: S₁[X,r]
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: ( t in X implies Vrootr r <= Vrootr t )
assume A17: t in X ; :: thesis: Vrootr r <= Vrootr t

per cases ( t in Y or t in {p} ) by A17, A12, XBOOLE_0:def 3;

suppose t in Y ; :: thesis: Vrootr r <= Vrootr t

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

end;

suppose t in {p} ; :: thesis: Vrootr r <= Vrootr t

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

end;

end;

end;

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

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: verum