let Gi be non trivial finite Subset of REAL; :: thesis: for xi being Real st xi in Gi holds
ex li being Element of REAL st [li,xi] is Gap of Gi

let xi be Real; :: thesis: ( xi in Gi implies ex li being Element of REAL st [li,xi] is Gap of Gi )
assume A1: xi in Gi ; :: thesis: ex li being Element of REAL st [li,xi] is Gap of Gi
defpred S1[ Element of REAL ] means \$1 < xi;
set Gi9 = { H1(li9) where li9 is Element of REAL : ( H1(li9) in Gi & S1[li9] ) } ;
A2: { H1(li9) where li9 is Element of REAL : ( H1(li9) in Gi & S1[li9] ) } c= Gi from then reconsider Gi9 = { H1(li9) where li9 is Element of REAL : ( H1(li9) in Gi & S1[li9] ) } 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 li being Element of REAL st [li,xi] 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 ri being Element of REAL such that
A7: ri in Gi and
A8: for xi9 being Real st xi9 in Gi holds
ri >= xi9 by Th9;
take ri ; :: thesis: [ri,xi] is Gap of Gi
A9: now :: thesis: ( ri = xi implies ( Gi = {xi} & contradiction ) )
assume A10: ri = 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: ri >= xi99 by ;
xi99 >= xi by ;
hence xi9 = xi by ; :: 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;
ri >= xi by A1, A8;
then A13: ri > xi by ;
for xi9 being Real st xi9 in Gi holds
( not xi9 > ri & not xi > xi9 ) by A4, A8;
hence [ri,xi] is Gap of Gi by A1, A7, A13, Th13; :: thesis: verum
end;
suppose not Gi9 is empty ; :: thesis: ex li being Element of REAL st [li,xi] is Gap of Gi
then reconsider Gi9 = Gi9 as non empty finite Subset of REAL ;
consider li being Element of REAL such that
A14: li in Gi9 and
A15: for li9 being Real st li9 in Gi9 holds
li9 <= li by Th9;
take li ; :: thesis: [li,xi] is Gap of Gi
now :: thesis: ( xi in Gi & li in Gi & xi > li & ( for xi9 being Real st xi9 in Gi & xi9 > li holds
not xi > xi9 ) )
thus xi in Gi by A1; :: thesis: ( li in Gi & xi > li & ( for xi9 being Real st xi9 in Gi & xi9 > li holds
not xi > xi9 ) )

thus li in Gi by ; :: thesis: ( xi > li & ( for xi9 being Real st xi9 in Gi & xi9 > li holds
not xi > xi9 ) )

ex li9 being Element of REAL st
( li9 = li & li9 in Gi & xi > li9 ) by A14;
hence xi > li ; :: thesis: for xi9 being Real st xi9 in Gi & xi9 > li holds
not xi > xi9

hereby :: thesis: verum
let xi9 be Real; :: thesis: ( xi9 in Gi & xi9 > li implies not xi > xi9 )
assume xi9 in Gi ; :: thesis: ( not xi9 > li or not xi > xi9 )
then ( xi9 >= xi or xi9 in Gi9 ) ;
hence ( not xi9 > li or not xi > xi9 ) by A15; :: thesis: verum
end;
end;
hence [li,xi] is Gap of Gi by Th13; :: thesis: verum
end;
end;