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 ( xi' in Gi & xi' > xi ) ; :: thesis: contradiction
then xi' in Gi' ;
hence contradiction by A3; :: thesis: verum

end;

consider li being Real such that
A5: ( li in Gi & ( for xi' being Real st xi' in Gi holds
li <= xi' ) ) by Th13;
take li ; :: thesis: [xi,li] is Gap of Gi

now

A6: now

assume A7: 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 A8: xi' in Gi ; :: thesis: xi' = xi
then reconsider xi'' = xi' as Element of REAL ;
( li <= xi'' & xi'' <= xi ) by A4, A5, A8;
hence xi' = xi by A7, 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, A5;
hence ( xi in Gi & li in Gi & li < xi ) by A1, A5, A6, XXREAL_0:1; :: thesis: for xi' being Real st xi' in Gi holds
( not xi < xi' & not xi' < li )
thus for xi' being Real st xi' in Gi holds
( not xi < xi' & not xi' < li ) by A4, A5; :: thesis: verum

end;

hence [xi,li] is Gap of Gi by 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
A9: ( ri in Gi' & ( 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, A9; :: 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 A9;
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 A9; :: thesis: verum

end;

end;

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

end;

end;