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))
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : LE b1,p1,P,p2,q1 } is set
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))
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : LE p1,b1,P,p2,q1 } is set
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))
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : LE b1,p2,P,q1,q2 } is set
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : LE p1,b1,P,q1,q2 } is set
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)
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : ( LE p1,b1,P or ( p1 in P & b1 = W-min P ) ) } is set
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)
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : ( LE p1,b1,P & LE b1,p2,P ) } is set
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
c8 is Element of K6( the carrier of p2)
[#] 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)
c8 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)
{S,c8} is non empty set
(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))
c8 is non empty Element of K6( the carrier of (TOP-REAL 2))
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])
c8 is V11() V12() ext-real Element of REAL
A9 is set
S . A9 is set
S . c8 is set
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
c8 is V11() V12() ext-real Element of REAL
S . c8 is set
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))
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : ( LE p1,b1,P,q1,q2 & LE b1,p2,P,q1,q2 ) } 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)
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))
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : ( LE p1,b1,P or ( p1 in P & b1 = W-min P ) ) } is set
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
c8 is V11() V12() ext-real Element of REAL
S . c8 is set
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : ( LE q1,b1,P,p1,p2 & LE b1,q2,P,p1,p2 ) } is set
c8 - S is V11() V12() ext-real Element of REAL
AffineMap ((c8 - S),S) is non empty Relation-like REAL -defined REAL -valued Function-like V29( REAL ) quasi_total Element of K6(K7(REAL,REAL))
S * (AffineMap ((c8 - S),S)) is Relation-like REAL -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like Element of K6(K7(REAL, the carrier of ((TOP-REAL 2) | P)))
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 ((c8 - S),S))) | [.0,1.] is Relation-like REAL -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like Element of K6(K7(REAL, the carrier of ((TOP-REAL 2) | P)))
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
(c8 - S) * m is V11() V12() ext-real Element of REAL
((c8 - S) * m) + S is V11() V12() ext-real Element of REAL
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)
(c8 - S) + S is V11() V12() ext-real Element of REAL
[.S,((c8 - S) + S).] is V166() V167() V168() Element of K6(REAL)
[.S,c8.] is V166() V167() V168() Element of K6(REAL)
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 ((c8 - S),S))) | [.0,1.]) is V166() V167() V168() Element of K6(REAL)
[#] I[01] is non empty non proper closed V166() V167() V168() Element of K6( the carrier of I[01])
Closed-Interval-TSpace (S,c8) is non empty strict TopSpace-like V111() SubSpace of R^1
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) / (c8 - S) is V11() V12() ext-real Element of REAL
o is V11() V12() ext-real Element of REAL
((S * (AffineMap ((c8 - S),S))) | [.0,1.]) . o is set
(c8 - S) / (c8 - S) is V11() V12() ext-real Element of REAL
S + 0 is V11() V12() ext-real Element of REAL
m . o is set
(c8 - S) * o is V11() V12() ext-real Element of REAL
((c8 - S) * o) + S is V11() V12() ext-real Element of REAL
(h - S) + S is V11() V12() ext-real Element of REAL
(g * m) . o is set
TS is set
((S * (AffineMap ((c8 - S),S))) | [.0,1.]) . TS is set
o is V11() V12() ext-real Element of REAL
(AffineMap ((c8 - S),S)) . o is V11() V12() ext-real Element of REAL
m . o is set
h . o is set
h is V11() V12() ext-real Element of REAL
rng ((S * (AffineMap ((c8 - S),S))) | [.0,1.]) 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))
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 ((c8 - S),S))) | [.0,1.]) is Element of K6( the carrier of ((TOP-REAL 2) | P))
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 ((c8 - S),S)) . 0 is V11() V12() ext-real Element of REAL
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 ((c8 - S),S)) is V166() V167() V168() Element of K6(REAL)
(g * m) . 0 is set
(AffineMap ((c8 - S),S)) . 1 is V11() V12() ext-real Element of REAL
(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))
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : ( LE q1,b1,P,p1,p2 & LE b1,q2,P,p1,p2 ) } is set
c8 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)
c8 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)
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))
{ b1 where b1 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2) : ( LE q2,b1,P,p1,p2 & LE b1,q1,P,p1,p2 ) } is set
c8 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)
c8 is V45(2) V115() V158() Element of the carrier of (TOP-REAL 2)
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))