let Gi be non trivial finite Subset of REAL ; :: thesis: for xi being Real st xi in Gi holds
ex li being Real st [li,xi] is Gap of Gi
let xi be Real; :: thesis: ( xi in Gi implies ex li being Real st [li,xi] is Gap of Gi )
assume A1: xi in Gi ; :: thesis: ex li being Real st [li,xi] is Gap of Gi
defpred S₁[ Real] means $1 < xi;
set Gi' = { H₁(li') where li' is Real : ( H₁(li') in Gi & S₁[li'] ) } ;
A2: { H₁(li') where li' is Real : ( H₁(li') in Gi & S₁[li'] ) } c= Gi from FRAENKEL:sch 17();
then reconsider Gi' = { H₁(li') where li' is Real : ( H₁(li') in Gi & S₁[li'] ) } 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 li being Real st [li,xi] 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 ri being Real such that
A5: ( ri in Gi & ( for xi' being Real st xi' in Gi holds
ri >= xi' ) ) by Th12;
take ri ; :: thesis: [ri,xi] is Gap of Gi

now

A6: now

assume A7: ri = 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 ;
( ri >= 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;

ri >= xi by A1, A5;
hence ( xi in Gi & ri in Gi & ri > xi ) by A1, A5, A6, XXREAL_0:1; :: thesis: for xi' being Real st xi' in Gi holds
( not xi' > ri & not xi > xi' )
thus for xi' being Real st xi' in Gi holds
( not xi' > ri & not xi > xi' ) by A4, A5; :: thesis: verum

end;

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

end;

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

then reconsider Gi' = Gi' as non empty finite Subset of REAL ;
consider li being Real such that
A9: ( li in Gi' & ( for li' being Real st li' in Gi' holds
li' <= li ) ) by Th12;
take li ; :: thesis: [li,xi] is Gap of Gi

now

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

hereby :: thesis: verum

let xi' be Real; :: thesis: ( xi' in Gi & xi' > li implies not xi > xi' )
assume xi' in Gi ; :: thesis: ( not xi' > li or not xi > xi' )
then ( xi' >= xi or xi' in Gi' ) ;
hence ( not xi' > li or not xi > xi' ) by A9; :: thesis: verum

end;

end;

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

end;

end;