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

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

( 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

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

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

( 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
( x <= ri or ri < x )
;

end;

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

suppose A8:
ri < x
; :: 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 ( ri >= 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 ( ri >= xi or xi = x ) by A5;

hence x >= xi by A8, XXREAL_0:2; :: thesis: verum