:: HELLY semantic presentation

REAL is complex-membered ext-real-membered real-membered V132() V135() V136() V138() set

NAT is non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() Element of K32(REAL)

K32(REAL) is set

omega is non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() set

K32(omega) is non trivial non finite set

K32(NAT) is non trivial non finite set

{} is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set

the empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set

1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

3 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

_GraphSelectors is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V135() Element of K32(NAT)

0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT

Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

{1} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() set

Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

{1,2} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() set

card {} is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set

T is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

T . 1 is set

<*(T . 1)*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

<*(T . 1)*> ^' T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (<*(T . 1)*> ^' T) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len (<*(T . 1)*> ^' T)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

len <*(T . 1)*> is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

len T is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(len <*(T . 1)*>) + (len T) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

(<*(T . 1)*> ^' T) . H is set

<*(T . 1)*> . 1 is set

T . H is set

H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len <*(T . 1)*>) + H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(<*(T . 1)*> ^' T) . H is set

T . H is set

1 + (len T) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

{ H

H9 is set

cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

len {} is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT

H9 is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() set

max H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() V139() set

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

mA is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

dom mA is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

len mA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

dom A is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

cA is set

mA . cA is set

T . cA is set

A . cA is set

H is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

H9 is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

H is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

H9 is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

cH is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

T is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

T . 1 is set

<*(T . 1)*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

dom <*(T . 1)*> is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

X is set

<*(T . 1)*> . X is set

T . X is set

len T is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

len <*(T . 1)*> is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

dom T is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

T is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

T . 1 is set

X is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X . 1 is set

(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

<*(T . 1)*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

len <*(T . 1)*> is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

(T,X) . H is set

T . H is set

dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

0 + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

T . H is set

X . H is set

(T,X) . H is set

T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len (T,X)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T . ((len (T,X)) + 1) is set

X . ((len (T,X)) + 1) is set

<*(T . ((len (T,X)) + 1))*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

(T,X) ^ <*(T . ((len (T,X)) + 1))*> is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

A is set

dom ((T,X) ^ <*(T . ((len (T,X)) + 1))*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

len ((T,X) ^ <*(T . ((len (T,X)) + 1))*>) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set

(T,X) . A is set

X . A is set

((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set

X . A is set

A is set

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set

(T,X) . A is set

T . A is set

((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set

T . A is set

len X is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

X .cut (H,H9) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len (X .cut (H,H9)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(H,H9) -cut X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of T) \/ (the_Edges_of T)

cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

X .cut (cH,A) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len (X .cut (cH,A)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

X .cut (H,H9) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

cH is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like trivial Trail-like Path-like vertex-distinct Walk of T

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

cH .cut (A,A) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like trivial Trail-like Path-like vertex-distinct Walk of T

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set

H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set

cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set

X .cut (H,H9) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len (X .cut (H,H9)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .cut (H,H9)) . cH is set

H + cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even set

(H + cH) - 1 is non empty V27() ext-real V73() V74() non even set

1 + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(1 + 1) - 1 is V27() ext-real V73() V74() set

A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set

X . A is set

1 - 1 is V27() ext-real V73() V74() set

cH - 1 is V27() ext-real V73() V74() even set

(len (X .cut (H,H9))) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

((len (X .cut (H,H9))) + 1) - 1 is non empty V27() ext-real V73() V74() non even set

B is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X .cut (mA,cA) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .cut (mA,cA)) . (B + 1) is set

H + B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (H + B) is set

(len (X .cut (H,H9))) + H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

mA + cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H9 + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(H9 + 1) - 1 is non empty V27() ext-real V73() V74() non even set

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .vertices() is finite Element of K32((the_Vertices_of T))

K32((the_Vertices_of T)) is non empty-membered set

X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))

H .vertices() is finite Element of K32((the_Vertices_of T))

H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))

H9 is set

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . cH is set

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

H . cH is set

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .edges() is finite Element of K32((the_Edges_of T))

K32((the_Edges_of T)) is set

X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))

H .edges() is finite Element of K32((the_Edges_of T))

H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))

H9 is set

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

X . cH is set

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

H . cH is set

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H .first() is Element of the_Vertices_of T

H . 1 is set

len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

dom (X .append H) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

cH is set

X . cH is set

(X .append H) . cH is set

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H .first() is Element of the_Vertices_of T

H . 1 is set

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H .first() is Element of the_Vertices_of T

H . 1 is set

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(len (X .append H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

1 + (len H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

1 - 1 is V27() ext-real V73() V74() set

H9 - 1 is V27() ext-real V73() V74() set

cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

1 + cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .append H) . (1 + cH) is set

cH + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (cH + 1) is set

(X .append H) . H9 is set

H . H9 is set

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Walk of T

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

X .edges() is finite Element of K32((the_Edges_of T))

K32((the_Edges_of T)) is set

X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))

H .edges() is finite Element of K32((the_Edges_of T))

H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))

X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

dom (X .append H) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

X . cH is set

(X .append H) . cH is set

X . A is set

(X .append H) . A is set

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .append H) . A is set

mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

mA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (mA + 1) is set

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

X . cH is set

(X .append H) . cH is set

cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .append H) . cH is set

H . (B + 1) is set

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

X .edges() is finite Element of K32((the_Edges_of T))

K32((the_Edges_of T)) is set

X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))

H .edges() is finite Element of K32((the_Edges_of T))

H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))

X .first() is Element of the_Vertices_of T

X . 1 is set

H .vertices() is finite Element of K32((the_Vertices_of T))

K32((the_Vertices_of T)) is non empty-membered set

H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))

H .last() is Element of the_Vertices_of T

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (len H) is set

X .vertices() is finite Element of K32((the_Vertices_of T))

X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))

(X .vertices()) /\ (H .vertices()) is finite Element of K32((the_Vertices_of T))

{(X .first()),(X .last())} is non empty finite set

X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .append H) . cH is set

(X .append H) . A is set

dom (X .append H) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

A + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (A + 1) is set

mA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

mA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (mA + 1) is set

cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (cA + 1) is set

B is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (B + 1) is set

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

X . cH is set

2 * 0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT

(2 * 0) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

2 * 0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT

(2 * 0) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . ((2 * 0) + 1) is set

(len (X .append H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(len X) + (mA + 1) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

X . cH is set

X . A is set

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

X .vertices() is finite Element of K32((the_Vertices_of T))

K32((the_Vertices_of T)) is non empty-membered set

X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))

H .vertices() is finite Element of K32((the_Vertices_of T))

H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))

(X .vertices()) /\ (H .vertices()) is finite Element of K32((the_Vertices_of T))

{(X .last())} is non empty trivial finite 1 -element set

X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

(X .append H) .first() is Element of the_Vertices_of T

(X .append H) . 1 is set

(X .append H) .last() is Element of the_Vertices_of T

len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .append H) . (len (X .append H)) is set

X .first() is Element of the_Vertices_of T

X . 1 is set

H .last() is Element of the_Vertices_of T

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (len H) is set

X .first() is Element of the_Vertices_of T

X . 1 is set

X .edges() is finite Element of K32((the_Edges_of T))

K32((the_Edges_of T)) is set

X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))

H .edges() is finite Element of K32((the_Edges_of T))

H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))

(X .edges()) /\ (H .edges()) is finite Element of K32((the_Edges_of T))

cH is set

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

mA + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

A is Element of the_Vertices_of T

H . mA is set

mA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (mA + 1) is set

A is Element of the_Vertices_of T

H . (mA + 2) is set

C is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

C + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

cA is Element of the_Vertices_of T

X . C is set

C + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (C + 1) is set

B is Element of the_Vertices_of T

X . (C + 2) is set

C + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

{cA,B} is non empty finite set

mA + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

{A,A} is non empty finite set

{(X .first()),(X .last())} is non empty finite set

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T

X .last() is Element of the_Vertices_of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len X) is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

H .last() is Element of the_Vertices_of T

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (len H) is set

X .first() is Element of the_Vertices_of T

X . 1 is set

X .edges() is finite Element of K32((the_Edges_of T))

K32((the_Edges_of T)) is set

X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))

H .edges() is finite Element of K32((the_Edges_of T))

H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T

K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))

X .vertices() is finite Element of K32((the_Vertices_of T))

K32((the_Vertices_of T)) is non empty-membered set

X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))

H .vertices() is finite Element of K32((the_Vertices_of T))

H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T

K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))

(X .vertices()) /\ (H .vertices()) is finite Element of K32((the_Vertices_of T))

{(X .last()),(X .first())} is non empty finite set

X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

(X .append H) .first() is Element of the_Vertices_of T

(X .append H) . 1 is set

(X .append H) .last() is Element of the_Vertices_of T

len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(X .append H) . (len (X .append H)) is set

T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set

cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

X . cH is set

H . cH is set

1 - 1 is V27() ext-real V73() V74() set

cH - 1 is V27() ext-real V73() V74() set

A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even set

A - 1 is non empty V27() ext-real V73() V74() non even set

A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . A is set

A + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (A + 2) is set

A + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (A + 1) is set

(A + 1) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (A + 2) is set

H . A is set

H . (A + 1) is set

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .first() is Element of the_Vertices_of T

X . 1 is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len (X,H)) - 1 is V27() ext-real V73() V74() set

cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

(len (X,H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . ((len (X,H)) + 1) is set

<*(X . ((len (X,H)) + 1))*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

(X,H) ^ <*(X . ((len (X,H)) + 1))*> is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len ((X,H) ^ <*(X . ((len (X,H)) + 1))*>) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

mA is set

dom ((X,H) ^ <*(X . ((len (X,H)) + 1))*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

dom (X,H) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set

(X,H) . mA is set

X . mA is set

((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set

X . mA is set

cH + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . cH is set

cH + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . (cH + 2) is set

H . (len (X,H)) is set

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . cH is set

X . (cH + 2) is set

X . (len (X,H)) is set

mA is set

cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set

dom (X,H) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)

((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set

(X,H) . mA is set

H . mA is set

((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set

H . mA is set

dom H is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)

T is V7() V10( NAT ) Function-like finite [Graph-like] set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .first() is Element of the_Vertices_of T

X . 1 is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len (X,H)) + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

T is V7() V10( NAT ) Function-like finite [Graph-like] non-multi non-Dmulti set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .first() is Element of the_Vertices_of T

X . 1 is set

H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H .first() is Element of the_Vertices_of T

H . 1 is set

(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT

(len (X,H)) + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . ((len (X,H)) + 2) is set

H . ((len (X,H)) + 2) is set

len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . (len (X,H)) is set

(len (X,H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

X . ((len (X,H)) + 1) is set

H . (len (X,H)) is set

len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT

H . ((len (X,H)) + 1) is set

T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set

the_Vertices_of T is non empty set

the_Edges_of T is set

(the_Vertices_of T) \/ (the_Edges_of T) is non empty set

X is non empty