set T = TOP-REAL 1;

A1: for p being Point of (TOP-REAL 1)

for U being open Subset of (TOP-REAL 1) st p in U holds

ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )

A10: ind (TOP-REAL 1) >= 1

hence ( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 ) by A1, A10, TOPDIM_1:15, XXREAL_0:1; :: thesis: verum

A1: for p being Point of (TOP-REAL 1)

for U being open Subset of (TOP-REAL 1) st p in U holds

ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )

proof

then A9:
TOP-REAL 1 is finite-ind
by TOPDIM_1:15;
let p be Point of (TOP-REAL 1); :: thesis: for U being open Subset of (TOP-REAL 1) st p in U holds

ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )

let U be open Subset of (TOP-REAL 1); :: thesis: ( p in U implies ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 ) )

assume A2: p in U ; :: thesis: ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )

reconsider p9 = p as Point of (Euclid 1) by Lm6;

set M = Euclid 1;

A3: TopStruct(# the carrier of (TopSpaceMetr (Euclid 1)), the topology of (TopSpaceMetr (Euclid 1)) #) = TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) by EUCLID:def 8;

then reconsider V = U as Subset of (TopSpaceMetr (Euclid 1)) ;

V is open by A3, PRE_TOPC:30;

then consider r being Real such that

A4: r > 0 and

A5: Ball (p9,r) c= U by A2, TOPMETR:15;

reconsider B = Ball (p9,r) as open Subset of (TOP-REAL 1) by KURATO_2:1;

take B ; :: thesis: ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 )

p9 is Tuple of 1, REAL by FINSEQ_2:131;

then consider p1 being Element of REAL such that

A6: p9 = <*p1*> by FINSEQ_2:97;

A7: Ball (p,r) = Ball (p9,r) by TOPREAL9:13;

then A8: Fr B = {<*(p1 - r)*>,<*(p1 + r)*>} by A4, A6, Th18;

TOP-REAL 1 is metrizable by A3, PCOMPS_1:def 8;

then (TOP-REAL 1) | (Fr B) is metrizable ;

hence ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 ) by A4, A5, A7, Th19, A8, JORDAN:16; :: thesis: verum

end;ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )

let U be open Subset of (TOP-REAL 1); :: thesis: ( p in U implies ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 ) )

assume A2: p in U ; :: thesis: ex W being open Subset of (TOP-REAL 1) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )

reconsider p9 = p as Point of (Euclid 1) by Lm6;

set M = Euclid 1;

A3: TopStruct(# the carrier of (TopSpaceMetr (Euclid 1)), the topology of (TopSpaceMetr (Euclid 1)) #) = TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) by EUCLID:def 8;

then reconsider V = U as Subset of (TopSpaceMetr (Euclid 1)) ;

V is open by A3, PRE_TOPC:30;

then consider r being Real such that

A4: r > 0 and

A5: Ball (p9,r) c= U by A2, TOPMETR:15;

reconsider B = Ball (p9,r) as open Subset of (TOP-REAL 1) by KURATO_2:1;

take B ; :: thesis: ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 )

p9 is Tuple of 1, REAL by FINSEQ_2:131;

then consider p1 being Element of REAL such that

A6: p9 = <*p1*> by FINSEQ_2:97;

A7: Ball (p,r) = Ball (p9,r) by TOPREAL9:13;

then A8: Fr B = {<*(p1 - r)*>,<*(p1 + r)*>} by A4, A6, Th18;

TOP-REAL 1 is metrizable by A3, PCOMPS_1:def 8;

then (TOP-REAL 1) | (Fr B) is metrizable ;

hence ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 ) by A4, A5, A7, Th19, A8, JORDAN:16; :: thesis: verum

A10: ind (TOP-REAL 1) >= 1

proof

ind (TOP-REAL 1) <= 1
by A1, A9, TOPDIM_1:16;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

reconsider p = <*(In (0,REAL))*>, q = <*jj*> as Point of (Euclid 1) by FINSEQ_2:98;

TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def 8;

then reconsider p9 = p as Point of (TOP-REAL 1) ;

A11: Ball (p,1) = Ball (p9,1) by TOPREAL9:13;

then reconsider B = Ball (p9,1) as open Subset of (TOP-REAL 1) by KURATO_2:1;

assume ind (TOP-REAL 1) < 1 ; :: thesis: contradiction

then ind (TOP-REAL 1) < 1 + 0 ;

then A12: ind (TOP-REAL 1) <= 0 by INT_1:7;

p in B by JORDAN:16;

then consider W being open Subset of (TOP-REAL 1) such that

A13: p in W and

A14: W c= B and

A15: ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) by A9, A12, TOPDIM_1:16;

Fr W = {} (TOP-REAL 1) by A15;

then A16: W is closed by TOPGEN_1:14;

A17: W \/ (W `) = [#] (TOP-REAL 1) by PRE_TOPC:2;

W misses W ` by SUBSET_1:24;

then ( [#] (TOP-REAL 1) is convex & W,W ` are_separated ) by A16, CONNSP_1:2;

then A18: W ` = {} (TOP-REAL 1) by A13, A17, CONNSP_1:15;

A19: B = { <*s*> where s is Real : ( 0 - 1 < s & s < 0 + 1 ) } by A11, JORDAN2B:27;

A20: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def 8;

not q in B

hence contradiction by A20, A18, XBOOLE_0:def 5; :: thesis: verum

end;reconsider p = <*(In (0,REAL))*>, q = <*jj*> as Point of (Euclid 1) by FINSEQ_2:98;

TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def 8;

then reconsider p9 = p as Point of (TOP-REAL 1) ;

A11: Ball (p,1) = Ball (p9,1) by TOPREAL9:13;

then reconsider B = Ball (p9,1) as open Subset of (TOP-REAL 1) by KURATO_2:1;

assume ind (TOP-REAL 1) < 1 ; :: thesis: contradiction

then ind (TOP-REAL 1) < 1 + 0 ;

then A12: ind (TOP-REAL 1) <= 0 by INT_1:7;

p in B by JORDAN:16;

then consider W being open Subset of (TOP-REAL 1) such that

A13: p in W and

A14: W c= B and

A15: ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) by A9, A12, TOPDIM_1:16;

Fr W = {} (TOP-REAL 1) by A15;

then A16: W is closed by TOPGEN_1:14;

A17: W \/ (W `) = [#] (TOP-REAL 1) by PRE_TOPC:2;

W misses W ` by SUBSET_1:24;

then ( [#] (TOP-REAL 1) is convex & W,W ` are_separated ) by A16, CONNSP_1:2;

then A18: W ` = {} (TOP-REAL 1) by A13, A17, CONNSP_1:15;

A19: B = { <*s*> where s is Real : ( 0 - 1 < s & s < 0 + 1 ) } by A11, JORDAN2B:27;

A20: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def 8;

not q in B

proof

then
not q in W
by A14;
assume
q in B
; :: thesis: contradiction

then ex s being Real st

( q = <*s*> & 0 - 1 < s & s < 0 + 1 ) by A19;

hence contradiction by FINSEQ_1:76; :: thesis: verum

end;then ex s being Real st

( q = <*s*> & 0 - 1 < s & s < 0 + 1 ) by A19;

hence contradiction by FINSEQ_1:76; :: thesis: verum

hence contradiction by A20, A18, XBOOLE_0:def 5; :: thesis: verum

hence ( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 ) by A1, A10, TOPDIM_1:15, XXREAL_0:1; :: thesis: verum