defpred S₁[ 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:
A1: for xi being Element of REAL st xi in X holds
S₁[{xi}]

let xi be Element of REAL ; :: thesis:
assume xi in X ; :: thesis:
take xi ; :: thesis:
thus ( xi in {xi} & ( for xi being Real st xi in {xi} holds
xi <= xi ) ) by TARSKI:def 1; :: thesis:

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}]

let x be Element of REAL ; :: thesis:
let B be non empty finite Subset of REAL; :: thesis:
assume that
x in X and
B c= X and
not x in B and
A3: S₁[B] ; :: thesis:
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};

end;

reconsider li = li as Element of REAL by XREAL_0:def 1;
take li ; :: thesis:
thus li in B \/ {x} by A4, A6; :: thesis:
let xi be Real; :: thesis:
assume xi in B \/ {x} ; :: thesis:
then ( xi in B or xi = x ) by A6;
hence li <= xi by A5, A7; :: thesis:

end;

end;