let Gi be non trivial finite Subset of REAL; 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 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 ;
( 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
;
S1[{li,ri}]A3:
now for li, ri being Real st li < ri holds
S1[{li,ri}]let li,
ri be
Real;
( li < ri implies S1[{li,ri}] )assume A4:
li < ri
;
S1[{li,ri}]thus
S1[
{li,ri}]
verumproof
take
li
;
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
;
( 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;
verum
end; end;
(
li < ri or
ri < li )
by A2, XXREAL_0:1;
hence
S1[
{li,ri}]
by A3;
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}]
thus
S1[Gi]
from CHAIN_1:sch 3(A1, A5); verum