:: JGRAPH_8 semantic presentation

REAL is non empty V36() V148() V149() V150() V154() V222() V223() V225() set

NAT is V148() V149() V150() V151() V152() V153() V154() V222() Element of K6(REAL)

K6(REAL) is set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected SubSpace of R^1

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

the carrier of I[01] is non empty V148() V149() V150() set

omega is V148() V149() V150() V151() V152() V153() V154() V222() set

K6(omega) is set

1 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

K7(1,1) is V22() V26( RAT ) V26( INT ) V138() V139() V140() V141() set

RAT is non empty V36() V148() V149() V150() V151() V154() set

INT is non empty V36() V148() V149() V150() V151() V152() V154() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is V22() V26( RAT ) V26( INT ) V138() V139() V140() V141() set

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

K7(K7(1,1),REAL) is V22() V138() V139() V140() set

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

K7(REAL,REAL) is V22() V138() V139() V140() set

K7(K7(REAL,REAL),REAL) is V22() V138() V139() V140() set

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

2 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

K7(2,2) is V22() V26( RAT ) V26( INT ) V138() V139() V140() V141() set

K7(K7(2,2),REAL) is V22() V138() V139() V140() set

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

K6(NAT) is set

COMPLEX is non empty V36() V148() V154() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct

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

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

K297( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M12( the carrier of (TOP-REAL 2))

K7( the carrier of (TOP-REAL 2),REAL) is V22() V138() V139() V140() set

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

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected TopStruct

the carrier of I[01] is non empty V148() V149() V150() set

RealSpace is strict V210() MetrStruct

the carrier of R^1 is non empty V148() V149() V150() set

K440(I[01],I[01]) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of K440(I[01],I[01]) is non empty set

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

the carrier of K440(R^1,R^1) is non empty set

K7( the carrier of K440(R^1,R^1), the carrier of (TOP-REAL 2)) is V22() set

K6(K7( the carrier of K440(R^1,R^1), the carrier of (TOP-REAL 2))) is set

{} is empty V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() set

the empty V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() set is empty V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() set

{{},1} is non empty set

3 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

Seg 1 is non empty V36() V43(1) V148() V149() V150() V151() V152() V153() V220() V221() V222() V223() V224() Element of K6(NAT)

0 is empty natural V11() real ext-real non positive non negative V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered integer V101() V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() Element of NAT

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

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

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

[.0,1.] is compact V148() V149() V150() V225() Element of K6(REAL)

0[01] is V11() real ext-real Element of the carrier of I[01]

1[01] is V11() real ext-real Element of the carrier of I[01]

TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct

a is set

<*a*> is non empty V22() V25( NAT ) Function-like V36() V43(1) FinSequence-like FinSubsequence-like set

b is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

len b is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

b ^ <*a*> is non empty V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

(b ^ <*a*>) . 1 is set

b . 1 is set

<*a*> ^ b is non empty V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

(len b) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(<*a*> ^ b) . ((len b) + 1) is set

b . (len b) is set

dom b is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

len <*a*> is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(len <*a*>) + (len b) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(<*a*> ^ b) . ((len <*a*>) + (len b)) is set

a is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

len a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

b is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

a /. b is V11() real ext-real Element of REAL

dom a is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

c is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

d is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

1 + d is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

b + (1 + d) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

a /. (b + (1 + d)) is V11() real ext-real Element of REAL

d + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

1 + (d + 1) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

b + (1 + (d + 1)) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

a /. (b + (1 + (d + 1))) is V11() real ext-real Element of REAL

b + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(b + 1) + d is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(b + (1 + d)) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

b + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

c -' (b + 1) is natural V11() real ext-real non negative integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

c - (b + 1) is V11() real ext-real integer Element of REAL

1 + (c -' (b + 1)) is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

b + (1 + (c -' (b + 1))) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

a . b is V11() real ext-real Element of REAL

1 + 0 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

b + (1 + 0) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

a /. (b + (1 + 0)) is V11() real ext-real Element of REAL

a /. c is V11() real ext-real Element of REAL

a . c is V11() real ext-real Element of REAL

a is V11() real ext-real set

b is V11() real ext-real set

c is V11() real ext-real set

d is V11() real ext-real set

closed_inside_of_rectangle (a,b,c,d) is functional Element of K6( the carrier of (TOP-REAL 2))

{ b

br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

LSeg (br,cr) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

dr is set

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

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

(1 - h) * br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

h * cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

((1 - h) * br) + (h * cr) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

((1 - h) * br) `1 is V11() real ext-real Element of REAL

((1 - h) * br) . 1 is V11() real ext-real Element of REAL

(h * cr) `1 is V11() real ext-real Element of REAL

(h * cr) . 1 is V11() real ext-real Element of REAL

(((1 - h) * br) `1) + ((h * cr) `1) is V11() real ext-real Element of REAL

((1 - h) * br) `2 is V11() real ext-real Element of REAL

((1 - h) * br) . 2 is V11() real ext-real Element of REAL

(h * cr) `2 is V11() real ext-real Element of REAL

(h * cr) . 2 is V11() real ext-real Element of REAL

(((1 - h) * br) `2) + ((h * cr) `2) is V11() real ext-real Element of REAL

|[((((1 - h) * br) `1) + ((h * cr) `1)),((((1 - h) * br) `2) + ((h * cr) `2))]| is non empty V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

cr `1 is V11() real ext-real Element of REAL

cr . 1 is V11() real ext-real Element of REAL

h * (cr `1) is V11() real ext-real Element of REAL

cr `2 is V11() real ext-real Element of REAL

cr . 2 is V11() real ext-real Element of REAL

h * (cr `2) is V11() real ext-real Element of REAL

|[(h * (cr `1)),(h * (cr `2))]| is non empty V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

br `1 is V11() real ext-real Element of REAL

br . 1 is V11() real ext-real Element of REAL

(1 - h) * (br `1) is V11() real ext-real Element of REAL

br `2 is V11() real ext-real Element of REAL

br . 2 is V11() real ext-real Element of REAL

(1 - h) * (br `2) is V11() real ext-real Element of REAL

|[((1 - h) * (br `1)),((1 - h) * (br `2))]| is non empty V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(((1 - h) * br) + (h * cr)) `2 is V11() real ext-real Element of REAL

(((1 - h) * br) + (h * cr)) . 2 is V11() real ext-real Element of REAL

((1 - h) * (br `2)) + (h * (cr `2)) is V11() real ext-real Element of REAL

Ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

Ar `1 is V11() real ext-real Element of REAL

Ar . 1 is V11() real ext-real Element of REAL

Ar `2 is V11() real ext-real Element of REAL

Ar . 2 is V11() real ext-real Element of REAL

Br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

Br `1 is V11() real ext-real Element of REAL

Br . 1 is V11() real ext-real Element of REAL

Br `2 is V11() real ext-real Element of REAL

Br . 2 is V11() real ext-real Element of REAL

(((1 - h) * br) + (h * cr)) `1 is V11() real ext-real Element of REAL

(((1 - h) * br) + (h * cr)) . 1 is V11() real ext-real Element of REAL

((1 - h) * (br `1)) + (h * (cr `1)) is V11() real ext-real Element of REAL

Ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

Ar `1 is V11() real ext-real Element of REAL

Ar . 1 is V11() real ext-real Element of REAL

Ar `2 is V11() real ext-real Element of REAL

Ar . 2 is V11() real ext-real Element of REAL

Br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

Br `1 is V11() real ext-real Element of REAL

Br . 1 is V11() real ext-real Element of REAL

Br `2 is V11() real ext-real Element of REAL

Br . 2 is V11() real ext-real Element of REAL

a is V11() real ext-real set

b is V11() real ext-real set

c is V11() real ext-real set

d is V11() real ext-real set

Trectangle (a,b,c,d) is TopSpace-like SubSpace of TOP-REAL 2

closed_inside_of_rectangle (a,b,c,d) is functional convex Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)) is strict TopSpace-like SubSpace of TOP-REAL 2

[#] (Trectangle (a,b,c,d)) is non proper closed Element of K6( the carrier of (Trectangle (a,b,c,d)))

the carrier of (Trectangle (a,b,c,d)) is set

K6( the carrier of (Trectangle (a,b,c,d))) is set

5 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

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

a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

TOP-REAL a is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct

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

K7( the carrier of I[01], the carrier of (TOP-REAL a)) is V22() set

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

Euclid a is non empty strict Reflexive discerning symmetric triangle MetrStruct

REAL a is non empty functional FinSequence-membered M12( REAL )

K298(a,REAL) is functional FinSequence-membered M12( REAL )

Pitag_dist a is V22() V25(K7((REAL a),(REAL a))) V26( REAL ) Function-like total V33(K7((REAL a),(REAL a)), REAL ) V138() V139() V140() Element of K6(K7(K7((REAL a),(REAL a)),REAL))

K7((REAL a),(REAL a)) is V22() set

K7(K7((REAL a),(REAL a)),REAL) is V22() V138() V139() V140() set

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

MetrStruct(# (REAL a),(Pitag_dist a) #) is strict MetrStruct

the carrier of (Euclid a) is non empty set

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

{ b

{1} is non empty V148() V149() V150() V151() V152() V153() V220() V222() set

b is set

[.0,1.] \/ {1} is non empty V148() V149() V150() set

b is non empty V11() real ext-real positive non negative set

c is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL a)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL a)) continuous Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL a)))

K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid a)) is V22() set

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

d is non empty V11() real ext-real positive non negative Element of REAL

d / 2 is V11() real ext-real non negative Element of REAL

ar is non empty V22() V25( the carrier of (Closed-Interval-MSpace (0,1))) V26( the carrier of (Euclid a)) Function-like total V33( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid a)) Element of K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid a)))

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

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

min (br,(1 / 2)) is V11() real ext-real set

(min (br,(1 / 2))) / 2 is V11() real ext-real Element of REAL

2 / (min (br,(1 / 2))) is V11() real ext-real Element of REAL

[/(2 / (min (br,(1 / 2))))\] is V11() real ext-real integer set

dr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

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

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

dist (h,v) is V11() real ext-real Element of REAL

ar /. h is Element of the carrier of (Euclid a)

ar . h is Element of the carrier of (Euclid a)

ar /. v is Element of the carrier of (Euclid a)

ar . v is Element of the carrier of (Euclid a)

dist ((ar /. h),(ar /. v)) is V11() real ext-real Element of REAL

(2 / (min (br,(1 / 2)))) - dr is V11() real ext-real Element of REAL

1 + ((2 / (min (br,(1 / 2)))) - dr) is V11() real ext-real Element of REAL

1 + 0 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

((min (br,(1 / 2))) / 2) * (1 + ((2 / (min (br,(1 / 2)))) - dr)) is V11() real ext-real Element of REAL

((min (br,(1 / 2))) / 2) * 1 is V11() real ext-real Element of REAL

Seg dr is V36() V43(dr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

h is natural V11() real ext-real integer set

h - 1 is V11() real ext-real integer Element of REAL

((min (br,(1 / 2))) / 2) * (h - 1) is V11() real ext-real Element of REAL

h is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

dom h is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

len h is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Seg (len h) is V36() V43( len h) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

<*1*> is non empty V22() V25( NAT ) V26( REAL ) Function-like V36() V43(1) FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

h ^ <*1*> is non empty V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

rng (h ^ <*1*>) is non empty set

v is set

len (h ^ <*1*>) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(len h) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

dom (h ^ <*1*>) is non empty V148() V149() V150() V151() V152() V153() V220() V222() Element of K6(NAT)

Ar is set

(h ^ <*1*>) . Ar is set

Seg (len (h ^ <*1*>)) is V36() V43( len (h ^ <*1*>)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

Br is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

h . Br is set

Br - 1 is V11() real ext-real integer Element of REAL

((min (br,(1 / 2))) / 2) * (Br - 1) is V11() real ext-real Element of REAL

v is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

len v is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(len h) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

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

4 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

4 + 1 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

h . Ar is set

Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

h . (Ar + 1) is set

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

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

Cr - Br is V11() real ext-real Element of REAL

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

((min (br,(1 / 2))) / 2) * ((Ar + 1) - 1) is V11() real ext-real Element of REAL

Ar - 1 is V11() real ext-real integer Element of REAL

((min (br,(1 / 2))) / 2) * (Ar - 1) is V11() real ext-real Element of REAL

((min (br,(1 / 2))) / 2) * Ar is V11() real ext-real Element of REAL

(((min (br,(1 / 2))) / 2) * Ar) - (((min (br,(1 / 2))) / 2) * (Ar - 1)) is V11() real ext-real Element of REAL

0 + 1 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT

h . 1 is set

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

((min (br,(1 / 2))) / 2) * (1 - 1) is V11() real ext-real Element of REAL

v . 1 is V11() real ext-real Element of REAL

2 * (min (br,(1 / 2))) is V11() real ext-real Element of REAL

((min (br,(1 / 2))) / 2) * (2 / (min (br,(1 / 2)))) is V11() real ext-real Element of REAL

(2 * (min (br,(1 / 2)))) / (2 * (min (br,(1 / 2)))) is V11() real ext-real Element of REAL

dr - 1 is V11() real ext-real integer Element of REAL

((min (br,(1 / 2))) / 2) * (dr - 1) is V11() real ext-real Element of REAL

1 - (((min (br,(1 / 2))) / 2) * (dr - 1)) is V11() real ext-real Element of REAL

(2 / (min (br,(1 / 2)))) - [/(2 / (min (br,(1 / 2))))\] is V11() real ext-real Element of REAL

1 + ((2 / (min (br,(1 / 2)))) - [/(2 / (min (br,(1 / 2))))\]) is V11() real ext-real Element of REAL

((min (br,(1 / 2))) / 2) * (1 + ((2 / (min (br,(1 / 2)))) - [/(2 / (min (br,(1 / 2))))\])) is V11() real ext-real Element of REAL

h . (len h) is set

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

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

Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

v /. (Ar + 1) is V11() real ext-real Element of REAL

v /. Ar is V11() real ext-real Element of REAL

(v /. (Ar + 1)) - (v /. Ar) is V11() real ext-real Element of REAL

v . (Ar + 1) is V11() real ext-real Element of REAL

h . (Ar + 1) is set

v . Ar is V11() real ext-real Element of REAL

h . Ar is set

v . Ar is V11() real ext-real Element of REAL

h . Ar is set

v . (Ar + 1) is V11() real ext-real Element of REAL

(2 / (min (br,(1 / 2)))) + 1 is V11() real ext-real Element of REAL

((2 / (min (br,(1 / 2)))) + 1) - 1 is V11() real ext-real Element of REAL

[/(2 / (min (br,(1 / 2))))\] - 1 is V11() real ext-real integer Element of REAL

Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

h . Ar is set

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

Ar - 1 is V11() real ext-real integer Element of REAL

((min (br,(1 / 2))) / 2) * (Ar - 1) is V11() real ext-real Element of REAL

Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

v /. (Ar + 1) is V11() real ext-real Element of REAL

v /. Ar is V11() real ext-real Element of REAL

v . (Ar + 1) is V11() real ext-real Element of REAL

h . (Ar + 1) is set

v . Ar is V11() real ext-real Element of REAL

h . Ar is set

v . (Ar + 1) is V11() real ext-real Element of REAL

v . Ar is V11() real ext-real Element of REAL

h . Ar is set

dom c is non empty V148() V149() V150() Element of K6( the carrier of I[01])

Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

v /. Ar is V11() real ext-real Element of REAL

Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

v /. (Ar + 1) is V11() real ext-real Element of REAL

[.(v /. Ar),(v /. (Ar + 1)).] is compact V148() V149() V150() V225() Element of K6(REAL)

Br is V148() V149() V150() Element of K6( the carrier of I[01])

c .: Br is functional Element of K6( the carrier of (TOP-REAL a))

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

Cr is Element of K6( the carrier of (Euclid a))

diameter Cr is V11() real ext-real Element of REAL

Dr is Element of the carrier of (Euclid a)

TR is Element of the carrier of (Euclid a)

dist (Dr,TR) is V11() real ext-real Element of REAL

TR is set

c . TR is V22() Function-like set

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

(v /. (Ar + 1)) - (v /. Ar) is V11() real ext-real Element of REAL

cr is set

c . cr is V22() Function-like set

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

ar . ar is Element of the carrier of (Euclid a)

ar /. ar is Element of the carrier of (Euclid a)

ar . dr is Element of the carrier of (Euclid a)

ar /. dr is Element of the carrier of (Euclid a)

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

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

br - h is V11() real ext-real Element of REAL

abs (br - h) is V11() real ext-real Element of REAL

dist (ar,dr) is V11() real ext-real Element of REAL

rng h is set

Ar is set

Br is set

h . Br is set

Cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

h . Cr is set

Cr - 1 is V11() real ext-real integer Element of REAL

((min (br,(1 / 2))) / 2) * (Cr - 1) is V11() real ext-real Element of REAL

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

rng <*1*> is non empty V148() V149() V150() Element of K6(REAL)

rng v is V148() V149() V150() Element of K6(REAL)

(rng h) \/ {1} is non empty set

v . (len v) is V11() real ext-real Element of REAL

a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

TOP-REAL a is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct

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

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

b is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)

c is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)

LSeg (b,c) is functional closed compact Element of K6( the carrier of (TOP-REAL a))

{ (((1 - b

d is functional Element of K6( the carrier of (TOP-REAL a))

ar is non empty functional Element of K6( the carrier of (TOP-REAL a))

(TOP-REAL a) | ar is non empty strict TopSpace-like SubSpace of TOP-REAL a

the carrier of ((TOP-REAL a) | ar) is non empty set

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

K6( the carrier of ((TOP-REAL a) | ar)) is set

cr is set

dr is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)

LSeg (dr,c) is functional closed compact Element of K6( the carrier of (TOP-REAL a))

{ (((1 - b

{dr} is non empty functional set

(LSeg (dr,c)) \ {dr} is functional Element of K6( the carrier of (TOP-REAL a))

LSeg (b,dr) is functional closed compact Element of K6( the carrier of (TOP-REAL a))

{ (((1 - b

(LSeg (b,dr)) \ {dr} is functional Element of K6( the carrier of (TOP-REAL a))

h is Element of K6( the carrier of ((TOP-REAL a) | ar))

Br is Element of K6( the carrier of ((TOP-REAL a) | ar))

h /\ Br is Element of K6( the carrier of ((TOP-REAL a) | ar))

v is Element of K6( the carrier of ((TOP-REAL a) | ar))

Cr is set

Cr is set

Cl Br is Element of K6( the carrier of ((TOP-REAL a) | ar))

Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))

Cl Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))

v /\ Br is Element of K6( the carrier of ((TOP-REAL a) | ar))

(h /\ Br) \ {dr} is Element of K6( the carrier of ((TOP-REAL a) | ar))

v /\ (Cl Ar) is Element of K6( the carrier of ((TOP-REAL a) | ar))

Cl h is Element of K6( the carrier of ((TOP-REAL a) | ar))

(LSeg (b,dr)) \/ (LSeg (dr,c)) is functional Element of K6( the carrier of (TOP-REAL a))

((LSeg (b,dr)) \ {dr}) \/ {dr} is non empty set

(((LSeg (b,dr)) \ {dr}) \/ {dr}) \/ (LSeg (dr,c)) is non empty set

{dr} \/ (LSeg (dr,c)) is non empty set

((LSeg (b,dr)) \ {dr}) \/ ({dr} \/ (LSeg (dr,c))) is non empty set

v \/ Br is Element of K6( the carrier of ((TOP-REAL a) | ar))

Br \ {dr} is Element of K6( the carrier of ((TOP-REAL a) | ar))

(Br \ {dr}) \/ {dr} is non empty set

v \/ ((Br \ {dr}) \/ {dr}) is non empty set

v \/ {dr} is non empty set

(v \/ {dr}) \/ Ar is non empty set

v \/ Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))

Cr is set

Cl v is Element of K6( the carrier of ((TOP-REAL a) | ar))

h /\ Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))

(Cl v) /\ Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))

br is Element of K6( the carrier of ((TOP-REAL a) | ar))

a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

TOP-REAL a is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct

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

b is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)

c is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)

LSeg (b,c) is functional closed compact Element of K6( the carrier of (TOP-REAL a))

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

{ (((1 - b

d is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL a)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL a)) continuous Path of b,c

rng d is non empty functional Element of K6( the carrier of (TOP-REAL a))

d . 1 is V22() Function-like set

d . 0 is V22() Function-like set

[#] I[01] is non empty non proper closed V148() V149() V150() Element of K6( the carrier of I[01])

d .: ([#] I[01]) is functional Element of K6( the carrier of (TOP-REAL a))

ar is set

dom d is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

br is set

d . br is V22() Function-like set

dom d is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

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

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

TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct

Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct

REAL 2 is non empty functional FinSequence-membered M12( REAL )

K298(2,REAL) is functional FinSequence-membered M12( REAL )

Pitag_dist 2 is V22() V25(K7((REAL 2),(REAL 2))) V26( REAL ) Function-like total V33(K7((REAL 2),(REAL 2)), REAL ) V138() V139() V140() Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))

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

K7(K7((REAL 2),(REAL 2)),REAL) is V22() V138() V139() V140() set

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

MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct

TopSpaceMetr (Euclid 2) is TopStruct

[#] I[01] is non empty non proper closed V148() V149() V150() Element of K6( the carrier of I[01])

a is non empty functional Element of K6( the carrier of (TOP-REAL 2))

b is non empty functional Element of K6( the carrier of (TOP-REAL 2))

c is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

d is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

c `1 is V11() real ext-real Element of REAL

c . 1 is V11() real ext-real Element of REAL

d `1 is V11() real ext-real Element of REAL

d . 1 is V11() real ext-real Element of REAL

ar `2 is V11() real ext-real Element of REAL

ar . 2 is V11() real ext-real Element of REAL

br `2 is V11() real ext-real Element of REAL

br . 2 is V11() real ext-real Element of REAL

cr is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) continuous Path of c,d

rng cr is non empty functional Element of K6( the carrier of (TOP-REAL 2))

dr is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) continuous Path of ar,br

rng dr is non empty functional Element of K6( the carrier of (TOP-REAL 2))

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

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

h is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))

v is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))

min_dist_min (h,v) is V11() real ext-real Element of REAL

(min_dist_min (h,v)) / 5 is V11() real ext-real Element of REAL

cr .: the carrier of I[01] is functional Element of K6( the carrier of (TOP-REAL 2))

dr .: ([#] I[01]) is functional Element of K6( the carrier of (TOP-REAL 2))

a /\ b is functional Element of K6( the carrier of (TOP-REAL 2))

0 / 5 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() Element of REAL

the carrier of (Euclid 2) is non empty set

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

Br is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

Br . 1 is V11() real ext-real Element of REAL

len Br is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Br . (len Br) is V11() real ext-real Element of REAL

rng Br is V148() V149() V150() Element of K6(REAL)

Cr is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

len Cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

dom Cr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

Cr is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

len Cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

dom Cr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

rng Cr is set

Dr is set

dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

TR is set

Cr . TR is set

Seg (len Cr) is V36() V43( len Cr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

Br . TR is V11() real ext-real Element of REAL

Cr . TR is set

cr . (Br . TR) is V22() Function-like set

Dr is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len Dr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Dr . 1 is V22() Function-like set

Dr /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

cr . 0 is V22() Function-like set

dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Dr /. ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

Dr /. (ar + 1) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(Dr /. ar) - (Dr /. (ar + 1)) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

|.((Dr /. ar) - (Dr /. (ar + 1))).| is V11() real ext-real non negative Element of REAL

Br . (ar + 1) is V11() real ext-real Element of REAL

Br /. (ar + 1) is V11() real ext-real Element of REAL

Cr . (ar + 1) is set

cr . (Br . (ar + 1)) is V22() Function-like set

TR is functional Element of K6( the carrier of (TOP-REAL 2))

E-bound TR is V11() real ext-real Element of REAL

W-bound TR is V11() real ext-real Element of REAL

(E-bound TR) - (W-bound TR) is V11() real ext-real Element of REAL

N-bound TR is V11() real ext-real Element of REAL

S-bound TR is V11() real ext-real Element of REAL

(N-bound TR) - (S-bound TR) is V11() real ext-real Element of REAL

((E-bound TR) - (W-bound TR)) + ((N-bound TR) - (S-bound TR)) is V11() real ext-real Element of REAL

(((E-bound TR) - (W-bound TR)) + ((N-bound TR) - (S-bound TR))) + 1 is V11() real ext-real Element of REAL

TR is Element of K6( the carrier of (Euclid 2))

cr is Element of the carrier of (Euclid 2)

dr is Element of the carrier of (Euclid 2)

dist (cr,dr) is V11() real ext-real Element of REAL

v is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

v `2 is V11() real ext-real Element of REAL

v . 2 is V11() real ext-real Element of REAL

h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

h `2 is V11() real ext-real Element of REAL

h . 2 is V11() real ext-real Element of REAL

(h `2) - (v `2) is V11() real ext-real Element of REAL

abs ((h `2) - (v `2)) is V11() real ext-real Element of REAL

v `1 is V11() real ext-real Element of REAL

v . 1 is V11() real ext-real Element of REAL

h `1 is V11() real ext-real Element of REAL

h . 1 is V11() real ext-real Element of REAL

(h `1) - (v `1) is V11() real ext-real Element of REAL

abs ((h `1) - (v `1)) is V11() real ext-real Element of REAL

(abs ((h `1) - (v `1))) + (abs ((h `2) - (v `2))) is V11() real ext-real Element of REAL

h - v is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

|.(h - v).| is V11() real ext-real non negative Element of REAL

dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

Br . ar is V11() real ext-real Element of REAL

Br /. ar is V11() real ext-real Element of REAL

[.(Br /. ar),(Br /. (ar + 1)).] is compact V148() V149() V150() V225() Element of K6(REAL)

Cr . ar is set

cr . (Br . ar) is V22() Function-like set

cr is V148() V149() V150() Element of K6( the carrier of I[01])

dr is Element of the carrier of (Euclid 2)

cr .: cr is functional Element of K6( the carrier of (TOP-REAL 2))

c `2 is V11() real ext-real Element of REAL

c . 2 is V11() real ext-real Element of REAL

h is Element of the carrier of (Euclid 2)

cr .: [.0,1.] is functional Element of K6( the carrier of (TOP-REAL 2))

v is Element of K6( the carrier of (Euclid 2))

dist (dr,h) is V11() real ext-real Element of REAL

diameter v is V11() real ext-real Element of REAL

dom Dr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(Dr /. TR) `2 is V11() real ext-real Element of REAL

(Dr /. TR) . 2 is V11() real ext-real Element of REAL

Dr . TR is V22() Function-like set

Br . TR is V11() real ext-real Element of REAL

cr . (Br . TR) is V22() Function-like set

dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

Y_axis Dr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

dom (Y_axis Dr) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(Y_axis Dr) . TR is V11() real ext-real Element of REAL

len (Y_axis Dr) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Seg (len (Y_axis Dr)) is V36() V43( len (Y_axis Dr)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

Seg (len Dr) is V36() V43( len Dr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(Dr /. TR) `2 is V11() real ext-real Element of REAL

(Dr /. TR) . 2 is V11() real ext-real Element of REAL

cr . 1 is V22() Function-like set

(Dr /. 1) `1 is V11() real ext-real Element of REAL

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

Dr /. (len Dr) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(Dr /. (len Dr)) `1 is V11() real ext-real Element of REAL

(Dr /. (len Dr)) . 1 is V11() real ext-real Element of REAL

Dr . (len Dr) is V22() Function-like set

cr . (Br . (len Br)) is V22() Function-like set

cr . (Br . 1) is V22() Function-like set

TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(Dr /. TR) `1 is V11() real ext-real Element of REAL

(Dr /. TR) . 1 is V11() real ext-real Element of REAL

Dr . TR is V22() Function-like set

Br . TR is V11() real ext-real Element of REAL

cr . (Br . TR) is V22() Function-like set

dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

X_axis Dr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

dom (X_axis Dr) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

(X_axis Dr) . 1 is V11() real ext-real Element of REAL

(X_axis Dr) . (len Dr) is V11() real ext-real Element of REAL

TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(X_axis Dr) . TR is V11() real ext-real Element of REAL

len (X_axis Dr) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Seg (len (X_axis Dr)) is V36() V43( len (X_axis Dr)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

Seg (len Dr) is V36() V43( len Dr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(Dr /. TR) `1 is V11() real ext-real Element of REAL

(Dr /. TR) . 1 is V11() real ext-real Element of REAL

Dr . (len Dr) is V22() Function-like set

TR is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

TR . 1 is V22() Function-like set

len TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

TR . (len TR) is V22() Function-like set

X_axis TR is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

Y_axis TR is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

TR /. (len TR) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

TR is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

TR . 1 is V11() real ext-real Element of REAL

len TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

TR . (len TR) is V11() real ext-real Element of REAL

rng TR is V148() V149() V150() Element of K6(REAL)

ar is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

len ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

dom ar is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

ar is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set

len ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

dom ar is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

rng ar is set

br is set

dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

cr is set

ar . cr is set

Seg (len ar) is V36() V43( len ar) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

dr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

TR . dr is V11() real ext-real Element of REAL

ar . dr is set

dr . (TR . dr) is V22() Function-like set

br is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len br is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

cr . (Br . 1) is V22() Function-like set

dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

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

br . (len br) is V22() Function-like set

br /. (len br) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

dr . 0 is V22() Function-like set

dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

h is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

h + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

br /. h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

br /. (h + 1) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(br /. h) - (br /. (h + 1)) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

|.((br /. h) - (br /. (h + 1))).| is V11() real ext-real non negative Element of REAL

TR . h is V11() real ext-real Element of REAL

TR /. h is V11() real ext-real Element of REAL

Seg (len TR) is V36() V43( len TR) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

TR . (h + 1) is V11() real ext-real Element of REAL

ar . (h + 1) is set

dr . (TR . (h + 1)) is V22() Function-like set

ar . h is set

dr . (TR . h) is V22() Function-like set

dr .: the carrier of I[01] is functional Element of K6( the carrier of (TOP-REAL 2))

cr is functional Element of K6( the carrier of (TOP-REAL 2))

v is non empty functional Element of K6( the carrier of (TOP-REAL 2))

E-bound v is V11() real ext-real Element of REAL

W-bound v is V11() real ext-real Element of REAL

(E-bound v) - (W-bound v) is V11() real ext-real Element of REAL

N-bound v is V11() real ext-real Element of REAL

S-bound v is V11() real ext-real Element of REAL

(N-bound v) - (S-bound v) is V11() real ext-real Element of REAL

((E-bound v) - (W-bound v)) + ((N-bound v) - (S-bound v)) is V11() real ext-real Element of REAL

(((E-bound v) - (W-bound v)) + ((N-bound v) - (S-bound v))) + 1 is V11() real ext-real Element of REAL

TR /. (h + 1) is V11() real ext-real Element of REAL

dr is Element of K6( the carrier of (Euclid 2))

g is Element of the carrier of (Euclid 2)

y is Element of the carrier of (Euclid 2)

dist (g,y) is V11() real ext-real Element of REAL

s is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

s `2 is V11() real ext-real Element of REAL

s . 2 is V11() real ext-real Element of REAL

t is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

t `2 is V11() real ext-real Element of REAL

t . 2 is V11() real ext-real Element of REAL

(t `2) - (s `2) is V11() real ext-real Element of REAL

abs ((t `2) - (s `2)) is V11() real ext-real Element of REAL

s `1 is V11() real ext-real Element of REAL

s . 1 is V11() real ext-real Element of REAL

t `1 is V11() real ext-real Element of REAL

t . 1 is V11() real ext-real Element of REAL

(t `1) - (s `1) is V11() real ext-real Element of REAL

abs ((t `1) - (s `1)) is V11() real ext-real Element of REAL

(abs ((t `1) - (s `1))) + (abs ((t `2) - (s `2))) is V11() real ext-real Element of REAL

t - s is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

|.(t - s).| is V11() real ext-real non negative Element of REAL

[.(TR /. h),(TR /. (h + 1)).] is compact V148() V149() V150() V225() Element of K6(REAL)

t is V148() V149() V150() Element of K6( the carrier of I[01])

g is Element of the carrier of (Euclid 2)

dr .: t is functional Element of K6( the carrier of (TOP-REAL 2))

ar `1 is V11() real ext-real Element of REAL

ar . 1 is V11() real ext-real Element of REAL

y is Element of the carrier of (Euclid 2)

dr .: [.0,1.] is functional Element of K6( the carrier of (TOP-REAL 2))

s is Element of K6( the carrier of (Euclid 2))

dist (g,y) is V11() real ext-real Element of REAL

diameter s is V11() real ext-real Element of REAL

br . (h + 1) is V22() Function-like set

dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

Seg (len TR) is V36() V43( len TR) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

TR . cr is V11() real ext-real Element of REAL

dr . (TR . cr) is V22() Function-like set

br . cr is V22() Function-like set

dom br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(br /. cr) `1 is V11() real ext-real Element of REAL

(br /. cr) . 1 is V11() real ext-real Element of REAL

Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

TR . cr is V11() real ext-real Element of REAL

dr . (TR . cr) is V22() Function-like set

dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

X_axis br is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

dom (X_axis br) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(X_axis br) . cr is V11() real ext-real Element of REAL

len (X_axis br) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Seg (len (X_axis br)) is V36() V43( len (X_axis br)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(br /. cr) `1 is V11() real ext-real Element of REAL

(br /. cr) . 1 is V11() real ext-real Element of REAL

dr . 1 is V22() Function-like set

br /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(br /. 1) `2 is V11() real ext-real Element of REAL

(br /. 1) . 2 is V11() real ext-real Element of REAL

(br /. (len br)) `2 is V11() real ext-real Element of REAL

(br /. (len br)) . 2 is V11() real ext-real Element of REAL

cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(br /. cr) `2 is V11() real ext-real Element of REAL

(br /. cr) . 2 is V11() real ext-real Element of REAL

Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

TR . cr is V11() real ext-real Element of REAL

dr . (TR . cr) is V22() Function-like set

dr . (TR . 1) is V22() Function-like set

dr . (TR . (len TR)) is V22() Function-like set

dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

Y_axis br is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

dom (Y_axis br) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

(Y_axis br) . 1 is V11() real ext-real Element of REAL

(Y_axis br) . (len br) is V11() real ext-real Element of REAL

cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

(Y_axis br) . cr is V11() real ext-real Element of REAL

len (Y_axis br) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

Seg (len (Y_axis br)) is V36() V43( len (Y_axis br)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)

br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(br /. cr) `2 is V11() real ext-real Element of REAL

(br /. cr) . 2 is V11() real ext-real Element of REAL

br . 1 is V22() Function-like set

cr is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

cr . 1 is V22() Function-like set

len cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT

cr . (len cr) is V22() Function-like set

Y_axis cr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

X_axis cr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL

dom cr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)

cr /. (len cr) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(X_axis TR) . (len TR) is V11() real ext-real Element of REAL

dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])

TR /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

cr /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

(Y_axis cr) . 1 is V11() real ext-real Element of REAL

(Y_axis cr) . (len cr) is V11() real ext-real Element of REAL

(X_axis TR) . 1 is V11() real ext-real Element of REAL

dr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)

dr `1 is V11() real ext-real Element of REAL

dr . 1 is V11() real ext-real Element of REAL

c `2 is V11() real ext-real Element of REAL

c . 2 is V11() real ext-real Element of REAL

ar `1 is V11() real ext-real Element of REAL

ar . 1 is V11() real ext-real Element of REAL

LSeg (ar,br) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

br `1 is V11() real ext-real Element of REAL

br . 1 is V11() real ext-real Element of REAL

(c `2) - (ar `2) is V11() real ext-real Element of REAL

(br `2) - (ar `2) is V11() real ext-real Element of REAL

((c `2) - (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL

(((c `2) - (ar `2)) / ((br `2) - (ar `2))) * (br `2) is V11() real ext-real Element of REAL

((c `2) - (ar `2)) * (br `2) is V11() real ext-real Element of REAL

(((c `2) - (ar `2)) * (br `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL

(c `2) * (br `2) is V11() real ext-real Element of REAL

(ar `2) * (br `2) is V11() real ext-real Element of REAL

((c `2) * (br `2)) - ((ar `2) * (br `2)) is V11() real ext-real Element of REAL

(((c `2) * (br `2)) - ((ar `2) * (br `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL

1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL

((br `2) - (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL

(((br `2) - (ar `2)) / ((br `2) - (ar `2))) - (((c `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL

((br `2) - (ar `2)) - ((c `2) - (ar `2)) is V11() real ext-real Element of REAL

(((br `2) - (ar `2)) - ((c `2) - (ar `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL

(br `2) - (c `2) is V11() real ext-real Element of REAL

((br `2) - (c `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL

(1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `2) is V11() real ext-real Element of REAL

((br `2)