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-