defpred S₁[ set ] means ex li being 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 Real st
( li in X & ( for xi being Real st xi in X holds
li <= xi ) )
A1: for xi being Real st xi in X holds
S₁[{xi}]

proof

let xi be 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 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 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 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

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: S₁[B \/ {x}]

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: 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 ( li <= 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