:: TOPMETR3 semantic presentation

REAL is non empty V36() V168() V169() V170() V174() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() Element of K6(REAL)

K6(REAL) is set

COMPLEX is non empty V36() V168() V174() set

omega is non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() set

K6(omega) is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

INT is non empty V36() V168() V169() V170() V171() V172() V174() set

K7(1,1) is RAT -valued INT -valued V158() V159() V160() V161() set

RAT is non empty V36() V168() V169() V170() V171() V174() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is RAT -valued INT -valued V158() V159() V160() V161() set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is V158() V159() V160() set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is V158() V159() V160() set

K7(K7(REAL,REAL),REAL) is V158() V159() V160() set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

K7(2,2) is RAT -valued INT -valued V158() V159() V160() V161() set

K7(K7(2,2),REAL) is V158() V159() V160() set

K6(K7(K7(2,2),REAL)) is set

K272() is V116() TopStruct

the carrier of K272() is V168() V169() V170() set

RealSpace is non empty strict Reflexive discerning V86() triangle Discerning V116() MetrStruct

R^1 is non empty strict TopSpace-like V116() TopStruct

K6(NAT) is set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() L15()

the carrier of (TOP-REAL 2) is non empty set

K6( the carrier of (TOP-REAL 2)) is set

K7( the carrier of (TOP-REAL 2),REAL) is V158() V159() V160() set

K6(K7( the carrier of (TOP-REAL 2),REAL)) is set

K7(COMPLEX,COMPLEX) is V158() set

K6(K7(COMPLEX,COMPLEX)) is set

K7(COMPLEX,REAL) is V158() V159() V160() set

K6(K7(COMPLEX,REAL)) is set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is V158() set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set

K7(RAT,RAT) is RAT -valued V158() V159() V160() set

K6(K7(RAT,RAT)) is set

K7(K7(RAT,RAT),RAT) is RAT -valued V158() V159() V160() set

K6(K7(K7(RAT,RAT),RAT)) is set

K7(INT,INT) is RAT -valued INT -valued V158() V159() V160() set

K6(K7(INT,INT)) is set

K7(K7(INT,INT),INT) is RAT -valued INT -valued V158() V159() V160() set

K6(K7(K7(INT,INT),INT)) is set

K7(NAT,NAT) is RAT -valued INT -valued V158() V159() V160() V161() set

K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued V158() V159() V160() V161() set

K6(K7(K7(NAT,NAT),NAT)) is set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V168() V169() V170() V171() V172() V173() V174() set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V120() V121() V168() V169() V170() V171() V172() V173() V174() Element of NAT

TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct

the carrier of R^1 is non empty V168() V169() V170() set

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V116() SubSpace of R^1

real_dist is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like V33(K7(REAL,REAL), REAL ) V158() V159() V160() Element of K6(K7(K7(REAL,REAL),REAL))

MetrStruct(# REAL,real_dist #) is strict MetrStruct

K7(NAT,REAL) is V158() V159() V160() set

K6(K7(NAT,REAL)) is set

K6( the carrier of R^1) is set

[.0,1.] is V168() V169() V170() Element of K6(REAL)

I[01] is TopSpace-like V116() SubSpace of R^1

the carrier of I[01] is V168() V169() V170() set

P is non empty Reflexive discerning V86() triangle Discerning MetrStruct

the carrier of P is non empty set

K7(NAT, the carrier of P) is set

K6(K7(NAT, the carrier of P)) is set

TopSpaceMetr P is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr P) is non empty set

K6( the carrier of (TopSpaceMetr P)) is set

P1 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))

lim P1 is Element of the carrier of P

U2 is Element of K6( the carrier of (TopSpaceMetr P))

U3 is Element of K6( the carrier of (TopSpaceMetr P))

f is V11() real ext-real set

Ball ((lim P1),f) is Element of K6( the carrier of P)

K6( the carrier of P) is set

r2 is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

P1 . r1 is Element of the carrier of P

dist ((P1 . r1),(lim P1)) is V11() real ext-real Element of REAL

U2 /\ U3 is Element of K6( the carrier of (TopSpaceMetr P))

U3 is Element of K6( the carrier of (TopSpaceMetr P))

Cl U3 is Element of K6( the carrier of (TopSpaceMetr P))

P is non empty Reflexive discerning V86() triangle Discerning MetrStruct

TopSpaceMetr P is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr P) is non empty set

P1 is non empty Reflexive discerning V86() triangle Discerning MetrStruct

TopSpaceMetr P1 is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr P1) is non empty set

K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) is set

K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1))) is set

the carrier of P is non empty set

K7(NAT, the carrier of P) is set

K6(K7(NAT, the carrier of P)) is set

the carrier of P1 is non empty set

K7(NAT, the carrier of P1) is set

K6(K7(NAT, the carrier of P1)) is set

U2 is Relation-like the carrier of (TopSpaceMetr P) -defined the carrier of (TopSpaceMetr P1) -valued Function-like V33( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) Element of K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)))

U3 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))

U2 * U3 is Relation-like NAT -defined the carrier of (TopSpaceMetr P1) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P1)))

K7(NAT, the carrier of (TopSpaceMetr P1)) is set

K6(K7(NAT, the carrier of (TopSpaceMetr P1))) is set

dom U2 is Element of K6( the carrier of (TopSpaceMetr P))

K6( the carrier of (TopSpaceMetr P)) is set

dom U3 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

rng U3 is Element of K6( the carrier of P)

K6( the carrier of P) is set

dom (U2 * U3) is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

P is non empty Reflexive discerning V86() triangle Discerning MetrStruct

TopSpaceMetr P is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr P) is non empty set

P1 is non empty Reflexive discerning V86() triangle Discerning MetrStruct

TopSpaceMetr P1 is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr P1) is non empty set

K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) is set

K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1))) is set

the carrier of P is non empty set

K7(NAT, the carrier of P) is set

K6(K7(NAT, the carrier of P)) is set

the carrier of P1 is non empty set

K7(NAT, the carrier of P1) is set

K6(K7(NAT, the carrier of P1)) is set

U2 is Relation-like the carrier of (TopSpaceMetr P) -defined the carrier of (TopSpaceMetr P1) -valued Function-like V33( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) Element of K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)))

U3 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))

U2 * U3 is Relation-like NAT -defined the carrier of (TopSpaceMetr P1) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P1)))

K7(NAT, the carrier of (TopSpaceMetr P1)) is set

K6(K7(NAT, the carrier of (TopSpaceMetr P1))) is set

f is Relation-like NAT -defined the carrier of P1 -valued Function-like V33( NAT , the carrier of P1) Element of K6(K7(NAT, the carrier of P1))

lim U3 is Element of the carrier of P

dom U2 is Element of K6( the carrier of (TopSpaceMetr P))

K6( the carrier of (TopSpaceMetr P)) is set

U2 . (lim U3) is set

rng U2 is Element of K6( the carrier of (TopSpaceMetr P1))

K6( the carrier of (TopSpaceMetr P1)) is set

Q is Element of the carrier of P1

g is V11() real ext-real Element of REAL

Ball (Q,g) is Element of K6( the carrier of P1)

K6( the carrier of P1) is set

r0 is Element of K6( the carrier of (TopSpaceMetr P1))

r1 is Element of the carrier of (TopSpaceMetr P)

t1 is Element of K6( the carrier of (TopSpaceMetr P))

U2 .: t1 is Element of K6( the carrier of (TopSpaceMetr P1))

S2 is V11() real ext-real set

Ball ((lim U3),S2) is Element of K6( the carrier of P)

K6( the carrier of P) is set

R2 is V11() real ext-real Element of REAL

s2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

S1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . S1 is Element of the carrier of P1

dist ((f . S1),Q) is V11() real ext-real Element of REAL

U3 . S1 is Element of the carrier of P

dist ((U3 . S1),(lim U3)) is V11() real ext-real Element of REAL

U2 . (U3 . S1) is set

dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

the carrier of RealSpace is non empty V168() V169() V170() set

K7(NAT, the carrier of RealSpace) is V158() V159() V160() set

K6(K7(NAT, the carrier of RealSpace)) is set

P is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

lim P is V11() real ext-real Element of REAL

P1 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))

lim P1 is V11() real ext-real Element of the carrier of RealSpace

U2 is V11() real ext-real set

f is V11() real ext-real Element of the carrier of RealSpace

r2 is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

P1 . Q is V11() real ext-real Element of the carrier of RealSpace

dist ((P1 . Q),f) is V11() real ext-real Element of REAL

P . Q is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

real_dist . (g,U2) is set

U3 is V11() real ext-real Element of REAL

g - U3 is V11() real ext-real Element of REAL

abs (g - U3) is V11() real ext-real Element of REAL

U2 is V11() real ext-real Element of the carrier of RealSpace

U3 is V11() real ext-real Element of REAL

f is V11() real ext-real set

r2 is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

P . Q is V11() real ext-real Element of REAL

(P . Q) - U3 is V11() real ext-real Element of REAL

abs ((P . Q) - U3) is V11() real ext-real Element of REAL

P1 . Q is V11() real ext-real Element of the carrier of RealSpace

dist ((P1 . Q),U2) is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

real_dist . (g,U3) is V11() real ext-real Element of REAL

g - U3 is V11() real ext-real Element of REAL

abs (g - U3) is V11() real ext-real Element of REAL

U2 is V11() real ext-real Element of REAL

U3 is V11() real ext-real set

f is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

P . r1 is V11() real ext-real Element of REAL

(P . r1) - U2 is V11() real ext-real Element of REAL

abs ((P . r1) - U2) is V11() real ext-real Element of REAL

P1 . r1 is V11() real ext-real Element of the carrier of RealSpace

dist ((P1 . r1),(lim P1)) is V11() real ext-real Element of REAL

real_dist . ((P . r1),U2) is V11() real ext-real Element of REAL

P is V11() real ext-real set

P1 is V11() real ext-real set

[.P,P1.] is V168() V169() V170() Element of K6(REAL)

Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set

K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set

K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

rng U2 is V168() V169() V170() Element of K6(REAL)

U2 . 0 is V11() real ext-real Element of REAL

dom U2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

U3 is V11() real ext-real Element of REAL

P is V11() real ext-real set

P1 is V11() real ext-real set

Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set

K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set

K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set

U2 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))

[.P,P1.] is V168() V169() V170() Element of K6(REAL)

dom U2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

rng U2 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))

K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set

P is V11() real ext-real set

P1 is V11() real ext-real set

Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set

K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set

K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set

U2 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))

lim U2 is Element of the carrier of (Closed-Interval-MSpace (P,P1))

U3 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))

lim U3 is V11() real ext-real Element of the carrier of RealSpace

[.P,P1.] is V168() V169() V170() Element of K6(REAL)

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . r2 is V11() real ext-real Element of the carrier of RealSpace

dom U2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

U2 . r2 is Element of the carrier of (Closed-Interval-MSpace (P,P1))

rng U2 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))

K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set

f is V168() V169() V170() Element of K6( the carrier of R^1)

r2 is V11() real ext-real Element of the carrier of RealSpace

r1 is Element of the carrier of (Closed-Interval-MSpace (P,P1))

Q is V11() real ext-real Element of REAL

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . r0 is Element of the carrier of (Closed-Interval-MSpace (P,P1))

dist ((U2 . r0),r1) is V11() real ext-real Element of REAL

the distance of (Closed-Interval-MSpace (P,P1)) is Relation-like K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) -defined REAL -valued Function-like V33(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL))

K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) is set

K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL) is V158() V159() V160() set

K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL)) is set

the distance of (Closed-Interval-MSpace (P,P1)) . ((U2 . r0),r1) is V11() real ext-real Element of REAL

the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V33(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))

K7( the carrier of RealSpace, the carrier of RealSpace) is V158() V159() V160() set

K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is V158() V159() V160() set

K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set

the distance of RealSpace . ((U2 . r0),r1) is set

U3 . r0 is V11() real ext-real Element of the carrier of RealSpace

dist ((U3 . r0),r2) is V11() real ext-real Element of REAL

r2 is Element of the carrier of (Closed-Interval-MSpace (P,P1))

r1 is V11() real ext-real Element of the carrier of RealSpace

Q is V11() real ext-real Element of REAL

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . r0 is V11() real ext-real Element of the carrier of RealSpace

dist ((U3 . r0),r1) is V11() real ext-real Element of REAL

U2 . r0 is Element of the carrier of (Closed-Interval-MSpace (P,P1))

dist ((U2 . r0),r2) is V11() real ext-real Element of REAL

the distance of (Closed-Interval-MSpace (P,P1)) is Relation-like K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) -defined REAL -valued Function-like V33(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL))

K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) is set

K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL) is V158() V159() V160() set

K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL)) is set

the distance of (Closed-Interval-MSpace (P,P1)) . ((U2 . r0),r2) is V11() real ext-real Element of REAL

the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V33(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))

K7( the carrier of RealSpace, the carrier of RealSpace) is V158() V159() V160() set

K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is V158() V159() V160() set

K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set

the distance of RealSpace . ((U2 . r0),r2) is set

r2 is V11() real ext-real Element of the carrier of RealSpace

r1 is V11() real ext-real Element of REAL

Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . g is V11() real ext-real Element of the carrier of RealSpace

dist ((U3 . g),r2) is V11() real ext-real Element of REAL

U2 . g is Element of the carrier of (Closed-Interval-MSpace (P,P1))

dist ((U2 . g),(lim U2)) is V11() real ext-real Element of REAL

the distance of (Closed-Interval-MSpace (P,P1)) is Relation-like K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) -defined REAL -valued Function-like V33(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL))

K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) is set

K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL) is V158() V159() V160() set

K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL)) is set

the distance of (Closed-Interval-MSpace (P,P1)) . ((U2 . g),(lim U2)) is V11() real ext-real Element of REAL

the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V33(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))

K7( the carrier of RealSpace, the carrier of RealSpace) is V158() V159() V160() set

K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is V158() V159() V160() set

K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set

the distance of RealSpace . ((U2 . g),(lim U2)) is set

P is V11() real ext-real set

P1 is V11() real ext-real set

Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set

K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set

K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

lim U2 is V11() real ext-real Element of REAL

U3 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))

lim U3 is Element of the carrier of (Closed-Interval-MSpace (P,P1))

f is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))

lim f is V11() real ext-real Element of the carrier of RealSpace

P is V11() real ext-real set

P1 is V11() real ext-real set

Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set

K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set

K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

U3 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))

P1 + 1 is V11() real ext-real Element of REAL

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . f is V11() real ext-real Element of REAL

dom U3 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

rng U3 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))

K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set

[.P,P1.] is V168() V169() V170() Element of K6(REAL)

P is V11() real ext-real set

P1 is V11() real ext-real set

Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set

K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set

K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

U3 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))

P - 1 is V11() real ext-real Element of REAL

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . f is V11() real ext-real Element of REAL

P + 1 is V11() real ext-real Element of REAL

dom U3 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

rng U3 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))

K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set

[.P,P1.] is V168() V169() V170() Element of K6(REAL)

P is non empty V168() V169() V170() Element of K6(REAL)

upper_bound P is V11() real ext-real Element of REAL

P1 is V11() real ext-real set

U2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

1 / (U2 + 1) is V11() real ext-real non negative Element of REAL

P1 - (1 / (U2 + 1)) is V11() real ext-real set

(U2 + 1) " is non empty V11() real ext-real positive non negative Element of REAL

U3 is V11() real ext-real set

f is V11() real ext-real set

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

U3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f is set

U3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . (U3 + 1) is V11() real ext-real Element of REAL

r1 is V11() real ext-real set

r2 is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . (r0 + 1) is V11() real ext-real Element of REAL

r1 is V11() real ext-real set

r2 is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . (r0 + 1) is V11() real ext-real Element of REAL

r1 is V11() real ext-real set

r2 is V11() real ext-real set

r1 is V11() real ext-real set

r2 is V11() real ext-real set

Q is set

g is set

r2 is set

r1 is set

U2 . 0 is V11() real ext-real Element of REAL

U3 is Relation-like Function-like set

dom U3 is set

U3 . 0 is set

U3 is Relation-like Function-like set

dom U3 is set

U3 . 0 is set

rng U3 is set

f is set

r2 is set

U3 . r2 is set

Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . Q is set

Q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . (Q + 1) is set

U2 . (Q + 1) is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . r1 is set

f is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . r2 is V11() real ext-real Element of REAL

f . r2 is V11() real ext-real Element of REAL

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . (r2 + 1) is V11() real ext-real Element of REAL

f . (r2 + 1) is V11() real ext-real Element of REAL

U3 . r2 is set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

f . 0 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r2 + 1) is V11() real ext-real Element of REAL

U2 . (r2 + 1) is V11() real ext-real Element of REAL

dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

U3 . r2 is set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r2 + 1) is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r2 + 1) is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r1 is V11() real ext-real Element of REAL

r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r1 + 1) is V11() real ext-real Element of REAL

U2 . (r1 + 1) is V11() real ext-real Element of REAL

U3 . r1 is set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r1 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

f . r1 is V11() real ext-real Element of REAL

rng f is V168() V169() V170() Element of K6(REAL)

r2 is set

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r1 is V11() real ext-real Element of REAL

r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r1 + 1) is V11() real ext-real Element of REAL

U2 . (r1 + 1) is V11() real ext-real Element of REAL

U3 . r1 is set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

U3 . (r1 + 1) is set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

r1 is set

f . r1 is V11() real ext-real Element of REAL

(upper_bound P) + 1 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

lim f is V11() real ext-real Element of REAL

r2 is V11() real ext-real Element of REAL

(upper_bound P) - r2 is V11() real ext-real Element of REAL

1 / r2 is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

(r1 + 1) * r2 is V11() real ext-real Element of REAL

(1 / r2) * r2 is V11() real ext-real Element of REAL

((r1 + 1) * r2) / (r1 + 1) is V11() real ext-real Element of REAL

1 / (r1 + 1) is V11() real ext-real non negative Element of REAL

P1 - (1 / (r1 + 1)) is V11() real ext-real Element of REAL

P1 - r2 is V11() real ext-real Element of REAL

U2 . r1 is V11() real ext-real Element of REAL

f . r1 is V11() real ext-real Element of REAL

(upper_bound P) - (lim f) is V11() real ext-real Element of REAL

r2 is V11() real ext-real Element of REAL

(upper_bound P) - r2 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

P is non empty V168() V169() V170() Element of K6(REAL)

lower_bound P is V11() real ext-real Element of REAL

P1 is V11() real ext-real set

U2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

1 / (U2 + 1) is V11() real ext-real non negative Element of REAL

P1 + (1 / (U2 + 1)) is V11() real ext-real set

(U2 + 1) " is non empty V11() real ext-real positive non negative Element of REAL

U3 is V11() real ext-real set

f is V11() real ext-real set

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

U3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f is set

U3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . (U3 + 1) is V11() real ext-real Element of REAL

r2 is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . (r0 + 1) is V11() real ext-real Element of REAL

r2 is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U2 . (r0 + 1) is V11() real ext-real Element of REAL

r2 is V11() real ext-real set

r1 is V11() real ext-real set

r2 is V11() real ext-real set

r1 is V11() real ext-real set

Q is set

g is set

r2 is set

r1 is set

U2 . 0 is V11() real ext-real Element of REAL

U3 is Relation-like Function-like set

dom U3 is set

U3 . 0 is set

U3 is Relation-like Function-like set

dom U3 is set

U3 . 0 is set

rng U3 is set

f is set

r2 is set

U3 . r2 is set

Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . Q is set

Q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . (Q + 1) is set

U2 . (Q + 1) is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

U3 . r1 is set

f is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

U2 . r2 is V11() real ext-real Element of REAL

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r2 + 1) is V11() real ext-real Element of REAL

U2 . (r2 + 1) is V11() real ext-real Element of REAL

U3 . r2 is set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

f . 0 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r2 + 1) is V11() real ext-real Element of REAL

f . r2 is V11() real ext-real Element of REAL

U2 . (r2 + 1) is V11() real ext-real Element of REAL

dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

U3 . r2 is set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

Q is V11() real ext-real set

r1 is V11() real ext-real set

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r2 + 1) is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r2 + 1) is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r1 is V11() real ext-real Element of REAL

r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r1 + 1) is V11() real ext-real Element of REAL

U2 . (r1 + 1) is V11() real ext-real Element of REAL

U3 . r1 is set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r1 is V11() real ext-real Element of REAL

f . r2 is V11() real ext-real Element of REAL

rng f is V168() V169() V170() Element of K6(REAL)

r2 is set

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r1 is V11() real ext-real Element of REAL

r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . (r1 + 1) is V11() real ext-real Element of REAL

U2 . (r1 + 1) is V11() real ext-real Element of REAL

U3 . r1 is set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

U3 . (r1 + 1) is set

g is V11() real ext-real set

Q is V11() real ext-real set

g is V11() real ext-real set

Q is V11() real ext-real set

r1 is set

f . r1 is V11() real ext-real Element of REAL

(lower_bound P) - 1 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

(lower_bound P) + 1 is V11() real ext-real Element of REAL

lim f is V11() real ext-real Element of REAL

r2 is V11() real ext-real Element of REAL

(lower_bound P) + r2 is V11() real ext-real Element of REAL

1 / r2 is V11() real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

(r1 + 1) * r2 is V11() real ext-real Element of REAL

(1 / r2) * r2 is V11() real ext-real Element of REAL

((r1 + 1) * r2) / (r1 + 1) is V11() real ext-real Element of REAL

1 / (r1 + 1) is V11() real ext-real non negative Element of REAL

P1 + r2 is V11() real ext-real Element of REAL

P1 + (1 / (r1 + 1)) is V11() real ext-real Element of REAL

U2 . r1 is V11() real ext-real Element of REAL

f . r1 is V11() real ext-real Element of REAL

(lim f) - (lower_bound P) is V11() real ext-real Element of REAL

r2 is V11() real ext-real Element of REAL

- (lower_bound P) is V11() real ext-real Element of REAL

(lim f) + (- (lower_bound P)) is V11() real ext-real Element of REAL

(lower_bound P) + ((lim f) + (- (lower_bound P))) is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

f . r2 is V11() real ext-real Element of REAL

(lower_bound P) + 1 is V11() real ext-real Element of REAL

P is non empty Reflexive discerning V86() triangle Discerning MetrStruct

TopSpaceMetr P is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr P) is non empty set

K7( the carrier of I[01], the carrier of (TopSpaceMetr P)) is set

K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr P))) is set

K6( the carrier of (TopSpaceMetr P)) is set

the carrier of P is non empty set

P1 is Relation-like the carrier of I[01] -defined the carrier of (TopSpaceMetr P) -valued Function-like V33( the carrier of I[01], the carrier of (TopSpaceMetr P)) Element of K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr P)))

U2 is Element of K6( the carrier of (TopSpaceMetr P))

U3 is Element of K6( the carrier of (TopSpaceMetr P))

U2 \/ U3 is Element of K6( the carrier of (TopSpaceMetr P))

U2 /\ U3 is Element of K6( the carrier of (TopSpaceMetr P))

f is V11() real ext-real Element of REAL

r2 is V11() real ext-real Element of REAL

P1 . f is set

P1 . r2 is set

{ b

r1 is set

Q is V11() real ext-real Element of REAL

P1 . Q is set

r1 is non empty V168() V169() V170() Element of K6(REAL)

Q is V11() real ext-real set

g is V11() real ext-real Element of REAL

P1 . g is set

Q is ext-real set

g is V11() real ext-real Element of REAL

P1 . g is set

upper_bound r1 is V11() real ext-real Element of REAL

Q is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

rng Q is V168() V169() V170() Element of K6(REAL)

lim Q is V11() real ext-real Element of REAL

g is set

r0 is V11() real ext-real Element of REAL

P1 . r0 is set

Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (0,1)) is non empty set

K7(NAT, the carrier of (Closed-Interval-MSpace (0,1))) is set

K6(K7(NAT, the carrier of (Closed-Interval-MSpace (0,1)))) is set

TopSpaceMetr (Closed-Interval-MSpace (0,1)) is non empty strict TopSpace-like TopStruct

K7(NAT, the carrier of P) is set

K6(K7(NAT, the carrier of P)) is set

g is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (0,1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (0,1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (0,1))))

P1 * g is Relation-like NAT -defined the carrier of (TopSpaceMetr P) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P)))

K7(NAT, the carrier of (TopSpaceMetr P)) is set

K6(K7(NAT, the carrier of (TopSpaceMetr P))) is set

r0 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))

dom P1 is V168() V169() V170() Element of K6( the carrier of I[01])

K6( the carrier of I[01]) is set

lim g is Element of the carrier of (Closed-Interval-MSpace (0,1))

P1 . (lim g) is set

rng P1 is Element of K6( the carrier of (TopSpaceMetr P))

S2 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))

lim S2 is V11() real ext-real Element of the carrier of RealSpace

t1 is Element of the carrier of P

R2 is V11() real ext-real Element of REAL

s2 is V11() real ext-real Element of REAL

S1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r0 . S2 is Element of the carrier of P

dist ((r0 . S2),t1) is V11() real ext-real Element of REAL

dom r0 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

g . S2 is Element of the carrier of (Closed-Interval-MSpace (0,1))

P1 . (g . S2) is set

dist ((lim g),(g . S2)) is V11() real ext-real Element of REAL

{ b

R2 is set

s2 is V11() real ext-real Element of REAL

P1 . s2 is set

R2 is non empty V168() V169() V170() Element of K6(REAL)

s2 is V11() real ext-real set

S1 is V11() real ext-real Element of REAL

P1 . S1 is set

s2 is ext-real set

S1 is V11() real ext-real Element of REAL

P1 . S1 is set

lower_bound R2 is V11() real ext-real Element of REAL

s2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))

rng s2 is V168() V169() V170() Element of K6(REAL)

lim s2 is V11() real ext-real Element of REAL

S1 is set

S2 is V11() real ext-real Element of REAL

P1 . S2 is set

S1 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (0,1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (0,1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (0,1))))

S2 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))

lim S2 is V11() real ext-real Element of the carrier of RealSpace

lim S1 is Element of the carrier of (Closed-Interval-MSpace (0,1))

S00 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

r0 . S00 is Element of the carrier of P

dom Q is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

Q . S00 is V11() real ext-real Element of REAL

dom r0 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

t1 is V11() real ext-real Element of REAL

P1 . t1 is set

lim r0 is Element of the carrier of P

P1 . (lim Q) is set

P1 * S1 is Relation-like NAT -defined the carrier of (TopSpaceMetr P) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P)))

P1 . (lim S1) is set

S00 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))

t1 is Element of the carrier of P

n4 is V11() real ext-real Element of REAL

rs0 is V11() real ext-real Element of REAL

r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

S00 . m is Element of the carrier of P

dist ((S00 . m),t1) is V11() real ext-real Element of REAL

dom S00 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

S1 . m is Element of the carrier of (Closed-Interval-MSpace (0,1))

P1 . (S1 . m) is set

dist ((lim S1),(S1 . m)) is V11() real ext-real Element of REAL

n4 is V11() real ext-real set

(upper_bound r1) + n4 is V11() real ext-real Element of REAL

r2 - (upper_bound r1) is V11() real ext-real Element of REAL

r2 - (upper_bound r1) is V11() real ext-real Element of REAL

min ((r2 - (upper_bound r1)),n4) is V11() real ext-real set

(min ((r2 - (upper_bound r1)),n4)) / 2 is V11() real ext-real Element of REAL

(upper_bound r1) + ((min ((r2 - (upper_bound r1)),n4)) / 2) is V11() real ext-real Element of REAL

(upper_bound r1) + (min ((r2 - (upper_bound r1)),n4)) is V11() real ext-real Element of REAL

(upper_bound r1) + (r2 - (upper_bound r1)) is V11() real ext-real Element of REAL

P1 . ((upper_bound r1) + ((min ((r2 - (upper_bound r1)),n4)) / 2)) is set

r2 - (upper_bound r1) is V11() real ext-real Element of REAL

r2 - (upper_bound r1) is V11() real ext-real Element of REAL

rs0 is V11() real ext-real set

lim S00 is Element of the carrier of P

n4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

S00 . n4 is Element of the carrier of P

dom s2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

s2 . n4 is V11() real ext-real Element of REAL

dom S00 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)

rs0 is V11() real ext-real Element of REAL

P1 . rs0 is set

P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT

TOP-REAL P is non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() L15()

the carrier of (TOP-REAL P) is non empty set

K6( the carrier of (TOP-REAL P)) is set

P1 is V43(P) V117() V160() Element of the carrier of (TOP-REAL P)

U2 is V43(P) V117() V160() Element of the carrier of (TOP-REAL P)

U3 is non empty Element of K6( the carrier of (TOP-REAL P))

f is non empty Element of K6( the carrier of (TOP-REAL P))

P is non empty compact Element of K6( the carrier of (TOP-REAL 2))

W-min P is V43(2) V117() V160() Element of the carrier of (TOP-REAL 2)

E-max P is V43(2) V117() V160() Element of the carrier of (TOP-REAL 2)

P1 is non empty compact Element of K6( the carrier of (TOP-REAL 2))

Upper_Arc P is non empty Element of K6( the carrier of (TOP-REAL 2))

Lower_Arc P is non empty Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))

K6( the carrier of ((TOP-REAL 2) | P)) is set

U2 is Element of K6( the carrier of ((TOP-REAL 2) | P))

(Upper_Arc P) /\ P is Element of K6( the carrier of (TOP-REAL 2))

(Upper_Arc P) \/ (Lower_Arc P) is non empty Element of K6( the carrier of (TOP-REAL 2))

U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))

(Lower_Arc P) /\ P is Element of K6( the carrier of (TOP-REAL 2))

(Upper_Arc P) /\ (Lower_Arc P) is Element of K6( the carrier of (TOP-REAL 2))

{(W-min P),(E-max P)} is non empty set

(TOP-REAL 2) | P1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P1) is non empty set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)) is set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1))) is set

f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P1) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)))

f . 0 is set

f . 1 is set

dom f is V168() V169() V170() Element of K6( the carrier of I[01])

K6( the carrier of I[01]) is set

[#] I[01] is non proper closed V168() V169() V170() Element of K6( the carrier of I[01])

rng f is Element of K6( the carrier of ((TOP-REAL 2) | P1))

K6( the carrier of ((TOP-REAL 2) | P1)) is set

[#] ((TOP-REAL 2) | P1) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P1))

r2 is set

r1 is set

f . r1 is set

Q is V11() real ext-real Element of REAL

r2 is set

r1 is set

f . r1 is set

Q is V11() real ext-real Element of REAL

r2 is V11() real ext-real Element of REAL

f . r2 is set

r2 is V11() real ext-real Element of REAL

f . r2 is set

r1 is V11() real ext-real Element of REAL

f . r1 is set

r1 is V11() real ext-real Element of REAL

f . r1 is set

Euclid 2 is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct

the carrier of (Euclid 2) is non empty set

K6( the carrier of (Euclid 2)) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

P1 \/ P is non empty Element of K6( the carrier of (TOP-REAL 2))

U2 \/ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))

Q is non empty Element of K6( the carrier of (Euclid 2))

(Euclid 2) | Q is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of Euclid 2

the carrier of ((Euclid 2) | Q) is non empty set

TopSpaceMetr ((Euclid 2) | Q) is non empty strict TopSpace-like TopStruct

g is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

U2 /\ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))

r0 is V11() real ext-real Element of REAL

g . r0 is set

Euclid 2 is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct

the carrier of (Euclid 2) is non empty set

K6( the carrier of (Euclid 2)) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

P1 \/ P is non empty Element of K6( the carrier of (TOP-REAL 2))

U2 \/ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))

Q is non empty Element of K6( the carrier of (Euclid 2))

(Euclid 2) | Q is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of Euclid 2

the carrier of ((Euclid 2) | Q) is non empty set

TopSpaceMetr ((Euclid 2) | Q) is non empty strict TopSpace-like TopStruct

g is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

U2 /\ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))

r0 is V11() real ext-real Element of REAL

g . r0 is set

r2 is V11() real ext-real Element of REAL

f . r2 is set

r2 is V11() real ext-real Element of REAL

f . r2 is set

r2 is V11() real ext-real Element of REAL

f . r2 is set

r2 is V11() real ext-real Element of REAL

f . r2 is set