let Gi be non trivial finite Subset of REAL; 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; ( xi in Gi implies ex li being Element of REAL st [li,xi] is Gap of Gi )
assume A1:
xi in Gi
; ex li being Element of REAL st [li,xi] is Gap of Gi
defpred S1[ Element of REAL ] means $1 < xi;
set Gi9 = { H1(li9) where li9 is Element of REAL : ( H1(li9) in Gi & S1[li9] ) } ;
A2:
{ H1(li9) where li9 is Element of REAL : ( H1(li9) in Gi & S1[li9] ) } c= Gi
from FRAENKEL:sch 17();
then reconsider Gi9 = { H1(li9) where li9 is Element of REAL : ( H1(li9) in Gi & S1[li9] ) } as finite Subset of REAL by XBOOLE_1:1;
per cases
( Gi9 is empty or not Gi9 is empty )
;
suppose A3:
Gi9 is
empty
;
ex li being Element of REAL st [li,xi] is Gap of GiA4:
now for xi9 being Real st xi9 in Gi holds
not xi9 < xilet xi9 be
Real;
( xi9 in Gi implies not xi9 < xi )assume that A5:
xi9 in Gi
and A6:
xi9 < xi
;
contradiction
xi9 in Gi9
by A5, A6;
hence
contradiction
by A3;
verum end; consider ri being
Element of
REAL such that A7:
ri in Gi
and A8:
for
xi9 being
Real st
xi9 in Gi holds
ri >= xi9
by Th9;
take
ri
;
[ri,xi] is Gap of GiA9:
now ( ri = xi implies ( Gi = {xi} & contradiction ) )assume A10:
ri = xi
;
( Gi = {xi} & contradiction )
for
xi9 being
object holds
(
xi9 in Gi iff
xi9 = xi )
proof
let xi9 be
object ;
( xi9 in Gi iff xi9 = xi )
hereby ( xi9 = xi implies xi9 in Gi )
end;
thus
(
xi9 = xi implies
xi9 in Gi )
by A1;
verum
end; hence
Gi = {xi}
by TARSKI:def 1;
contradictionhence
contradiction
;
verum end;
ri >= xi
by A1, A8;
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;
verum end; suppose
not
Gi9 is
empty
;
ex li being Element of REAL st [li,xi] is Gap of Githen 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
;
[li,xi] is Gap of Ginow ( xi in Gi & li in Gi & xi > li & ( for xi9 being Real st xi9 in Gi & xi9 > li holds
not xi > xi9 ) )thus
xi in Gi
by A1;
( 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;
( 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
;
for xi9 being Real st xi9 in Gi & xi9 > li holds
not xi > xi9hereby verum
let xi9 be
Real;
( xi9 in Gi & xi9 > li implies not xi > xi9 )assume
xi9 in Gi
;
( not xi9 > li or not xi > xi9 )then
(
xi9 >= xi or
xi9 in Gi9 )
;
hence
( not
xi9 > li or not
xi > xi9 )
by A15;
verum
end; end; hence
[li,xi] is
Gap of
Gi
by Th13;
verum end; end;