let Gi be non trivial finite Subset of REAL; :: thesis:
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 ) );

let li, ri be Element of REAL ; :: thesis:
assume that
li in Gi and
ri in Gi and
A2: li <> ri ; :: thesis:

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

proof

take li ; :: thesis:
take ri ; :: thesis:
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:

end;

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

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:
let B be non trivial finite Subset of REAL; :: thesis:
assume that
x in Gi and
B c= Gi and
A6: not x in B and
A7: S₁[B] ; :: thesis:
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 by A6, A8, A9, XXREAL_0:1;

suppose A12: x < li ; :: thesis:

take li ; :: thesis:
take ri ; :: thesis:
thus ( li in B \/ {x} & ri in B \/ {x} & li < ri ) by A8, A9, A10, XBOOLE_0:def 3; :: thesis:
let xi be Real; :: thesis:
assume xi in B \/ {x} ; :: thesis:
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:

end;

suppose A13: ( li < x & x < ri ) ; :: thesis:

take li ; :: thesis:
take x ; :: thesis:
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:
let xi be Real; :: thesis:
assume xi in B \/ {x} ; :: thesis:
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:

end;

suppose A14: ri < x ; :: thesis:

end;

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