:: JORDAN1K semantic presentation

REAL is V45() V46() V47() V51() set

NAT is V45() V46() V47() V48() V49() V50() V51() Element of K6(REAL)

K6(REAL) is set

COMPLEX is V45() V51() set

RAT is V45() V46() V47() V48() V51() set

INT is V45() V46() V47() V48() V49() V51() set

omega is V45() V46() V47() V48() V49() V50() V51() set

K6(omega) is set

K6(NAT) is set

K7(COMPLEX,COMPLEX) is V33() set

K6(K7(COMPLEX,COMPLEX)) is set

K7(COMPLEX,REAL) is V33() V34() V35() set

K6(K7(COMPLEX,REAL)) is set

1 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

K7(1,1) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set

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

K7(K7(1,1),REAL) is V33() V34() V35() set

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

K7(REAL,REAL) is V33() V34() V35() set

K7(K7(REAL,REAL),REAL) is V33() V34() V35() set

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

2 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

K7(2,2) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set

K7(K7(2,2),REAL) is V33() V34() V35() set

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

K6(K7(REAL,REAL)) is set

K386() is non empty V142() L10()

the carrier of K386() is non empty set

K391() is non empty V142() V164() V165() V166() V168() V194() V195() V196() V197() V198() V199() L10()

K392() is non empty V142() V166() V168() V197() V198() V199() M16(K391())

K393() is non empty V142() V164() V166() V168() V197() V198() V199() V200() M19(K391(),K392())

K395() is non empty V142() V164() V166() V168() L10()

K396() is non empty V142() V164() V166() V168() V200() M16(K395())

K479() is V220() TopStruct

the carrier of K479() is V45() V46() V47() set

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V220() MetrStruct

K484() is non empty strict TopSpace-like T_2 V220() TopStruct

the carrier of K484() is non empty V45() V46() V47() set

TOP-REAL 2 is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct

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

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

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

[#] (TOP-REAL 2) is non empty non proper non proper open open connected a_component V260( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

K292((TOP-REAL 2)) is V16() Function-like V33() V34() V35() V69(2) V70() V83( TOP-REAL 2) Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

{K292((TOP-REAL 2))} is non empty functional V52() set

([#] (TOP-REAL 2)) \ {K292((TOP-REAL 2))} is Element of K6( the carrier of (TOP-REAL 2))

K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))) is set

K6(K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)))) is set

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

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

K7(K7(COMPLEX,COMPLEX),COMPLEX) is V33() set

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

K7(RAT,RAT) is V20( RAT ) V33() V34() V35() set

K6(K7(RAT,RAT)) is set

K7(K7(RAT,RAT),RAT) is V20( RAT ) V33() V34() V35() set

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

K7(INT,INT) is V20( RAT ) V20( INT ) V33() V34() V35() set

K6(K7(INT,INT)) is set

K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) V33() V34() V35() set

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

K7(NAT,NAT) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set

K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set

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

{} is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set

the empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set

union {} is V52() set

0 is empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() V52() V56() Element of NAT

|[0,0]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K6( the carrier of K484()) is set

A is set

B is non empty set

K7(A,B) is set

K6(K7(A,B)) is set

P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))

rng P is Element of K6(B)

K6(B) is set

p is Element of B

A is set

B is non empty set

K7(A,B) is set

K6(K7(A,B)) is set

P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))

p is Element of B

q is set

P . q is set

A is set

K6(A) is set

B is non empty set

K7(A,B) is set

K6(K7(A,B)) is set

P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))

p is Element of K6(A)

P .: p is Element of K6(B)

K6(B) is set

(P .: p) ` is Element of K6(B)

B \ (P .: p) is set

p ` is Element of K6(A)

A \ p is set

P .: (p `) is Element of K6(B)

q is set

a is Element of B

r is set

P . r is set

r is Element of A

A is set

K6(A) is set

B is non empty set

K7(A,B) is set

K6(K7(A,B)) is set

P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))

p is Element of K6(A)

p ` is Element of K6(A)

A \ p is set

P .: (p `) is Element of K6(B)

K6(B) is set

P .: p is Element of K6(B)

(P .: p) ` is Element of K6(B)

B \ (P .: p) is set

q is set

a is Element of B

r is set

P . r is set

r is set

P . r is set

A is set

K6(A) is set

B is non empty set

K7(A,B) is set

K6(K7(A,B)) is set

P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))

p is Element of K6(A)

P .: p is Element of K6(B)

K6(B) is set

(P .: p) ` is Element of K6(B)

B \ (P .: p) is set

p ` is Element of K6(A)

A \ p is set

P .: (p `) is Element of K6(B)

A is TopSpace-like TopStruct

the carrier of A is set

K6( the carrier of A) is set

{} A is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact Element of K6( the carrier of A)

B is Element of K6( the carrier of A)

A | ({} A) is empty V81() V82() {} -element strict T_2 compact SubSpace of A

the carrier of (A | ({} A)) is empty V2() Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set

K6( the carrier of (A | ({} A))) is V52() V56() set

P is functional V45() V46() V47() V48() V49() V50() V52() V56() Element of K6( the carrier of (A | ({} A)))

p is functional V45() V46() V47() V48() V49() V50() V52() V56() Element of K6( the carrier of (A | ({} A)))

A is non empty TopSpace-like TopStruct

the carrier of A is non empty set

K6( the carrier of A) is set

B is Element of K6( the carrier of A)

P is Element of K6( the carrier of A)

p is Element of K6( the carrier of A)

{} A is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact Element of K6( the carrier of A)

A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct

REAL A is non empty V72() M12( REAL )

K257(A,REAL) is V72() M12( REAL )

Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))

K7((REAL A),(REAL A)) is set

K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() 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

P is Element of K6( the carrier of (Euclid A))

P ` is Element of K6( the carrier of (Euclid A))

the carrier of (Euclid A) \ P is set

P \/ (P `) is Element of K6( the carrier of (Euclid A))

[#] (Euclid A) is non empty non proper Element of K6( the carrier of (Euclid A))

B is Element of K6( the carrier of (Euclid A))

A is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

TopSpaceMetr A is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr A) is non empty set

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

B is non empty Element of K6( the carrier of (TopSpaceMetr A))

dist_min B is non empty V16() V19( the carrier of (TopSpaceMetr A)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr A)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484()))

K7( the carrier of (TopSpaceMetr A), the carrier of K484()) is V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484())) is set

P is Element of the carrier of (TopSpaceMetr A)

(dist_min B) . P is V11() real ext-real Element of the carrier of K484()

the carrier of A is non empty set

Family_open_set A is Element of K6(K6( the carrier of A))

K6( the carrier of A) is set

K6(K6( the carrier of A)) is set

TopStruct(# the carrier of A,(Family_open_set A) #) is strict TopStruct

p is Element of the carrier of A

dist p is non empty V16() V19( the carrier of (TopSpaceMetr A)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr A)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484()))

(dist p) .: B is V45() V46() V47() Element of K6( the carrier of K484())

[#] ((dist p) .: B) is V45() V46() V47() Element of K6(REAL)

a is V11() real ext-real set

dom (dist p) is Element of K6( the carrier of (TopSpaceMetr A))

r is set

(dist p) . r is V11() real ext-real set

r is Element of the carrier of A

dist (p,r) is V11() real ext-real Element of REAL

dom (dist p) is Element of K6( the carrier of (TopSpaceMetr A))

lower_bound ([#] ((dist p) .: B)) is V11() real ext-real Element of REAL

lower_bound ((dist p) .: B) is V11() real ext-real Element of REAL

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

B is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

TopSpaceMetr B is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr B) is non empty set

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

the carrier of B is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr B))

dist_min P is non empty V16() V19( the carrier of (TopSpaceMetr B)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr B)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484()))

K7( the carrier of (TopSpaceMetr B), the carrier of K484()) is V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484())) is set

p is Element of the carrier of B

(dist_min P) . p is V11() real ext-real set

dist p is non empty V16() V19( the carrier of (TopSpaceMetr B)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr B)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484()))

(dist p) .: P is V45() V46() V47() Element of K6( the carrier of K484())

[#] ((dist p) .: P) is V45() V46() V47() Element of K6(REAL)

Family_open_set B is Element of K6(K6( the carrier of B))

K6( the carrier of B) is set

K6(K6( the carrier of B)) is set

TopStruct(# the carrier of B,(Family_open_set B) #) is strict TopStruct

a is V11() real ext-real set

dom (dist p) is Element of K6( the carrier of (TopSpaceMetr B))

r is set

(dist p) . r is V11() real ext-real set

r is Element of the carrier of B

dist (p,r) is V11() real ext-real Element of REAL

dom (dist p) is Element of K6( the carrier of (TopSpaceMetr B))

lower_bound ([#] ((dist p) .: P)) is V11() real ext-real Element of REAL

lower_bound ((dist p) .: P) is V11() real ext-real Element of REAL

A is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

TopSpaceMetr A is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr A) is non empty set

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

B is non empty Element of K6( the carrier of (TopSpaceMetr A))

P is non empty Element of K6( the carrier of (TopSpaceMetr A))

min_dist_min (B,P) is V11() real ext-real Element of REAL

dist_min B is non empty V16() V19( the carrier of (TopSpaceMetr A)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr A)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484()))

K7( the carrier of (TopSpaceMetr A), the carrier of K484()) is V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484())) is set

(dist_min B) .: P is V45() V46() V47() Element of K6( the carrier of K484())

[#] ((dist_min B) .: P) is V45() V46() V47() Element of K6(REAL)

q is V11() real ext-real set

dom (dist_min B) is Element of K6( the carrier of (TopSpaceMetr A))

a is set

(dist_min B) . a is V11() real ext-real set

r is Element of the carrier of (TopSpaceMetr A)

(dist_min B) . r is V11() real ext-real Element of the carrier of K484()

dom (dist_min B) is Element of K6( the carrier of (TopSpaceMetr A))

lower_bound ([#] ((dist_min B) .: P)) is V11() real ext-real Element of REAL

lower_bound ((dist_min B) .: P) is V11() real ext-real Element of REAL

A is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

TopSpaceMetr A is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr A) is non empty set

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

B is compact Element of K6( the carrier of (TopSpaceMetr A))

P is compact Element of K6( the carrier of (TopSpaceMetr A))

min_dist_min (B,P) is V11() real ext-real Element of REAL

p is set

the carrier of A is non empty set

Family_open_set A is Element of K6(K6( the carrier of A))

K6( the carrier of A) is set

K6(K6( the carrier of A)) is set

TopStruct(# the carrier of A,(Family_open_set A) #) is strict TopStruct

q is Element of the carrier of A

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

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

B is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

TopSpaceMetr B is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr B) is non empty set

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

the carrier of B is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr B))

p is non empty Element of K6( the carrier of (TopSpaceMetr B))

min_dist_min (P,p) is V11() real ext-real Element of REAL

dist_min P is non empty V16() V19( the carrier of (TopSpaceMetr B)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr B)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484()))

K7( the carrier of (TopSpaceMetr B), the carrier of K484()) is V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484())) is set

(dist_min P) .: p is V45() V46() V47() Element of K6( the carrier of K484())

[#] ((dist_min P) .: p) is V45() V46() V47() Element of K6(REAL)

a is V11() real ext-real set

dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr B))

r is set

(dist_min P) . r is V11() real ext-real set

r is Element of the carrier of (TopSpaceMetr B)

s is Element of the carrier of B

q9 is Element of the carrier of B

dist (s,q9) is V11() real ext-real Element of REAL

dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr B))

lower_bound ([#] ((dist_min P) .: p)) is V11() real ext-real Element of REAL

lower_bound ((dist_min P) .: p) is V11() real ext-real Element of REAL

A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct

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

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

P is Element of K6( the carrier of (TOP-REAL A))

P ` is Element of K6( the carrier of (TOP-REAL A))

the carrier of (TOP-REAL A) \ P is set

B is Element of K6( the carrier of (TOP-REAL A))

A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct

{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))

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

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

BDD ({} (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))

{ b

[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))

the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))

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

TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct

[#] TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is non proper Element of K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #))

the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is set

K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #)) is set

(TOP-REAL A) | ([#] (TOP-REAL A)) is strict SubSpace of TOP-REAL A

P is set

p is Element of K6( the carrier of (TOP-REAL A))

({} (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))

the carrier of (TOP-REAL A) \ ({} (TOP-REAL A)) is set

A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct

[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))

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

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

BDD ([#] (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))

{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))

([#] (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))

the carrier of (TOP-REAL A) \ ([#] (TOP-REAL A)) is set

A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct

{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))

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

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

UBD ({} (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))

[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))

{ b

the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))

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

TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct

[#] TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is non proper Element of K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #))

the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is set

K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #)) is set

(TOP-REAL A) | ([#] (TOP-REAL A)) is strict SubSpace of TOP-REAL A

({} (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))

the carrier of (TOP-REAL A) \ ({} (TOP-REAL A)) is set

union { b

A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct

[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))

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

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

UBD ([#] (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))

{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))

([#] (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))

the carrier of (TOP-REAL A) \ ([#] (TOP-REAL A)) is set

A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct

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

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

B is connected Element of K6( the carrier of (TOP-REAL A))

P is Element of K6( the carrier of (TOP-REAL A))

UBD P is Element of K6( the carrier of (TOP-REAL A))

BDD P is Element of K6( the carrier of (TOP-REAL A))

[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))

[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))

P ` is Element of K6( the carrier of (TOP-REAL A))

the carrier of (TOP-REAL A) \ P is set

(P `) ` is Element of K6( the carrier of (TOP-REAL A))

the carrier of (TOP-REAL A) \ (P `) is set

{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))

p is Element of K6( the carrier of (TOP-REAL A))

[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))

Euclid 2 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct

REAL 2 is non empty V72() M12( REAL )

K257(2,REAL) is V72() M12( REAL )

Pitag_dist 2 is V16() V19(K7((REAL 2),(REAL 2))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))

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

K7(K7((REAL 2),(REAL 2)),REAL) is V33() V34() V35() set

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

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

the carrier of (Euclid 2) is non empty set

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

dist (|[0,0]|,A) is V11() real ext-real Element of REAL

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

B * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (|[0,0]|,(B * A)) is V11() real ext-real Element of REAL

abs B is V11() real ext-real Element of REAL

(abs B) * (dist (|[0,0]|,A)) is V11() real ext-real Element of REAL

B ^2 is V11() real ext-real Element of REAL

K37(B,B) is V11() real ext-real set

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

(A `1) ^2 is V11() real ext-real Element of REAL

K37((A `1),(A `1)) is V11() real ext-real set

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

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

K37((A `2),(A `2)) is V11() real ext-real set

|[0,0]| `1 is V11() real ext-real Element of REAL

|[0,0]| `2 is V11() real ext-real Element of REAL

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

(0 - (A `1)) ^2 is V11() real ext-real Element of REAL

K37((0 - (A `1)),(0 - (A `1))) is V11() real ext-real set

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

(0 - (A `2)) ^2 is V11() real ext-real Element of REAL

K37((0 - (A `2)),(0 - (A `2))) is V11() real ext-real set

((0 - (A `1)) ^2) + ((0 - (A `2)) ^2) is V11() real ext-real Element of REAL

sqrt (((0 - (A `1)) ^2) + ((0 - (A `2)) ^2)) is V11() real ext-real Element of REAL

((A `1) ^2) + ((A `2) ^2) is V11() real ext-real Element of REAL

sqrt (((A `1) ^2) + ((A `2) ^2)) is V11() real ext-real Element of REAL

(B * A) `1 is V11() real ext-real Element of REAL

0 - ((B * A) `1) is V11() real ext-real Element of REAL

(0 - ((B * A) `1)) ^2 is V11() real ext-real Element of REAL

K37((0 - ((B * A) `1)),(0 - ((B * A) `1))) is V11() real ext-real set

(B * A) `2 is V11() real ext-real Element of REAL

0 - ((B * A) `2) is V11() real ext-real Element of REAL

(0 - ((B * A) `2)) ^2 is V11() real ext-real Element of REAL

K37((0 - ((B * A) `2)),(0 - ((B * A) `2))) is V11() real ext-real set

((0 - ((B * A) `1)) ^2) + ((0 - ((B * A) `2)) ^2) is V11() real ext-real Element of REAL

sqrt (((0 - ((B * A) `1)) ^2) + ((0 - ((B * A) `2)) ^2)) is V11() real ext-real Element of REAL

((B * A) `1) ^2 is V11() real ext-real Element of REAL

K37(((B * A) `1),((B * A) `1)) is V11() real ext-real set

- ((B * A) `2) is V11() real ext-real Element of REAL

(- ((B * A) `2)) ^2 is V11() real ext-real Element of REAL

K37((- ((B * A) `2)),(- ((B * A) `2))) is V11() real ext-real set

(((B * A) `1) ^2) + ((- ((B * A) `2)) ^2) is V11() real ext-real Element of REAL

sqrt ((((B * A) `1) ^2) + ((- ((B * A) `2)) ^2)) is V11() real ext-real Element of REAL

B * (A `1) is V11() real ext-real Element of REAL

(B * (A `1)) ^2 is V11() real ext-real Element of REAL

K37((B * (A `1)),(B * (A `1))) is V11() real ext-real set

((B * A) `2) ^2 is V11() real ext-real Element of REAL

K37(((B * A) `2),((B * A) `2)) is V11() real ext-real set

((B * (A `1)) ^2) + (((B * A) `2) ^2) is V11() real ext-real Element of REAL

sqrt (((B * (A `1)) ^2) + (((B * A) `2) ^2)) is V11() real ext-real Element of REAL

(B ^2) * ((A `1) ^2) is V11() real ext-real Element of REAL

B * (A `2) is V11() real ext-real Element of REAL

(B * (A `2)) ^2 is V11() real ext-real Element of REAL

K37((B * (A `2)),(B * (A `2))) is V11() real ext-real set

((B ^2) * ((A `1) ^2)) + ((B * (A `2)) ^2) is V11() real ext-real Element of REAL

sqrt (((B ^2) * ((A `1) ^2)) + ((B * (A `2)) ^2)) is V11() real ext-real Element of REAL

(B ^2) * (((A `1) ^2) + ((A `2) ^2)) is V11() real ext-real Element of REAL

sqrt ((B ^2) * (((A `1) ^2) + ((A `2) ^2))) is V11() real ext-real Element of REAL

sqrt (B ^2) is V11() real ext-real Element of REAL

(sqrt (B ^2)) * (sqrt (((A `1) ^2) + ((A `2) ^2))) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

A + B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

P + B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(P,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((A + B),(P + B)) is V11() real ext-real Element of REAL

dist (A,P) is V11() real ext-real Element of REAL

(A + B) `1 is V11() real ext-real Element of REAL

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

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

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

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

(A `1) + (B `1) is V11() real ext-real Element of REAL

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

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

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

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

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

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

(A + B) `2 is V11() real ext-real Element of REAL

(P + B) `2 is V11() real ext-real Element of REAL

((A + B) `2) - ((P + B) `2) is V11() real ext-real Element of REAL

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

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

(A `2) + (B `2) is V11() real ext-real Element of REAL

((A `2) + (B `2)) - ((P + B) `2) is V11() real ext-real Element of REAL

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

(P `2) + (B `2) is V11() real ext-real Element of REAL

((A `2) + (B `2)) - ((P `2) + (B `2)) is V11() real ext-real Element of REAL

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

((A `2) - (P `2)) + 0 is V11() real ext-real Element of REAL

(((A + B) `1) - ((P + B) `1)) ^2 is V11() real ext-real Element of REAL

K37((((A + B) `1) - ((P + B) `1)),(((A + B) `1) - ((P + B) `1))) is V11() real ext-real set

(((A + B) `2) - ((P + B) `2)) ^2 is V11() real ext-real Element of REAL

K37((((A + B) `2) - ((P + B) `2)),(((A + B) `2) - ((P + B) `2))) is V11() real ext-real set

((((A + B) `1) - ((P + B) `1)) ^2) + ((((A + B) `2) - ((P + B) `2)) ^2) is V11() real ext-real Element of REAL

sqrt (((((A + B) `1) - ((P + B) `1)) ^2) + ((((A + B) `2) - ((P + B) `2)) ^2)) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

dist (A,B) is V11() real ext-real Element of REAL

P is Element of the carrier of (Euclid 2)

p is Element of the carrier of (Euclid 2)

dist (P,p) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

P - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(P,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((A - B),(P - B)) is V11() real ext-real Element of REAL

dist (A,P) is V11() real ext-real Element of REAL

- B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K367(B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

A + (- B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(A,(- B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

P + (- B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(P,(- B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

- A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K367(A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

dist (A,B) is V11() real ext-real Element of REAL

- B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K367(B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((- A),(- B)) is V11() real ext-real Element of REAL

B - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(B,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((B - B),(A - B)) is V11() real ext-real Element of REAL

A + (- B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(A,(- B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((B - B),(A + (- B))) is V11() real ext-real Element of REAL

dist (|[0,0]|,(A + (- B))) is V11() real ext-real Element of REAL

A - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(A,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((A - A),(A + (- B))) is V11() real ext-real Element of REAL

A + (- A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(A,(- A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((A + (- A)),(A + (- B))) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

A - P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((A - B),(A - P)) is V11() real ext-real Element of REAL

dist (B,P) is V11() real ext-real Element of REAL

- (A - B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K367((A - B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

B - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(B,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

- (A - P) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K367((A - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

P - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(P,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((B - A),(P - A)) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

dist (A,B) is V11() real ext-real Element of REAL

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

P * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

P * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(B,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((P * A),(P * B)) is V11() real ext-real Element of REAL

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

(abs P) * (dist (A,B)) is V11() real ext-real Element of REAL

(P * A) - (P * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369((P * A),(P * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

(P * A) - (P * B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369((P * A),(P * B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (((P * A) - (P * A)),((P * A) - (P * B))) is V11() real ext-real Element of REAL

dist (|[0,0]|,((P * A) - (P * B))) is V11() real ext-real Element of REAL

A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

P * (A - B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371((A - B),P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (|[0,0]|,(P * (A - B))) is V11() real ext-real Element of REAL

dist (|[0,0]|,(A - B)) is V11() real ext-real Element of REAL

(abs P) * (dist (|[0,0]|,(A - B))) is V11() real ext-real Element of REAL

A - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(A,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist ((A - A),(A - B)) is V11() real ext-real Element of REAL

(abs P) * (dist ((A - A),(A - B))) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

dist (A,B) is V11() real ext-real Element of REAL

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

P * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

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

(1 - P) * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(B,(1 - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

(P * A) + ((1 - P) * B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365((P * A),((1 - P) * B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (A,((P * A) + ((1 - P) * B))) is V11() real ext-real Element of REAL

(1 - P) * (dist (A,B)) is V11() real ext-real Element of REAL

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

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

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

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

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

(P + (1 - P)) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,(P + (1 - P))) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (((P + (1 - P)) * A),((P * A) + ((1 - P) * B))) is V11() real ext-real Element of REAL

(1 - P) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,(1 - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

(P * A) + ((1 - P) * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365((P * A),((1 - P) * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (((P * A) + ((1 - P) * A)),((P * A) + ((1 - P) * B))) is V11() real ext-real Element of REAL

dist (((1 - P) * A),((1 - P) * B)) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

dist (B,A) is V11() real ext-real Element of REAL

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

P * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(B,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

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

(1 - P) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,(1 - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

(P * B) + ((1 - P) * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365((P * B),((1 - P) * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (A,((P * B) + ((1 - P) * A))) is V11() real ext-real Element of REAL

P * (dist (B,A)) is V11() real ext-real Element of REAL

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

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

(P + (1 - P)) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,(P + (1 - P))) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (((P * B) + ((1 - P) * A)),((P + (1 - P)) * A)) is V11() real ext-real Element of REAL

P * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

(P * A) + ((1 - P) * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365((P * A),((1 - P) * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

dist (((P * A) + ((1 - P) * A)),((P * B) + ((1 - P) * A))) is V11() real ext-real Element of REAL

dist ((P * A),(P * B)) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

dist (B,A) is V11() real ext-real Element of REAL

P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

LSeg (B,P) is connected Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

dist (A,P) is V11() real ext-real Element of REAL

(dist (B,A)) + (dist (A,P)) is V11() real ext-real Element of REAL

dist (B,P) is V11() real ext-real Element of REAL

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

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

(1 - p) * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(B,(1 - p)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

p * P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(P,p) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

((1 - p) * B) + (p * P) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(((1 - p) * B),(p * P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

p * (dist (B,P)) is V11() real ext-real Element of REAL

dist (P,A) is V11() real ext-real Element of REAL

(1 - p) * (dist (B,P)) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

LSeg (B,P) is connected Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

dist (B,P) is V11() real ext-real Element of REAL

dist (A,P) is V11() real ext-real Element of REAL

dist (B,A) is V11() real ext-real Element of REAL

(dist (B,A)) + (dist (A,P)) is V11() real ext-real Element of REAL

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

{ b

B is Element of the carrier of (Euclid 2)

Ball (B,A) is Element of K6( the carrier of (Euclid 2))

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

{ b

q is set

a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

|[0,0]| - a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(|[0,0]|,a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

|.(|[0,0]| - a).| is V11() real ext-real non negative Element of REAL

K373((|[0,0]| - a)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL

sqrt K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL

a - |[0,0]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(a,|[0,0]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

|.(a - |[0,0]|).| is V11() real ext-real non negative Element of REAL

K373((a - |[0,0]|)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL

sqrt K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL

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

K373(a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

K379(K373(a)) is V11() real ext-real Element of REAL

sqrt K379(K373(a)) is V11() real ext-real Element of REAL

q is set

a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

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

K373(a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

K379(K373(a)) is V11() real ext-real Element of REAL

sqrt K379(K373(a)) is V11() real ext-real Element of REAL

|[0,0]| - a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(|[0,0]|,a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

|.(|[0,0]| - a).| is V11() real ext-real non negative Element of REAL

K373((|[0,0]| - a)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL

sqrt K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL

a - |[0,0]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K369(a,|[0,0]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

|.(a - |[0,0]|).| is V11() real ext-real non negative Element of REAL

K373((a - |[0,0]|)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL

sqrt K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

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

B * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

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

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

AffineMap (B,P,B,p) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

(AffineMap (B,P,B,p)) . A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

|[P,p]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(B * A) + |[P,p]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365((B * A),|[P,p]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

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

B * (A `1) is V11() real ext-real Element of REAL

(B * (A `1)) + P is V11() real ext-real Element of REAL

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

B * (A `2) is V11() real ext-real Element of REAL

(B * (A `2)) + p is V11() real ext-real Element of REAL

|[((B * (A `1)) + P),((B * (A `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(B * A) `1 is V11() real ext-real Element of REAL

((B * A) `1) + P is V11() real ext-real Element of REAL

|[(((B * A) `1) + P),((B * (A `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(B * A) `2 is V11() real ext-real Element of REAL

((B * A) `2) + p is V11() real ext-real Element of REAL

|[(((B * A) `1) + P),(((B * A) `2) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

|[((B * A) `1),((B * A) `2)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

|[((B * A) `1),((B * A) `2)]| + |[P,p]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365(|[((B * A) `1),((B * A) `2)]|,|[P,p]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

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

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

B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

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

AffineMap (P,(A `1),P,(A `2)) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

(AffineMap (P,(A `1),P,(A `2))) . B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

P * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K371(B,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

(P * B) + A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365((P * B),A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

|[(A `1),(A `2)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(P * B) + |[(A `1),(A `2)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

K365((P * B),|[(A `1),(A `2)]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )

id (REAL 2) is non empty V16() V19( REAL 2) V20( REAL 2) Function-like one-to-one V26( REAL 2) quasi_total Element of K6(K7((REAL 2),(REAL 2)))

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

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

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

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

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

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

P / A is V11() real ext-real Element of REAL

- (P / A) is V11() real ext-real Element of REAL

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

p / B is V11() real ext-real Element of REAL

- (p / B) is V11() real ext-real Element of REAL

AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

AffineMap (A,P,B,p) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

(AffineMap (A,P,B,p)) * (AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B)))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))

a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

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

(1 / A) * (a `1) is V11() real ext-real Element of REAL

((1 / A) * (a `1)) - (P / A) is V11() real ext-real Element of REAL

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

(1 / B) * (a `2) is V11() real ext-real Element of REAL

((1 / B) * (a `2)) - (p / B) is V11() real ext-real Element of REAL

|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2 is V11() real ext-real Element of REAL

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

((AffineMap (A,P,B,p)) * (AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B))))) . a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B)))) . a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(AffineMap (A,P,B,p)) . ((AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B)))) . a) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

((1 / A) * (a `1)) + (- (P / A)) is V11() real ext-real Element of REAL

((1 / B) * (a `2)) + (- (p / B)) is V11() real ext-real Element of REAL

|[(((1 / A) * (a `1)) + (- (P / A))),(((1 / B) * (a `2)) + (- (p / B)))]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(AffineMap (A,P,B,p)) . |[(((1 / A) * (a `1)) + (- (P / A))),(((1 / B) * (a `2)) + (- (p / B)))]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1 is V11() real ext-real Element of REAL

A * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1) is V11() real ext-real Element of REAL

(A * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1)) + P is V11() real ext-real Element of REAL

B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2) is V11() real ext-real Element of REAL

(B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p is V11() real ext-real Element of REAL

|[((A * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1)) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

A * (((1 / A) * (a `1)) - (P / A)) is V11() real ext-real Element of REAL

(A * (((1 / A) * (a `1)) - (P / A))) + P is V11() real ext-real Element of REAL

|[((A * (((1 / A) * (a `1)) - (P / A))) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

(A * (1 / A)) * (a `1) is V11() real ext-real Element of REAL

A * (P / A) is V11() real ext-real Element of REAL

((A * (1 / A)) * (a `1)) - (A * (P / A)) is V11() real ext-real Element of REAL

(((A * (1 / A)) * (a `1)) - (A * (P / A))) + P is V11() real ext-real Element of REAL

|[((((A * (1 / A)) * (a `1)) - (A * (P / A))) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

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

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

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

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

|[(((1 * (a `1)) - (1 * P)) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B * ((1 / B) * (a `2)) is V11() real ext-real Element of REAL

B * (p / B) is V11() real ext-real Element of REAL

(B * ((1 / B) * (a `2))) - (B * (p / B)) is V11() real ext-real Element of REAL

((B * ((1 / B) * (a `2))) - (B * (p / B))) + p is V11() real ext-real Element of REAL

|[(a `1),(((B * ((1 / B) * (a `2))) - (B * (p / B))) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)

B