let Gi be non trivial finite Subset of REAL; :: thesis: for xi being Real st xi in Gi holds
ex ri being Element of REAL st [xi,ri] is Gap of Gi
let xi be Real; :: thesis: ( xi in Gi implies ex ri being Element of REAL st [xi,ri] is Gap of Gi )
assume A1: xi in Gi ; :: thesis: ex ri being Element of REAL st [xi,ri] is Gap of Gi
defpred S1[ Element of REAL ] means $1 > xi;
set Gi9 = { H1(ri9) where ri9 is Element of REAL : ( H1(ri9) in Gi & S1[ri9] ) } ;
A2: { H1(ri9) where ri9 is Element of REAL : ( H1(ri9) in Gi & S1[ri9] ) } c= Gi from FRAENKEL:sch 17();
 then reconsider Gi9 = { H1(ri9) where ri9 is Element of REAL : ( H1(ri9) in Gi & S1[ri9] ) } as finite Subset of REAL by XBOOLE_1:1;
per cases ( Gi9 is empty or not Gi9 is empty ) ;
suppose A3: Gi9 is empty ; :: thesis: ex ri being Element of REAL st [xi,ri] is Gap of Gi
A4: now :: thesis: for xi9 being Real st xi9 in Gi holds
not xi9 > xi
let xi9 be Real; :: thesis: ( xi9 in Gi implies not xi9 > xi )
assume that
A5: xi9 in Gi and
A6: xi9 > xi ; :: thesis: contradiction
xi9 in Gi9 by A5, A6;
hence contradiction by A3; :: thesis: verum
end;
consider li being Element of REAL such that
A7: li in Gi and
A8: for xi9 being Real st xi9 in Gi holds
li <= xi9 by Th10;
take li ; :: thesis: [xi,li] is Gap of Gi
A9: now :: thesis: ( li = xi implies ( Gi = {xi} & contradiction ) )
assume A10: li = xi ; :: thesis: ( Gi = {xi} & contradiction )
for xi9 being object holds
( xi9 in Gi iff xi9 = xi )
proof
let xi9 be object ; :: thesis: ( xi9 in Gi iff xi9 = xi )
hereby :: thesis: ( xi9 = xi implies xi9 in Gi )
assume A11: xi9 in Gi ; :: thesis: xi9 = xi
then reconsider xi99 = xi9 as Element of REAL ;
A12: li <= xi99 by A8, A11;
xi99 <= xi by A4, A11;
hence xi9 = xi by A10, A12, XXREAL_0:1; :: thesis: verum
end;
thus ( xi9 = xi implies xi9 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 xi9 being Real st xi9 in Gi holds
( not xi < xi9 & not xi9 < li ) by A4, A8;
hence [xi,li] is Gap of Gi by A1, A7, A13, Th13; :: thesis: verum
end;
suppose not Gi9 is empty ; :: thesis: ex ri being Element of REAL st [xi,ri] is Gap of Gi
then reconsider Gi9 = Gi9 as non empty finite Subset of REAL ;
consider ri being Element of REAL such that
A14: ri in Gi9 and
A15: for ri9 being Real st ri9 in Gi9 holds
ri9 >= ri by Th10;
take ri ; :: thesis: [xi,ri] is Gap of Gi
now :: thesis: ( xi in Gi & ri in Gi & xi < ri & ( for xi9 being Real st xi9 in Gi & xi < xi9 holds
not xi9 < ri ) )
thus xi in Gi by A1; :: thesis: ( ri in Gi & xi < ri & ( for xi9 being Real st xi9 in Gi & xi < xi9 holds
not xi9 < ri ) )
thus ri in Gi by A2, A14; :: thesis: ( xi < ri & ( for xi9 being Real st xi9 in Gi & xi < xi9 holds
not xi9 < ri ) )
ex ri9 being Element of REAL st
( ri9 = ri & ri9 in Gi & xi < ri9 ) by A14;
hence xi < ri ; :: thesis: for xi9 being Real st xi9 in Gi & xi < xi9 holds
not xi9 < ri
hereby :: thesis: verum
let xi9 be Real; :: thesis: ( xi9 in Gi & xi < xi9 implies not xi9 < ri )
assume xi9 in Gi ; :: thesis: ( not xi < xi9 or not xi9 < ri )
then ( xi9 <= xi or xi9 in Gi9 ) ;
hence ( not xi < xi9 or not xi9 < ri ) by A15; :: thesis: verum
end;
end;
hence [xi,ri] is Gap of Gi by Th13; :: thesis: verum
end;
end;