let Gi be non trivial finite Subset of REAL; :: thesis: for xi being Real st xi in Gi holds

ex ri being Element of REAL st [xi,ri] is Gap of Gi

let xi be Real; :: thesis: ( xi in Gi implies ex ri being Element of REAL st [xi,ri] is Gap of Gi )

assume A1: xi in Gi ; :: thesis: ex ri being Element of REAL st [xi,ri] is Gap of Gi

defpred S_{1}[ Element of REAL ] means $1 > xi;

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

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

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

ex ri being Element of REAL st [xi,ri] is Gap of Gi

let xi be Real; :: thesis: ( xi in Gi implies ex ri being Element of REAL st [xi,ri] is Gap of Gi )

assume A1: xi in Gi ; :: thesis: ex ri being Element of REAL st [xi,ri] 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 ri being Element of REAL st [xi,ri] is Gap of Gi

A7: li in Gi and

A8: for xi9 being Real st xi9 in Gi holds

li <= xi9 by Th10;

take li ; :: thesis: [xi,li] is Gap of Gi

then A13: li < xi by A9, XXREAL_0:1;

for xi9 being Real st xi9 in Gi holds

( not xi < xi9 & not xi9 < li ) by A4, A8;

hence [xi,li] 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 li 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: li in Gi and

A8: for xi9 being Real st xi9 in Gi holds

li <= xi9 by Th10;

take li ; :: thesis: [xi,li] is Gap of Gi

A9: now :: thesis: ( li = xi implies ( Gi = {xi} & contradiction ) )

li <= xi
by A1, A8;assume A10:
li = 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: li <= 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: li <= 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: li < xi by A9, XXREAL_0:1;

for xi9 being Real st xi9 in Gi holds

( not xi < xi9 & not xi9 < li ) by A4, A8;

hence [xi,li] is Gap of Gi by A1, A7, A13, Th13; :: thesis: verum

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

then reconsider Gi9 = Gi9 as non empty finite Subset of REAL ;

consider ri being Element of REAL such that

A14: ri in Gi9 and

A15: for ri9 being Real st ri9 in Gi9 holds

ri9 >= ri by Th10;

take ri ; :: thesis: [xi,ri] is Gap of Gi

end;consider ri being Element of REAL such that

A14: ri in Gi9 and

A15: for ri9 being Real st ri9 in Gi9 holds

ri9 >= ri by Th10;

take ri ; :: thesis: [xi,ri] is Gap of Gi

now :: thesis: ( xi in Gi & ri in Gi & xi < ri & ( for xi9 being Real st xi9 in Gi & xi < xi9 holds

not xi9 < ri ) )

hence
[xi,ri] is Gap of Gi
by Th13; :: thesis: verumnot xi9 < ri ) )

thus
xi in Gi
by A1; :: thesis: ( ri in Gi & xi < ri & ( for xi9 being Real st xi9 in Gi & xi < xi9 holds

not xi9 < ri ) )

thus ri in Gi by A2, A14; :: thesis: ( xi < ri & ( for xi9 being Real st xi9 in Gi & xi < xi9 holds

not xi9 < ri ) )

ex ri9 being Element of REAL st

( ri9 = ri & ri9 in Gi & xi < ri9 ) by A14;

hence xi < ri ; :: thesis: for xi9 being Real st xi9 in Gi & xi < xi9 holds

not xi9 < ri

end;not xi9 < ri ) )

thus ri in Gi by A2, A14; :: thesis: ( xi < ri & ( for xi9 being Real st xi9 in Gi & xi < xi9 holds

not xi9 < ri ) )

ex ri9 being Element of REAL st

( ri9 = ri & ri9 in Gi & xi < ri9 ) by A14;

hence xi < ri ; :: thesis: for xi9 being Real st xi9 in Gi & xi < xi9 holds

not xi9 < ri

hereby :: thesis: verum

let xi9 be Real; :: thesis: ( xi9 in Gi & xi < xi9 implies not xi9 < ri )

assume xi9 in Gi ; :: thesis: ( not xi < xi9 or not xi9 < ri )

then ( xi9 <= xi or xi9 in Gi9 ) ;

hence ( not xi < xi9 or not xi9 < ri ) by A15; :: thesis: verum

end;assume xi9 in Gi ; :: thesis: ( not xi < xi9 or not xi9 < ri )

then ( xi9 <= xi or xi9 in Gi9 ) ;

hence ( not xi < xi9 or not xi9 < ri ) by A15; :: thesis: verum