:: JORDAN22 semantic presentation

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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