defpred S_{1}[ 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

S_{1}[{xi}]

for B being non empty finite Subset of REAL st x in X & B c= X & not x in B & S_{1}[B] holds

S_{1}[B \/ {x}]
_{1}[X]
from CHAIN_1:sch 2(A1, A2); :: thesis: verum

( 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

S

proof

A2:
for x being Element of REAL
let xi be Element of REAL ; :: thesis: ( xi in X implies S_{1}[{xi}] )

assume xi in X ; :: thesis: S_{1}[{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;assume xi in X ; :: thesis: S

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

for B being non empty finite Subset of REAL st x in X & B c= X & not x in B & S

S

proof

thus
S
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_{1}[B] holds

S_{1}[B \/ {x}]

let B be non empty finite Subset of REAL; :: thesis: ( x in X & B c= X & not x in B & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

x in X and

B c= X and

not x in B and

A3: S_{1}[B]
; :: thesis: S_{1}[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};

end;S

let B be non empty finite Subset of REAL; :: thesis: ( x in X & B c= X & not x in B & S

assume that

x in X and

B c= X and

not x in B and

A3: S

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 ) )

( 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;( 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

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

end;

suppose A7:
li <= x
; :: thesis: S_{1}[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;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

suppose A8:
x < li
; :: thesis: S_{1}[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;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