:: JORDAN9 semantic presentation

REAL is set

K6(REAL) is set

K6(omega) is set
K6(NAT) is set

RAT is set
INT is set

K7(1,1) is Relation-like set
K6(K7(1,1)) is set
K7(K7(1,1),1) is Relation-like set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is Relation-like set
K6(K7(K7(1,1),REAL)) is set

K7(K7(REAL,REAL),REAL) is Relation-like set
K6(K7(K7(REAL,REAL),REAL)) is set

K7(2,2) is Relation-like set
K7(K7(2,2),REAL) is Relation-like set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V118() V143() V144() V145() V146() V147() V148() V149() strict RLTopStruct
the carrier of () is non empty set
K7( the carrier of (),REAL) is Relation-like set
K6(K7( the carrier of (),REAL)) is set
K6( the carrier of ()) is set
the carrier of () * is non empty functional FinSequence-membered M11( the carrier of ())
{} is set

the carrier of () is non empty set

((n + 1) + 1) - 1 is V11() real ext-real Element of REAL
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
K6( the carrier of n) is set
C is Element of K6( the carrier of n)
f is Element of K6( the carrier of n)
f is Element of K6( the carrier of n)
G is Element of K6( the carrier of n)
n is non empty set

C is non empty set

dom f is V26() Element of K6(NAT)

dom (Rev f) is V26() Element of K6(NAT)

f /. n is Element of C

(Rev f) /. G is Element of C

C is non empty set

dom (Rev f) is V26() Element of K6(NAT)
dom f is V26() Element of K6(NAT)

(Rev f) /. n is Element of C
f /. n is Element of C

(Rev f) /. G is Element of C
f /. G is Element of C
n is non empty set
n * is non empty functional FinSequence-membered M11(n)

dom (Rev f) is V26() Element of K6(NAT)
Indices C is set

(Rev f) /. G is Element of n
(Rev f) /. (G + 1) is Element of n
dom f is V26() Element of K6(NAT)

f /. f is Element of n

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set

[S,N] is set
{S,N} is V26() set
{S} is V26() set
{{S,N},{S}} is V26() V30() set
C * (W,E) is Element of n
C * (S,N) is Element of n
W - S is V11() real ext-real set
abs (W - S) is V11() real ext-real Element of REAL
E - N is V11() real ext-real set
abs (E - N) is V11() real ext-real Element of REAL
(abs (W - S)) + (abs (E - N)) is V11() real ext-real Element of REAL
S - W is V11() real ext-real set
abs (S - W) is V11() real ext-real Element of REAL
N - E is V11() real ext-real set
abs (N - E) is V11() real ext-real Element of REAL

f /. k is Element of n

(Rev f) /. G is Element of n
dom f is V26() Element of K6(NAT)

f /. f is Element of n

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is Element of n
dom f is V26() Element of K6(NAT)

f /. G is Element of n
f /. (G + 1) is Element of n

(Rev f) /. f is Element of n

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set

[S,N] is set
{S,N} is V26() set
{S} is V26() set
{{S,N},{S}} is V26() V30() set
C * (W,E) is Element of n
C * (S,N) is Element of n
W - S is V11() real ext-real set
abs (W - S) is V11() real ext-real Element of REAL
E - N is V11() real ext-real set
abs (E - N) is V11() real ext-real Element of REAL
(abs (W - S)) + (abs (E - N)) is V11() real ext-real Element of REAL
S - W is V11() real ext-real set
abs (S - W) is V11() real ext-real Element of REAL
N - E is V11() real ext-real set
abs (N - E) is V11() real ext-real Element of REAL

(Rev f) /. k is Element of n

f /. G is Element of n

(Rev f) /. f is Element of n

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is Element of n

Values C is V26() set

f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
dom f is V26() Element of K6(NAT)
f . n is set
rng f is V26() set

Indices C is set

f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
dom f is V26() Element of K6(NAT)

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()

L~ (C /^ n) is closed compact Element of K6( the carrier of ())
f is set

LSeg ((C /^ n),G) is closed Element of K6( the carrier of ())
(len C) - n is V11() real ext-real Element of REAL

LSeg (C,(n + G)) is closed Element of K6( the carrier of ())

f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
left_cell (f,n,C) is Element of K6( the carrier of ())
right_cell (f,n,C) is Element of K6( the carrier of ())
LSeg (f,n) is closed Element of K6( the carrier of ())
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of ()
LSeg ((f /. n),(f /. (n + 1))) is closed compact Element of K6( the carrier of ())
(left_cell (f,n,C)) /\ (right_cell (f,n,C)) is Element of K6( the carrier of ())

left_cell (f,n,C) is Element of K6( the carrier of ())
Int (left_cell (f,n,C)) is Element of K6( the carrier of ())
right_cell (f,n,C) is Element of K6( the carrier of ())
Int (right_cell (f,n,C)) is Element of K6( the carrier of ())
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of ()

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of ()

cell (C,G,f) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,(G -' 1),f) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,G,(f -' 1)) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,(f -' 1)) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of ())
cell (C,G,f) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,W,E) is Element of K6( the carrier of ())
v_strip (C,W) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,W,(E -' 1)) is Element of K6( the carrier of ())
h_strip (C,(E -' 1)) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of ())
cell (C,(G -' 1),E) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,G,E) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())

left_cell (f,n,C) is Element of K6( the carrier of ())
Int (left_cell (f,n,C)) is Element of K6( the carrier of ())
right_cell (f,n,C) is Element of K6( the carrier of ())
Int (right_cell (f,n,C)) is Element of K6( the carrier of ())
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of ()

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of ()

cell (C,G,f) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,(G -' 1),f) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,G,(f -' 1)) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,(f -' 1)) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of ())
cell (C,G,f) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,W,E) is Element of K6( the carrier of ())
v_strip (C,W) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,W,(E -' 1)) is Element of K6( the carrier of ())
h_strip (C,(E -' 1)) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of ())
cell (C,(G -' 1),E) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,G,E) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())

left_cell (f,n,C) is Element of K6( the carrier of ())
Int (left_cell (f,n,C)) is Element of K6( the carrier of ())
Cl (Int (left_cell (f,n,C))) is Element of K6( the carrier of ())
right_cell (f,n,C) is Element of K6( the carrier of ())
Int (right_cell (f,n,C)) is Element of K6( the carrier of ())
Cl (Int (right_cell (f,n,C))) is Element of K6( the carrier of ())
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of ()

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of ()

cell (C,G,f) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,(G -' 1),f) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,G,(f -' 1)) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,(f -' 1)) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of ())
cell (C,G,f) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,W,E) is Element of K6( the carrier of ())
v_strip (C,W) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,W,(E -' 1)) is Element of K6( the carrier of ())
h_strip (C,(E -' 1)) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of ())
cell (C,(G -' 1),E) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,G,E) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())

LSeg (f,n) is closed Element of K6( the carrier of ())

Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()
C * (1,f) is 2 -element FinSequence-like V86() Element of the carrier of ()
(C * (1,f)) `2 is V11() real ext-real Element of REAL
W is 2 -element FinSequence-like V86() Element of the carrier of ()
W `2 is V11() real ext-real Element of REAL

(f /. n) `2 is V11() real ext-real Element of REAL

C * (1,1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(C * (1,1)) `2 is V11() real ext-real Element of REAL
G is 2 -element FinSequence-like V86() Element of the carrier of ()
G `2 is V11() real ext-real Element of REAL

LSeg (f,n) is closed Element of K6( the carrier of ())

Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()
C * (G,1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(C * (G,1)) `1 is V11() real ext-real Element of REAL
W is 2 -element FinSequence-like V86() Element of the carrier of ()
W `1 is V11() real ext-real Element of REAL

(f /. n) `1 is V11() real ext-real Element of REAL

C * (1,1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(C * (1,1)) `1 is V11() real ext-real Element of REAL
G is 2 -element FinSequence-like V86() Element of the carrier of ()
G `1 is V11() real ext-real Element of REAL

cell (f,n,C) is Element of K6( the carrier of ())
v_strip (f,n) is Element of K6( the carrier of ())
h_strip (f,C) is Element of K6( the carrier of ())
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of ())
Int (cell (f,n,C)) is Element of K6( the carrier of ())

L~ G is closed compact Element of K6( the carrier of ())
Int (v_strip (f,n)) is Element of K6( the carrier of ())
Int (h_strip (f,C)) is Element of K6( the carrier of ())
(Int (v_strip (f,n))) /\ (Int (h_strip (f,C))) is Element of K6( the carrier of ())
f is set

{ (LSeg (G,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT : ( 1 <= b1 & b1 + 1 <= len G ) } is set
union { (LSeg (G,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT : ( 1 <= b1 & b1 + 1 <= len G ) } is set
W is set

LSeg (G,E) is closed Element of K6( the carrier of ())

f * (1,N) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (1,N)) `2 is V11() real ext-real Element of REAL

S is 2 -element FinSequence-like V86() Element of the carrier of ()
f * (1,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (1,C)) `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
f * (1,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (1,(C + 1))) `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL

f * (N,1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (N,1)) `1 is V11() real ext-real Element of REAL

S is 2 -element FinSequence-like V86() Element of the carrier of ()
f * (n,1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,1)) `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
f * ((n + 1),1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL

left_cell (f,n,C) is Element of K6( the carrier of ())
Int (left_cell (f,n,C)) is Element of K6( the carrier of ())
L~ f is closed compact Element of K6( the carrier of ())
right_cell (f,n,C) is Element of K6( the carrier of ())
Int (right_cell (f,n,C)) is Element of K6( the carrier of ())
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of ()

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of ()

cell (C,G,f) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,(G -' 1),f) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,G,(f -' 1)) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
h_strip (C,(f -' 1)) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of ())
cell (C,G,f) is Element of K6( the carrier of ())
h_strip (C,f) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of ())
cell (C,W,E) is Element of K6( the carrier of ())
v_strip (C,W) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,W,(E -' 1)) is Element of K6( the carrier of ())
h_strip (C,(E -' 1)) is Element of K6( the carrier of ())
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of ())
cell (C,(G -' 1),E) is Element of K6( the carrier of ())
v_strip (C,(G -' 1)) is Element of K6( the carrier of ())
h_strip (C,E) is Element of K6( the carrier of ())
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of ())
cell (C,G,E) is Element of K6( the carrier of ())
v_strip (C,G) is Element of K6( the carrier of ())
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of ())

f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,C)) `1 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,(C + 1))) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),C)) `2 is V11() real ext-real Element of REAL
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),(C + 1))) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),(C + 1))) `2 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
f * (n,1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,1)) `1 is V11() real ext-real Element of REAL
f * (1,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (1,C)) `2 is V11() real ext-real Element of REAL
f * ((n + 1),1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
f * (1,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (1,(C + 1))) `2 is V11() real ext-real Element of REAL

C is 2 -element FinSequence-like V86() Element of the carrier of ()
C `1 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL

cell (n,f,G) is Element of K6( the carrier of ())
v_strip (n,f) is Element of K6( the carrier of ())
h_strip (n,G) is Element of K6( the carrier of ())
(v_strip (n,f)) /\ (h_strip (n,G)) is Element of K6( the carrier of ())
n * (f,G) is 2 -element FinSequence-like V86() Element of the carrier of ()
(n * (f,G)) `1 is V11() real ext-real Element of REAL
n * ((f + 1),G) is 2 -element FinSequence-like V86() Element of the carrier of ()
(n * ((f + 1),G)) `1 is V11() real ext-real Element of REAL
(n * (f,G)) `2 is V11() real ext-real Element of REAL
n * (f,(G + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(n * (f,(G + 1))) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (n * (f,G)) `2 <= b2 & b2 <= (n * (f,(G + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (n * (f,G)) `1 <= b1 & b1 <= (n * ((f + 1),G)) `1 ) } is set
f is V11() real ext-real Element of REAL
W is V11() real ext-real Element of REAL
|[f,W]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of ()
f is V11() real ext-real Element of REAL
W is V11() real ext-real Element of REAL
|[f,W]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of ()
|[(C `1),(C `2)]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of ()

cell (f,n,C) is Element of K6( the carrier of ())
v_strip (f,n) is Element of K6( the carrier of ())
h_strip (f,C) is Element of K6( the carrier of ())
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of ())
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,C)) `1 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (f * (n,C)) `1 <= b1 & b1 <= (f * ((n + 1),C)) `1 & (f * (n,C)) `2 <= b2 & b2 <= (f * (n,(C + 1))) `2 ) } is set
f is set
W is 2 -element FinSequence-like V86() Element of the carrier of ()
W `2 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
|[(W `1),(W `2)]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of ()
f is set
W is V11() real ext-real Element of REAL
E is V11() real ext-real Element of REAL
|[W,E]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of ()
S is 2 -element FinSequence-like V86() Element of the carrier of ()
S `1 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL

Values f is V26() set
cell (f,n,C) is Element of K6( the carrier of ())
v_strip (f,n) is Element of K6( the carrier of ())
h_strip (f,C) is Element of K6( the carrier of ())
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of ())
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of ()
G is 2 -element FinSequence-like V86() Element of the carrier of ()
Indices f is set
{ (f * (b1,b2)) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT : [b1,b2] in Indices f } is set

f * (f,W) is 2 -element FinSequence-like V86() Element of the carrier of ()
[f,W] is set
{f,W} is V26() set
{f} is V26() set
{{f,W},{f}} is V26() V30() set
f * (f,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (f,C)) `2 is V11() real ext-real Element of REAL
(f * (f,W)) `2 is V11() real ext-real Element of REAL
f * (1,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (1,C)) `2 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
(f * (f,W)) `2 is V11() real ext-real Element of REAL
f * (f,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (f,(C + 1))) `2 is V11() real ext-real Element of REAL
f * (1,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (1,(C + 1))) `2 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
f * (n,W) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,W)) `1 is V11() real ext-real Element of REAL
(f * (f,W)) `1 is V11() real ext-real Element of REAL
f * (n,1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,1)) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `1 is V11() real ext-real Element of REAL
(f * (f,W)) `1 is V11() real ext-real Element of REAL
f * ((n + 1),W) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),W)) `1 is V11() real ext-real Element of REAL
f * ((n + 1),1) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL

f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
cell (f,n,C) is Element of K6( the carrier of ())
v_strip (f,n) is Element of K6( the carrier of ())
h_strip (f,C) is Element of K6( the carrier of ())
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of ())
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,C)) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
(f * ((n + 1),(C + 1))) `1 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),(C + 1))) `2 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `2 is V11() real ext-real Element of REAL

Values f is V26() set
cell (f,n,C) is Element of K6( the carrier of ())
v_strip (f,n) is Element of K6( the carrier of ())
h_strip (f,C) is Element of K6( the carrier of ())
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of ())
G is 2 -element FinSequence-like V86() Element of the carrier of ()
f is 2 -element FinSequence-like V86() Element of the carrier of ()
W is 2 -element FinSequence-like V86() Element of the carrier of ()
LSeg (f,W) is closed compact Element of K6( the carrier of ())
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
G `2 is V11() real ext-real Element of REAL
W `2 is V11() real ext-real Element of REAL
G `1 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
W `2 is V11() real ext-real Element of REAL
G `2 is V11() real ext-real Element of REAL
G `1 is V11() real ext-real Element of REAL
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,C)) `1 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
G `1 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
G `2 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
W `2 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of ()
G `2 is V11() real ext-real Element of REAL
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
(f * (n,C)) `2 is V11() real ext-real Element of REAL
W `2 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
G `1 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of ()
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of ()

LSeg (f,n) is closed Element of K6( the carrier of ())
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of ()
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of ()

[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of ()

[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of ()

LSeg ((f /. n),(f /. (n + 1))) is closed compact Element of K6( the carrier of ())

cell (C,S,N) is Element of K6( the carrier of ())
v_strip (C,S) is Element of K6( the carrier of ())
h_strip (C,N) is Element of K6( the carrier of ())
(v_strip (C,S)) /\ (h_strip (C,N)) is Element of K6( the carrier of ())

2 - 1 is V11() real ext-real Element of REAL

cell (C,S,N) is Element of K6( the carrier of ())
v_strip (C,S) is Element of K6( the carrier of ())
h_strip (C,N) is Element of K6( the carrier of ())
(v_strip (C,S)) /\ (h_strip (C,N)) is Element of K6( the carrier of ())

cell (C,k,i) is Element of K6( the carrier of ())
v_strip (C,k) is Element of K6( the carrier of ())
h_strip (C,i) is Element of K6( the carrier of ())
(v_strip (C,k)) /\ (h_strip (C,i)) is Element of K6( the carrier of ())