let Gi be non trivial finite Subset of REAL; :: thesis: ex li, ri being Real st

( li in Gi & ri in Gi & li < ri & ( for xi being Real st xi in Gi & li < xi holds

not xi < ri ) )

defpred S_{1}[ set ] means ex li, ri being Real st

( li in $1 & ri in $1 & li < ri & ( for xi being Real st xi in $1 & li < xi holds

not xi < ri ) );

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

S_{1}[B \/ {x}]
_{1}[Gi]
from CHAIN_1:sch 3(A1, A5); :: thesis: verum

( li in Gi & ri in Gi & li < ri & ( for xi being Real st xi in Gi & li < xi holds

not xi < ri ) )

defpred S

( li in $1 & ri in $1 & li < ri & ( for xi being Real st xi in $1 & li < xi holds

not xi < ri ) );

A1: now :: thesis: for li, ri being Element of REAL st li in Gi & ri in Gi & li <> ri holds

S_{1}[{li,ri}]

A5:
for x being Element of REAL S

let li, ri be Element of REAL ; :: thesis: ( li in Gi & ri in Gi & li <> ri implies S_{1}[{li,ri}] )

assume that

li in Gi and

ri in Gi and

A2: li <> ri ; :: thesis: S_{1}[{li,ri}]

hence S_{1}[{li,ri}]
by A3; :: thesis: verum

end;assume that

li in Gi and

ri in Gi and

A2: li <> ri ; :: thesis: S

A3: now :: thesis: for li, ri being Real st li < ri holds

S_{1}[{li,ri}]

( li < ri or ri < li )
by A2, XXREAL_0:1;S

let li, ri be Real; :: thesis: ( li < ri implies S_{1}[{li,ri}] )

assume A4: li < ri ; :: thesis: S_{1}[{li,ri}]

thus S_{1}[{li,ri}]
:: thesis: verum

end;assume A4: li < ri ; :: thesis: S

thus S

proof

take
li
; :: thesis: ex ri being Real st

( li in {li,ri} & ri in {li,ri} & li < ri & ( for xi being Real st xi in {li,ri} & li < xi holds

not xi < ri ) )

take ri ; :: thesis: ( li in {li,ri} & ri in {li,ri} & li < ri & ( for xi being Real st xi in {li,ri} & li < xi holds

not xi < ri ) )

thus ( li in {li,ri} & ri in {li,ri} & li < ri & ( for xi being Real st xi in {li,ri} & li < xi holds

not xi < ri ) ) by A4, TARSKI:def 2; :: thesis: verum

end;( li in {li,ri} & ri in {li,ri} & li < ri & ( for xi being Real st xi in {li,ri} & li < xi holds

not xi < ri ) )

take ri ; :: thesis: ( li in {li,ri} & ri in {li,ri} & li < ri & ( for xi being Real st xi in {li,ri} & li < xi holds

not xi < ri ) )

thus ( li in {li,ri} & ri in {li,ri} & li < ri & ( for xi being Real st xi in {li,ri} & li < xi holds

not xi < ri ) ) by A4, TARSKI:def 2; :: thesis: verum

hence S

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

S

proof

thus
S
let x be Element of REAL ; :: thesis: for B being non trivial finite Subset of REAL st x in Gi & B c= Gi & not x in B & S_{1}[B] holds

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

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

assume that

x in Gi and

B c= Gi and

A6: not x in B and

A7: S_{1}[B]
; :: thesis: S_{1}[B \/ {x}]

consider li, ri being Real such that

A8: li in B and

A9: ri in B and

A10: li < ri and

A11: for xi being Real st xi in B & li < xi holds

not xi < ri by A7;

end;S

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

assume that

x in Gi and

B c= Gi and

A6: not x in B and

A7: S

consider li, ri being Real such that

A8: li in B and

A9: ri in B and

A10: li < ri and

A11: for xi being Real st xi in B & li < xi holds

not xi < ri by A7;

per cases
( x < li or ( li < x & x < ri ) or ri < x )
by A6, A8, A9, XXREAL_0:1;

end;

suppose A12:
x < li
; :: thesis: S_{1}[B \/ {x}]

take
li
; :: thesis: ex ri being Real st

( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

take ri ; :: thesis: ( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

thus ( li in B \/ {x} & ri in B \/ {x} & li < ri ) by A8, A9, A10, XBOOLE_0:def 3; :: thesis: for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri

let xi be Real; :: thesis: ( xi in B \/ {x} & li < xi implies not xi < ri )

assume xi in B \/ {x} ; :: thesis: ( not li < xi or not xi < ri )

then ( xi in B or xi in {x} ) by XBOOLE_0:def 3;

hence ( not li < xi or not xi < ri ) by A11, A12, TARSKI:def 1; :: thesis: verum

end;( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

take ri ; :: thesis: ( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

thus ( li in B \/ {x} & ri in B \/ {x} & li < ri ) by A8, A9, A10, XBOOLE_0:def 3; :: thesis: for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri

let xi be Real; :: thesis: ( xi in B \/ {x} & li < xi implies not xi < ri )

assume xi in B \/ {x} ; :: thesis: ( not li < xi or not xi < ri )

then ( xi in B or xi in {x} ) by XBOOLE_0:def 3;

hence ( not li < xi or not xi < ri ) by A11, A12, TARSKI:def 1; :: thesis: verum

suppose A13:
( li < x & x < ri )
; :: thesis: S_{1}[B \/ {x}]

take
li
; :: thesis: ex ri being Real st

( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

take x ; :: thesis: ( li in B \/ {x} & x in B \/ {x} & li < x & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < x ) )

x in {x} by TARSKI:def 1;

hence ( li in B \/ {x} & x in B \/ {x} & li < x ) by A8, A13, XBOOLE_0:def 3; :: thesis: for xi being Real st xi in B \/ {x} & li < xi holds

not xi < x

let xi be Real; :: thesis: ( xi in B \/ {x} & li < xi implies not xi < x )

assume xi in B \/ {x} ; :: thesis: ( not li < xi or not xi < x )

then ( xi in B or xi in {x} ) by XBOOLE_0:def 3;

then ( not li < xi or not xi < ri or xi = x ) by A11, TARSKI:def 1;

hence ( not li < xi or not xi < x ) by A13, XXREAL_0:2; :: thesis: verum

end;( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

take x ; :: thesis: ( li in B \/ {x} & x in B \/ {x} & li < x & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < x ) )

x in {x} by TARSKI:def 1;

hence ( li in B \/ {x} & x in B \/ {x} & li < x ) by A8, A13, XBOOLE_0:def 3; :: thesis: for xi being Real st xi in B \/ {x} & li < xi holds

not xi < x

let xi be Real; :: thesis: ( xi in B \/ {x} & li < xi implies not xi < x )

assume xi in B \/ {x} ; :: thesis: ( not li < xi or not xi < x )

then ( xi in B or xi in {x} ) by XBOOLE_0:def 3;

then ( not li < xi or not xi < ri or xi = x ) by A11, TARSKI:def 1;

hence ( not li < xi or not xi < x ) by A13, XXREAL_0:2; :: thesis: verum

suppose A14:
ri < x
; :: thesis: S_{1}[B \/ {x}]

take
li
; :: thesis: ex ri being Real st

( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

take ri ; :: thesis: ( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

thus ( li in B \/ {x} & ri in B \/ {x} & li < ri ) by A8, A9, A10, XBOOLE_0:def 3; :: thesis: for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri

let xi be Real; :: thesis: ( xi in B \/ {x} & li < xi implies not xi < ri )

assume xi in B \/ {x} ; :: thesis: ( not li < xi or not xi < ri )

then ( xi in B or xi in {x} ) by XBOOLE_0:def 3;

hence ( not li < xi or not xi < ri ) by A11, A14, TARSKI:def 1; :: thesis: verum

end;( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

take ri ; :: thesis: ( li in B \/ {x} & ri in B \/ {x} & li < ri & ( for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri ) )

thus ( li in B \/ {x} & ri in B \/ {x} & li < ri ) by A8, A9, A10, XBOOLE_0:def 3; :: thesis: for xi being Real st xi in B \/ {x} & li < xi holds

not xi < ri

let xi be Real; :: thesis: ( xi in B \/ {x} & li < xi implies not xi < ri )

assume xi in B \/ {x} ; :: thesis: ( not li < xi or not xi < ri )

then ( xi in B or xi in {x} ) by XBOOLE_0:def 3;

hence ( not li < xi or not xi < ri ) by A11, A14, TARSKI:def 1; :: thesis: verum