:: JORDAN_A semantic presentation

REAL is non empty non trivial non finite V147() V148() V149() V153() V181() non bounded_below non bounded_above interval set

NAT is non empty epsilon-transitive epsilon-connected ordinal V147() V148() V149() V150() V151() V152() V153() V181() left_end bounded_below Element of bool REAL

bool REAL is non empty set

COMPLEX is non empty non trivial non finite V147() V153() set

omega is non empty epsilon-transitive epsilon-connected ordinal V147() V148() V149() V150() V151() V152() V153() V181() left_end bounded_below set

bool omega is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V19() V100() V147() V148() V149() V150() V151() V152() left_end bounded_below Element of NAT

[:1,1:] is non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty set

bool [:[:1,1:],1:] is non empty set

[:[:1,1:],REAL:] is non empty set

bool [:[:1,1:],REAL:] is non empty set

[:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty set

bool [:[:REAL,REAL:],REAL:] is non empty set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V19() V100() V147() V148() V149() V150() V151() V152() left_end bounded_below Element of NAT

[:2,2:] is non empty set

[:[:2,2:],REAL:] is non empty set

bool [:[:2,2:],REAL:] is non empty set

bool NAT is non empty set

RAT is non empty non trivial non finite V147() V148() V149() V150() V153() set

INT is non empty non trivial non finite V147() V148() V149() V150() V151() V153() set

bool [:REAL,REAL:] is non empty set

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V113() V159() V160() V161() V162() V163() V164() V165() V171() L15()

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

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

ExtREAL is non empty V148() interval set

K496() is non empty strict TopSpace-like V211() TopStruct

the carrier of K496() is non empty V147() V148() V149() set

RealSpace is strict V211() MetrStruct

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V211() TopStruct

the carrier of R^1 is non empty V147() V148() V149() set

[:COMPLEX,COMPLEX:] is non empty set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is non empty set

bool [:COMPLEX,REAL:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:RAT,RAT:] is non empty set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is non empty set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is non empty set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is non empty set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty set

[:[:NAT,NAT:],NAT:] is non empty set

bool [:[:NAT,NAT:],NAT:] is non empty set

[: the carrier of (TOP-REAL 2),REAL:] is non empty set

bool [: the carrier of (TOP-REAL 2),REAL:] is non empty set

{} is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real Function-like functional finite V42() FinSequence-membered V147() V148() V149() V150() V151() V152() V153() bounded_below bounded_above real-bounded interval set

the empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real Function-like functional finite V42() FinSequence-membered V147() V148() V149() V150() V151() V152() V153() bounded_below bounded_above real-bounded interval set is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real Function-like functional finite V42() FinSequence-membered V147() V148() V149() V150() V151() V152() V153() bounded_below bounded_above real-bounded interval set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V19() V100() V147() V148() V149() V150() V151() V152() left_end bounded_below Element of NAT

0 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real V19() Function-like functional finite V42() FinSequence-membered V100() V147() V148() V149() V150() V151() V152() V153() bounded_below bounded_above real-bounded interval Element of NAT

8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V19() V100() V147() V148() V149() V150() V151() V152() left_end bounded_below Element of NAT

Euclid 2 is non empty strict Reflexive discerning V86() triangle MetrStruct

REAL 2 is non empty functional FinSequence-membered M12( REAL )

K326(2,REAL) is functional FinSequence-membered M12( REAL )

Pitag_dist 2 is V21() V24([:(REAL 2),(REAL 2):]) V25( REAL ) Function-like V35([:(REAL 2),(REAL 2):], REAL ) Element of bool [:[:(REAL 2),(REAL 2):],REAL:]

[:(REAL 2),(REAL 2):] is non empty set

[:[:(REAL 2),(REAL 2):],REAL:] is non empty set

bool [:[:(REAL 2),(REAL 2):],REAL:] is non empty set

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

the carrier of (Euclid 2) is non empty set

bool the carrier of (Euclid 2) is non empty set

K503() is non empty strict TopSpace-like T_0 T_1 T_2 V211() SubSpace of R^1

the carrier of K503() is non empty V147() V148() V149() set

bool the carrier of R^1 is non empty set

len {} is V43() set

C is non empty TopSpace-like TopStruct

the carrier of C is non empty set

[: the carrier of C,REAL:] is non empty set

bool [: the carrier of C,REAL:] is non empty set

bool the carrier of C is non empty set

S is V21() V24( the carrier of C) V25( REAL ) Function-like V35( the carrier of C, REAL ) continuous Element of bool [: the carrier of C,REAL:]

F is compact Element of bool the carrier of C

S .: F is V147() V148() V149() Element of bool REAL

[: the carrier of C, the carrier of R^1:] is non empty set

bool [: the carrier of C, the carrier of R^1:] is non empty set

S2 is V21() V24( the carrier of C) V25( the carrier of R^1) Function-like V35( the carrier of C, the carrier of R^1) continuous Element of bool [: the carrier of C, the carrier of R^1:]

S2 .: F is V147() V148() V149() Element of bool the carrier of R^1

[#] (S2 .: F) is V147() V148() V149() Element of bool REAL

C is compact closed V147() V148() V149() Element of bool REAL

S is non empty V147() V148() V149() Element of bool REAL

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

Cl S is non empty closed V147() V148() V149() Element of bool REAL

lower_bound (Cl S) is V11() real ext-real Element of REAL

C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V113() V159() V160() V161() V162() V163() V164() V165() V171() L15()

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

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

[:(TOP-REAL C),(TOP-REAL C):] is non empty strict TopSpace-like TopStruct

the carrier of [:(TOP-REAL C),(TOP-REAL C):] is non empty set

[: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

[: the carrier of (TOP-REAL C),REAL:] is non empty set

bool [: the carrier of (TOP-REAL C),REAL:] is non empty set

F is non empty functional closed compact Element of bool the carrier of (TOP-REAL C)

S is non empty functional closed compact Element of bool the carrier of (TOP-REAL C)

[:S,F:] is non empty Element of bool the carrier of [:(TOP-REAL C),(TOP-REAL C):]

bool the carrier of [:(TOP-REAL C),(TOP-REAL C):] is non empty set

S2 is V21() V24( the carrier of [:(TOP-REAL C),(TOP-REAL C):]) V25( REAL ) Function-like V35( the carrier of [:(TOP-REAL C),(TOP-REAL C):], REAL ) continuous Element of bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:]

S2 .: [:S,F:] is non empty V147() V148() V149() Element of bool REAL

lower_bound (S2 .: [:S,F:]) is V11() real ext-real Element of REAL

F is V21() V24( the carrier of (TOP-REAL C)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL C), REAL ) Element of bool [: the carrier of (TOP-REAL C),REAL:]

F .: S is non empty V147() V148() V149() Element of bool REAL

lower_bound (F .: S) is V11() real ext-real Element of REAL

X is set

e is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

F . e is V11() real ext-real Element of REAL

i is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

{ (S2 . (e,b

j is V147() V148() V149() Element of bool REAL

lower_bound j is V11() real ext-real Element of REAL

S2 . (e,i) is set

[e,i] is non empty set

{e,i} is non empty functional finite V42() set

{e} is non empty trivial functional finite V42() set

{{e,i},{e}} is non empty finite V42() set

S2 . [e,i] is set

S2 is set

mm is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S2 . (e,mm) is set

[e,mm] is non empty set

{e,mm} is non empty functional finite V42() set

{{e,mm},{e}} is non empty finite V42() set

S2 . [e,mm] is set

[e,mm] is non empty Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

X is V11() real ext-real set

e is Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

S2 . e is V11() real ext-real Element of REAL

[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):] is non empty set

i is set

j is set

[i,j] is non empty set

{i,j} is non empty finite set

{i} is non empty trivial finite set

{{i,j},{i}} is non empty finite V42() set

S2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

{ (S2 . (S2,b

F . S2 is V11() real ext-real Element of REAL

c

lower_bound c

q2 is set

U is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S2 . (S2,U) is set

[S2,U] is non empty set

{S2,U} is non empty functional finite V42() set

{S2} is non empty trivial functional finite V42() set

{{S2,U},{S2}} is non empty finite V42() set

S2 . [S2,U] is set

[S2,U] is non empty Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

mm is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S2 . (S2,mm) is set

[S2,mm] is non empty set

{S2,mm} is non empty functional finite V42() set

{S2} is non empty trivial functional finite V42() set

{{S2,mm},{S2}} is non empty finite V42() set

S2 . [S2,mm] is set

X is V11() real ext-real set

(lower_bound (F .: S)) + X is V11() real ext-real Element of REAL

e is V11() real ext-real set

C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V113() V159() V160() V161() V162() V163() V164() V165() V171() L15()

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

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

[:(TOP-REAL C),(TOP-REAL C):] is non empty strict TopSpace-like TopStruct

the carrier of [:(TOP-REAL C),(TOP-REAL C):] is non empty set

[: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

[: the carrier of (TOP-REAL C),REAL:] is non empty set

bool [: the carrier of (TOP-REAL C),REAL:] is non empty set

S is non empty functional closed compact Element of bool the carrier of (TOP-REAL C)

F is non empty functional closed compact Element of bool the carrier of (TOP-REAL C)

[:S,F:] is non empty Element of bool the carrier of [:(TOP-REAL C),(TOP-REAL C):]

bool the carrier of [:(TOP-REAL C),(TOP-REAL C):] is non empty set

S2 is V21() V24( the carrier of [:(TOP-REAL C),(TOP-REAL C):]) V25( REAL ) Function-like V35( the carrier of [:(TOP-REAL C),(TOP-REAL C):], REAL ) continuous Element of bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:]

S2 .: [:S,F:] is non empty V147() V148() V149() Element of bool REAL

lower_bound (S2 .: [:S,F:]) is V11() real ext-real Element of REAL

F is V21() V24( the carrier of (TOP-REAL C)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL C), REAL ) Element of bool [: the carrier of (TOP-REAL C),REAL:]

F .: F is non empty V147() V148() V149() Element of bool REAL

lower_bound (F .: F) is V11() real ext-real Element of REAL

X is set

e is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

F . e is V11() real ext-real Element of REAL

i is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

{ (S2 . (b

j is V147() V148() V149() Element of bool REAL

lower_bound j is V11() real ext-real Element of REAL

S2 . (i,e) is set

[i,e] is non empty set

{i,e} is non empty functional finite V42() set

{i} is non empty trivial functional finite V42() set

{{i,e},{i}} is non empty finite V42() set

S2 . [i,e] is set

S2 is set

mm is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S2 . (mm,e) is set

[mm,e] is non empty set

{mm,e} is non empty functional finite V42() set

{mm} is non empty trivial functional finite V42() set

{{mm,e},{mm}} is non empty finite V42() set

S2 . [mm,e] is set

[mm,e] is non empty Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

X is V11() real ext-real set

e is Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

S2 . e is V11() real ext-real Element of REAL

[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):] is non empty set

i is set

j is set

[i,j] is non empty set

{i,j} is non empty finite set

{i} is non empty trivial finite set

{{i,j},{i}} is non empty finite V42() set

mm is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

{ (S2 . (b

F . mm is V11() real ext-real Element of REAL

c

lower_bound c

q2 is set

U is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S2 . (U,mm) is set

[U,mm] is non empty set

{U,mm} is non empty functional finite V42() set

{U} is non empty trivial functional finite V42() set

{{U,mm},{U}} is non empty finite V42() set

S2 . [U,mm] is set

[U,mm] is non empty Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

S2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S2 . (S2,mm) is set

[S2,mm] is non empty set

{S2,mm} is non empty functional finite V42() set

{S2} is non empty trivial functional finite V42() set

{{S2,mm},{S2}} is non empty finite V42() set

S2 . [S2,mm] is set

X is V11() real ext-real set

(lower_bound (F .: F)) + X is V11() real ext-real Element of REAL

e is V11() real ext-real set

C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)

Lower_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj1 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj1 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

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

[: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

W-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj2 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(N-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SW-corner C),(NW-corner C)) is functional Element of bool the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SW-corner C),(NW-corner C)) /\ C is functional Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (W-most C) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (W-most C) is V21() V24( the carrier of ((TOP-REAL 2) | (W-most C))) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | (W-most C)), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:]

the carrier of ((TOP-REAL 2) | (W-most C)) is non empty set

[: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:] is non empty set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

|[(E-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

|[(E-bound C),(N-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) is functional Element of bool the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) /\ C is functional Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (E-most C) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (E-most C) is V21() V24( the carrier of ((TOP-REAL 2) | (E-most C))) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:]

the carrier of ((TOP-REAL 2) | (E-most C)) is non empty set

[: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is non empty V147() V148() V149() Element of bool REAL

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)

Upper_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

E-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj1 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj1 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

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

[: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj2 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(N-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) is functional Element of bool the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) /\ C is functional Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (E-most C) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (E-most C) is V21() V24( the carrier of ((TOP-REAL 2) | (E-most C))) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:]

the carrier of ((TOP-REAL 2) | (E-most C)) is non empty set

[: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is non empty V147() V148() V149() Element of bool REAL

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

W-bound C is V11() real ext-real Element of REAL

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

W-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

|[(W-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

|[(W-bound C),(N-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SW-corner C),(NW-corner C)) is functional Element of bool the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SW-corner C),(NW-corner C)) /\ C is functional Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (W-most C) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (W-most C) is V21() V24( the carrier of ((TOP-REAL 2) | (W-most C))) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | (W-most C)), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:]

the carrier of ((TOP-REAL 2) | (W-most C)) is non empty set

[: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:] is non empty set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V113() V159() V160() V161() V162() V163() V164() V165() V171() L15()

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

[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):] is non empty set

[:(TOP-REAL C),(TOP-REAL C):] is non empty strict TopSpace-like TopStruct

the carrier of [:(TOP-REAL C),(TOP-REAL C):] is non empty set

[: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

S is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S - F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(S,F) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

[:[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):],REAL:] is non empty set

bool [:[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):],REAL:] is non empty set

S is V21() V24([: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):]) V25( REAL ) Function-like V35([: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):], REAL ) Element of bool [:[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):],REAL:]

F is V21() V24( the carrier of [:(TOP-REAL C),(TOP-REAL C):]) V25( REAL ) Function-like V35( the carrier of [:(TOP-REAL C),(TOP-REAL C):], REAL ) Element of bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:]

S2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

F . (S2,F) is set

[S2,F] is non empty set

{S2,F} is non empty functional finite V42() set

{S2} is non empty trivial functional finite V42() set

{{S2,F},{S2}} is non empty finite V42() set

F . [S2,F] is set

S2 - F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(S2,F) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

S is V21() V24( the carrier of [:(TOP-REAL C),(TOP-REAL C):]) V25( REAL ) Function-like V35( the carrier of [:(TOP-REAL C),(TOP-REAL C):], REAL ) Element of bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:]

F is V21() V24( the carrier of [:(TOP-REAL C),(TOP-REAL C):]) V25( REAL ) Function-like V35( the carrier of [:(TOP-REAL C),(TOP-REAL C):], REAL ) Element of bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:]

S2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

S . (S2,F) is set

[S2,F] is non empty set

{S2,F} is non empty functional finite V42() set

{S2} is non empty trivial functional finite V42() set

{{S2,F},{S2}} is non empty finite V42() set

S . [S2,F] is set

S2 - F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(S2,F) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

F . (S2,F) is set

F . [S2,F] is set

C is non empty TopSpace-like TopStruct

the carrier of C is non empty set

[: the carrier of C,REAL:] is non empty set

bool [: the carrier of C,REAL:] is non empty set

S is V21() V24( the carrier of C) V25( REAL ) Function-like V35( the carrier of C, REAL ) Element of bool [: the carrier of C,REAL:]

F is Element of the carrier of C

S . F is V11() real ext-real Element of REAL

S2 is open V147() V148() V149() Neighbourhood of S . F

S2 ` is V147() V148() V149() Element of bool REAL

S " (S2 `) is Element of bool the carrier of C

bool the carrier of C is non empty set

S " S2 is Element of bool the carrier of C

(S " S2) ` is Element of bool the carrier of C

F is a_neighborhood of F

S .: F is V147() V148() V149() Element of bool REAL

F is V147() V148() V149() Element of bool REAL

S " F is Element of bool the carrier of C

bool the carrier of C is non empty set

F ` is V147() V148() V149() Element of bool REAL

(F `) ` is V147() V148() V149() Element of bool REAL

(S " F) ` is Element of bool the carrier of C

S2 is Element of the carrier of C

S " (F `) is Element of bool the carrier of C

S . S2 is V11() real ext-real Element of REAL

F is open V147() V148() V149() Neighbourhood of S . S2

X is a_neighborhood of S2

S .: X is V147() V148() V149() Element of bool REAL

S " (S .: X) is Element of bool the carrier of C

((S " F) `) ` is Element of bool the carrier of C

C is TopSpace-like TopStruct

S is TopSpace-like TopStruct

[:C,S:] is strict TopSpace-like TopStruct

the carrier of [:C,S:] is set

the topology of [:C,S:] is non empty V73([:C,S:]) Element of bool (bool the carrier of [:C,S:])

bool the carrier of [:C,S:] is non empty set

bool (bool the carrier of [:C,S:]) is non empty set

TopStruct(# the carrier of [:C,S:], the topology of [:C,S:] #) is strict TopSpace-like TopStruct

the carrier of C is set

the topology of C is non empty V73(C) Element of bool (bool the carrier of C)

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

TopStruct(# the carrier of C, the topology of C #) is strict TopSpace-like TopStruct

the carrier of S is set

the topology of S is non empty V73(S) Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct

[:TopStruct(# the carrier of C, the topology of C #),TopStruct(# the carrier of S, the topology of S #):] is strict TopSpace-like TopStruct

the carrier of [:TopStruct(# the carrier of C, the topology of C #),TopStruct(# the carrier of S, the topology of S #):] is set

the carrier of TopStruct(# the carrier of C, the topology of C #) is set

the carrier of TopStruct(# the carrier of S, the topology of S #) is set

[: the carrier of TopStruct(# the carrier of C, the topology of C #), the carrier of TopStruct(# the carrier of S, the topology of S #):] is set

bool the carrier of [:TopStruct(# the carrier of C, the topology of C #),TopStruct(# the carrier of S, the topology of S #):] is non empty set

bool (bool the carrier of [:TopStruct(# the carrier of C, the topology of C #),TopStruct(# the carrier of S, the topology of S #):]) is non empty set

bool the carrier of TopStruct(# the carrier of C, the topology of C #) is non empty set

bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set

the topology of TopStruct(# the carrier of C, the topology of C #) is non empty V73( TopStruct(# the carrier of C, the topology of C #)) Element of bool (bool the carrier of TopStruct(# the carrier of C, the topology of C #))

bool (bool the carrier of TopStruct(# the carrier of C, the topology of C #)) is non empty set

the topology of TopStruct(# the carrier of S, the topology of S #) is non empty V73( TopStruct(# the carrier of S, the topology of S #)) Element of bool (bool the carrier of TopStruct(# the carrier of S, the topology of S #))

bool (bool the carrier of TopStruct(# the carrier of S, the topology of S #)) is non empty set

{ [:b

{ (union b

{ [:b

{ (union b

the topology of [:TopStruct(# the carrier of C, the topology of C #),TopStruct(# the carrier of S, the topology of S #):] is non empty V73([:TopStruct(# the carrier of C, the topology of C #),TopStruct(# the carrier of S, the topology of S #):]) Element of bool (bool the carrier of [:TopStruct(# the carrier of C, the topology of C #),TopStruct(# the carrier of S, the topology of S #):])

C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V113() V159() V160() V161() V162() V163() V164() V165() V171() L15()

[:(TOP-REAL C),(TOP-REAL C):] is non empty strict TopSpace-like TopStruct

(C) is V21() V24( the carrier of [:(TOP-REAL C),(TOP-REAL C):]) V25( REAL ) Function-like V35( the carrier of [:(TOP-REAL C),(TOP-REAL C):], REAL ) Element of bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:]

the carrier of [:(TOP-REAL C),(TOP-REAL C):] is non empty set

[: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

bool [: the carrier of [:(TOP-REAL C),(TOP-REAL C):],REAL:] is non empty set

F is Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

(C) . F is V11() real ext-real Element of REAL

S2 is open V147() V148() V149() Neighbourhood of (C) . F

F is V11() real ext-real set

((C) . F) - F is V11() real ext-real Element of REAL

((C) . F) + F is V11() real ext-real Element of REAL

].(((C) . F) - F),(((C) . F) + F).[ is open V147() V148() V149() non left_end non right_end interval Element of bool REAL

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

[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):] is non empty set

X is set

e is set

[X,e] is non empty set

{X,e} is non empty finite set

{X} is non empty trivial finite set

{{X,e},{X}} is non empty finite V42() set

Euclid C is non empty strict Reflexive discerning V86() triangle MetrStruct

REAL C is non empty functional FinSequence-membered M12( REAL )

K326(C,REAL) is functional FinSequence-membered M12( REAL )

Pitag_dist C is V21() V24([:(REAL C),(REAL C):]) V25( REAL ) Function-like V35([:(REAL C),(REAL C):], REAL ) Element of bool [:[:(REAL C),(REAL C):],REAL:]

[:(REAL C),(REAL C):] is non empty set

[:[:(REAL C),(REAL C):],REAL:] is non empty set

bool [:[:(REAL C),(REAL C):],REAL:] is non empty set

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

the carrier of (Euclid C) is non empty set

i is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

j is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

the topology of (TOP-REAL C) is non empty V73( TOP-REAL C) Element of bool (bool the carrier of (TOP-REAL C))

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

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

TopStruct(# the carrier of (TOP-REAL C), the topology of (TOP-REAL C) #) is non empty strict TopSpace-like TopStruct

TopSpaceMetr (Euclid C) is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr (Euclid C)) is non empty set

c

S2 is Element of the carrier of (Euclid C)

F / 2 is V11() real ext-real Element of REAL

Ball (S2,(F / 2)) is Element of bool the carrier of (Euclid C)

bool the carrier of (Euclid C) is non empty set

q2 is Element of the carrier of (TopSpaceMetr (Euclid C))

mm is Element of the carrier of (Euclid C)

Ball (mm,(F / 2)) is Element of bool the carrier of (Euclid C)

U is a_neighborhood of c

W is a_neighborhood of q2

[:U,W:] is a_neighborhood of [c

[:(TopSpaceMetr (Euclid C)),(TopSpaceMetr (Euclid C)):] is non empty strict TopSpace-like TopStruct

[c

the carrier of [:(TopSpaceMetr (Euclid C)),(TopSpaceMetr (Euclid C)):] is non empty set

{c

{c

{{c

V is a_neighborhood of F

(C) .: V is V147() V148() V149() Element of bool REAL

s is set

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

q is Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

(C) . q is V11() real ext-real Element of REAL

q1 is set

q2 is set

[q1,q2] is non empty set

{q1,q2} is non empty finite set

{q1} is non empty trivial finite set

{{q1,q2},{q1}} is non empty finite V42() set

q1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

q2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

q19 is Element of the carrier of (Euclid C)

q29 is Element of the carrier of (Euclid C)

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

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

q1 - i is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(q1,i) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

q2 - j is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(q2,j) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

(F / 2) + (F / 2) is V11() real ext-real Element of REAL

|.(q1 - i).| + |.(q2 - j).| is V11() real ext-real non negative Element of REAL

p is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

q is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

[p,q] is non empty Element of the carrier of [:(TOP-REAL C),(TOP-REAL C):]

{p,q} is non empty functional finite V42() set

{p} is non empty trivial functional finite V42() set

{{p,q},{p}} is non empty finite V42() set

(C) . [p,q] is V11() real ext-real Element of REAL

p - q is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(p,q) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

(C) . (p,q) is set

[p,q] is non empty set

(C) . [p,q] is set

i - j is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(i,j) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

q1 - q2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(q1,q2) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

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

(q1 - q2) - (i - j) is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638((q1 - q2),(i - j)) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

(q1 - q2) - i is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638((q1 - q2),i) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

((q1 - q2) - i) + j is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K634(((q1 - q2) - i),j) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

q2 + i is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K634(q2,i) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

q1 - (q2 + i) is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638(q1,(q2 + i)) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

(q1 - (q2 + i)) + j is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K634((q1 - (q2 + i)),j) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

(q1 - i) - q2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638((q1 - i),q2) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

((q1 - i) - q2) + j is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K634(((q1 - i) - q2),j) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

(q1 - i) - (q2 - j) is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638((q1 - i),(q2 - j)) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

|.((q1 - i) - (q2 - j)).| is V11() real ext-real non negative Element of REAL

s - ((C) . F) is V11() real ext-real Element of REAL

|.((q1 - q2) - (i - j)).| is V11() real ext-real non negative Element of REAL

((C) . F) - s is V11() real ext-real Element of REAL

(i - j) - (q1 - q2) is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C)

K638((i - j),(q1 - q2)) is V21() V24( NAT ) V25( REAL ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL

|.((i - j) - (q1 - q2)).| is V11() real ext-real non negative Element of REAL

C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V113() V159() V160() V161() V162() V163() V164() V165() V171() L15()

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

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

S is non empty functional closed compact Element of bool the carrier of (TOP-REAL C)

F is non empty functional closed compact Element of bool the carrier of (TOP-REAL C)

dist_min (S,F) is V11() real ext-real Element of REAL

the topology of (TOP-REAL C) is non empty V73( TOP-REAL C) Element of bool (bool the carrier of (TOP-REAL C))

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

TopStruct(# the carrier of (TOP-REAL C), the topology of (TOP-REAL C) #) is non empty strict TopSpace-like TopStruct

Euclid C is non empty strict Reflexive discerning V86() triangle MetrStruct

REAL C is non empty functional FinSequence-membered M12( REAL )

K326(C,REAL) is functional FinSequence-membered M12( REAL )

Pitag_dist C is V21() V24([:(REAL C),(REAL C):]) V25( REAL ) Function-like V35([:(REAL C),(REAL C):], REAL ) Element of bool [:[:(REAL C),(REAL C):],REAL:]

[:(REAL C),(REAL C):] is non empty set

[:[:(REAL C),(REAL C):],REAL:] is non empty set

bool [:[:(REAL C),(REAL C):],REAL:] is non empty set

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

TopSpaceMetr (Euclid C) is non empty strict TopSpace-like TopStruct

the carrier of (TopSpaceMetr (Euclid C)) is non empty set

bool the carrier of (TopSpaceMetr (Euclid C)) is non empty set

S2 is Element of bool the carrier of (TopSpaceMetr (Euclid C))

F is Element of bool the carrier of (TopSpaceMetr (Euclid C))

min_dist_min (S2,F) is V11() real ext-real Element of REAL

C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)

E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

E-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj1 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj1 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

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

[: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj2 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(N-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) is functional Element of bool the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) /\ C is functional Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (E-most C) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (E-most C) is V21() V24( the carrier of ((TOP-REAL 2) | (E-most C))) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:]

the carrier of ((TOP-REAL 2) | (E-most C)) is non empty set

[: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is non empty V147() V148() V149() Element of bool REAL

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

Upper_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

W-bound C is V11() real ext-real Element of REAL

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

W-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

|[(W-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

|[(W-bound C),(N-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SW-corner C),(NW-corner C)) is functional Element of bool the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SW-corner C),(NW-corner C)) /\ C is functional Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (W-most C) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (W-most C) is V21() V24( the carrier of ((TOP-REAL 2) | (W-most C))) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | (W-most C)), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:]

the carrier of ((TOP-REAL 2) | (W-most C)) is non empty set

[: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | (W-most C)),REAL:] is non empty set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

Segment (S,F,C) is functional Element of bool the carrier of (TOP-REAL 2)

Segment ((Upper_Arc C),(W-min C),(E-max C),S,F) is functional Element of bool the carrier of (TOP-REAL 2)

S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

(Upper_Arc C) /\ (Lower_Arc C) is functional Element of bool the carrier of (TOP-REAL 2)

{(W-min C),(E-max C)} is non empty functional finite V42() set

Lower_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

(Upper_Arc C) /\ (Lower_Arc C) is functional Element of bool the carrier of (TOP-REAL 2)

{(W-min C),(E-max C)} is non empty functional finite V42() set

{ H

{ H

C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)

E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

E-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj1 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj1 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

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

[: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | C),REAL:] is non empty set

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) Function-like V35( the carrier of (TOP-REAL 2), REAL ) continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]

proj2 | C is V21() V24( the carrier of ((TOP-REAL 2) | C)) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | C), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | C),REAL:]

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is non empty V147() V148() V149() Element of bool REAL

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NE-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(N-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) is functional Element of bool the carrier of (TOP-REAL 2)

K334((TOP-REAL 2),(SE-corner C),(NE-corner C)) /\ C is functional Element of bool the carrier of (TOP-REAL 2)

(TOP-REAL 2) | (E-most C) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2

proj2 | (E-most C) is V21() V24( the carrier of ((TOP-REAL 2) | (E-most C))) V25( REAL ) Function-like V35( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) continuous Element of bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:]

the carrier of ((TOP-REAL 2) | (E-most C)) is non empty set

[: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

bool [: the carrier of ((TOP-REAL 2) | (E-most C)),REAL:] is non empty set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is non empty V147() V148() V149() Element of bool REAL

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)

W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

W-bound C is V11() real ext-real Element of REAL

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

W-most C is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)

SW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

|[(W-bound C),(S-bound C)]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)

NW-corner C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-