REAL is non empty V36() V142() V143() V144() V148() set
NAT is V142() V143() V144() V145() V146() V147() V148() Element of bool REAL
bool REAL is set
COMPLEX is non empty V36() V142() V148() set
omega is V142() V143() V144() V145() V146() V147() V148() set
bool omega is set
bool NAT is set
1 is non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
2 is non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
[:2,2:] is set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is set
RAT is non empty V36() V142() V143() V144() V145() V148() set
INT is non empty V36() V142() V143() V144() V145() V146() V148() set
bool [:REAL,REAL:] is set
TOP-REAL 2 is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty functional set
bool the carrier of (TOP-REAL 2) is set
[: the carrier of (TOP-REAL 2),REAL:] is set
bool [: the carrier of (TOP-REAL 2),REAL:] is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:COMPLEX,REAL:] is set
bool [:COMPLEX,REAL:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
{} is empty V142() V143() V144() V145() V146() V147() V148() set
the empty V142() V143() V144() V145() V146() V147() V148() set is empty V142() V143() V144() V145() V146() V147() V148() set
0 is empty natural V11() real ext-real non positive non negative V79() V80() V142() V143() V144() V145() V146() V147() V148() Element of NAT
proj1 is V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) Function-like V33( the carrier of (TOP-REAL 2), REAL ) Element of bool [: the carrier of (TOP-REAL 2),REAL:]
proj2 is V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) Function-like V33( the carrier of (TOP-REAL 2), REAL ) Element of bool [: the carrier of (TOP-REAL 2),REAL:]
dom proj1 is Element of bool the carrier of (TOP-REAL 2)
dom proj2 is Element of bool the carrier of (TOP-REAL 2)
C is V11() real ext-real set
p1 is V11() real ext-real set
C - p1 is V11() real ext-real set
(C - p1) ^2 is V11() real ext-real set
(C - p1) * (C - p1) is V11() real ext-real set
p1 - C is V11() real ext-real set
(p1 - C) ^2 is V11() real ext-real set
(p1 - C) * (p1 - C) is V11() real ext-real set
C is non empty TopStruct
the carrier of C is non empty set
p1 is non empty TopStruct
the carrier of p1 is non empty set
[: the carrier of C, the carrier of p1:] is set
bool [: the carrier of C, the carrier of p1:] is set
bool the carrier of p1 is set
p2 is V19() V22( the carrier of C) V23( the carrier of p1) Function-like V33( the carrier of C, the carrier of p1) Element of bool [: the carrier of C, the carrier of p1:]
q1 is Element of bool the carrier of p1
p2 " q1 is Element of bool the carrier of C
bool the carrier of C is set
rng p2 is Element of bool the carrier of p1
[#] p1 is non empty non proper Element of bool the carrier of p1
p2 " is V19() V22( the carrier of p1) V23( the carrier of C) Function-like V33( the carrier of p1, the carrier of C) Element of bool [: the carrier of p1, the carrier of C:]
[: the carrier of p1, the carrier of C:] is set
bool [: the carrier of p1, the carrier of C:] is set
rng (p2 ") is Element of bool the carrier of C
[#] C is non empty non proper Element of bool the carrier of C
(p2 ") .: q1 is Element of bool the carrier of C
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj2 .: (north_halfline C) is V142() V143() V144() Element of bool REAL
C `2 is V11() real ext-real Element of REAL
p1 is ext-real set
p2 is set
proj2 . p2 is set
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 `2 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj2 .: (south_halfline C) is V142() V143() V144() Element of bool REAL
C `2 is V11() real ext-real Element of REAL
p1 is ext-real set
p2 is set
proj2 . p2 is set
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 `2 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
west_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj1 .: (west_halfline C) is V142() V143() V144() Element of bool REAL
C `1 is V11() real ext-real Element of REAL
p1 is ext-real set
p2 is set
proj1 . p2 is set
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 `1 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
east_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj1 .: (east_halfline C) is V142() V143() V144() Element of bool REAL
C `1 is V11() real ext-real Element of REAL
p1 is ext-real set
p2 is set
proj1 . p2 is set
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 `1 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj2 .: (north_halfline C) is V142() V143() V144() Element of bool REAL
south_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj2 .: (south_halfline C) is V142() V143() V144() Element of bool REAL
west_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj1 .: (west_halfline C) is V142() V143() V144() Element of bool REAL
east_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj1 .: (east_halfline C) is V142() V143() V144() Element of bool REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj2 .: (north_halfline C) is non empty V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (north_halfline C)) is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real set
q1 is set
proj2 . q1 is set
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 `2 is V11() real ext-real Element of REAL
q1 is V11() real ext-real set
(C `2) + q1 is V11() real ext-real set
p2 is V11() real ext-real set
p2 + 0 is V11() real ext-real set
q2 is V11() real ext-real set
proj2 . C is set
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj2 .: (south_halfline C) is non empty V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (south_halfline C)) is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real set
q1 is set
proj2 . q1 is set
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 `2 is V11() real ext-real Element of REAL
q1 is V11() real ext-real set
p2 is V11() real ext-real set
p2 - 0 is V11() real ext-real set
(C `2) - q1 is V11() real ext-real set
q2 is V11() real ext-real set
proj2 . C is set
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
west_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj1 .: (west_halfline C) is non empty V142() V143() V144() Element of bool REAL
upper_bound (proj1 .: (west_halfline C)) is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
p2 is V11() real ext-real set
q1 is set
proj1 . q1 is set
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 `1 is V11() real ext-real Element of REAL
q1 is V11() real ext-real set
p2 is V11() real ext-real set
p2 - 0 is V11() real ext-real set
(C `1) - q1 is V11() real ext-real set
q2 is V11() real ext-real set
proj1 . C is set
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
east_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
proj1 .: (east_halfline C) is non empty V142() V143() V144() Element of bool REAL
lower_bound (proj1 .: (east_halfline C)) is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
p2 is V11() real ext-real set
q1 is set
proj1 . q1 is set
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 `1 is V11() real ext-real Element of REAL
q1 is V11() real ext-real set
(C `1) + q1 is V11() real ext-real set
p2 is V11() real ext-real set
p2 + 0 is V11() real ext-real set
q2 is V11() real ext-real set
proj1 . C is set
the topology of (TOP-REAL 2) is open Element of bool (bool the carrier of (TOP-REAL 2))
bool (bool the carrier of (TOP-REAL 2)) is set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is strict TopStruct
Euclid 2 is non empty strict Reflexive discerning V91() triangle MetrStruct
TopSpaceMetr (Euclid 2) is TopStruct
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
(north_halfline C) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (north_halfline C) is set
the carrier of (TopSpaceMetr (Euclid 2)) is set
bool the carrier of (TopSpaceMetr (Euclid 2)) is set
p2 is Element of bool the carrier of (TOP-REAL 2)
the carrier of (Euclid 2) is non empty set
q2 is Element of the carrier of (Euclid 2)
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
(P `1) - (C `1) is V11() real ext-real set
abs ((P `1) - (C `1)) is V11() real ext-real Element of REAL
P1 is V11() real ext-real Element of REAL
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(P `1) - (c `1) is V11() real ext-real set
abs ((P `1) - (c `1)) is V11() real ext-real Element of REAL
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
P `2 is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(P `2) - (c `2) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(abs ((P `1) - (c `1))) ^2 is V11() real ext-real Element of REAL
(abs ((P `1) - (c `1))) * (abs ((P `1) - (c `1))) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + 0 is V11() real ext-real set
C `2 is V11() real ext-real Element of REAL
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
(C `2) - (P `2) is V11() real ext-real set
P1 is V11() real ext-real set
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(c `2) - (P `2) is V11() real ext-real set
((C `2) - (P `2)) ^2 is V11() real ext-real set
((C `2) - (P `2)) * ((C `2) - (P `2)) is V11() real ext-real set
((c `2) - (P `2)) ^2 is V11() real ext-real set
((c `2) - (P `2)) * ((c `2) - (P `2)) is V11() real ext-real set
P `1 is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(P `1) - (c `1) is V11() real ext-real set
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
(P `2) - (c `2) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
0 + (((P `2) - (c `2)) ^2) is V11() real ext-real set
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
P `2 is V11() real ext-real Element of REAL
q1 is Element of bool the carrier of (TopSpaceMetr (Euclid 2))
p2 ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ p2 is set
south_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
(south_halfline C) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (south_halfline C) is set
the carrier of (TopSpaceMetr (Euclid 2)) is set
bool the carrier of (TopSpaceMetr (Euclid 2)) is set
p2 is Element of bool the carrier of (TOP-REAL 2)
the carrier of (Euclid 2) is non empty set
q2 is Element of the carrier of (Euclid 2)
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
(P `1) - (C `1) is V11() real ext-real set
abs ((P `1) - (C `1)) is V11() real ext-real Element of REAL
P1 is V11() real ext-real Element of REAL
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(P `1) - (c `1) is V11() real ext-real set
abs ((P `1) - (c `1)) is V11() real ext-real Element of REAL
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
P `2 is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(P `2) - (c `2) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(abs ((P `1) - (c `1))) ^2 is V11() real ext-real Element of REAL
(abs ((P `1) - (c `1))) * (abs ((P `1) - (c `1))) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + 0 is V11() real ext-real set
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
(P `2) - (C `2) is V11() real ext-real set
P1 is V11() real ext-real set
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(P `2) - (c `2) is V11() real ext-real set
((P `2) - (C `2)) ^2 is V11() real ext-real set
((P `2) - (C `2)) * ((P `2) - (C `2)) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
P `1 is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(P `1) - (c `1) is V11() real ext-real set
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
0 + (((P `2) - (c `2)) ^2) is V11() real ext-real set
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
P `2 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
q1 is Element of bool the carrier of (TopSpaceMetr (Euclid 2))
p2 ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ p2 is set
east_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
(east_halfline C) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (east_halfline C) is set
the carrier of (TopSpaceMetr (Euclid 2)) is set
bool the carrier of (TopSpaceMetr (Euclid 2)) is set
p2 is Element of bool the carrier of (TOP-REAL 2)
the carrier of (Euclid 2) is non empty set
q2 is Element of the carrier of (Euclid 2)
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
(P `2) - (C `2) is V11() real ext-real set
abs ((P `2) - (C `2)) is V11() real ext-real Element of REAL
P1 is V11() real ext-real Element of REAL
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(P `2) - (c `2) is V11() real ext-real set
abs ((P `2) - (c `2)) is V11() real ext-real Element of REAL
P `1 is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(P `1) - (c `1) is V11() real ext-real set
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(abs ((P `2) - (c `2))) ^2 is V11() real ext-real Element of REAL
(abs ((P `2) - (c `2))) * (abs ((P `2) - (c `2))) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
(((P `2) - (c `2)) ^2) + 0 is V11() real ext-real set
C `1 is V11() real ext-real Element of REAL
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
(C `1) - (P `1) is V11() real ext-real set
P1 is V11() real ext-real set
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(c `1) - (P `1) is V11() real ext-real set
((C `1) - (P `1)) ^2 is V11() real ext-real set
((C `1) - (P `1)) * ((C `1) - (P `1)) is V11() real ext-real set
((c `1) - (P `1)) ^2 is V11() real ext-real set
((c `1) - (P `1)) * ((c `1) - (P `1)) is V11() real ext-real set
P `2 is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(P `2) - (c `2) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
(P `1) - (c `1) is V11() real ext-real set
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + 0 is V11() real ext-real set
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
P `1 is V11() real ext-real Element of REAL
q1 is Element of bool the carrier of (TopSpaceMetr (Euclid 2))
p2 ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ p2 is set
west_halfline C is non empty Element of bool the carrier of (TOP-REAL 2)
(west_halfline C) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (west_halfline C) is set
the carrier of (TopSpaceMetr (Euclid 2)) is set
bool the carrier of (TopSpaceMetr (Euclid 2)) is set
p2 is Element of bool the carrier of (TOP-REAL 2)
the carrier of (Euclid 2) is non empty set
q2 is Element of the carrier of (Euclid 2)
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
(P `2) - (C `2) is V11() real ext-real set
abs ((P `2) - (C `2)) is V11() real ext-real Element of REAL
P1 is V11() real ext-real Element of REAL
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(P `2) - (c `2) is V11() real ext-real set
abs ((P `2) - (c `2)) is V11() real ext-real Element of REAL
P `1 is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(P `1) - (c `1) is V11() real ext-real set
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(abs ((P `2) - (c `2))) ^2 is V11() real ext-real Element of REAL
(abs ((P `2) - (c `2))) * (abs ((P `2) - (c `2))) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
(((P `2) - (c `2)) ^2) + 0 is V11() real ext-real set
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
(P `1) - (C `1) is V11() real ext-real set
P1 is V11() real ext-real set
Ball (q2,P1) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
A is set
c9 is Element of the carrier of (Euclid 2)
dist (q2,c9) is V11() real ext-real Element of REAL
c is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
dist (P,c) is V11() real ext-real Element of REAL
c `1 is V11() real ext-real Element of REAL
(P `1) - (c `1) is V11() real ext-real set
((P `1) - (C `1)) ^2 is V11() real ext-real set
((P `1) - (C `1)) * ((P `1) - (C `1)) is V11() real ext-real set
((P `1) - (c `1)) ^2 is V11() real ext-real set
((P `1) - (c `1)) * ((P `1) - (c `1)) is V11() real ext-real set
P `2 is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
(P `2) - (c `2) is V11() real ext-real set
((P `2) - (c `2)) ^2 is V11() real ext-real set
((P `2) - (c `2)) * ((P `2) - (c `2)) is V11() real ext-real set
(((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2) is V11() real ext-real set
sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2)) is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) ^2 is V11() real ext-real set
(sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) * (sqrt ((((P `1) - (c `1)) ^2) + (((P `2) - (c `2)) ^2))) is V11() real ext-real set
0 + (((P `1) - (c `1)) ^2) is V11() real ext-real set
P is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P `2 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
P `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
q1 is Element of bool the carrier of (TopSpaceMetr (Euclid 2))
p2 ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ p2 is set
C is Element of bool the carrier of (TOP-REAL 2)
BDD C is Element of bool the carrier of (TOP-REAL 2)
UBD C is Element of bool the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline p1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
C is Element of bool the carrier of (TOP-REAL 2)
BDD C is Element of bool the carrier of (TOP-REAL 2)
UBD C is Element of bool the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline p1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
C is Element of bool the carrier of (TOP-REAL 2)
BDD C is Element of bool the carrier of (TOP-REAL 2)
UBD C is Element of bool the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
east_halfline p1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
C is Element of bool the carrier of (TOP-REAL 2)
BDD C is Element of bool the carrier of (TOP-REAL 2)
UBD C is Element of bool the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
west_halfline p1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
C is being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
p2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
{p2,q1} is non empty set
q2 is non empty Element of bool the carrier of (TOP-REAL 2)
P is non empty Element of bool the carrier of (TOP-REAL 2)
q2 \/ P is non empty Element of bool the carrier of (TOP-REAL 2)
q2 /\ P is Element of bool the carrier of (TOP-REAL 2)
P1 is non empty Element of bool the carrier of (TOP-REAL 2)
A is non empty Element of bool the carrier of (TOP-REAL 2)
c9 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 \/ A is non empty Element of bool the carrier of (TOP-REAL 2)
p1 /\ A is Element of bool the carrier of (TOP-REAL 2)
p1 \/ P1 is non empty Element of bool the carrier of (TOP-REAL 2)
p1 /\ P1 is Element of bool the carrier of (TOP-REAL 2)
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
p1 is Element of bool the carrier of (TOP-REAL 2)
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (north_halfline C) is Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p1 /\ (north_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(lower_bound (proj2 .: (p1 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (south_halfline C) is Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p1 /\ (south_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p1 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C is Element of bool the carrier of (TOP-REAL 2)
(p1,C) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 `1 is V11() real ext-real Element of REAL
north_halfline p1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
C /\ (north_halfline p1) is Element of bool the carrier of (TOP-REAL 2)
proj2 .: (C /\ (north_halfline p1)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (C /\ (north_halfline p1))) is V11() real ext-real Element of REAL
|[(p1 `1),(lower_bound (proj2 .: (C /\ (north_halfline p1))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(p1,C) `1 is V11() real ext-real Element of REAL
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 is Element of bool the carrier of (TOP-REAL 2)
(q1,p2) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 `1 is V11() real ext-real Element of REAL
south_halfline q1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
p2 /\ (south_halfline q1) is Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p2 /\ (south_halfline q1)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p2 /\ (south_halfline q1))) is V11() real ext-real Element of REAL
|[(q1 `1),(upper_bound (proj2 .: (p2 /\ (south_halfline q1))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(q1,p2) `1 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
BDD p1 is open Element of bool the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
p1 /\ (north_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p1 /\ (north_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(lower_bound (proj2 .: (p1 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 /\ (south_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p1 /\ (south_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p1 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
UBD p1 is non empty open Element of bool the carrier of (TOP-REAL 2)
q1 is set
proj2 . q1 is set
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 `2 is V11() real ext-real Element of REAL
(C,p1) `2 is V11() real ext-real Element of REAL
q2 `1 is V11() real ext-real Element of REAL
(C,p1) `1 is V11() real ext-real Element of REAL
P1 is set
proj2 . P1 is set
A is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
A `1 is V11() real ext-real Element of REAL
(C,p1) `1 is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
(C,p1) `2 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
p1 is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
BDD p1 is open Element of bool the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (south_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p1 /\ (south_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p1 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) `2 is V11() real ext-real Element of REAL
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (north_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p1 /\ (north_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(lower_bound (proj2 .: (p1 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) `2 is V11() real ext-real Element of REAL
(C,p1) `1 is V11() real ext-real Element of REAL
proj2 .: (south_halfline C) is non empty V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (south_halfline C)) is V11() real ext-real Element of REAL
(C,p1) `1 is V11() real ext-real Element of REAL
proj2 .: (north_halfline C) is non empty V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (north_halfline C)) is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
BDD p1 is open Element of bool the carrier of (TOP-REAL 2)
p1 /\ (north_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p1 /\ (north_halfline C))) is V11() real ext-real Element of REAL
p1 /\ (south_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p1 /\ (south_halfline C))) is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p1 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) `2 is V11() real ext-real Element of REAL
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
|[(C `1),(lower_bound (proj2 .: (p1 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) `2 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
BDD p1 is open Element of bool the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (south_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p1 /\ (south_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p1 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (north_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p1 /\ (north_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(lower_bound (proj2 .: (p1 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) `2 is V11() real ext-real Element of REAL
(C,p1) `2 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (north_halfline C) is Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p1 /\ (north_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(lower_bound (proj2 .: (p1 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (south_halfline C) is Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p1 /\ (south_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p1 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
LSeg ((C,p1),(C,p1)) is Element of bool the carrier of (TOP-REAL 2)
(C,p1) `1 is V11() real ext-real Element of REAL
(C,p1) `1 is V11() real ext-real Element of REAL
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
BDD p1 is open Element of bool the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (north_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p1 /\ (north_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(lower_bound (proj2 .: (p1 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p1) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p1 /\ (south_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p1 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p1 /\ (south_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p1 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
LSeg ((C,p1),(C,p1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((C,p1),(C,p1))) /\ p1 is Element of bool the carrier of (TOP-REAL 2)
{(C,p1),(C,p1)} is non empty set
(C,p1) `2 is V11() real ext-real Element of REAL
(C,p1) `2 is V11() real ext-real Element of REAL
(C,p1) `1 is V11() real ext-real Element of REAL
q1 is set
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 `1 is V11() real ext-real Element of REAL
(C,p1) `1 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
q2 `2 is V11() real ext-real Element of REAL
proj2 . q2 is set
q1 is set
C is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 `1 is V11() real ext-real Element of REAL
p2 is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
BDD p2 is open Element of bool the carrier of (TOP-REAL 2)
(C,p2) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p2 /\ (north_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p2 /\ (north_halfline C)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p2 /\ (north_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(lower_bound (proj2 .: (p2 /\ (north_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(p1,p2) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline p1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
p2 /\ (south_halfline p1) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p2 /\ (south_halfline p1)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p2 /\ (south_halfline p1))) is V11() real ext-real Element of REAL
|[(p1 `1),(upper_bound (proj2 .: (p2 /\ (south_halfline p1))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(p1,p2) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
north_halfline p1 is non empty closed Element of bool the carrier of (TOP-REAL 2)
p2 /\ (north_halfline p1) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p2 /\ (north_halfline p1)) is V142() V143() V144() Element of bool REAL
lower_bound (proj2 .: (p2 /\ (north_halfline p1))) is V11() real ext-real Element of REAL
|[(p1 `1),(lower_bound (proj2 .: (p2 /\ (north_halfline p1))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p2) is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
south_halfline C is non empty closed Element of bool the carrier of (TOP-REAL 2)
p2 /\ (south_halfline C) is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: (p2 /\ (south_halfline C)) is V142() V143() V144() Element of bool REAL
upper_bound (proj2 .: (p2 /\ (south_halfline C))) is V11() real ext-real Element of REAL
|[(C `1),(upper_bound (proj2 .: (p2 /\ (south_halfline C))))]| is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
(C,p2) `1 is V11() real ext-real Element of REAL
(C,p2) `1 is V11() real ext-real Element of REAL
(p1,p2) `2 is V11() real ext-real Element of REAL
(p1,p2) `2 is V11() real ext-real Element of REAL
(C,p2) `2 is V11() real ext-real Element of REAL
(C,p2) `2 is V11() real ext-real Element of REAL
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
p1 is Element of bool the carrier of (TOP-REAL C)
p2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q1 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
{q1,q2} is non empty set
P is Element of bool the carrier of (TOP-REAL C)
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
p1 is Element of bool the carrier of (TOP-REAL C)
p2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q1 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
P is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
{q2,P} is non empty set
P1 is Element of bool the carrier of (TOP-REAL C)
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
p1 is Element of bool the carrier of (TOP-REAL C)
p2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q1 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
P is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
{q2,P} is non empty set
P1 is Element of bool the carrier of (TOP-REAL C)
{P,q2} is non empty set
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
p1 is Element of bool the carrier of (TOP-REAL C)
p2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q1 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
P is Element of bool the carrier of (TOP-REAL C)
{p2,q2} is non empty set
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
p1 is Element of bool the carrier of (TOP-REAL C)
p2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q1 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
P is Element of bool the carrier of (TOP-REAL C)
{q2,q1} is non empty set
{q1,q2} is non empty set
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
p1 is Element of bool the carrier of (TOP-REAL C)
p2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q1 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
P is Element of bool the carrier of (TOP-REAL C)
{q1,q2} is non empty set
C is natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
TOP-REAL C is non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
bool the carrier of (TOP-REAL C) is set
p1 is Element of bool the carrier of (TOP-REAL C)
p2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q1 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
q2 is V43(C) V76() V134() Element of the carrier of (TOP-REAL C)
P is Element of bool the carrier of (TOP-REAL C)
{q2,p2} is non empty set
{p2,q2} is non empty set
C is being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
{p1,p2} is non empty set
q2 is non empty Element of bool the carrier of (TOP-REAL 2)
P is non empty Element of bool the carrier of (TOP-REAL 2)
q2 \/ P is non empty Element of bool the carrier of (TOP-REAL 2)
q2 /\ P is Element of bool the carrier of (TOP-REAL 2)
{q1,q1} is non empty set
{q1,q1} is non empty set
C is being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
P is Element of bool the carrier of (TOP-REAL 2)
{p1,p2} is non empty set
{q1,q2} is non empty set
P1 is non empty Element of bool the carrier of (TOP-REAL 2)
P \/ P1 is non empty Element of bool the carrier of (TOP-REAL 2)
P /\ P1 is Element of bool the carrier of (TOP-REAL 2)
A is non empty Element of bool the carrier of (TOP-REAL 2)
C is being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
p1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
q2 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
{p1,p2} is non empty set
P is non empty Element of bool the carrier of (TOP-REAL 2)
P1 is non empty Element of bool the carrier of (TOP-REAL 2)
P \/ P1 is non empty Element of bool the carrier of (TOP-REAL 2)
P /\ P1 is Element of bool the carrier of (TOP-REAL 2)
{q1,q2} is non empty set
Segment (P,p1,p2,p1,q1) is Element of bool the carrier of (TOP-REAL 2)
A is Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : ( LE p1,b1,P,p1,p2 & LE b1,q1,P,p1,p2 ) } is set
c9 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
{p2,q2} is non empty set
A is Element of bool the carrier of (TOP-REAL 2)
Segment (P1,p1,p2,p1,q1) is Element of bool the carrier of (TOP-REAL 2)
A is Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2) : ( LE p1,b1,P1,p1,p2 & LE b1,q1,P1,p1,p2 ) } is set
c9 is V43(2) V76() V134() Element of the carrier of (TOP-REAL 2)
{p2,q2} is non empty set
A is Element of bool the carrier of (TOP-REAL 2)