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₁[ 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 ) );

A1: now :: thesis: for li, ri being Element of REAL st li in Gi & ri in Gi & li <> ri holds
S₁[{li,ri}]

let li, ri be Element of REAL ; :: thesis: ( li in Gi & ri in Gi & li <> ri implies S₁[{li,ri}] )
assume that
li in Gi and
ri in Gi and
A2: li <> ri ; :: thesis: S₁[{li,ri}]

A3: now :: thesis: for li, ri being Real st li < ri holds
S₁[{li,ri}]

let li, ri be Real; :: thesis: ( li < ri implies S₁[{li,ri}] )
assume A4: li < ri ; :: thesis: S₁[{li,ri}]
thus S₁[{li,ri}] :: thesis: verum

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;

end;

( li < ri or ri < li ) by A2, XXREAL_0:1;
hence S₁[{li,ri}] by A3; :: thesis: verum

end;

A5: for x being Element of REAL
for B being non trivial finite Subset of REAL st x in Gi & B c= Gi & not x in B & S₁[B] holds
S₁[B \/ {x}]

proof

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₁[B] holds
S₁[B \/ {x}]
let B be non trivial finite Subset of REAL; :: thesis: ( x in Gi & B c= Gi & not x in B & S₁[B] implies S₁[B \/ {x}] )
assume that
x in Gi and
B c= Gi and
A6: not x in B and
A7: S₁[B] ; :: thesis: S₁[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;

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

suppose A12: x < li ; :: thesis: S₁[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;

suppose A13: ( li < x & x < ri ) ; :: thesis: S₁[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;

suppose A14: ri < x ; :: thesis: S₁[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;

end;

end;

thus S₁[Gi] from CHAIN_1:sch 3(A1, A5); :: thesis: verum