:: JORDAN18 semantic presentation

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

c

dist (q2,c

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

c

dist (q2,c

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

c

dist (q2,c

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

c

dist (q2,c

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

c

dist (q2,c

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

c

dist (q2,c

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

c

dist (q2,c

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

c

dist (q2,c

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)

c

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)

{ b

c

{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)

{ b

c

{p2,q2} is non empty set

A is Element of bool the carrier of (TOP-REAL 2)