JORDAN11

:: JORDAN11 semantic presentation

REAL is non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval set
NAT is non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below Element of K6(REAL)
K6(REAL) is non empty set
COMPLEX is non empty V34() V130() V136() set
omega is non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below set
K6(omega) is non empty set
K6(NAT) is non empty set
RAT is non empty V34() V130() V131() V132() V133() V136() set
INT is non empty V34() V130() V131() V132() V133() V134() V136() set
K7(COMPLEX,COMPLEX) is non empty V120() set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V120() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K7(REAL,REAL) is non empty V120() V121() V122() set
K6(K7(REAL,REAL)) is non empty set
K7(K7(REAL,REAL),REAL) is non empty V120() V121() V122() set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
K7(RAT,RAT) is non empty V25( RAT ) V120() V121() V122() set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is non empty V25( RAT ) V120() V121() V122() set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is non empty V25( RAT ) V25( INT ) V120() V121() V122() set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is non empty V25( RAT ) V25( INT ) V120() V121() V122() set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is non empty V25( RAT ) V25( INT ) V120() V121() V122() V123() set
K7(K7(NAT,NAT),NAT) is non empty V25( RAT ) V25( INT ) V120() V121() V122() V123() set
K6(K7(K7(NAT,NAT),NAT)) is non empty set
K302() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
K7(1,1) is non empty V25( RAT ) V25( INT ) V120() V121() V122() V123() set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty V25( RAT ) V25( INT ) V120() V121() V122() V123() set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is non empty V120() V121() V122() set
K6(K7(K7(1,1),REAL)) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
K7(2,2) is non empty V25( RAT ) V25( INT ) V120() V121() V122() V123() set
K7(K7(2,2),REAL) is non empty V120() V121() V122() set
K6(K7(K7(2,2),REAL)) is non empty set
TOP-REAL 2 is non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty V29() set
K7( the carrier of (TOP-REAL 2),REAL) is non empty V120() V121() V122() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is non empty set
K6( the carrier of (TOP-REAL 2)) is non empty set
K646() is TopStruct
the carrier of K646() is set
RealSpace is strict MetrStruct
K651() is TopSpace-like T_2 TopStruct
the carrier of K651() is set
K292( the carrier of (TOP-REAL 2)) is M9( the carrier of (TOP-REAL 2))
K6(K6( the carrier of (TOP-REAL 2))) is non empty set
K7(COMPLEX,REAL) is non empty V120() V121() V122() set
K6(K7(COMPLEX,REAL)) is non empty set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer ext-real non positive non negative V130() V131() V132() V133() V134() V135() V136() bounded_below interval set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer ext-real non positive non negative V130() V131() V132() V133() V134() V135() V136() bounded_below interval set
0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
proj2 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) V26() V46( the carrier of (TOP-REAL 2), REAL ) V120() V121() V122() V195( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj1 is V21() V24( the carrier of (TOP-REAL 2)) V25( REAL ) V26() V46( the carrier of (TOP-REAL 2), REAL ) V120() V121() V122() V195( TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
K7(NAT,K6(REAL)) is non empty set
K6(K7(NAT,K6(REAL))) is non empty set
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid 2) is non empty set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
p is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Gauge (p,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
width (Gauge (p,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Center (Gauge (p,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (p,n)) * ((Center (Gauge (p,n))),C) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(Gauge (p,n)) * ((Center (Gauge (p,n))),e) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
Cage (p,n) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (p,n)) is non empty proper closed V91( TOP-REAL 2) connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (p,n))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e)))) /\ (Upper_Arc (L~ (Cage (p,n)))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
{((Gauge (p,n)) * ((Center (Gauge (p,n))),C))} is set
Lower_Arc (L~ (Cage (p,n))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e)))) /\ (Lower_Arc (L~ (Cage (p,n)))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
{((Gauge (p,n)) * ((Center (Gauge (p,n))),e))} is set
RightComp (Cage (p,n)) is Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (p,n))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (p,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
len (Gauge (p,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
[(Center (Gauge (p,n))),C] is set
{(Center (Gauge (p,n))),C} is V130() V131() V132() V133() V134() V135() bounded_below set
{(Center (Gauge (p,n)))} is V130() V131() V132() V133() V134() V135() bounded_below set
{{(Center (Gauge (p,n))),C},{(Center (Gauge (p,n)))}} is set
Indices (Gauge (p,n)) is set
Upper_Seq (p,n) is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (Upper_Seq (p,n)) is V91( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
[(Center (Gauge (p,n))),e] is set
{(Center (Gauge (p,n))),e} is V130() V131() V132() V133() V134() V135() bounded_below set
{{(Center (Gauge (p,n))),e},{(Center (Gauge (p,n)))}} is set
Lower_Seq (p,n) is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (Lower_Seq (p,n)) is V91( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e))} is set
(LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e)))) \ {((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e))} is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e)))) /\ (L~ (Cage (p,n))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc (L~ (Cage (p,n)))) \/ (Lower_Arc (L~ (Cage (p,n)))) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e)))) /\ ((Upper_Arc (L~ (Cage (p,n)))) \/ (Lower_Arc (L~ (Cage (p,n))))) is Element of K6( the carrier of (TOP-REAL 2))
((LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e)))) /\ (Upper_Arc (L~ (Cage (p,n))))) \/ ((LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),C)),((Gauge (p,n)) * ((Center (Gauge (p,n))),e)))) /\ (Lower_Arc (L~ (Cage (p,n))))) is Element of K6( the carrier of (TOP-REAL 2))
(L~ (Cage (p,n))) ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ (L~ (Cage (p,n))) is set
LSeg (((Gauge (p,n)) * ((Center (Gauge (p,n))),e)),((Gauge (p,n)) * ((Center (Gauge (p,n))),C))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc p is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
{((Gauge (p,n)) * ((Center (Gauge (p,n))),C))} \/ {((Gauge (p,n)) * ((Center (Gauge (p,n))),e))} is set
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
W-bound n is V11() real ext-real Element of REAL
(TOP-REAL 2) | n is strict T_2 compact SubSpace of TOP-REAL 2
proj1 | n is V21() V24( the carrier of ((TOP-REAL 2) | n)) V25( REAL ) V26() V46( the carrier of ((TOP-REAL 2) | n), REAL ) V120() V121() V122() V195((TOP-REAL 2) | n) Element of K6(K7( the carrier of ((TOP-REAL 2) | n),REAL))
the carrier of ((TOP-REAL 2) | n) is set
K7( the carrier of ((TOP-REAL 2) | n),REAL) is V120() V121() V122() set
K6(K7( the carrier of ((TOP-REAL 2) | n),REAL)) is non empty set
lower_bound (proj1 | n) is V11() real ext-real Element of REAL
(proj1 | n) .: the carrier of ((TOP-REAL 2) | n) is V130() V131() V132() Element of K6(REAL)
lower_bound ((proj1 | n) .: the carrier of ((TOP-REAL 2) | n)) is V11() real ext-real Element of REAL
E-bound n is V11() real ext-real Element of REAL
upper_bound (proj1 | n) is V11() real ext-real Element of REAL
upper_bound ((proj1 | n) .: the carrier of ((TOP-REAL 2) | n)) is V11() real ext-real Element of REAL
(W-bound n) + (E-bound n) is V11() real ext-real Element of REAL
((W-bound n) + (E-bound n)) / 2 is V11() real ext-real Element of REAL
Gauge (n,1) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
X-SpanStart (n,1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (1 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (1 -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
len (Gauge (n,1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1)))) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(Gauge (n,1)) * ((X-SpanStart (n,1)),1) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
width (Gauge (n,1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Center (Gauge (n,1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(len (Gauge (n,1))) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
((len (Gauge (n,1))) div 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
((Gauge (n,1)) * ((X-SpanStart (n,1)),1)) `1 is V11() real ext-real Element of REAL
Vertical_Line (((W-bound n) + (E-bound n)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
(len (Gauge (n,1))) div 2 is V11() real integer ext-real set
((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))) `2 is V11() real ext-real Element of REAL
((Gauge (n,1)) * ((X-SpanStart (n,1)),1)) `2 is V11() real ext-real Element of REAL
proj2 . ((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))) is V11() real ext-real Element of REAL
proj2 . ((Gauge (n,1)) * ((X-SpanStart (n,1)),1)) is V11() real ext-real Element of REAL
LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc n is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Upper_Arc n) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc n is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Lower_Arc n) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1)))))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
K7(NAT,REAL) is non empty V120() V121() V122() set
K6(K7(NAT,REAL)) is non empty set
C9 is V21() V24( NAT ) V25( REAL ) V26() V46( NAT , REAL ) V120() V121() V122() Element of K6(K7(NAT,REAL))
proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Upper_Arc n)) is V130() V131() V132() Element of K6(REAL)
proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Lower_Arc n)) is V130() V131() V132() Element of K6(REAL)
K7(NAT, the carrier of (TOP-REAL 2)) is non empty set
K6(K7(NAT, the carrier of (TOP-REAL 2))) is non empty set
r3 is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V46( NAT , the carrier of (TOP-REAL 2)) Element of K6(K7(NAT, the carrier of (TOP-REAL 2)))
((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))) `1 is V11() real ext-real Element of REAL
D9 is compact V130() V131() V132() Element of K6(REAL)
x3 is compact V130() V131() V132() Element of K6(REAL)
Fs is set
F is V11() real ext-real Element of REAL
S is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . S is V11() real ext-real Element of REAL
r is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . r is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
r `2 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
r `1 is V11() real ext-real Element of REAL
(Upper_Arc n) /\ (Lower_Arc n) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
W-min n is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
W-most n is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
SW-corner n is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
S-bound n is V11() real ext-real Element of REAL
proj2 | n is V21() V24( the carrier of ((TOP-REAL 2) | n)) V25( REAL ) V26() V46( the carrier of ((TOP-REAL 2) | n), REAL ) V120() V121() V122() V195((TOP-REAL 2) | n) Element of K6(K7( the carrier of ((TOP-REAL 2) | n),REAL))
lower_bound (proj2 | n) is V11() real ext-real Element of REAL
(proj2 | n) .: the carrier of ((TOP-REAL 2) | n) is V130() V131() V132() Element of K6(REAL)
lower_bound ((proj2 | n) .: the carrier of ((TOP-REAL 2) | n)) is V11() real ext-real Element of REAL
|[(W-bound n),(S-bound n)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
NW-corner n is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
N-bound n is V11() real ext-real Element of REAL
upper_bound (proj2 | n) is V11() real ext-real Element of REAL
upper_bound ((proj2 | n) .: the carrier of ((TOP-REAL 2) | n)) is V11() real ext-real Element of REAL
|[(W-bound n),(N-bound n)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner n),(NW-corner n)) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact V234() convex Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner n),(NW-corner n))) /\ n is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most n) is strict T_2 compact SubSpace of TOP-REAL 2
proj2 | (W-most n) is V21() V24( the carrier of ((TOP-REAL 2) | (W-most n))) V25( REAL ) V26() V46( the carrier of ((TOP-REAL 2) | (W-most n)), REAL ) V120() V121() V122() V195((TOP-REAL 2) | (W-most n)) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most n)),REAL))
the carrier of ((TOP-REAL 2) | (W-most n)) is set
K7( the carrier of ((TOP-REAL 2) | (W-most n)),REAL) is V120() V121() V122() set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most n)),REAL)) is non empty set
lower_bound (proj2 | (W-most n)) is V11() real ext-real Element of REAL
(proj2 | (W-most n)) .: the carrier of ((TOP-REAL 2) | (W-most n)) is V130() V131() V132() Element of K6(REAL)
lower_bound ((proj2 | (W-most n)) .: the carrier of ((TOP-REAL 2) | (W-most n))) is V11() real ext-real Element of REAL
|[(W-bound n),(lower_bound (proj2 | (W-most n)))]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
E-max n is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
E-most n is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
SE-corner n is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
|[(E-bound n),(S-bound n)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
NE-corner n is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
|[(E-bound n),(N-bound n)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner n),(NE-corner n)) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact V234() convex Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner n),(NE-corner n))) /\ n is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most n) is strict T_2 compact SubSpace of TOP-REAL 2
proj2 | (E-most n) is V21() V24( the carrier of ((TOP-REAL 2) | (E-most n))) V25( REAL ) V26() V46( the carrier of ((TOP-REAL 2) | (E-most n)), REAL ) V120() V121() V122() V195((TOP-REAL 2) | (E-most n)) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most n)),REAL))
the carrier of ((TOP-REAL 2) | (E-most n)) is set
K7( the carrier of ((TOP-REAL 2) | (E-most n)),REAL) is V120() V121() V122() set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most n)),REAL)) is non empty set
upper_bound (proj2 | (E-most n)) is V11() real ext-real Element of REAL
(proj2 | (E-most n)) .: the carrier of ((TOP-REAL 2) | (E-most n)) is V130() V131() V132() Element of K6(REAL)
upper_bound ((proj2 | (E-most n)) .: the carrier of ((TOP-REAL 2) | (E-most n))) is V11() real ext-real Element of REAL
|[(E-bound n),(upper_bound (proj2 | (E-most n)))]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
{(W-min n),(E-max n)} is set
(W-min n) `1 is V11() real ext-real Element of REAL
(E-max n) `1 is V11() real ext-real Element of REAL
Fs is V21() V24( NAT ) V25( REAL ) V26() V46( NAT , REAL ) V120() V121() V122() Element of K6(K7(NAT,REAL))
F is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V46( NAT , the carrier of (TOP-REAL 2)) Element of K6(K7(NAT, the carrier of (TOP-REAL 2)))
bool REAL is non empty Element of K6(K6(REAL))
K6(K6(REAL)) is non empty set
K7(NAT,(bool REAL)) is non empty set
K6(K7(NAT,(bool REAL))) is non empty set
S is V21() V24( NAT ) V25( bool REAL) V26() V46( NAT , bool REAL) Element of K6(K7(NAT,(bool REAL)))
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
r3 . r is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Cage (n,(r + 1)) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (n,(r + 1))) is non empty proper closed V91( TOP-REAL 2) connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (n,(r + 1)))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
p is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: p is V130() V131() V132() Element of K6(REAL)
dom proj2 is Element of K6( the carrier of (TOP-REAL 2))
(dom proj2) /\ p is Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (n,(r + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(r + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((r + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((r + 1) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Gauge (n,(r + 1)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
Center (Gauge (n,(r + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(r + 1))) * ((X-SpanStart (n,(r + 1))),1) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
len (Gauge (n,(r + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(r + 1))) * ((X-SpanStart (n,(r + 1))),(len (Gauge (n,(r + 1))))) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,(r + 1))) * ((X-SpanStart (n,(r + 1))),1)),((Gauge (n,(r + 1))) * ((X-SpanStart (n,(r + 1))),(len (Gauge (n,(r + 1))))))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
n is compact V130() V131() V132() Element of K6(REAL)
C9 . r is V11() real ext-real Element of REAL
lower_bound n is V11() real ext-real Element of REAL
i is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . i is V11() real ext-real Element of REAL
|[(((W-bound n) + (E-bound n)) / 2),(C9 . r)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(r3 . r) `2 is V11() real ext-real Element of REAL
i `2 is V11() real ext-real Element of REAL
(r3 . r) `1 is V11() real ext-real Element of REAL
i `1 is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
F . r is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Cage (n,(r + 1)) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (n,(r + 1))) is non empty proper closed V91( TOP-REAL 2) connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (n,(r + 1)))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (n,(r + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(r + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((r + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((r + 1) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Gauge (n,(r + 1)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
Center (Gauge (n,(r + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
r3 . r is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . r)) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . r))) /\ (Lower_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
p is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: p is V130() V131() V132() Element of K6(REAL)
Upper_Arc (L~ (Cage (n,(r + 1)))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
dom proj2 is Element of K6( the carrier of (TOP-REAL 2))
(dom proj2) /\ p is Element of K6( the carrier of (TOP-REAL 2))
C9 . r is V11() real ext-real Element of REAL
|[(((W-bound n) + (E-bound n)) / 2),(C9 . r)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(r3 . r) `1 is V11() real ext-real Element of REAL
LSeg ((r3 . r),((Gauge (n,1)) * ((X-SpanStart (n,1)),1))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(r3 . r) `2 is V11() real ext-real Element of REAL
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(r + 1)))))) is V130() V131() V132() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))))) is V11() real ext-real Element of REAL
width (Gauge (n,(r + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(r + 1))) * ((X-SpanStart (n,(r + 1))),i) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
n is compact V130() V131() V132() Element of K6(REAL)
Fs . r is V11() real ext-real Element of REAL
upper_bound n is V11() real ext-real Element of REAL
i is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . i is V11() real ext-real Element of REAL
|[(((W-bound n) + (E-bound n)) / 2),(Fs . r)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(F . r) `2 is V11() real ext-real Element of REAL
i `2 is V11() real ext-real Element of REAL
(F . r) `1 is V11() real ext-real Element of REAL
i `1 is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
S . r is V130() V131() V132() Element of bool REAL
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Cage (n,(r + 1)) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (n,(r + 1))) is non empty proper closed V91( TOP-REAL 2) connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (n,(r + 1)))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
r is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: r is V130() V131() V132() Element of K6(REAL)
X-SpanStart (n,(r + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(r + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((r + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((r + 1) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Gauge (n,(r + 1)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
Center (Gauge (n,(r + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
dom proj2 is Element of K6( the carrier of (TOP-REAL 2))
(dom proj2) /\ r is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),1) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
len (Gauge (n,(r + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),(len (Gauge (n,(r + 1))))) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),1)),((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),(len (Gauge (n,(r + 1))))))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
p is compact V130() V131() V132() Element of K6(REAL)
C9 . r is V11() real ext-real Element of REAL
lower_bound p is V11() real ext-real Element of REAL
n is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . n is V11() real ext-real Element of REAL
r3 . r is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . r)) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (n,(r + 1)))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . r))) /\ (Lower_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
i is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: i is V130() V131() V132() Element of K6(REAL)
(dom proj2) /\ i is Element of K6( the carrier of (TOP-REAL 2))
|[(((W-bound n) + (E-bound n)) / 2),(C9 . r)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(r3 . r) `1 is V11() real ext-real Element of REAL
F . r is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
Fs . r is V11() real ext-real Element of REAL
|[(((W-bound n) + (E-bound n)) / 2),(Fs . r)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(F . r) `1 is V11() real ext-real Element of REAL
(F . r) `2 is V11() real ext-real Element of REAL
proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . r))) /\ (Lower_Arc (L~ (Cage (n,(r + 1)))))) is V130() V131() V132() Element of K6(REAL)
upper_bound (proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . r))) /\ (Lower_Arc (L~ (Cage (n,(r + 1))))))) is V11() real ext-real Element of REAL
(r3 . r) `2 is V11() real ext-real Element of REAL
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(r + 1)))))) is V130() V131() V132() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))))) is V11() real ext-real Element of REAL
width (Gauge (n,(r + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
c₂₂ is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(r + 1))) * ((X-SpanStart (n,(r + 1))),c₂₂) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
CC is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),CC) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
W is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(r + 1))) * ((X-SpanStart (n,(r + 1))),W) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
j is compact V130() V131() V132() Element of K6(REAL)
n `2 is V11() real ext-real Element of REAL
W is V11() real ext-real set
E0 is set
proj2 . E0 is V11() real ext-real Element of REAL
DD is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
DD `2 is V11() real ext-real Element of REAL
upper_bound j is V11() real ext-real Element of REAL
n `1 is V11() real ext-real Element of REAL
W is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . W is V11() real ext-real Element of REAL
W `2 is V11() real ext-real Element of REAL
LSeg ((r3 . r),((Gauge (n,1)) * ((X-SpanStart (n,1)),1))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
W `1 is V11() real ext-real Element of REAL
LSeg ((r3 . r),(F . r)) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((r3 . r),(F . r))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
E0 is set
DD is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: DD is V130() V131() V132() Element of K6(REAL)
dd is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . dd is V11() real ext-real Element of REAL
D is compact V130() V131() V132() Element of K6(REAL)
dd `2 is V11() real ext-real Element of REAL
lower_bound D is V11() real ext-real Element of REAL
dd `1 is V11() real ext-real Element of REAL
(Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),c₂₂) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),CC)),((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),c₂₂))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),CC)),((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),c₂₂)))) /\ (Upper_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
{((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),c₂₂))} is set
E0 is set
E0 is set
(LSeg ((r3 . r),(F . r))) /\ (Lower_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
E0 is set
DD is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: DD is V130() V131() V132() Element of K6(REAL)
dd is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . dd is V11() real ext-real Element of REAL
D is compact V130() V131() V132() Element of K6(REAL)
dd `2 is V11() real ext-real Element of REAL
upper_bound D is V11() real ext-real Element of REAL
dd `1 is V11() real ext-real Element of REAL
proj2 .: (LSeg ((r3 . r),(F . r))) is V130() V131() V132() Element of K6(REAL)
(LSeg (((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),CC)),((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),c₂₂)))) /\ (Lower_Arc (L~ (Cage (n,(r + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
{((Gauge (n,(r + 1))) * ((Center (Gauge (n,(r + 1)))),CC))} is set
E0 is set
E0 is set
proj2 .: (LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) is V130() V131() V132() Element of K6(REAL)
[.(proj2 . ((Gauge (n,1)) * ((X-SpanStart (n,1)),1))),(proj2 . ((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1)))))).] is compact V130() V131() V132() interval Element of K6(REAL)
D9 \/ x3 is V130() V131() V132() Element of K6(REAL)
r is V11() real ext-real set
r is V11() real ext-real Element of REAL
|[(((W-bound n) + (E-bound n)) / 2),r]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
|[(((W-bound n) + (E-bound n)) / 2),r]| `1 is V11() real ext-real Element of REAL
BDD-Family n is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
n is set
{ (Cl (BDD (L~ (Cage (n,b₁))))) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT : verum } is set
i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Cage (n,i) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (n,i)) is non empty proper closed V91( TOP-REAL 2) connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (n,i))) is non empty open Element of K6( the carrier of (TOP-REAL 2))
Cl (BDD (L~ (Cage (n,i)))) is Element of K6( the carrier of (TOP-REAL 2))
j is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
S . j is V130() V131() V132() Element of bool REAL
F . j is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . (F . j) is V11() real ext-real Element of REAL
(F . j) `2 is V11() real ext-real Element of REAL
r3 . j is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . j)) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Cage (n,(j + 1)) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (n,(j + 1))) is non empty proper closed V91( TOP-REAL 2) connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc (L~ (Cage (n,(j + 1)))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . j))) /\ (Lower_Arc (L~ (Cage (n,(j + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
CC is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: CC is V130() V131() V132() Element of K6(REAL)
Gauge (n,(j + 1)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
Center (Gauge (n,(j + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
len (Gauge (n,(j + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
c₂₂ is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: c₂₂ is V130() V131() V132() Element of K6(REAL)
dom proj2 is Element of K6( the carrier of (TOP-REAL 2))
(dom proj2) /\ CC is Element of K6( the carrier of (TOP-REAL 2))
RightComp (Cage (n,(j + 1))) is Element of K6( the carrier of (TOP-REAL 2))
Cage (n,j) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (n,j)) is Element of K6( the carrier of (TOP-REAL 2))
RightComp (Cage (n,i)) is Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (n,(j + 1)))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
Cl (RightComp (Cage (n,i))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc (L~ (Cage (n,(j + 1)))) is non empty proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
X-SpanStart (n,(j + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(j + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((j + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((j + 1) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
proj2 . (r3 . j) is V11() real ext-real Element of REAL
(r3 . j) `2 is V11() real ext-real Element of REAL
DD is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: DD is V130() V131() V132() Element of K6(REAL)
Fs . j is V11() real ext-real Element of REAL
D is compact V130() V131() V132() Element of K6(REAL)
upper_bound D is V11() real ext-real Element of REAL
(dom proj2) /\ DD is Element of K6( the carrier of (TOP-REAL 2))
C9 . j is V11() real ext-real Element of REAL
|[(((W-bound n) + (E-bound n)) / 2),(C9 . j)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(r3 . j) `1 is V11() real ext-real Element of REAL
(LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(j + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(j + 1)))))) is V130() V131() V132() Element of K6(REAL)
lower_bound (proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))))) /\ (Upper_Arc (L~ (Cage (n,(j + 1))))))) is V11() real ext-real Element of REAL
width (Gauge (n,(j + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
dd is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(j + 1))) * ((X-SpanStart (n,(j + 1))),dd) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
dd is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . dd is V11() real ext-real Element of REAL
LSeg ((r3 . j),((Gauge (n,1)) * ((X-SpanStart (n,1)),1))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
DD is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
proj2 .: DD is V130() V131() V132() Element of K6(REAL)
(dom proj2) /\ DD is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (n,(j + 1))) * ((Center (Gauge (n,(j + 1)))),1) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(Gauge (n,(j + 1))) * ((Center (Gauge (n,(j + 1)))),(len (Gauge (n,(j + 1))))) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,(j + 1))) * ((Center (Gauge (n,(j + 1)))),1)),((Gauge (n,(j + 1))) * ((Center (Gauge (n,(j + 1)))),(len (Gauge (n,(j + 1))))))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
D is compact V130() V131() V132() Element of K6(REAL)
|[(((W-bound n) + (E-bound n)) / 2),(Fs . j)]| is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
(F . j) `1 is V11() real ext-real Element of REAL
dd `2 is V11() real ext-real Element of REAL
dd `1 is V11() real ext-real Element of REAL
lower_bound D is V11() real ext-real Element of REAL
dd is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 . dd is V11() real ext-real Element of REAL
dd `2 is V11() real ext-real Element of REAL
LSeg ((r3 . j),(F . j)) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (LSeg ((r3 . j),(F . j))) is V130() V131() V132() Element of K6(REAL)
[.(proj2 . (F . j)),(proj2 . (r3 . j)).] is compact V130() V131() V132() interval Element of K6(REAL)
(LSeg ((r3 . j),(F . j))) /\ (Lower_Arc (L~ (Cage (n,(j + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
j is set
E0 is compact V130() V131() V132() Element of K6(REAL)
upper_bound E0 is V11() real ext-real Element of REAL
k is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
k `2 is V11() real ext-real Element of REAL
proj2 . k is V11() real ext-real Element of REAL
k `1 is V11() real ext-real Element of REAL
{(F . j)} is set
W is compact V130() V131() V132() Element of K6(REAL)
j is V11() real ext-real set
k is set
proj2 . k is V11() real ext-real Element of REAL
x is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
x `2 is V11() real ext-real Element of REAL
upper_bound W is V11() real ext-real Element of REAL
dd `1 is V11() real ext-real Element of REAL
(LSeg ((r3 . j),(F . j))) /\ (Upper_Arc (L~ (Cage (n,(j + 1))))) is proper closed bounded compact Element of K6( the carrier of (TOP-REAL 2))
j is set
k is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
k `2 is V11() real ext-real Element of REAL
proj2 . k is V11() real ext-real Element of REAL
k `1 is V11() real ext-real Element of REAL
{(r3 . j)} is set
j is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(j + 1))) * ((X-SpanStart (n,(j + 1))),j) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . j))) /\ (Lower_Arc (L~ (Cage (n,(j + 1)))))) is V130() V131() V132() Element of K6(REAL)
upper_bound (proj2 .: ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),1)),(r3 . j))) /\ (Lower_Arc (L~ (Cage (n,(j + 1))))))) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,(j + 1))) * ((X-SpanStart (n,(j + 1))),k) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
meet (BDD-Family n) is Element of K6( the carrier of (TOP-REAL 2))
(Lower_Arc n) \/ (Upper_Arc n) is Element of K6( the carrier of (TOP-REAL 2))
((Lower_Arc n) \/ (Upper_Arc n)) /\ (LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) is Element of K6( the carrier of (TOP-REAL 2))
((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Upper_Arc n)) \/ ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Lower_Arc n)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 . |[(((W-bound n) + (E-bound n)) / 2),r]| is V11() real ext-real Element of REAL
proj2 .: (((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Upper_Arc n)) \/ ((LSeg (((Gauge (n,1)) * ((X-SpanStart (n,1)),(len (Gauge (n,1))))),((Gauge (n,1)) * ((X-SpanStart (n,1)),1)))) /\ (Lower_Arc n))) is V130() V131() V132() Element of K6(REAL)
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
n \/ (BDD n) is Element of K6( the carrier of (TOP-REAL 2))
i is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Gauge (n,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
len (Gauge (n,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
width (Gauge (n,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,n)) * (i,j) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
((Gauge (n,n)) * (i,j)) `1 is V11() real ext-real Element of REAL
cell ((Gauge (n,n)),i,j) is Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (n,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (n,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,n)),((X-SpanStart (n,n)) -' 1),j) is Element of K6( the carrier of (TOP-REAL 2))
Center (Gauge (n,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(Gauge (n,n)) * ((X-SpanStart (n,n)),j) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
((Gauge (n,n)) * ((X-SpanStart (n,n)),j)) `1 is V11() real ext-real Element of REAL
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT : S₁[b₁] } is set
e is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
p is non empty V130() V131() V132() V133() V134() V135() left_end bounded_below Element of K6(NAT)
min p is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Gauge (n,(n)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
width (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
X-SpanStart (n,(n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((n) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((n) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (n,(n))) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT : S₁[b₁] } is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),p) is Element of K6( the carrier of (TOP-REAL 2))
B is non empty V130() V131() V132() V133() V134() V135() left_end bounded_below Element of K6(NAT)
min B is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),(min B)) is Element of K6( the carrier of (TOP-REAL 2))
B is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),B) is Element of K6( the carrier of (TOP-REAL 2))
B is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),B) is Element of K6( the carrier of (TOP-REAL 2))
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),C) is Element of K6( the carrier of (TOP-REAL 2))
e is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),e) is Element of K6( the carrier of (TOP-REAL 2))
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
X-SpanStart (n,(n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((n) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((n) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (n,(n))) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Gauge (n,(n)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
len (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),0) is Element of K6( the carrier of (TOP-REAL 2))
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
width (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),1) is Element of K6( the carrier of (TOP-REAL 2))
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
n ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ n is set
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
width (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),0) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),(0 + 1)) is Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),0)) /\ (cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),(0 + 1))) is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (n,(n))) * (((X-SpanStart (n,(n))) -' 1),(0 + 1)) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
((X-SpanStart (n,(n))) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(Gauge (n,(n))) * ((((X-SpanStart (n,(n))) -' 1) + 1),(0 + 1)) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,(n))) * (((X-SpanStart (n,(n))) -' 1),(0 + 1))),((Gauge (n,(n))) * ((((X-SpanStart (n,(n))) -' 1) + 1),(0 + 1)))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Gauge (n,(n)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
width (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
X-SpanStart (n,(n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((n) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((n) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (n,(n))) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
len (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(width (Gauge (n,(n)))) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),((width (Gauge (n,(n)))) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
n ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ n is set
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),(width (Gauge (n,(n))))) is Element of K6( the carrier of (TOP-REAL 2))
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
(width (Gauge (n,(n)))) - 1 is V11() real integer ext-real Element of REAL
((width (Gauge (n,(n)))) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),(width (Gauge (n,(n)))))) /\ (cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),((width (Gauge (n,(n)))) -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (n,(n))) * (((X-SpanStart (n,(n))) -' 1),(width (Gauge (n,(n))))) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
((X-SpanStart (n,(n))) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(Gauge (n,(n))) * ((((X-SpanStart (n,(n))) -' 1) + 1),(width (Gauge (n,(n))))) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,(n))) * (((X-SpanStart (n,(n))) -' 1),(width (Gauge (n,(n)))))),((Gauge (n,(n))) * ((((X-SpanStart (n,(n))) -' 1) + 1),(width (Gauge (n,(n))))))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
X-SpanStart (n,C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (C -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (C -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
Gauge (n,C) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
width (Gauge (n,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C -' (n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (C -' (n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) -' 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (C -' (n))) * ((n) -' 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
((2 |^ (C -' (n))) * ((n) -' 2)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (n,C)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT : S₁[b₁] } is set
Gauge (n,(n)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
width (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
2 |^ (n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(2 |^ (n)) + (2 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(2 |^ (n)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
((2 |^ (n)) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(2 |^ (C -' (n))) * (2 |^ (n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C -' (n)) + (n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((C -' (n)) + (n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ C is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((n) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((n) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
len (Gauge (n,(n))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
X-SpanStart (n,(n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(X-SpanStart (n,(n))) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,(n))),((X-SpanStart (n,(n))) -' 1),(n)) is Element of K6( the carrier of (TOP-REAL 2))
(n) - 2 is V11() real integer ext-real Element of REAL
(2 |^ (C -' (n))) * ((n) - 2) is V11() real integer ext-real Element of REAL
((2 |^ (C -' (n))) * ((n) - 2)) + 2 is V11() real integer ext-real Element of REAL
(C -' (n)) + ((n) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(n) - 1 is V11() real integer ext-real Element of REAL
(C -' (n)) + ((n) - 1) is V11() real integer ext-real Element of REAL
((C -' (n)) + (n)) - 1 is V11() real integer ext-real Element of REAL
C - 1 is V11() real integer ext-real Element of REAL
(X-SpanStart (n,(n))) - 2 is V11() real integer ext-real Element of REAL
(2 |^ (C -' (n))) * ((X-SpanStart (n,(n))) - 2) is V11() real integer ext-real Element of REAL
((2 |^ (C -' (n))) * ((X-SpanStart (n,(n))) - 2)) + 2 is V11() real integer ext-real Element of REAL
cell ((Gauge (n,C)),((X-SpanStart (n,C)) -' 1),r2) is Element of K6( the carrier of (TOP-REAL 2))
(2 |^ C) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
((2 |^ C) + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(2 |^ C) + (1 + 2) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
len (Gauge (n,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
r2 is non empty V130() V131() V132() V133() V134() V135() left_end bounded_below Element of K6(NAT)
min r2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (n,C)),((X-SpanStart (n,C)) -' 1),x2) is Element of K6( the carrier of (TOP-REAL 2))
C9 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' (C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' (C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
X-SpanStart (C,(C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((C) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((C) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,(C))) - 2 is V11() real integer ext-real Element of REAL
(2 |^ (n -' (C))) * ((X-SpanStart (C,(C))) - 2) is V11() real integer ext-real Element of REAL
((2 |^ (n -' (C))) * ((X-SpanStart (C,(C))) - 2)) + 2 is V11() real integer ext-real Element of REAL
(n -' (C)) + ((C) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) - 1 is V11() real integer ext-real Element of REAL
(n -' (C)) + ((C) - 1) is V11() real integer ext-real Element of REAL
(n -' (C)) + (C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
((n -' (C)) + (C)) - 1 is V11() real integer ext-real Element of REAL
n - 1 is V11() real integer ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
(C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' (C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' (C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) -' 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' (C))) * ((C) -' 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
((2 |^ (n -' (C))) * ((C) -' 2)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
X-SpanStart (C,(C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ ((C) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ ((C) -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(C) - 2 is V11() real integer ext-real Element of REAL
Gauge (C,(C)) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
width (Gauge (C,(C))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
2 |^ (C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
len (Gauge (C,(C))) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (C)) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,(C))) - 2 is V11() real integer ext-real Element of REAL
(2 |^ (n -' (C))) * ((X-SpanStart (C,(C))) - 2) is V11() real integer ext-real Element of REAL
((2 |^ (n -' (C))) * ((X-SpanStart (C,(C))) - 2)) + 2 is V11() real integer ext-real Element of REAL
B is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(X-SpanStart (C,(C))) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (C,(C))),((X-SpanStart (C,(C))) -' 1),(C)) is Element of K6( the carrier of (TOP-REAL 2))
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
(X-SpanStart (C,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),B) is Element of K6( the carrier of (TOP-REAL 2))
width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(C,n)) is Element of K6( the carrier of (TOP-REAL 2))
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
(C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' (C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' (C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) -' 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' (C))) * ((C) -' 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
((2 |^ (n -' (C))) * ((C) -' 2)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
(C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
Gauge (C,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
len (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is Element of K6( the carrier of (TOP-REAL 2))
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
C ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ C is set
UBD C is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is Element of K6( the carrier of (TOP-REAL 2))
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1)) is Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1)) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
((X-SpanStart (C,n)) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
[(X-SpanStart (C,n)),(C,n)] is set
{(X-SpanStart (C,n)),(C,n)} is V130() V131() V132() V133() V134() V135() bounded_below set
{(X-SpanStart (C,n))} is V130() V131() V132() V133() V134() V135() bounded_below set
{{(X-SpanStart (C,n)),(C,n)},{(X-SpanStart (C,n))}} is set
Gauge (C,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
[((X-SpanStart (C,n)) -' 1),(C,n)] is set
{((X-SpanStart (C,n)) -' 1),(C,n)} is V130() V131() V132() V133() V134() V135() bounded_below set
{((X-SpanStart (C,n)) -' 1)} is V130() V131() V132() V133() V134() V135() bounded_below set
{{((X-SpanStart (C,n)) -' 1),(C,n)},{((X-SpanStart (C,n)) -' 1)}} is set
Gauge (C,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C,n) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((C,n) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(C,n) - 1 is V11() real integer ext-real Element of REAL
(C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' (C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' (C)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C) -' 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' (C))) * ((C) -' 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
((2 |^ (n -' (C))) * ((C) -' 2)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
p is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),p) is Element of K6( the carrier of (TOP-REAL 2))
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
C ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ C is set
width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
{ b₁ where b₁ is Element of K6( the carrier of (TOP-REAL 2)) : b₁ is_inside_component_of C } is set
len (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
union { b₁ where b₁ is Element of K6( the carrier of (TOP-REAL 2)) : b₁ is_inside_component_of C } is set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,n)) - 1 is V11() real integer ext-real Element of REAL
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(p + 1)) is Element of K6( the carrier of (TOP-REAL 2))
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),p)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(p + 1))) is Element of K6( the carrier of (TOP-REAL 2))
(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(p + 1)) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
((X-SpanStart (C,n)) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(p + 1)) is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(p + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(p + 1)))) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
B is set
r2 is Element of K6( the carrier of (TOP-REAL 2))
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Gauge (C,n) is V21() V23() V24( NAT ) V25(K292( the carrier of (TOP-REAL 2))) V26() FinSequence-like tabular V257() V258() V259() V260() FinSequence of K292( the carrier of (TOP-REAL 2))
X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
2 |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(2 |^ (n -' 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below Element of NAT
(X-SpanStart (C,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
(C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(C,n)) is Element of K6( the carrier of (TOP-REAL 2))
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
K6( the carrier of (Euclid 2)) is non empty set
e is bounded Element of K6( the carrier of (Euclid 2))
p is V11() real ext-real Element of REAL
B is Element of the carrier of (Euclid 2)
Ball (B,p) is bounded Element of K6( the carrier of (Euclid 2))
B is bounded Element of K6( the carrier of (Euclid 2))
r2 is V11() real ext-real Element of REAL
x2 is Element of the carrier of (Euclid 2)
Ball (x2,r2) is bounded Element of K6( the carrier of (Euclid 2))
(Ball (B,p)) ` is Element of K6( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ (Ball (B,p)) is set
(Ball (x2,r2)) ` is Element of K6( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ (Ball (x2,r2)) is set
(Ball (B,p)) \/ (Ball (x2,r2)) is Element of K6( the carrier of (Euclid 2))
x3 is Element of the carrier of (Euclid 2)
r3 is V11() real ext-real Element of REAL
Ball (x3,r3) is bounded Element of K6( the carrier of (Euclid 2))
D9 is connected Element of K6( the carrier of (TOP-REAL 2))
C9 is connected Element of K6( the carrier of (TOP-REAL 2))
(Ball (x3,r3)) ` is Element of K6( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ (Ball (x3,r3)) is set
((Ball (B,p)) \/ (Ball (x2,r2))) ` is Element of K6( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ ((Ball (B,p)) \/ (Ball (x2,r2))) is set
((Ball (B,p)) `) /\ ((Ball (x2,r2)) `) is Element of K6( the carrier of (Euclid 2))
B ` is Element of K6( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ B is set
e ` is Element of K6( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ e is set
{} (Euclid 2) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer ext-real non positive non negative bounded V130() V131() V132() V133() V134() V135() V136() bounded_below interval Element of K6( the carrier of (Euclid 2))
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
C is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
dist (C,n) is V11() real ext-real Element of REAL
e is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
dist (C,e) is V11() real ext-real non negative Element of REAL
n ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ n is set
LSeg (e,C) is non empty proper proper closed closed V91( TOP-REAL 2) connected bounded bounded compact compact convex Element of K6( the carrier of (TOP-REAL 2))
p is set
B is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
dist (C,B) is V11() real ext-real non negative Element of REAL
{ b₁ where b₁ is Element of K6( the carrier of (TOP-REAL 2)) : b₁ is_inside_component_of n } is set
union { b₁ where b₁ is Element of K6( the carrier of (TOP-REAL 2)) : b₁ is_inside_component_of n } is set
p is set
B is Element of K6( the carrier of (TOP-REAL 2))
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
C is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
dist (C,n) is V11() real ext-real Element of REAL
dist (C,(BDD n)) is V11() real ext-real Element of REAL
n ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ n is set
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
(BDD n) \/ (UBD n) is Element of K6( the carrier of (TOP-REAL 2))
e is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
dist (C,e) is V11() real ext-real non negative Element of REAL
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
e is set
p is V41(2) FinSequence-like V122() Element of the carrier of (TOP-REAL 2)
dist (p,n) is V11() real ext-real Element of REAL
dist (p,(BDD n)) is V11() real ext-real Element of REAL
dist (p,(BDD C)) is V11() real ext-real Element of REAL
dist (p,C) is V11() real ext-real Element of REAL
n is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
UBD n is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
BDD C is non empty open Element of K6( the carrier of (TOP-REAL 2))
BDD n is non empty open Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below Element of NAT
C is non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
Cage (C,n) is non empty V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard V236() FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (C,n)) is non empty proper closed V91( TOP-REAL 2) connected bounded being_simple_closed_curve compact V233() V234() Element of K6( the carrier of (TOP-REAL 2))
UBD C is non empty open connected Element of K6( the carrier of (TOP-REAL 2))
BDD (L~ (Cage (C,n))) is non empty open Element of K6( the carrier of (TOP-REAL 2))