:: JORDAN_A semantic presentation

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

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

bool omega is non empty set

[: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
is non empty set
is non empty set
bool is non empty set

[: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 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 () is non empty functional set
bool the carrier of () 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

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

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

REAL 2 is non empty 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),() #) is strict MetrStruct
the carrier of () is non empty set
bool the carrier of () 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

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

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 () is non empty functional set
bool the carrier of () is non empty set
[:(),():] is non empty strict TopSpace-like TopStruct
the carrier of [:(),():] is non empty set
[: the carrier of [:(),():],REAL:] is non empty set
bool [: the carrier of [:(),():],REAL:] is non empty set
[: the carrier of (),REAL:] is non empty set
bool [: the carrier of (),REAL:] is non empty set
F is non empty functional closed compact Element of bool the carrier of ()
S is non empty functional closed compact Element of bool the carrier of ()
[:S,F:] is non empty Element of bool the carrier of [:(),():]
bool the carrier of [:(),():] is non empty set
S2 is V21() V24( the carrier of [:(),():]) V25( REAL ) Function-like V35( the carrier of [:(),():], REAL ) continuous Element of bool [: the carrier of [:(),():],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 ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) Element of bool [: the carrier of (),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 ()
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 ()
{ (S2 . (e,b1)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of () : b1 in F } is set
j is V147() V148() V149() Element of bool 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 ()
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 [:(),():]
X is V11() real ext-real set
e is Element of the carrier of [:(),():]
S2 . e is V11() real ext-real Element of REAL
[: the carrier of (), the carrier of ():] 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 ()
{ (S2 . (S2,b1)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of () : b1 in F } is set
F . S2 is V11() real ext-real Element of REAL
c12 is V147() V148() V149() Element of bool REAL

q2 is set
U is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
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 [:(),():]
mm is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
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

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 () is non empty functional set
bool the carrier of () is non empty set
[:(),():] is non empty strict TopSpace-like TopStruct
the carrier of [:(),():] is non empty set
[: the carrier of [:(),():],REAL:] is non empty set
bool [: the carrier of [:(),():],REAL:] is non empty set
[: the carrier of (),REAL:] is non empty set
bool [: the carrier of (),REAL:] is non empty set
S is non empty functional closed compact Element of bool the carrier of ()
F is non empty functional closed compact Element of bool the carrier of ()
[:S,F:] is non empty Element of bool the carrier of [:(),():]
bool the carrier of [:(),():] is non empty set
S2 is V21() V24( the carrier of [:(),():]) V25( REAL ) Function-like V35( the carrier of [:(),():], REAL ) continuous Element of bool [: the carrier of [:(),():],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 ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) Element of bool [: the carrier of (),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 ()
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 ()
{ (S2 . (b1,e)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of () : b1 in S } is set
j is V147() V148() V149() Element of bool 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 ()
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 [:(),():]
X is V11() real ext-real set
e is Element of the carrier of [:(),():]
S2 . e is V11() real ext-real Element of REAL
[: the carrier of (), the carrier of ():] 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 ()
{ (S2 . (b1,mm)) where b1 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of () : b1 in S } is set
F . mm is V11() real ext-real Element of REAL
c12 is V147() V148() V149() Element of bool REAL

q2 is set
U is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
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 [:(),():]
S2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
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 ()
Lower_Arc C is non empty functional Element of bool the carrier of ()
W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

proj1 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj1 | C 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:]
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
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
W-most C is non empty functional closed compact Element of bool the carrier of ()

proj2 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj2 | C 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:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
K334((),(),()) is functional Element of bool the carrier of ()
K334((),(),()) /\ C is functional Element of bool the carrier of ()

proj2 | () is V21() V24( the carrier of (() | ())) V25( REAL ) Function-like V35( the carrier of (() | ()), REAL ) continuous Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is non empty V147() V148() V149() Element of bool REAL
lower_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(lower_bound (proj2 | ()))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
E-most C is non empty functional closed compact Element of bool the carrier of ()

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

|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
K334((),(),()) is functional Element of bool the carrier of ()
K334((),(),()) /\ C is functional Element of bool the carrier of ()

proj2 | () is V21() V24( the carrier of (() | ())) V25( REAL ) Function-like V35( the carrier of (() | ()), REAL ) continuous Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty set
bool [: the carrier of (() | ()),REAL:] is non empty set
upper_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is non empty V147() V148() V149() Element of bool REAL
upper_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(upper_bound (proj2 | ()))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
Upper_Arc C is non empty functional Element of bool the carrier of ()
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of ()
Upper_Arc C is non empty functional Element of bool the carrier of ()
E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

proj1 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj1 | C 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:]
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
upper_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
E-most C is non empty functional closed compact Element of bool the carrier of ()

proj2 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj2 | C 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:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
K334((),(),()) is functional Element of bool the carrier of ()
K334((),(),()) /\ C is functional Element of bool the carrier of ()

proj2 | () is V21() V24( the carrier of (() | ())) V25( REAL ) Function-like V35( the carrier of (() | ()), REAL ) continuous Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty set
bool [: the carrier of (() | ()),REAL:] is non empty set
upper_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is non empty V147() V148() V149() Element of bool REAL
upper_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(upper_bound (proj2 | ()))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
Lower_Arc C is non empty functional Element of bool the carrier of ()
W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

lower_bound () is V11() real ext-real Element of REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
W-most C is non empty functional closed compact Element of bool the carrier of ()

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

|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
K334((),(),()) is functional Element of bool the carrier of ()
K334((),(),()) /\ C is functional Element of bool the carrier of ()

proj2 | () is V21() V24( the carrier of (() | ())) V25( REAL ) Function-like V35( the carrier of (() | ()), REAL ) continuous Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is non empty V147() V148() V149() Element of bool REAL
lower_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(lower_bound (proj2 | ()))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

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 () is non empty functional set
[: the carrier of (), the carrier of ():] is non empty set
[:(),():] is non empty strict TopSpace-like TopStruct
the carrier of [:(),():] is non empty set
[: the carrier of [:(),():],REAL:] is non empty set
bool [: the carrier of [:(),():],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 ()
F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
S - F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

|.(S - F).| is V11() real ext-real non negative Element of REAL
[:[: the carrier of (), the carrier of ():],REAL:] is non empty set
bool [:[: the carrier of (), the carrier of ():],REAL:] is non empty set
S is V21() V24([: the carrier of (), the carrier of ():]) V25( REAL ) Function-like V35([: the carrier of (), the carrier of ():], REAL ) Element of bool [:[: the carrier of (), the carrier of ():],REAL:]
F is V21() V24( the carrier of [:(),():]) V25( REAL ) Function-like V35( the carrier of [:(),():], REAL ) Element of bool [: the carrier of [:(),():],REAL:]
S2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
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 ()

|.(S2 - F).| is V11() real ext-real non negative Element of REAL
S is V21() V24( the carrier of [:(),():]) V25( REAL ) Function-like V35( the carrier of [:(),():], REAL ) Element of bool [: the carrier of [:(),():],REAL:]
F is V21() V24( the carrier of [:(),():]) V25( REAL ) Function-like V35( the carrier of [:(),():], REAL ) Element of bool [: the carrier of [:(),():],REAL:]
S2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
F is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
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 ()

|.(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

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 #):])

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V113() V159() V160() V161() V162() V163() V164() V165() V171() L15()
[:(),():] is non empty strict TopSpace-like TopStruct
(C) is V21() V24( the carrier of [:(),():]) V25( REAL ) Function-like V35( the carrier of [:(),():], REAL ) Element of bool [: the carrier of [:(),():],REAL:]
the carrier of [:(),():] is non empty set
[: the carrier of [:(),():],REAL:] is non empty set
bool [: the carrier of [:(),():],REAL:] is non empty set
F is Element of the carrier of [:(),():]
(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 () is non empty functional set
[: the carrier of (), the carrier of ():] 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

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),() #) is strict MetrStruct
the carrier of () is non empty set
i is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
j is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
the topology of () is non empty V73( TOP-REAL C) Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is non empty strict TopSpace-like TopStruct

the carrier of () is non empty set
c12 is Element of the carrier of ()
S2 is Element of the carrier of ()
F / 2 is V11() real ext-real Element of REAL
Ball (S2,(F / 2)) is Element of bool the carrier of ()
bool the carrier of () is non empty set
q2 is Element of the carrier of ()
mm is Element of the carrier of ()
Ball (mm,(F / 2)) is Element of bool the carrier of ()
U is a_neighborhood of c12
W is a_neighborhood of q2
[:U,W:] is a_neighborhood of [c12,q2]
[:(),():] is non empty strict TopSpace-like TopStruct
[c12,q2] is non empty Element of the carrier of [:(),():]
the carrier of [:(),():] 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 [:(),():]
(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 ()
q2 is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
q19 is Element of the carrier of ()
q29 is Element of the carrier of ()
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 ()

|.(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 ()

|.(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 ()
q is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
[p,q] is non empty Element of the carrier of [:(),():]
{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 ()

|.(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 ()

|.(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 ()

|.(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 ()
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 ()
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 ()
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 ()

q1 - (q2 + i) is V21() V24( NAT ) Function-like finite V45(C) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
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 ()
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 ()
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 ()
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 ()
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 ()
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

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 () is non empty functional set
bool the carrier of () is non empty set
S is non empty functional closed compact Element of bool the carrier of ()
F is non empty functional closed compact Element of bool the carrier of ()
dist_min (S,F) is V11() real ext-real Element of REAL
the topology of () is non empty V73( TOP-REAL C) Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is non empty strict TopSpace-like TopStruct

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),() #) is strict MetrStruct

the carrier of () is non empty set
bool the carrier of () is non empty set
S2 is Element of bool the carrier of ()
F is Element of bool the carrier of ()
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 ()
E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

proj1 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj1 | C 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:]
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
upper_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
E-most C is non empty functional closed compact Element of bool the carrier of ()

proj2 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj2 | C 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:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
K334((),(),()) is functional Element of bool the carrier of ()
K334((),(),()) /\ C is functional Element of bool the carrier of ()

proj2 | () is V21() V24( the carrier of (() | ())) V25( REAL ) Function-like V35( the carrier of (() | ()), REAL ) continuous Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty set
bool [: the carrier of (() | ()),REAL:] is non empty set
upper_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is non empty V147() V148() V149() Element of bool REAL
upper_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(upper_bound (proj2 | ()))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
Upper_Arc C is non empty functional Element of bool the carrier of ()
W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

lower_bound () is V11() real ext-real Element of REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
W-most C is non empty functional closed compact Element of bool the carrier of ()

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

|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
K334((),(),()) is functional Element of bool the carrier of ()
K334((),(),()) /\ C is functional Element of bool the carrier of ()

proj2 | () is V21() V24( the carrier of (() | ())) V25( REAL ) Function-like V35( the carrier of (() | ()), REAL ) continuous Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty set
bool [: the carrier of (() | ()),REAL:] is non empty set
lower_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is non empty V147() V148() V149() Element of bool REAL
lower_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(lower_bound (proj2 | ()))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
S is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
F is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
Segment (S,F,C) is functional Element of bool the carrier of ()
Segment ((),(),(),S,F) is functional Element of bool the carrier of ()
S2 is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
Lower_Arc C is non empty functional Element of bool the carrier of ()
() /\ () is functional Element of bool the carrier of ()
{(),()} is non empty functional finite V42() set
Lower_Arc C is non empty functional Element of bool the carrier of ()
() /\ () is functional Element of bool the carrier of ()
{(),()} 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 () : 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 () : S2[b1] } is set
C is non empty functional closed being_simple_closed_curve compact Element of bool the carrier of ()
E-max C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

proj1 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj1 | C 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:]
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
upper_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
E-most C is non empty functional closed compact Element of bool the carrier of ()

proj2 is V21() V24( the carrier of ()) V25( REAL ) Function-like V35( the carrier of (), REAL ) continuous Element of bool [: the carrier of (),REAL:]
proj2 | C 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:]
lower_bound () is V11() real ext-real Element of REAL
() .: the carrier of (() | C) is non empty V147() V148() V149() Element of bool REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

upper_bound () is V11() real ext-real Element of REAL
upper_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
|[(),()]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
K334((),(),()) is functional Element of bool the carrier of ()
K334((),(),()) /\ C is functional Element of bool the carrier of ()

proj2 | () is V21() V24( the carrier of (() | ())) V25( REAL ) Function-like V35( the carrier of (() | ()), REAL ) continuous Element of bool [: the carrier of (() | ()),REAL:]
the carrier of (() | ()) is non empty set
[: the carrier of (() | ()),REAL:] is non empty set
bool [: the carrier of (() | ()),REAL:] is non empty set
upper_bound (proj2 | ()) is V11() real ext-real Element of REAL
(proj2 | ()) .: the carrier of (() | ()) is non empty V147() V148() V149() Element of bool REAL
upper_bound ((proj2 | ()) .: the carrier of (() | ())) is V11() real ext-real Element of REAL
|[(),(upper_bound (proj2 | ()))]| is non empty V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()
Lower_Arc C is non empty functional Element of bool the carrier of ()
W-min C is V21() V24( NAT ) Function-like finite V45(2) FinSequence-like FinSubsequence-like V139() Element of the carrier of ()

lower_bound () is V11() real ext-real Element of REAL
lower_bound (() .: the carrier of (() | C)) is V11() real ext-real Element of REAL
W-most C is non empty functional closed compact Element of bool the carrier of ()

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