let Gi be non trivial finite Subset of ; :: 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 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 that
A5: xi' in Gi and
A6: xi' < xi ; :: thesis: contradiction
xi' in Gi' by A5, A6;
hence contradiction by A3; :: thesis: verum

end;

consider ri being Real such that
A7: ri in Gi and
A8: for xi' being Real st xi' in Gi holds
ri >= xi' by Th12;
take ri ; :: thesis: [ri,xi] is Gap of Gi

A9: now

assume A10: 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 A11: xi' in Gi ; :: thesis: xi' = xi
then reconsider xi'' = xi' as Element of REAL ;
A12: ri >= xi'' by A8, A11;
xi'' >= xi by A4, A11;
hence xi' = xi by A10, A12, 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, A8;
then A13: ri > xi by A9, XXREAL_0:1;
for xi' being Real st xi' in Gi holds
( not xi' > ri & not xi > xi' ) by A4, A8;
hence [ri,xi] is Gap of Gi by A1, A7, A13, 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 ;
consider li being Real such that
A14: li in Gi' and
A15: 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, A14; :: 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 A14;
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 A15; :: thesis: verum

end;

end;

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

end;

end;