defpred S₁[ set ] means ex ri being Element of REAL st
( ri in $1 & ( for xi being Real st xi in $1 holds
ri >= xi ) );
let X be non empty finite Subset of REAL; :: thesis: ex ri being Element of REAL st
( ri in X & ( for xi being Real st xi in X holds
ri >= xi ) )
A1: for xi being Element of REAL st xi in X holds
S₁[{xi}]

proof

let xi be Element of REAL ; :: thesis: ( xi in X implies S₁[{xi}] )
assume xi in X ; :: thesis: S₁[{xi}]
take xi ; :: thesis: ( xi in {xi} & ( for xi being Real st xi in {xi} holds
xi >= xi ) )
thus ( xi in {xi} & ( for xi being Real st xi in {xi} holds
xi >= xi ) ) by TARSKI:def 1; :: thesis: verum

end;

A2: for x being Element of REAL
for B being non empty finite Subset of REAL st x in X & B c= X & not x in B & S₁[B] holds
S₁[B \/ {x}]

proof

let x be Element of REAL ; :: thesis: for B being non empty finite Subset of REAL st x in X & B c= X & not x in B & S₁[B] holds
S₁[B \/ {x}]
let B be non empty finite Subset of REAL; :: thesis: ( x in X & B c= X & not x in B & S₁[B] implies S₁[B \/ {x}] )
assume that
x in X and
B c= X and
not x in B and
A3: S₁[B] ; :: thesis: S₁[B \/ {x}]
consider ri being Real such that
A4: ri in B and
A5: for xi being Real st xi in B holds
ri >= xi by A3;
set B9 = B \/ {x};

A6: now :: thesis: for xi being Real holds
( xi in B \/ {x} iff ( xi in B or xi = x ) )

let xi be Real; :: thesis: ( xi in B \/ {x} iff ( xi in B or xi = x ) )
( xi in {x} iff xi = x ) by TARSKI:def 1;
hence ( xi in B \/ {x} iff ( xi in B or xi = x ) ) by XBOOLE_0:def 3; :: thesis: verum

end;

per cases ( x <= ri or ri < x ) ;

suppose A7: x <= ri ; :: thesis: S₁[B \/ {x}]

reconsider ri = ri as Element of REAL by XREAL_0:def 1;
take ri ; :: thesis: ( ri in B \/ {x} & ( for xi being Real st xi in B \/ {x} holds
ri >= xi ) )
thus ri in B \/ {x} by A4, A6; :: thesis: for xi being Real st xi in B \/ {x} holds
ri >= xi
let xi be Real; :: thesis: ( xi in B \/ {x} implies ri >= xi )
assume xi in B \/ {x} ; :: thesis: ri >= xi
then ( xi in B or xi = x ) by A6;
hence ri >= xi by A5, A7; :: thesis: verum

end;

suppose A8: ri < x ; :: thesis: S₁[B \/ {x}]

take x ; :: thesis: ( x in B \/ {x} & ( for xi being Real st xi in B \/ {x} holds
x >= xi ) )
thus x in B \/ {x} by A6; :: thesis: for xi being Real st xi in B \/ {x} holds
x >= xi
let xi be Real; :: thesis: ( xi in B \/ {x} implies x >= xi )
assume xi in B \/ {x} ; :: thesis: x >= xi
then ( xi in B or xi = x ) by A6;
then ( ri >= xi or xi = x ) by A5;
hence x >= xi by A8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

thus S₁[X] from CHAIN_1:sch 2(A1, A2); :: thesis: verum