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 S₁[ Element of REAL ] means $1 < xi;
set Gi9 = { H₁(li9) where li9 is Element of REAL : ( H₁(li9) in Gi & S₁[li9] ) } ;
A2: { H₁(li9) where li9 is Element of REAL : ( H₁(li9) in Gi & S₁[li9] ) } c= Gi from FRAENKEL:sch 17();
then reconsider Gi9 = { H₁(li9) where li9 is Element of REAL : ( H₁(li9) in Gi & S₁[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 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;

ri >= xi by A1, A8;
then A13: ri > xi by A9, XXREAL_0:1;
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 A2, A14; :: 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;