let Gi be non trivial finite Subset of REAL ; :: thesis: for xi being Real st xi in Gi holds
ex ri being Real st [xi,ri] is Gap of Gi
let xi be Real; :: thesis: ( xi in Gi implies ex ri being Real st [xi,ri] is Gap of Gi )
assume A1: xi in Gi ; :: thesis: ex ri being Real st [xi,ri] is Gap of Gi
defpred S₁[ Real] means $1 > xi;
set Gi' = { H₁(ri') where ri' is Real : ( H₁(ri') in Gi & S₁[ri'] ) } ;
A2: { H₁(ri') where ri' is Real : ( H₁(ri') in Gi & S₁[ri'] ) } c= Gi from FRAENKEL:sch 17();
then reconsider Gi' = { H₁(ri') where ri' is Real : ( H₁(ri') in Gi & S₁[ri'] ) } as finite Subset of REAL by XBOOLE_1:1;

per cases ( Gi' is zero or not Gi' is zero ) ;

suppose A3: Gi' is zero ; :: thesis: ex ri being Real st [xi,ri] is Gap of Gi

A4: now

let xi' be Real; :: thesis: ( xi' in Gi implies not xi' > xi )
assume that
A5: xi' in Gi and
A6: xi' > xi ; :: thesis: contradiction
xi' in Gi' by A5, A6;
hence contradiction by A3; :: thesis: verum

end;

consider li being Real such that
A7: li in Gi and
A8: for xi' being Real st xi' in Gi holds
li <= xi' by Th13;
take li ; :: thesis: [xi,li] is Gap of Gi

A9: now

assume A10: li = xi ; :: thesis: ( Gi = {xi} & contradiction )
for xi' being set holds
( xi' in Gi iff xi' = xi )

proof

let xi' be set ; :: thesis: ( xi' in Gi iff xi' = xi )

hereby :: thesis: ( xi' = xi implies xi' in Gi )

assume A11: xi' in Gi ; :: thesis: xi' = xi
then reconsider xi'' = xi' as Element of REAL ;
A12: li <= xi'' by A8, A11;
xi'' <= xi by A4, A11;
hence xi' = xi by A10, A12, XXREAL_0:1; :: thesis: verum

end;

thus ( xi' = xi implies xi' in Gi ) by A1; :: thesis: verum

end;

hence Gi = {xi} by TARSKI:def 1; :: thesis: contradiction
hence contradiction ; :: thesis: verum

end;

li <= xi by A1, A8;
then A13: li < xi by A9, XXREAL_0:1;
for xi' being Real st xi' in Gi holds
( not xi < xi' & not xi' < li ) by A4, A8;
hence [xi,li] is Gap of Gi by A1, A7, A13, Th17; :: thesis: verum

end;

suppose not Gi' is zero ; :: thesis: ex ri being Real st [xi,ri] is Gap of Gi

then reconsider Gi' = Gi' as non empty finite Subset of REAL ;
consider ri being Real such that
A14: ri in Gi' and
A15: for ri' being Real st ri' in Gi' holds
ri' >= ri by Th13;
take ri ; :: thesis: [xi,ri] is Gap of Gi

now

thus xi in Gi by A1; :: thesis: ( ri in Gi & xi < ri & ( for xi' being Real st xi' in Gi & xi < xi' holds
not xi' < ri ) )
thus ri in Gi by A2, A14; :: thesis: ( xi < ri & ( for xi' being Real st xi' in Gi & xi < xi' holds
not xi' < ri ) )
ex ri' being Real st
( ri' = ri & ri' in Gi & xi < ri' ) by A14;
hence xi < ri ; :: thesis: for xi' being Real st xi' in Gi & xi < xi' holds
not xi' < ri

hereby :: thesis: verum

let xi' be Real; :: thesis: ( xi' in Gi & xi < xi' implies not xi' < ri )
assume xi' in Gi ; :: thesis: ( not xi < xi' or not xi' < ri )
then ( xi' <= xi or xi' in Gi' ) ;
hence ( not xi < xi' or not xi' < ri ) by A15; :: thesis: verum

end;

end;

hence [xi,ri] is Gap of Gi by Th17; :: thesis: verum

end;

end;