let X, Z be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: for Y being set st Z = X \ Y holds
MaxVl Z <= MaxVl X
let Y be set ; :: thesis: ( Z = X \ Y implies MaxVl Z <= MaxVl X )
assume A1: Z = X \ Y ; :: thesis: MaxVl Z <= MaxVl X

per cases ( X misses Y or X meets Y ) ;

suppose X misses Y ; :: thesis: MaxVl Z <= MaxVl X

hence MaxVl Z <= MaxVl X by XBOOLE_1:83, A1; :: thesis: verum

end;

suppose X meets Y ; :: thesis: MaxVl Z <= MaxVl X

A2: X = Z \/ (X \ Z) by XBOOLE_1:45, A1, XBOOLE_1:36;

per cases ( X = Z or X <> Z ) ;

suppose X = Z ; :: thesis: MaxVl Z <= MaxVl X

hence MaxVl Z <= MaxVl X ; :: thesis: verum

end;

suppose X <> Z ; :: thesis: MaxVl Z <= MaxVl X

then Z c< X by A1, XBOOLE_1:36, XBOOLE_0:def 8;
then reconsider W = X \ Z as non empty finite Subset of (BinFinTrees IndexedREAL) by XBOOLE_1:105;
MaxVl X = max ((MaxVl Z),(MaxVl W)) by Th2, A2;
hence MaxVl Z <= MaxVl X by XXREAL_0:25; :: thesis: verum

end;

end;

end;

end;