defpred S1[ 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
S1[{xi}]
proof
let xi be Element of REAL ; :: thesis: ( xi in X implies S1[{xi}] )
assume xi in X ; :: thesis: S1[{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 & S1[B] holds
S1[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 & S1[B] holds
S1[B \/ {x}]

let B be non empty finite Subset of REAL; :: thesis: ( x in X & B c= X & not x in B & S1[B] implies S1[B \/ {x}] )
assume that
x in X and
B c= X and
not x in B and
A3: S1[B] ; :: thesis: S1[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: S1[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: S1[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 ; :: thesis: verum
end;
end;
end;
thus S1[X] from CHAIN_1:sch 2(A1, A2); :: thesis: verum