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 S1[ 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
S1[{li,ri}]
let li, ri be Element of REAL ; :: thesis: ( li in Gi & ri in Gi & li <> ri implies S1[{li,ri}] )
assume that
li in Gi and
ri in Gi and
A2: li <> ri ; :: thesis: S1[{li,ri}]
A3: now :: thesis: for li, ri being Real st li < ri holds
S1[{li,ri}]
let li, ri be Real; :: thesis: ( li < ri implies S1[{li,ri}] )
assume A4: li < ri ; :: thesis: S1[{li,ri}]
thus S1[{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 ; :: thesis: verum
end;
end;
( li < ri or ri < li ) by ;
hence S1[{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 & S1[B] holds
S1[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 & S1[B] holds
S1[B \/ {x}]

let B be non trivial finite Subset of REAL; :: thesis: ( x in Gi & B c= Gi & not x in B & S1[B] implies S1[B \/ {x}] )
assume that
x in Gi and
B c= Gi and
A6: not x in B and
A7: S1[B] ; :: thesis: S1[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 ;
suppose A12: x < li ; :: thesis: S1[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 ; :: 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 ; :: thesis: verum
end;
suppose A13: ( li < x & x < ri ) ; :: thesis: S1[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 ; :: 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 ;
hence ( not li < xi or not xi < x ) by ; :: thesis: verum
end;
suppose A14: ri < x ; :: thesis: S1[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 ; :: 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 ; :: thesis: verum
end;
end;
end;
thus S1[Gi] from CHAIN_1:sch 3(A1, A5); :: thesis: verum