REAL is non empty V34() V158() V159() V160() V164() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V158() V159() V160() V161() V162() V163() V164() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V34() V158() V164() set
omega is non empty epsilon-transitive epsilon-connected ordinal V158() V159() V160() V161() V162() V163() V164() set
K6(omega) is set
K6(NAT) is set
RAT is non empty V34() V158() V159() V160() V161() V164() set
INT is non empty V34() V158() V159() V160() V161() V162() V164() set
K7(COMPLEX,COMPLEX) is V148() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V148() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V148() V149() V150() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V148() V149() V150() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V23( RAT ) V148() V149() V150() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V23( RAT ) V148() V149() V150() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V23( RAT ) V23( INT ) V148() V149() V150() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V23( RAT ) V23( INT ) V148() V149() V150() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V23( RAT ) V23( INT ) V148() V149() V150() V151() set
K7(K7(NAT,NAT),NAT) is V23( RAT ) V23( INT ) V148() V149() V150() V151() set
K6(K7(K7(NAT,NAT),NAT)) is set
K295() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
K455() is non empty V107() L9()
the carrier of K455() is non empty set
K460() is non empty L9()
K461() is non empty V107() M20(K460())
K462() is non empty V107() V129() V186() M23(K460(),K461())
K464() is non empty V107() V129() V131() V133() L9()
K465() is non empty V107() V129() V186() M20(K464())
K7(1,1) is V23( RAT ) V23( INT ) V148() V149() V150() V151() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V23( RAT ) V23( INT ) V148() V149() V150() V151() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V148() V149() V150() set
K6(K7(K7(1,1),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
K7(2,2) is V23( RAT ) V23( INT ) V148() V149() V150() V151() set
K7(K7(2,2),REAL) is V148() V149() V150() set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty V69() TopSpace-like T_2 V105() V171() V203() V204() V205() V206() V207() V208() V209() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty V2() functional set
K7(NAT,REAL) is V148() V149() V150() set
K6(K7(NAT,REAL)) is set
K285( the carrier of (TOP-REAL 2)) is M9( the carrier of (TOP-REAL 2))
K7( the carrier of (TOP-REAL 2),REAL) is V148() V149() V150() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
K6( the carrier of (TOP-REAL 2)) is set
K700() is TopStruct
the carrier of K700() is set
RealSpace is strict MetrStruct
K705() is TopSpace-like T_2 TopStruct
the carrier of K705() is set
K6(K6( the carrier of (TOP-REAL 2))) is set
K636( the carrier of (TOP-REAL 2)) is Element of K6(K6( the carrier of (TOP-REAL 2)))
K7(NAT,K636( the carrier of (TOP-REAL 2))) is set
K6(K7(NAT,K636( the carrier of (TOP-REAL 2)))) is set
K7(COMPLEX,REAL) is V148() V149() V150() set
K6(K7(COMPLEX,REAL)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V32() V158() V159() V160() V161() V162() V163() V164() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V32() V49() V158() V159() V160() V161() V162() V163() V164() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
proj2 is V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) Function-like V46( the carrier of (TOP-REAL 2), REAL ) V148() V149() V150() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
C is V11() real ext-real set
x is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: x is V158() V159() V160() Element of K6(REAL)
x is set
proj2 . x is V11() real ext-real set
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Upper_Appr C is V19() V22( NAT ) V23(K636( the carrier of (TOP-REAL 2))) Function-like V46( NAT ,K636( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K636( the carrier of (TOP-REAL 2))))
Cage (C,0) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (C,0)) is functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (C,0))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Upper_Appr C) . x is functional Element of K636( the carrier of (TOP-REAL 2))
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (C,x))) is non empty functional closed bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Lower_Appr C is V19() V22( NAT ) V23(K636( the carrier of (TOP-REAL 2))) Function-like V46( NAT ,K636( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K636( the carrier of (TOP-REAL 2))))
Cage (C,0) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (C,0)) is functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (C,0))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Lower_Appr C) . x is functional Element of K636( the carrier of (TOP-REAL 2))
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (C,x))) is non empty functional closed bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc C is non empty functional closed bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
W-min C is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
E-max C is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
Lower_Arc C is non empty functional closed bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
E-max C is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
W-min C is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Upper_Appr C is V19() V22( NAT ) V23(K636( the carrier of (TOP-REAL 2))) Function-like V46( NAT ,K636( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K636( the carrier of (TOP-REAL 2))))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Upper_Appr C) . x is functional Element of K636( the carrier of (TOP-REAL 2))
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (C,x))) is non empty functional closed connected bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Lower_Appr C is V19() V22( NAT ) V23(K636( the carrier of (TOP-REAL 2))) Function-like V46( NAT ,K636( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K636( the carrier of (TOP-REAL 2))))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Lower_Appr C) . x is functional Element of K636( the carrier of (TOP-REAL 2))
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (C,x))) is non empty functional closed connected bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
North_Arc C is functional Element of K6( the carrier of (TOP-REAL 2))
Upper_Appr C is V19() V22( NAT ) V23(K636( the carrier of (TOP-REAL 2))) Function-like V46( NAT ,K636( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K636( the carrier of (TOP-REAL 2))))
Cage (C,0) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (C,0)) is functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (C,0))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Upper_Appr C) . x is functional Element of K636( the carrier of (TOP-REAL 2))
Lim_inf (Upper_Appr C) is functional Element of K6( the carrier of (TOP-REAL 2))
South_Arc C is functional Element of K6( the carrier of (TOP-REAL 2))
Lower_Appr C is V19() V22( NAT ) V23(K636( the carrier of (TOP-REAL 2))) Function-like V46( NAT ,K636( the carrier of (TOP-REAL 2))) Element of K6(K7(NAT,K636( the carrier of (TOP-REAL 2))))
Cage (C,0) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (C,0)) is functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (C,0))) is functional closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Lower_Appr C) . x is functional Element of K636( the carrier of (TOP-REAL 2))
Lim_inf (Lower_Appr C) is functional Element of K6( the carrier of (TOP-REAL 2))
dom proj2 is functional Element of K6( the carrier of (TOP-REAL 2))
C is non empty functional Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[1,1] is Element of K7(NAT,NAT)
{1,1} is non empty V158() V159() V160() V161() V162() V163() set
{1} is non empty V158() V159() V160() V161() V162() V163() set
{{1,1},{1}} is non empty set
C is non empty functional Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Indices (Gauge (C,x)) is set
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
width (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[1,2] is Element of K7(NAT,NAT)
{1,2} is non empty V158() V159() V160() V161() V162() V163() set
{{1,2},{1}} is non empty set
C is non empty functional Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Indices (Gauge (C,x)) is set
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
width (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[2,1] is Element of K7(NAT,NAT)
{2,1} is non empty V158() V159() V160() V161() V162() V163() set
{2} is non empty V158() V159() V160() V161() V162() V163() set
{{2,1},{2}} is non empty set
C is non empty functional Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Indices (Gauge (C,x)) is set
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
width (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[C,e] is Element of K7(NAT,NAT)
{C,e} is non empty V158() V159() V160() V161() V162() V163() set
{C} is non empty V158() V159() V160() V161() V162() V163() set
{{C,e},{C}} is non empty set
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[C,(e + 1)] is Element of K7(NAT,NAT)
{C,(e + 1)} is non empty V158() V159() V160() V161() V162() V163() set
{{C,(e + 1)},{C}} is non empty set
A is non empty functional closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Gauge (A,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Indices (Gauge (A,x)) is set
(Gauge (A,x)) * (C,e) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (A,x)) * (C,(e + 1)) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (A,x)) * (C,e)),((Gauge (A,x)) * (C,(e + 1)))) is V11() real ext-real Element of REAL
Gauge (A,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (A,x)) * (C,e) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (A,x)) * (C,(e + 1)) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (A,x)) * (C,e)),((Gauge (A,x)) * (C,(e + 1)))) is V11() real ext-real Element of REAL
len (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
len (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
width (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
width (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
N-bound A is V11() real ext-real Element of REAL
S-bound A is V11() real ext-real Element of REAL
(N-bound A) - (S-bound A) is V11() real ext-real Element of REAL
Indices (Gauge (A,x)) is set
2 |^ x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
((N-bound A) - (S-bound A)) / (2 |^ x) is V11() real ext-real Element of COMPLEX
2 |^ x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
((N-bound A) - (S-bound A)) / (2 |^ x) is V11() real ext-real Element of COMPLEX
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is non empty functional closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Gauge (x,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (x,x)) * (1,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (x,x)) * (1,2) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,x)) * (1,1)),((Gauge (x,x)) * (1,2))) is V11() real ext-real Element of REAL
Gauge (x,C) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (x,C)) * (1,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (x,C)) * (1,2) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,C)) * (1,1)),((Gauge (x,C)) * (1,2))) is V11() real ext-real Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[1,(1 + 1)] is Element of K7(NAT,NAT)
{1,(1 + 1)} is non empty V158() V159() V160() V161() V162() V163() set
{{1,(1 + 1)},{1}} is non empty set
Indices (Gauge (x,x)) is set
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[C,e] is Element of K7(NAT,NAT)
{C,e} is non empty V158() V159() V160() V161() V162() V163() set
{C} is non empty V158() V159() V160() V161() V162() V163() set
{{C,e},{C}} is non empty set
[(C + 1),e] is Element of K7(NAT,NAT)
{(C + 1),e} is non empty V158() V159() V160() V161() V162() V163() set
{(C + 1)} is non empty V158() V159() V160() V161() V162() V163() set
{{(C + 1),e},{(C + 1)}} is non empty set
A is non empty functional closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Gauge (A,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Indices (Gauge (A,x)) is set
(Gauge (A,x)) * (C,e) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (A,x)) * ((C + 1),e) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (A,x)) * (C,e)),((Gauge (A,x)) * ((C + 1),e))) is V11() real ext-real Element of REAL
Gauge (A,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (A,x)) * (C,e) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (A,x)) * ((C + 1),e) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (A,x)) * (C,e)),((Gauge (A,x)) * ((C + 1),e))) is V11() real ext-real Element of REAL
len (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
len (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
E-bound A is V11() real ext-real Element of REAL
W-bound A is V11() real ext-real Element of REAL
(E-bound A) - (W-bound A) is V11() real ext-real Element of REAL
width (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
width (Gauge (A,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Indices (Gauge (A,x)) is set
2 |^ x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
((E-bound A) - (W-bound A)) / (2 |^ x) is V11() real ext-real Element of COMPLEX
2 |^ x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
((E-bound A) - (W-bound A)) / (2 |^ x) is V11() real ext-real Element of COMPLEX
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is non empty functional closed bounded compact non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Gauge (x,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (x,x)) * (1,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (x,x)) * (2,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,x)) * (1,1)),((Gauge (x,x)) * (2,1))) is V11() real ext-real Element of REAL
Gauge (x,C) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (x,C)) * (1,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (x,C)) * (2,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (x,C)) * (1,1)),((Gauge (x,C)) * (2,1))) is V11() real ext-real Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
[(1 + 1),1] is Element of K7(NAT,NAT)
{(1 + 1),1} is non empty V158() V159() V160() V161() V162() V163() set
{(1 + 1)} is non empty V158() V159() V160() V161() V162() V163() set
{{(1 + 1),1},{(1 + 1)}} is non empty set
Indices (Gauge (x,x)) is set
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
x is V11() real ext-real set
e is V11() real ext-real set
A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Gauge (C,A) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (C,A)) * (1,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (C,A)) * (1,2) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,A)) * (1,1)),((Gauge (C,A)) * (1,2))) is V11() real ext-real Element of REAL
(Gauge (C,A)) * (2,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,A)) * (1,1)),((Gauge (C,A)) * (2,1))) is V11() real ext-real Element of REAL
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Gauge (C,(x + 1)) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (C,(x + 1))) * (1,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (C,(x + 1))) * (1,2) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,(x + 1))) * (1,1)),((Gauge (C,(x + 1))) * (1,2))) is V11() real ext-real Element of REAL
(Gauge (C,(x + 1))) * (2,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,(x + 1))) * (1,1)),((Gauge (C,(x + 1))) * (2,1))) is V11() real ext-real Element of REAL
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
(Gauge (C,x)) * (1,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(Gauge (C,x)) * (2,1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,x)) * (1,1)),((Gauge (C,x)) * (2,1))) is V11() real ext-real Element of REAL
(Gauge (C,x)) * (1,2) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
dist (((Gauge (C,x)) * (1,1)),((Gauge (C,x)) * (1,2))) is V11() real ext-real Element of REAL
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Center (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))) is non empty functional closed closed connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))))) is V158() V159() V160() Element of K6(REAL)
upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))))) is V11() real ext-real Element of REAL
E-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
W-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
(E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))) is V158() V159() V160() Element of K6(REAL)
upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))) is V11() real ext-real Element of REAL
width (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
((Gauge (C,x)) * ((Center (Gauge (C,x))),1)) `1 is V11() real ext-real Element of REAL
W-bound C is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of REAL
(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL
((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of COMPLEX
(W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Upper_Arc (L~ (Cage (C,x))) is non empty functional closed connected bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))) `1 is V11() real ext-real Element of REAL
(L~ (Cage (C,x))) /\ (L~ (Cage (C,x))) is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ (Cage (C,x))) /\ (L~ (Cage (C,x)))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))) is functional Element of K6( the carrier of (TOP-REAL 2))
r is V11() real ext-real set
r is V11() real ext-real set
(upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))))) - r is V11() real ext-real Element of REAL
k is V11() real ext-real set
k is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
proj2 . k is V11() real ext-real Element of REAL
k `1 is V11() real ext-real Element of REAL
GoB (Cage (C,x)) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
((Gauge (C,x)) * ((Center (Gauge (C,x))),1)) `2 is V11() real ext-real Element of REAL
k `2 is V11() real ext-real Element of REAL
((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))) `2 is V11() real ext-real Element of REAL
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Center (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))) is non empty functional closed closed connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))))) is V158() V159() V160() Element of K6(REAL)
lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))))) is V11() real ext-real Element of REAL
E-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
W-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
(E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))) is V158() V159() V160() Element of K6(REAL)
lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))) is V11() real ext-real Element of REAL
width (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
((Gauge (C,x)) * ((Center (Gauge (C,x))),1)) `1 is V11() real ext-real Element of REAL
W-bound C is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of REAL
(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL
((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of COMPLEX
(W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Upper_Arc (L~ (Cage (C,x))) is non empty functional closed connected bounded compact with_the_max_arc Element of K6( the carrier of (TOP-REAL 2))
((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))) `1 is V11() real ext-real Element of REAL
(L~ (Cage (C,x))) /\ (L~ (Cage (C,x))) is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ (Cage (C,x))) /\ (L~ (Cage (C,x)))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))) is functional Element of K6( the carrier of (TOP-REAL 2))
r is V11() real ext-real set
r is V11() real ext-real set
(lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))))) + r is V11() real ext-real Element of REAL
k is V11() real ext-real set
k is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
proj2 . k is V11() real ext-real Element of REAL
k `1 is V11() real ext-real Element of REAL
GoB (Cage (C,x)) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
((Gauge (C,x)) * ((Center (Gauge (C,x))),1)) `2 is V11() real ext-real Element of REAL
k `2 is V11() real ext-real Element of REAL
((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))) `2 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
UMP (L~ (Cage (C,x))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
W-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
(E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))) is V158() V159() V160() Element of K6(REAL)
upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Center (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))) is non empty functional closed closed connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))))) is V158() V159() V160() Element of K6(REAL)
upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))))) is V11() real ext-real Element of REAL
|[(((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
LMP (L~ (Cage (C,x))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
W-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
(E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))) is V158() V159() V160() Element of K6(REAL)
lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
Center (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),1) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
(Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))) is non empty functional closed closed connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x)))))))) is V158() V159() V160() Element of K6(REAL)
lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))))) is V11() real ext-real Element of REAL
|[(((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (LSeg (((Gauge (C,x)) * ((Center (Gauge (C,x))),1)),((Gauge (C,x)) * ((Center (Gauge (C,x))),(len (Gauge (C,x))))))))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
UMP C is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
E-bound C is V11() real ext-real Element of REAL
W-bound C is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound C) + (W-bound C)) / 2 } is set
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V158() V159() V160() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(UMP C) `2 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
UMP (L~ (Cage (C,x))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
W-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
(E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))) is V158() V159() V160() Element of K6(REAL)
upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(UMP (L~ (Cage (C,x)))) `2 is V11() real ext-real Element of REAL
(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL
((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of COMPLEX
(UMP C) `1 is V11() real ext-real Element of REAL
|[((UMP C) `1),((UMP C) `2)]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(UMP (L~ (Cage (C,x)))) `1 is V11() real ext-real Element of REAL
|[((UMP (L~ (Cage (C,x)))) `1),((UMP (L~ (Cage (C,x)))) `2)]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((W-bound C) + (E-bound C)) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V158() V159() V160() Element of K6(REAL)
upper_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
north_halfline (UMP (L~ (Cage (C,x)))) is non empty functional connected convex Element of K6( the carrier of (TOP-REAL 2))
{(UMP (L~ (Cage (C,x))))} is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(north_halfline (UMP (L~ (Cage (C,x))))) \ {(UMP (L~ (Cage (C,x))))} is functional Element of K6( the carrier of (TOP-REAL 2))
m is set
OO is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
OO `2 is V11() real ext-real Element of REAL
OO `1 is V11() real ext-real Element of REAL
proj2 . OO is V11() real ext-real Element of REAL
UBD (L~ (Cage (C,x))) is non empty functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,x))) is functional open Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
LMP C is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
E-bound C is V11() real ext-real Element of REAL
W-bound C is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound C) + (W-bound C)) / 2 } is set
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V158() V159() V160() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(LMP C) `2 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Cage (C,x) is non empty V2() V19() V22( NAT ) V23( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard V272() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,x)) is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
LMP (L~ (Cage (C,x))) is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
W-bound (L~ (Cage (C,x))) is V11() real ext-real Element of REAL
(E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2))) is V158() V159() V160() Element of K6(REAL)
lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,x)))) + (W-bound (L~ (Cage (C,x))))) / 2)))))]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(LMP (L~ (Cage (C,x)))) `2 is V11() real ext-real Element of REAL
(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL
((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of COMPLEX
(LMP C) `1 is V11() real ext-real Element of REAL
|[((LMP C) `1),((LMP C) `2)]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(LMP (L~ (Cage (C,x)))) `1 is V11() real ext-real Element of REAL
|[((LMP (L~ (Cage (C,x)))) `1),((LMP (L~ (Cage (C,x)))) `2)]| is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
(W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x)))) is V11() real ext-real Element of REAL
((W-bound (L~ (Cage (C,x)))) + (E-bound (L~ (Cage (C,x))))) / 2 is V11() real ext-real Element of COMPLEX
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((W-bound C) + (E-bound C)) / 2 } is set
(L~ (Cage (C,x))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V158() V159() V160() Element of K6(REAL)
lower_bound (proj2 .: ((L~ (Cage (C,x))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
south_halfline (LMP (L~ (Cage (C,x)))) is non empty functional connected convex Element of K6( the carrier of (TOP-REAL 2))
{(LMP (L~ (Cage (C,x))))} is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(south_halfline (LMP (L~ (Cage (C,x))))) \ {(LMP (L~ (Cage (C,x))))} is functional Element of K6( the carrier of (TOP-REAL 2))
m is set
OO is V19() Function-like V41(2) FinSequence-like V148() V149() V150() Element of the carrier of (TOP-REAL 2)
OO `2 is V11() real ext-real Element of REAL
OO `1 is V11() real ext-real Element of REAL
proj2 . OO is V11() real ext-real Element of REAL
UBD (L~ (Cage (C,x))) is non empty functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,x))) is functional open Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty functional open connected V224( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
C is non empty functional closed connected bounded being_simple_closed_curve compact with_the_max_arc non horizontal non vertical Element of K6( the carrier of (TOP-REAL 2))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Gauge (C,x) is V19() non empty-yielding V22( NAT ) V23(K285( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K285( the carrier of (TOP-REAL 2))
len (Gauge (C,x)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V32() V49() V158() V159() V160() V161() V162() V163() Element of NAT
Cage (C