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,b1)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C) : b1 in F } is set
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,b1)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C) : b1 in F } is set
F . S2 is V11() real ext-real Element of REAL
c12 is V147() V148() V149() Element of bool REAL
lower_bound c12 is V11() real ext-real Element of REAL
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 . (b1,e)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C) : b1 in S } is set
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 . (b1,mm)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL C) : b1 in S } is set
F . mm is V11() real ext-real Element of REAL
c12 is V147() V148() V149() Element of bool REAL
lower_bound c12 is V11() real ext-real Element of REAL
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
{ [:b1,b2:] where b1 is Element of bool the carrier of TopStruct(# the carrier of C, the topology of C #), b2 is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #) : ( b1 in the topology of TopStruct(# the carrier of C, the topology of C #) & b2 in the topology of TopStruct(# the carrier of S, the topology of S #) ) } is set
{ (union b1) where b1 is 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 #):]) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of TopStruct(# the carrier of C, the topology of C #), b3 is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #) : ( b1 in the topology of TopStruct(# the carrier of C, the topology of C #) & b2 in the topology of TopStruct(# the carrier of S, the topology of S #) ) } } is set
{ [:b1,b2:] where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier of S : ( b1 in the topology of C & b2 in the topology of S ) } is set
{ (union b1) where b1 is 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 #):]) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of C, b3 is Element of bool the carrier of S : ( b1 in the topology of C & b2 in the topology of S ) } } is set
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
c12 is Element of the carrier of (TopSpaceMetr (Euclid 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 c12
W is a_neighborhood of q2
[:U,W:] is a_neighborhood of [c12,q2]
[:(TopSpaceMetr (Euclid C)),(TopSpaceMetr (Euclid C)):] is non empty strict TopSpace-like TopStruct
[c12,q2] is non empty Element of the carrier of [:(TopSpaceMetr (Euclid C)),(TopSpaceMetr (Euclid C)):]
the carrier of [:(TopSpaceMetr (Euclid C)),(TopSpaceMetr (Euclid C)):] is non empty set
{c12,q2} is non empty finite set
{c12} is non empty trivial finite set
{{c12,q2},{c12}} is non empty finite V42() set
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
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
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-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)
Segment ((E-max C),S,C) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),S) 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)
Upper_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
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
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)
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)
Lower_Arc C is non empty functional Element of bool 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)
Segment (S,(W-min C),C) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),S,(W-min C)) 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)
Upper_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)
{(E-max C),(W-min C)} is non empty functional finite V42() set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
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-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 ((Lower_Arc C),(E-max C),(W-min 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)
Upper_Arc C is non empty functional Element of bool the carrier of (TOP-REAL 2)
(Lower_Arc C) /\ (Upper_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
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
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)
Lower_Arc C is non empty functional Element of bool 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)
R_Segment ((Upper_Arc C),(W-min C),(E-max C),S) is functional Element of bool 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)
L_Segment ((Lower_Arc C),(E-max C),(W-min C),F) is functional Element of bool the carrier of (TOP-REAL 2)
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),S)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),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) /\ (Upper_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
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S3[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S4[b1] } is set
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : ( S2[b1] or S3[b1] ) } is set
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } \/ { b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S3[b1] } is set
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)
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)
Upper_Arc C is non empty functional 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)
L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) is functional Element of bool 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)
Segment (S,(W-min C),C) is functional Element of bool the carrier of (TOP-REAL 2)
R_Segment ((Upper_Arc C),(W-min C),(E-max C),S) is functional Element of bool the carrier of (TOP-REAL 2)
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),S)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) 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) /\ (Upper_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) \/ (Upper_Arc C) is non empty functional Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S3[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ H1(b1) where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S4[b1] } is set
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : ( S2[b1] or S3[b1] ) } is set
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S2[b1] } \/ { b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : S3[b1] } is set
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)
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)
R_Segment ((Upper_Arc C),(W-min C),(E-max C),S) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Upper_Arc C),(W-min C),(E-max C),S,(E-max C)) is functional Element of bool the carrier of (TOP-REAL 2)
L_Segment ((Upper_Arc C),(W-min C),(E-max C),(E-max C)) is functional Element of bool the carrier of (TOP-REAL 2)
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),S)) /\ (Upper_Arc C) is 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)
Lower_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)
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)
L_Segment ((Lower_Arc C),(E-max C),(W-min C),S) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),S) is functional Element of bool the carrier of (TOP-REAL 2)
R_Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C)) is functional Element of bool the carrier of (TOP-REAL 2)
(Lower_Arc C) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),S)) is 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)
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)
F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment (F,(W-min C),C) is 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
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)
Upper_Arc C is non empty functional 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)
R_Segment ((Upper_Arc C),(W-min C),(E-max C),F) is functional Element of bool the carrier of (TOP-REAL 2)
L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) is functional Element of bool the carrier of (TOP-REAL 2)
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),F)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Upper_Arc C),(W-min C),(E-max C),F,(E-max C)) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),(W-min C)) is 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
{(E-max C)} is non empty trivial functional finite V42() set
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),F)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),F,(W-min C)) is 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)
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)
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)
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)
Upper_Arc C is non empty functional 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)
Segment ((Upper_Arc C),(W-min C),(E-max C),S,F) is functional Element of bool the carrier of (TOP-REAL 2)
R_Segment ((Upper_Arc C),(W-min C),(E-max C),S) is functional Element of bool the carrier of (TOP-REAL 2)
L_Segment ((Lower_Arc C),(E-max C),(W-min C),F) is functional Element of bool the carrier of (TOP-REAL 2)
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),S)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),F)) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Upper_Arc C),(W-min C),(E-max C),S,(E-max C)) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),F) is 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
{(E-max C)} is non empty trivial functional finite V42() set
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),S)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),F)) is functional Element of bool the carrier of (TOP-REAL 2)
R_Segment ((Upper_Arc C),(W-min C),(E-max C),S) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Upper_Arc C),(W-min C),(E-max C),S,(E-max C)) is functional Element of bool the carrier of (TOP-REAL 2)
L_Segment ((Lower_Arc C),(E-max C),(W-min C),F) is functional Element of bool the carrier of (TOP-REAL 2)
{(E-max C)} is non empty trivial functional finite V42() set
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),S)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),F)) is functional Element of bool the carrier of (TOP-REAL 2)
L_Segment ((Lower_Arc C),(E-max C),(W-min C),F) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),F) is functional Element of bool the carrier of (TOP-REAL 2)
R_Segment ((Upper_Arc C),(W-min C),(E-max C),S) is functional Element of bool the carrier of (TOP-REAL 2)
{(E-max C)} is non empty trivial functional finite V42() set
(R_Segment ((Upper_Arc C),(W-min C),(E-max C),S)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),F)) is functional Element of bool the carrier of (TOP-REAL 2)
Segment ((Lower_Arc C),(E-max C),(W-min C),S,F) is 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)
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)
Segment ((W-min C),(W-min C),C) is functional Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : ( LE W-min C,b1,C or ( W-min C in C & b1 = W-min C ) ) } is set
F is set
S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of 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)
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)
S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment (S,(W-min C),C) is 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)
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)
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)
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)
{S} is non empty trivial functional finite V42() set
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)
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)
C is non empty functional closed being_simple_closed_curve compact 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)
S is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
S . 1 is V21() Function-like set
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
rng S is functional finite closed compact Element of bool the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. (len S)),(S /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
S /. 2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. 1),(S /. 2),C) is functional Element of bool the carrier of (TOP-REAL 2)
(Segment ((S /. (len S)),(S /. 1),C)) /\ (Segment ((S /. 1),(S /. 2),C)) is functional Element of bool the carrier of (TOP-REAL 2)
{(S /. 1)} is non empty trivial functional finite V42() set
(len S) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. ((len S) -' 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. ((len S) -' 1)),(S /. (len S)),C) is functional Element of bool the carrier of (TOP-REAL 2)
(Segment ((S /. ((len S) -' 1)),(S /. (len S)),C)) /\ (Segment ((S /. (len S)),(S /. 1),C)) is functional Element of bool the carrier of (TOP-REAL 2)
{(S /. (len S))} is non empty trivial functional finite V42() set
F is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
F /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
len F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
rng F is functional finite closed compact Element of bool the carrier of (TOP-REAL 2)
F /. (len F) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. (len F)),(F /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
F /. 2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. 1),(F /. 2),C) is functional Element of bool the carrier of (TOP-REAL 2)
(Segment ((F /. (len F)),(F /. 1),C)) /\ (Segment ((F /. 1),(F /. 2),C)) is functional Element of bool the carrier of (TOP-REAL 2)
{(F /. 1)} is non empty trivial functional finite V42() set
(len F) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. ((len F) -' 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. ((len F) -' 1)),(F /. (len F)),C) is functional Element of bool the carrier of (TOP-REAL 2)
(Segment ((F /. ((len F) -' 1)),(F /. (len F)),C)) /\ (Segment ((F /. (len F)),(F /. 1),C)) is functional Element of bool the carrier of (TOP-REAL 2)
{(F /. (len F))} is non empty trivial functional finite V42() set
dom F is finite V147() V148() V149() V150() V151() V152() bounded_below bounded_above real-bounded Element of bool NAT
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. (S2 + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F /. (S2 + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. S2),(F /. (S2 + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
S2 + 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. (S2 + 2) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. (S2 + 1)),(F /. (S2 + 2)),C) is functional Element of bool the carrier of (TOP-REAL 2)
(Segment ((F /. S2),(F /. (S2 + 1)),C)) /\ (Segment ((F /. (S2 + 1)),(F /. (S2 + 2)),C)) is functional Element of bool the carrier of (TOP-REAL 2)
{(F /. (S2 + 1))} is non empty trivial functional finite V42() set
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. (S2 + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. S2),(F /. (S2 + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
F /. F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. (F + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. F),(F /. (F + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F /. (S2 + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. S2),(F /. (S2 + 1)),C) is 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)
S is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
dom S is non empty non trivial finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
rng S is functional finite closed compact 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)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
F is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. (S + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. S),(F /. (S + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
F /. (len F) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. (len F)),(F /. 1),C) is 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)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
dom F is non empty non trivial finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(C,S,F) is functional Element of bool the carrier of (TOP-REAL 2)
len F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. (S + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. S),(F /. (S + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
F /. (len F) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. (len F)),(F /. 1),C) is 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)
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
(C,F,S) is functional Element of bool the carrier of (TOP-REAL 2)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (F + 1) 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),(S /. (F + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. (len S)),(S /. 1),C) is 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 | 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 | 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)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
dom S is non empty non trivial finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( b1 in dom S & LE S /. b1,F,C ) } is set
F is set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. X is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of 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 | 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 | 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)
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F is non empty finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
sup F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() set
(C,(sup F),S) is functional Element of bool the carrier of (TOP-REAL 2)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(sup F) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. ((sup F) + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
rng S is functional finite closed compact Element of bool the carrier of (TOP-REAL 2)
S /. (sup F) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : ( LE S /. (sup F),b1,C & LE b1,S /. ((sup F) + 1),C ) } is set
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. e is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. (sup F)),(S /. ((sup F) + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. e is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
rng S is functional finite closed compact Element of bool the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{ b1 where b1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2) : ( LE S /. (len S),b1,C or ( S /. (len S) in C & b1 = W-min C ) ) } is set
Segment ((S /. (len S)),(S /. 1),C) is 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,S2,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (F + 1) 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),(S /. (F + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
S /. S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (S2 + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. S2),(S /. (S2 + 1)),C) is 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(len S) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. (len S)),(S /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
F + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S /. (F + 1) 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),(S /. (F + 1)),C) is 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
F + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (F + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{(S /. (F + 1))} is non empty trivial functional finite V42() set
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,S2,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,F,S) /\ (C,S2,S) is functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. 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),(S /. (F + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
S /. S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (S2 + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. S2),(S /. (S2 + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,S2,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,F,S) /\ (C,S2,S) is functional closed compact Element of bool the carrier of (TOP-REAL 2)
F + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (F + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{(S /. (F + 1))} is non empty trivial functional finite V42() set
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,1,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,(len S),S) /\ (C,1,S) is functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{(S /. 1)} is non empty trivial functional finite V42() set
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. (len S)),(S /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. (1 + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. 1),(S /. (1 + 1)),C) is 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,1,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,(len S),S) /\ (C,1,S) is functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{(S /. 1)} is non empty trivial functional finite V42() set
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(len S) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,((len S) -' 1),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,(len S),S) /\ (C,((len S) -' 1),S) is functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{(S /. (len S))} is non empty trivial functional finite V42() set
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. (len S)),(S /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
((len S) -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S /. ((len S) -' 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. ((len S) -' 1)),(S /. (len S)),C) is 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(len S) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,((len S) -' 1),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,(len S),S) /\ (C,((len S) -' 1),S) is functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
{(S /. (len S))} is non empty trivial functional finite V42() 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
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
bool the carrier of (Euclid C) is non empty set
S is functional Element of bool 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 (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
Family_open_set (Euclid C) is Element of bool (bool the carrier of (Euclid C))
bool (bool the carrier of (Euclid C)) is non empty set
TopStruct(# the carrier of (Euclid C),(Family_open_set (Euclid C)) #) is non empty strict TopStruct
F is Element of bool the carrier of (Euclid C)
diameter F is V11() real ext-real Element of REAL
F is Element of bool the carrier of (Euclid C)
F is V11() real ext-real Element of REAL
diameter F is V11() real ext-real Element of REAL
X is Element of bool the carrier of (Euclid C)
S2 is V11() real ext-real Element of REAL
diameter X 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
dom S is non empty non trivial finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ (2,(C,b1,S)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : b1 in dom S } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : S1[b1] } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : b1 in dom S } is set
(C,1,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(2,(C,1,S)) is V11() real ext-real Element of REAL
F is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
sup F is V11() real ext-real set
X is V11() real ext-real Element of REAL
F is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
F is V11() real ext-real Element of REAL
sup F is V11() real ext-real set
X is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
S2 is V11() real ext-real Element of REAL
sup X 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
(C,S) is V11() real ext-real Element of REAL
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(2,(C,F,S)) is V11() real ext-real Element of REAL
dom S is non empty non trivial finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ (2,(C,b1,S)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : b1 in dom S } is set
S2 is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
sup S2 is V11() real ext-real set
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
S /. (len S) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S /. (len S)),(S /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
(C,S) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
dom S is non empty non trivial finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ (2,(C,b1,S)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : b1 in dom S } is set
S2 is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
sup S2 is V11() real ext-real set
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(2,(C,F,S)) 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)
S is V11() real ext-real Element of REAL
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 | 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 | 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)
F is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
F . 1 is V21() Function-like set
len F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
rng F is functional finite closed compact Element of bool the carrier of (TOP-REAL 2)
F /. (len F) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. (len F)),(F /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
F /. 2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. 1),(F /. 2),C) is functional Element of bool the carrier of (TOP-REAL 2)
(Segment ((F /. (len F)),(F /. 1),C)) /\ (Segment ((F /. 1),(F /. 2),C)) is functional Element of bool the carrier of (TOP-REAL 2)
{(F /. 1)} is non empty trivial functional finite V42() set
(len F) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
F /. ((len F) -' 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((F /. ((len F) -' 1)),(F /. (len F)),C) is functional Element of bool the carrier of (TOP-REAL 2)
(Segment ((F /. ((len F) -' 1)),(F /. (len F)),C)) /\ (Segment ((F /. (len F)),(F /. 1),C)) is functional Element of bool the carrier of (TOP-REAL 2)
{(F /. (len F))} is non empty trivial functional finite V42() set
dom F is finite V147() V148() V149() V150() V151() V152() bounded_below bounded_above real-bounded Element of bool NAT
S2 is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
(C,S2) is V11() real ext-real Element of REAL
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S2) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(2,(C,F,S2)) is V11() real ext-real Element of REAL
len S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S2 /. F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
F + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S2 /. (F + 1) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S2 /. F),(S2 /. (F + 1)),C) is functional Element of bool the carrier of (TOP-REAL 2)
X is Element of bool the carrier of (Euclid 2)
diameter X is V11() real ext-real Element of REAL
len S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S2 /. (len S2) is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
S2 /. 1 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of (TOP-REAL 2)
Segment ((S2 /. (len S2)),(S2 /. 1),C) is functional Element of bool the carrier of (TOP-REAL 2)
X is Element of bool the carrier of (Euclid 2)
diameter X is V11() real ext-real Element of REAL
len S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of (TOP-REAL 2)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
{ (dist_min ((C,b1,S),(C,b2,S))) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( 1 <= b1 & not b2 <= b1 & not len S <= b2 & not b1,b2 are_adjacent1 ) } is set
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(len S) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
{ (dist_min ((C,(len S),S),(C,b1,S))) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( not b1 <= 1 & not (len S) -' 1 <= b1 ) } is set
dom S is non empty non trivial finite V147() V148() V149() V150() V151() V152() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ H2(b1,b2) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : S3[b1,b2] } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : S1[b1] } is set
{ H2(b1,b2) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : S4[b1,b2] } is set
{ H2(b1,b2) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( b1 in dom S & b2 in dom S ) } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : S2[b1] } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : b1 in dom S } is set
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
j is set
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,S2,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
mm is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,mm,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,S2,S),(C,mm,S)) is V11() real ext-real Element of REAL
j is set
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,S2,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,(len S),S),(C,S2,S)) is V11() real ext-real Element of REAL
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
3 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
7 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
7 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,1,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(C,3,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,1,S),(C,3,S)) is V11() real ext-real Element of REAL
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,2,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,(len S),S),(C,2,S)) is V11() real ext-real Element of REAL
j is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
inf j is V11() real ext-real set
S2 is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
inf S2 is V11() real ext-real set
min ((inf j),(inf S2)) is V11() real ext-real set
mm is V11() real ext-real Element of REAL
F is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
X is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
F is V11() real ext-real Element of REAL
inf F is V11() real ext-real set
inf X is V11() real ext-real set
min ((inf F),(inf X)) is V11() real ext-real set
e is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
i is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
S2 is V11() real ext-real Element of REAL
inf e is V11() real ext-real set
inf i is V11() real ext-real set
min ((inf e),(inf i)) 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
{ (dist_min ((C,b1,S),(C,b2,S))) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( 1 <= b1 & not b2 <= b1 & b2 <= len S & (C,b1,S) misses (C,b2,S) ) } is set
(C,S) is V11() real ext-real Element of REAL
{ (dist_min ((C,b1,S),(C,b2,S))) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( 1 <= b1 & not b2 <= b1 & not len S <= b2 & not b1,b2 are_adjacent1 ) } is set
(C,(len S),S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
(len S) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
{ (dist_min ((C,(len S),S),(C,b1,S))) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( not b1 <= 1 & not (len S) -' 1 <= b1 ) } is set
F is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
S2 is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
inf F is V11() real ext-real set
inf S2 is V11() real ext-real set
min ((inf F),(inf S2)) is V11() real ext-real set
F \/ S2 is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
F is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
inf F is V11() real ext-real set
e is set
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,i,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,j,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,i,S),(C,j,S)) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,i,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,(len S),S),(C,i,S)) is V11() real ext-real Element of REAL
e is set
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,i,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,j,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,i,S),(C,j,S)) 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)
S is non empty non trivial V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like (C)
(C,S) is V11() real ext-real Element of REAL
len S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
{ (dist_min ((C,b1,S),(C,b2,S))) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT : ( 1 <= b1 & not b2 <= b1 & b2 <= len S & (C,b1,S) misses (C,b2,S) ) } is set
F is non empty compact closed finite V147() V148() V149() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
inf F is V11() real ext-real set
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,S2,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V19() V100() V147() V148() V149() V150() V151() V152() bounded_below Element of NAT
(C,F,S) is non empty functional closed compact Element of bool the carrier of (TOP-REAL 2)
dist_min ((C,S2,S),(C,F,S)) is V11() real ext-real Element of REAL