:: JORDAN16 semantic presentation

REAL is non empty V38() V166() V167() V168() V172() set

NAT is V166() V167() V168() V169() V170() V171() V172() Element of K6(REAL)

K6(REAL) is set

K7(REAL,REAL) is set

K6(K7(REAL,REAL)) is set

NAT is V166() V167() V168() V169() V170() V171() V172() set

K6(NAT) is set

K230() is non empty strict TopSpace-like V111() TopStruct

the carrier of K230() is non empty V166() V167() V168() set

1 is non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() Element of NAT

K7(1,1) is set

K6(K7(1,1)) is set

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

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

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

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

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

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

2 is non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() Element of NAT

K7(2,2) is set

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

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

K258() is V97() V111() L7()

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

K6(NAT) is set

COMPLEX is non empty V38() V166() V172() set

RAT is non empty V38() V166() V167() V168() V169() V172() set

INT is non empty V38() V166() V167() V168() V169() V170() V172() set

TOP-REAL 2 is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() L15()

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

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

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

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

{} is empty Function-like functional V166() V167() V168() V169() V170() V171() V172() set

the carrier of R^1 is non empty V166() V167() V168() set

0 is empty V10() V11() V12() ext-real non positive non negative Function-like functional V118() V119() V166() V167() V168() V169() V170() V171() V172() Element of NAT

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

K7( the carrier of R^1, the carrier of R^1) is set

K6(K7( the carrier of R^1, the carrier of R^1)) is set

[.0,1.] is V166() V167() V168() Element of K6(REAL)

I[01] is non empty strict TopSpace-like V111() SubSpace of R^1

the carrier of I[01] is non empty V166() V167() V168() set

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

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

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

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

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

E-max P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

Segment (P,p1,p2,q1,q2) is Element of K6( the carrier of (TOP-REAL 2))

R_Segment (P,p1,p2,q1) is Element of K6( the carrier of (TOP-REAL 2))

L_Segment (P,p1,p2,q2) is Element of K6( the carrier of (TOP-REAL 2))

(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) is Element of K6( the carrier of (TOP-REAL 2))

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

L_Segment (P,p2,q1,p1) is Element of K6( the carrier of (TOP-REAL 2))

{ b

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

R_Segment (P,p2,q1,p1) is Element of K6( the carrier of (TOP-REAL 2))

{ b

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

Segment (P,q1,q2,p1,p2) is Element of K6( the carrier of (TOP-REAL 2))

R_Segment (P,q1,q2,p1) is Element of K6( the carrier of (TOP-REAL 2))

L_Segment (P,q1,q2,p2) is Element of K6( the carrier of (TOP-REAL 2))

(R_Segment (P,q1,q2,p1)) /\ (L_Segment (P,q1,q2,p2)) is Element of K6( the carrier of (TOP-REAL 2))

{ b

{ b

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

Segment (p1,p2,P) is Element of K6( the carrier of (TOP-REAL 2))

q2 is set

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

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

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

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

{ b

S is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

{ b

S is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

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

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

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

E-max P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

E-max P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p1 is non empty TopSpace-like TopStruct

P is non empty TopSpace-like TopStruct

the carrier of P is non empty set

the carrier of p1 is non empty set

K7( the carrier of P, the carrier of p1) is set

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

p2 is non empty TopSpace-like SubSpace of p1

the carrier of p2 is non empty set

K7( the carrier of P, the carrier of p2) is set

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

q1 is non empty Relation-like the carrier of P -defined the carrier of p1 -valued Function-like V29( the carrier of P) quasi_total Element of K6(K7( the carrier of P, the carrier of p1))

q2 is non empty Relation-like the carrier of P -defined the carrier of p2 -valued Function-like V29( the carrier of P) quasi_total Element of K6(K7( the carrier of P, the carrier of p2))

S is Element of the carrier of P

q2 . S is Element of the carrier of p2

S is a_neighborhood of q2 . S

K6( the carrier of p2) is set

c

[#] p2 is non empty non proper closed Element of K6( the carrier of p2)

[#] p1 is non empty non proper closed Element of K6( the carrier of p1)

K6( the carrier of p1) is set

S is Element of K6( the carrier of p1)

S /\ ([#] p2) is Element of K6( the carrier of p2)

A9 is Element of the carrier of p1

f is a_neighborhood of S

q1 .: f is Element of K6( the carrier of p1)

q2 .: f is Element of K6( the carrier of p2)

P is non empty TopSpace-like TopStruct

p1 is non empty TopSpace-like TopStruct

the carrier of P is non empty set

the carrier of p1 is non empty set

K7( the carrier of P, the carrier of p1) is set

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

p2 is non empty TopSpace-like SubSpace of P

the carrier of p2 is non empty set

q1 is non empty TopSpace-like SubSpace of p1

the carrier of q1 is non empty set

K7( the carrier of p2, the carrier of q1) is set

K6(K7( the carrier of p2, the carrier of q1)) is set

q2 is non empty Relation-like the carrier of P -defined the carrier of p1 -valued Function-like V29( the carrier of P) quasi_total Element of K6(K7( the carrier of P, the carrier of p1))

q2 | p2 is non empty Relation-like the carrier of p2 -defined the carrier of p1 -valued Function-like V29( the carrier of p2) quasi_total Element of K6(K7( the carrier of p2, the carrier of p1))

K7( the carrier of p2, the carrier of p1) is set

K6(K7( the carrier of p2, the carrier of p1)) is set

rng q2 is Element of K6( the carrier of p1)

K6( the carrier of p1) is set

[#] p1 is non empty non proper closed Element of K6( the carrier of p1)

q2 " is non empty Relation-like the carrier of p1 -defined the carrier of P -valued Function-like V29( the carrier of p1) quasi_total Element of K6(K7( the carrier of p1, the carrier of P))

K7( the carrier of p1, the carrier of P) is set

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

S is non empty Relation-like the carrier of p2 -defined the carrier of q1 -valued Function-like V29( the carrier of p2) quasi_total Element of K6(K7( the carrier of p2, the carrier of q1))

q2 | the carrier of p2 is Relation-like the carrier of P -defined the carrier of p1 -valued Function-like Element of K6(K7( the carrier of P, the carrier of p1))

q2 .: the carrier of p2 is Element of K6( the carrier of p1)

rng S is Element of K6( the carrier of q1)

K6( the carrier of q1) is set

dom S is Element of K6( the carrier of p2)

K6( the carrier of p2) is set

[#] p2 is non empty non proper closed Element of K6( the carrier of p2)

[#] q1 is non empty non proper closed Element of K6( the carrier of q1)

S " is non empty Relation-like the carrier of q1 -defined the carrier of p2 -valued Function-like V29( the carrier of q1) quasi_total Element of K6(K7( the carrier of q1, the carrier of p2))

K7( the carrier of q1, the carrier of p2) is set

K6(K7( the carrier of q1, the carrier of p2)) is set

q2 | the carrier of p2 is Relation-like Function-like set

(q2 | the carrier of p2) " is Relation-like Function-like set

q2 " is Relation-like Function-like set

(q2 ") | (q2 .: the carrier of p2) is Relation-like Function-like set

(q2 ") | the carrier of q1 is Relation-like the carrier of p1 -defined the carrier of P -valued Function-like Element of K6(K7( the carrier of p1, the carrier of P))

(q2 ") | q1 is non empty Relation-like the carrier of q1 -defined the carrier of P -valued Function-like V29( the carrier of q1) quasi_total Element of K6(K7( the carrier of q1, the carrier of P))

K7( the carrier of q1, the carrier of P) is set

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

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

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

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

p1 /\ p2 is Element of K6( the carrier of (TOP-REAL 2))

p1 \/ p2 is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (p1 \/ p2) is strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | (p1 \/ p2)) is set

[#] ((TOP-REAL 2) | (p1 \/ p2)) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2)))

K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2))) is set

S is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

c

{S,c

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

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

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

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

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

A9 . 0 is set

A9 . 1 is set

q2 is Element of K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2)))

p1 /\ (p1 \/ p2) is Element of K6( the carrier of (TOP-REAL 2))

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

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

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

Euclid 2 is non empty V97() V102() V103() V104() V105() L7()

the carrier of (Euclid 2) is non empty set

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

S is Element of K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2)))

p2 /\ (p1 \/ p2) is Element of K6( the carrier of (TOP-REAL 2))

dom A9 is V166() V167() V168() Element of K6( the carrier of I[01])

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

[#] I[01] is non empty non proper closed V166() V167() V168() Element of K6( the carrier of I[01])

f is set

g is set

A9 . g is set

m is V11() V12() ext-real Element of REAL

f is set

g is set

A9 . g is set

m is V11() V12() ext-real Element of REAL

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

A9 . f is set

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

A9 . f is set

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

A9 . g is set

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

A9 . g is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (p1 \/ p2))) is set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (p1 \/ p2)))) is set

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

q2 \/ S is Element of K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2)))

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

(Euclid 2) | S is non empty V97() V102() V103() V104() V105() SubSpace of Euclid 2

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

TopSpaceMetr ((Euclid 2) | S) is TopStruct

m is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (p1 \/ p2)) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (p1 \/ p2))))

q2 /\ S is Element of K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2)))

m is V11() V12() ext-real Element of REAL

m . m is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (p1 \/ p2))) is set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (p1 \/ p2)))) is set

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

q2 \/ S is Element of K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2)))

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

(Euclid 2) | S is non empty V97() V102() V103() V104() V105() SubSpace of Euclid 2

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

TopSpaceMetr ((Euclid 2) | S) is TopStruct

m is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (p1 \/ p2)) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (p1 \/ p2))))

q2 /\ S is Element of K6( the carrier of ((TOP-REAL 2) | (p1 \/ p2)))

m is V11() V12() ext-real Element of REAL

m . m is set

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

A9 . f is set

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

A9 . f is set

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

A9 . f is set

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

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

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

p1 \/ p2 is Element of K6( the carrier of (TOP-REAL 2))

p1 /\ p2 is Element of K6( the carrier of (TOP-REAL 2))

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

{q1,q2} is non empty set

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

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

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

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

c

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

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

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

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

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

S is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

{q2,S} is non empty set

S is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

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

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

p1 /\ p2 is Element of K6( the carrier of (TOP-REAL 2))

p1 \/ p2 is Element of K6( the carrier of (TOP-REAL 2))

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

{q1,q2} is non empty set

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

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

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

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p1 \/ p2 is Element of K6( the carrier of (TOP-REAL 2))

p1 /\ p2 is Element of K6( the carrier of (TOP-REAL 2))

{q1,q2} is non empty set

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

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

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

E-max P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

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

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

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

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

S . 0 is set

S . 1 is set

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

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

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

dom S is V166() V167() V168() Element of K6( the carrier of I[01])

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

S is set

S . S is set

[#] I[01] is non empty non proper closed V166() V167() V168() Element of K6( the carrier of I[01])

c

A9 is set

S . A9 is set

S . c

S is V11() V12() ext-real Element of REAL

S . S is set

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

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

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

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

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

S . 0 is set

S . 1 is set

S is V11() V12() ext-real Element of REAL

S . S is set

c

S . c

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

Segment (P,q1,q2,p1,p2) is Element of K6( the carrier of (TOP-REAL 2))

{ b

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

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

Segment (p1,(W-min P),P) is Element of K6( the carrier of (TOP-REAL 2))

{ b

P is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like V29( the carrier of R^1) quasi_total Element of K6(K7( the carrier of R^1, the carrier of R^1))

p1 is V11() V12() ext-real Element of REAL

p2 is V11() V12() ext-real Element of REAL

AffineMap (p1,p2) is non empty Relation-like REAL -defined REAL -valued Function-like V29( REAL ) quasi_total Element of K6(K7(REAL,REAL))

dom P is V166() V167() V168() Element of K6( the carrier of R^1)

K6( the carrier of R^1) is set

[#] R^1 is non empty non proper closed V166() V167() V168() Element of K6( the carrier of R^1)

rng P is V166() V167() V168() Element of K6( the carrier of R^1)

P " is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like V29( the carrier of R^1) quasi_total Element of K6(K7( the carrier of R^1, the carrier of R^1))

q1 is V11() V12() ext-real Element of REAL

P . q1 is set

p1 * q1 is V11() V12() ext-real Element of REAL

(p1 * q1) + p2 is V11() V12() ext-real Element of REAL

P " is Relation-like Function-like set

p1 " is V11() V12() ext-real Element of REAL

p2 / p1 is V11() V12() ext-real Element of REAL

- (p2 / p1) is V11() V12() ext-real Element of REAL

AffineMap ((p1 "),(- (p2 / p1))) is non empty Relation-like REAL -defined REAL -valued Function-like V29( REAL ) quasi_total Element of K6(K7(REAL,REAL))

q1 is V11() V12() ext-real Element of REAL

(P ") . q1 is set

(p1 ") * q1 is V11() V12() ext-real Element of REAL

((p1 ") * q1) + (- (p2 / p1)) is V11() V12() ext-real Element of REAL

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

Segment (P,p1,p2,q1,q2) is Element of K6( the carrier of (TOP-REAL 2))

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

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

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

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

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

S . 0 is set

S . 1 is set

S is V11() V12() ext-real Element of REAL

S . S is set

c

S . c

{ b

c

AffineMap ((c

S * (AffineMap ((c

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

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

(S * (AffineMap ((c

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

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

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

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

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

m is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like V29( the carrier of R^1) quasi_total Element of K6(K7( the carrier of R^1, the carrier of R^1))

m is V11() V12() ext-real Element of REAL

m . m is set

(c

((c

m is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like V29( the carrier of R^1) quasi_total continuous Element of K6(K7( the carrier of R^1, the carrier of R^1))

m | I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like V29( the carrier of I[01]) quasi_total continuous Element of K6(K7( the carrier of I[01], the carrier of R^1))

K7( the carrier of I[01], the carrier of R^1) is set

K6(K7( the carrier of I[01], the carrier of R^1)) is set

m | [.0,1.] is Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like Element of K6(K7( the carrier of R^1, the carrier of R^1))

rng (m | I[01]) is V166() V167() V168() Element of K6( the carrier of R^1)

K6( the carrier of R^1) is set

m .: [.0,1.] is V166() V167() V168() Element of K6( the carrier of R^1)

(c

[.S,((c

[.S,c

dom m is V166() V167() V168() Element of K6( the carrier of R^1)

dom (m | I[01]) is V166() V167() V168() Element of K6( the carrier of I[01])

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

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

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

h is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of I[01]))

g is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | A9) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | A9)))

g * h is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | A9) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | A9)))

dom g is V166() V167() V168() Element of K6( the carrier of I[01])

CIT is set

g * m is Relation-like the carrier of R^1 -defined the carrier of ((TOP-REAL 2) | A9) -valued Function-like Element of K6(K7( the carrier of R^1, the carrier of ((TOP-REAL 2) | A9)))

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

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

dom (g * m) is V166() V167() V168() Element of K6( the carrier of R^1)

dom ((S * (AffineMap ((c

[#] I[01] is non empty non proper closed V166() V167() V168() Element of K6( the carrier of I[01])

Closed-Interval-TSpace (S,c

CIT is non empty TopSpace-like V111() SubSpace of I[01]

the carrier of CIT is non empty V166() V167() V168() set

rng h is V166() V167() V168() Element of K6( the carrier of I[01])

(TOP-REAL 2) | (Segment (P,p1,p2,q1,q2)) is strict TopSpace-like SubSpace of TOP-REAL 2

[#] ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2))))

the carrier of ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2))) is set

K6( the carrier of ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2)))) is set

f is set

TS is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

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

rng g is Element of K6( the carrier of ((TOP-REAL 2) | A9))

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

o is set

g . o is set

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

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

(h - S) / (c

o is V11() V12() ext-real Element of REAL

((S * (AffineMap ((c

(c

S + 0 is V11() V12() ext-real Element of REAL

m . o is set

(c

((c

(h - S) + S is V11() V12() ext-real Element of REAL

(g * m) . o is set

TS is set

((S * (AffineMap ((c

o is V11() V12() ext-real Element of REAL

(AffineMap ((c

m . o is set

h . o is set

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

rng ((S * (AffineMap ((c

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

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

o is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

(g * m) . o is set

g . h is set

rng ((S * (AffineMap ((c

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

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2)))) is set

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

f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2))) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2)))))

f . 0 is set

f . 1 is set

(AffineMap ((c

g | CIT is non empty Relation-like the carrier of CIT -defined the carrier of ((TOP-REAL 2) | A9) -valued Function-like V29( the carrier of CIT) quasi_total Element of K6(K7( the carrier of CIT, the carrier of ((TOP-REAL 2) | A9)))

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

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

dom (g | CIT) is V166() V167() V168() Element of K6( the carrier of CIT)

K6( the carrier of CIT) is set

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

dom (g | the carrier of CIT) is V166() V167() V168() Element of K6( the carrier of I[01])

(dom g) /\ the carrier of CIT is V166() V167() V168() Element of K6( the carrier of I[01])

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

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

h is non empty Relation-like the carrier of I[01] -defined the carrier of CIT -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of CIT))

rng h is V166() V167() V168() Element of K6( the carrier of CIT)

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

(g | CIT) * h is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | A9) -valued Function-like V29( the carrier of I[01]) quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | A9)))

rng (g | CIT) is Element of K6( the carrier of ((TOP-REAL 2) | A9))

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

rng f is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p1,p2,q1,q2))))

TS is non empty TopSpace-like SubSpace of (TOP-REAL 2) | A9

the carrier of TS is non empty set

K7( the carrier of CIT, the carrier of TS) is set

K6(K7( the carrier of CIT, the carrier of TS)) is set

o is non empty Relation-like the carrier of CIT -defined the carrier of TS -valued Function-like V29( the carrier of CIT) quasi_total Element of K6(K7( the carrier of CIT, the carrier of TS))

dom (AffineMap ((c

(g * m) . 0 is set

(AffineMap ((c

(g * m) . 1 is set

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

W-min P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

E-max P is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

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

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

Segment (q2,p1,p2,(W-min P),(E-max P)) is Element of K6( the carrier of (TOP-REAL 2))

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

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

Segment (q2,p1,p2,(E-max P),(W-min P)) is Element of K6( the carrier of (TOP-REAL 2))

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

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

{p1,p2} is non empty set

Segment (P,p1,p2,q1,q2) is Element of K6( the carrier of (TOP-REAL 2))

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

{ b

c

c

Segment (P,p1,p2,q2,q1) is Element of K6( the carrier of (TOP-REAL 2))

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

{ b

c

c

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

p1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

p2 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

q1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)

Segment (P,p1,p2,p1,q1) is Element of K6( the carrier of (TOP-REAL 2))