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_{1}[ Element of REAL ] means $1 < xi;

set Gi9 = { H_{1}(li9) where li9 is Element of REAL : ( H_{1}(li9) in Gi & S_{1}[li9] ) } ;

A2: { H_{1}(li9) where li9 is Element of REAL : ( H_{1}(li9) in Gi & S_{1}[li9] ) } c= Gi
from FRAENKEL:sch 17();

then reconsider Gi9 = { H_{1}(li9) where li9 is Element of REAL : ( H_{1}(li9) in Gi & S_{1}[li9] ) } as finite Subset of REAL by XBOOLE_1:1;

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

set Gi9 = { H

A2: { H

then reconsider Gi9 = { H

per cases
( Gi9 is empty or not Gi9 is empty )
;

end;

suppose A3:
Gi9 is empty
; :: thesis: ex li being Element of REAL st [li,xi] is Gap of Gi

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

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;

A4: now :: thesis: for xi9 being Real st xi9 in Gi holds

not xi9 < xi

consider ri being Element of REAL such that 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;assume that

A5: xi9 in Gi and

A6: xi9 < xi ; :: thesis: contradiction

xi9 in Gi9 by A5, A6;

hence contradiction by A3; :: thesis: verum

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 ) )

ri >= xi
by A1, A8;assume A10:
ri = xi
; :: thesis: ( Gi = {xi} & contradiction )

for xi9 being object holds

( xi9 in Gi iff xi9 = xi )

hence contradiction ; :: thesis: verum

end;for xi9 being object holds

( xi9 in Gi iff xi9 = xi )

proof

hence
Gi = {xi}
by TARSKI:def 1; :: thesis: contradiction
let xi9 be object ; :: thesis: ( xi9 in Gi iff xi9 = xi )

end;hereby :: thesis: ( xi9 = xi implies xi9 in Gi )

thus
( xi9 = xi implies xi9 in Gi )
by A1; :: thesis: verumassume 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;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

hence contradiction ; :: thesis: verum

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

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

end;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 ) )

hence
[li,xi] is Gap of Gi
by Th13; :: thesis: verumnot 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

end;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;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