defpred S1[ set ] means ex li being Element of REAL st
( li in \$1 & ( for xi being Real st xi in \$1 holds
li <= xi ) );
let X be non empty finite Subset of REAL; :: thesis: ex li being Element of REAL st
( li in X & ( for xi being Real st xi in X holds
li <= 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 li being Real such that
A4: li in B and
A5: for xi being Real st xi in B holds
li <= 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 ( li <= x or x < li ) ;
suppose A7: li <= x ; :: thesis: S1[B \/ {x}]
reconsider li = li as Element of REAL by XREAL_0:def 1;
take li ; :: thesis: ( li in B \/ {x} & ( for xi being Real st xi in B \/ {x} holds
li <= xi ) )

thus li in B \/ {x} by A4, A6; :: thesis: for xi being Real st xi in B \/ {x} holds
li <= xi

let xi be Real; :: thesis: ( xi in B \/ {x} implies li <= xi )
assume xi in B \/ {x} ; :: thesis: li <= xi
then ( xi in B or xi = x ) by A6;
hence li <= xi by A5, A7; :: thesis: verum
end;
suppose A8: x < li ; :: 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 ( li <= 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