:: CHORD semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V141() V148() V149() V151() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V146() V148() Element of bool REAL

bool REAL is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite complex-membered V141() set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V146() V148() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V141() set

INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V141() set

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() set

the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

_GraphSelectors is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V148() Element of bool NAT

VertexSelector is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

EdgeSelector is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

SourceSelector is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

TargetSelector is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of bool NAT

0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() V121() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() 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 V146() V147() V148() V149() V150() Element of bool NAT

dom {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() set

rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() set

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real positive non negative set

G - 1 is complex V25() integer ext-real set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(0 + 1) - 1 is complex V25() integer ext-real set

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

G - 1 is complex V25() integer even ext-real set

S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

S is complex V25() integer ext-real set

G is complex V25() integer ext-real set

G + 2 is complex V25() integer ext-real set

P is complex V25() integer ext-real set

P - G is complex V25() integer ext-real set

(P - G) + 1 is complex V25() integer ext-real set

P - S is complex V25() integer ext-real set

(P - S) + 1 is complex V25() integer ext-real set

((P - S) + 1) + 2 is complex V25() integer ext-real set

((P - G) + 1) - 3 is complex V25() integer ext-real set

(P - S) + 3 is complex V25() integer ext-real set

((P - S) + 3) - 3 is complex V25() integer ext-real set

P - (G + 2) is complex V25() integer ext-real set

S is non empty complex V25() integer non even ext-real set

G is non empty complex V25() integer non even ext-real set

S - 2 is complex V25() integer ext-real set

G + 1 is complex V25() integer even ext-real set

- 1 is complex V25() integer ext-real non positive set

(G + 1) + (- 1) is complex V25() integer ext-real set

S + (- 1) is complex V25() integer ext-real set

S - 1 is complex V25() integer even ext-real set

(S - 1) + (- 1) is complex V25() integer ext-real set

G is non empty complex V25() integer non even ext-real set

S is non empty complex V25() integer non even ext-real set

S + 2 is non empty complex V25() integer non even ext-real set

S + 1 is complex V25() integer even ext-real set

(S + 1) + 1 is non empty complex V25() integer non even ext-real set

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

2 * 0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() even V121() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() Element of NAT

(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(1 + 2) - 2 is complex V25() integer ext-real set

G - 2 is complex V25() integer ext-real set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

G - (2 * 1) is non empty complex V25() integer non even ext-real set

S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

S + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

2 * 2 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

6 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

2 * 3 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

8 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

7 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

2 * 4 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

7 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

6 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

6 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

2 * 0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() even V121() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() Element of NAT

(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(2 * 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

2 * 2 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(2 * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

2 * 3 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(2 * 3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

6 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

5 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

P is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

G + P is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real positive non negative set

x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

2 * x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

2 * x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

G + (2 * x) is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real positive non negative set

G . S is set

(G . S) .. G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

dom G is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

rng G is finite set

G . ((G . S) .. G) is set

G is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng G is non empty finite set

bool (rng G) is non empty finite V32() set

S is non empty finite Element of bool (rng G)

P is Element of S

P .. G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

x is set

x .. G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

S is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

len G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(S,(len G)) -cut G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng ((S,(len G)) -cut G) is finite set

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng G is finite set

dom G is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

S is set

S .. G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

P is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

(G,P) is finite set

len G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(P,(len G)) -cut G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng ((P,(len G)) -cut G) is finite set

G . (S .. G) is set

dom ((P,(len G)) -cut G) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

((P,(len G)) -cut G) . x is set

P + x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

G . x is set

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

P + x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

len ((P,(len G)) -cut G) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len ((P,(len G)) -cut G)) + P is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len G) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x + P is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

- P is complex V25() integer ext-real non positive set

(x + P) + (- P) is complex V25() integer ext-real set

(len G) + (- P) is complex V25() integer ext-real set

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(len G) - P is complex V25() integer ext-real set

((len G) - P) + 1 is complex V25() integer ext-real set

((P,(len G)) -cut G) . (x + 1) is set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

P is set

<*P*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

<*P*> ^ S is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real positive non negative set

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(G,(x + 1)) is finite set

len G is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

((x + 1),(len G)) -cut G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (((x + 1),(len G)) -cut G) is finite set

(S,x) is finite set

len S is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(x,(len S)) -cut S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng ((x,(len S)) -cut S) is finite set

len <*P*> is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

1 + (len S) is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

len (((x + 1),(len G)) -cut G) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len (((x + 1),(len G)) -cut G)) + (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(len G) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

len ((x,(len S)) -cut S) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len ((x,(len S)) -cut S)) + x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(len S) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

dom (((x + 1),(len G)) -cut G) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

Seg (len ((x,(len S)) -cut S)) is finite len ((x,(len S)) -cut S) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

dom ((x,(len S)) -cut S) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

dom S is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

(len <*P*>) + x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G . ((len <*P*>) + x) is set

S . x is set

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G . (x + 1) is set

x is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

(len G) - x is complex V25() integer ext-real set

0 + ((len G) - x) is complex V25() integer ext-real set

- 1 is complex V25() integer ext-real non positive set

(- 1) + x is complex V25() integer ext-real set

1 + (- 1) is complex V25() integer ext-real set

x + (- 1) is complex V25() integer ext-real set

x - 1 is complex V25() integer ext-real set

x + x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real positive non negative set

x + ((len G) - x) is complex V25() integer ext-real set

n is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

n + x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real positive non negative set

(n + x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

((n + x) + 1) + (- 1) is complex V25() integer ext-real set

((len S) + 1) + (- 1) is complex V25() integer ext-real set

1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x + n is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real positive non negative set

(((x + 1),(len G)) -cut G) . x is set

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(((x + 1),(len G)) -cut G) . (n + 1) is set

(x + 1) + n is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G . ((x + 1) + n) is set

(x + n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G . ((x + n) + 1) is set

S . (x + n) is set

((x,(len S)) -cut S) . (n + 1) is set

((x,(len S)) -cut S) . x is set

x is set

n is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

(((x + 1),(len G)) -cut G) . n is set

((x,(len S)) -cut S) . n is set

n is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal ext-real non negative set

((x,(len S)) -cut S) . n is set

(((x + 1),(len G)) -cut G) . n is set

G is set

S is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G

bool S is non empty finite V32() set

len S is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

P is Relation-like NAT -defined G -valued Function-like finite FinSubsequence-like Element of bool S

Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (Seq P) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

card P is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of omega

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

bool (the_Vertices_of G) is non empty set

S is Element of bool (the_Vertices_of G)

G .edgesBetween S is Element of bool (the_Edges_of G)

the_Edges_of G is set

G . EdgeSelector is set

bool (the_Edges_of G) is non empty set

G .edgesInto S is Element of bool (the_Edges_of G)

G .edgesOutOf S is Element of bool (the_Edges_of G)

(G .edgesInto S) /\ (G .edgesOutOf S) is Element of bool (the_Edges_of G)

P is Relation-like NAT -defined Function-like finite [Graph-like] inducedSubgraph of G,S,G .edgesBetween S

x is set

x is set

H is set

n is non empty Element of bool (the_Vertices_of G)

G .edgesBetween n is Element of bool (the_Edges_of G)

G .edgesInto n is Element of bool (the_Edges_of G)

G .edgesOutOf n is Element of bool (the_Edges_of G)

(G .edgesInto n) /\ (G .edgesOutOf n) is Element of bool (the_Edges_of G)

the_Edges_of P is Element of bool (the_Edges_of G)

P . EdgeSelector is set

the_Target_of P is Relation-like the_Edges_of P -defined the_Vertices_of P -valued Function-like V39( the_Edges_of P) V40( the_Edges_of P, the_Vertices_of P) Element of bool [:(the_Edges_of P),(the_Vertices_of P):]

the_Edges_of P is set

the_Vertices_of P is non empty set

P . VertexSelector is set

[:(the_Edges_of P),(the_Vertices_of P):] is Relation-like set

bool [:(the_Edges_of P),(the_Vertices_of P):] is non empty set

P . TargetSelector is set

the_Target_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like V39( the_Edges_of G) V40( the_Edges_of G, the_Vertices_of G) Element of bool [:(the_Edges_of G),(the_Vertices_of G):]

[:(the_Edges_of G),(the_Vertices_of G):] is Relation-like set

bool [:(the_Edges_of G),(the_Vertices_of G):] is non empty set

G . TargetSelector is set

(the_Target_of G) | (the_Edges_of P) is Relation-like the_Edges_of P -defined the_Edges_of G -defined the_Vertices_of G -valued Function-like set

(the_Target_of P) . H is set

(the_Target_of G) . H is set

the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like V39( the_Edges_of G) V40( the_Edges_of G, the_Vertices_of G) Element of bool [:(the_Edges_of G),(the_Vertices_of G):]

G . SourceSelector is set

(the_Source_of G) . H is set

the_Source_of P is Relation-like the_Edges_of P -defined the_Vertices_of P -valued Function-like V39( the_Edges_of P) V40( the_Edges_of P, the_Vertices_of P) Element of bool [:(the_Edges_of P),(the_Vertices_of P):]

P . SourceSelector is set

(the_Source_of G) | (the_Edges_of P) is Relation-like the_Edges_of P -defined the_Edges_of G -defined the_Vertices_of G -valued Function-like set

(the_Source_of P) . H is set

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

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

S is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of G

len S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

S .edges() is finite Element of bool (the_Edges_of G)

bool (the_Edges_of G) is non empty set

S .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of G

K426((the_Edges_of G),(S .edgeSeq())) is finite Element of bool (the_Edges_of G)

card (S .edges()) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of omega

2 * (card (S .edges())) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(2 * (card (S .edges()))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

len (S .edgeSeq()) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

2 * (len (S .edgeSeq())) is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(2 * (len (S .edgeSeq()))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

bool (the_Vertices_of G) is non empty set

the_Edges_of G is set

G . EdgeSelector is set

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

S is Element of bool (the_Vertices_of G)

(the_Vertices_of G) \ S is Element of bool (the_Vertices_of G)

G .edgesBetween ((the_Vertices_of G) \ S) is Element of bool (the_Edges_of G)

bool (the_Edges_of G) is non empty set

G .edgesInto ((the_Vertices_of G) \ S) is Element of bool (the_Edges_of G)

G .edgesOutOf ((the_Vertices_of G) \ S) is Element of bool (the_Edges_of G)

(G .edgesInto ((the_Vertices_of G) \ S)) /\ (G .edgesOutOf ((the_Vertices_of G) \ S)) is Element of bool (the_Edges_of G)

P is Relation-like NAT -defined Function-like finite [Graph-like] inducedSubgraph of G,(the_Vertices_of G) \ S,G .edgesBetween ((the_Vertices_of G) \ S)

the_Vertices_of P is non empty set

P . VertexSelector is set

the_Edges_of P is set

P . EdgeSelector is set

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

x is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of G

len x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x .last() is Element of the_Vertices_of G

x . (len x) is set

the_Edges_of P is Element of bool (the_Edges_of G)

x .edges() is finite Element of bool (the_Edges_of G)

x .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of G

K426((the_Edges_of G),(x .edgeSeq())) is finite Element of bool (the_Edges_of G)

x .vertices() is finite Element of bool (the_Vertices_of G)

x .vertexSeq() is Relation-like NAT -defined the_Vertices_of G -valued Function-like finite FinSequence-like FinSubsequence-like VertexSeq of G

K426((the_Vertices_of G),(x .vertexSeq())) is finite Element of bool (the_Vertices_of G)

G .edgesBetween (x .vertices()) is Element of bool (the_Edges_of G)

G .edgesInto (x .vertices()) is Element of bool (the_Edges_of G)

G .edgesOutOf (x .vertices()) is Element of bool (the_Edges_of G)

(G .edgesInto (x .vertices())) /\ (G .edgesOutOf (x .vertices())) is Element of bool (the_Edges_of G)

the_Vertices_of P is non empty Element of bool (the_Vertices_of G)

x is set

n is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x . n is set

G .edgesBetween (the_Vertices_of P) is Element of bool (the_Edges_of G)

G .edgesInto (the_Vertices_of P) is Element of bool (the_Edges_of G)

G .edgesOutOf (the_Vertices_of P) is Element of bool (the_Edges_of G)

(G .edgesInto (the_Vertices_of P)) /\ (G .edgesOutOf (the_Vertices_of P)) is Element of bool (the_Edges_of G)

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

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

S is set

P is set

{S,P} is non empty finite set

x is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of G

x .vertices() is finite Element of bool (the_Vertices_of G)

bool (the_Vertices_of G) is non empty set

x .vertexSeq() is Relation-like NAT -defined the_Vertices_of G -valued Function-like finite FinSequence-like FinSubsequence-like VertexSeq of G

K426((the_Vertices_of G),(x .vertexSeq())) is finite Element of bool (the_Vertices_of G)

x .first() is Element of the_Vertices_of G

x . 1 is set

x is set

{x} is non empty trivial finite 1 -element set

n is set

{S,P} \ {x} is finite Element of bool {S,P}

bool {S,P} is non empty finite V32() set

x .find n is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x . (x .find n) is set

y is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

y + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

len x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x . y is set

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x . (y + 1) is set

{P} is non empty trivial finite 1 -element set

{S} is non empty trivial finite 1 -element set

{S,P} \ {S} is finite Element of bool {S,P}

{S} is non empty trivial finite 1 -element set

{P} is non empty trivial finite 1 -element set

{S,P} \ {P} is finite Element of bool {S,P}

x is set

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

bool (the_Vertices_of G) is non empty set

the_Edges_of G is set

G . EdgeSelector is set

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

S is non empty Element of bool (the_Vertices_of G)

G .edgesBetween S is Element of bool (the_Edges_of G)

bool (the_Edges_of G) is non empty set

G .edgesInto S is Element of bool (the_Edges_of G)

G .edgesOutOf S is Element of bool (the_Edges_of G)

(G .edgesInto S) /\ (G .edgesOutOf S) is Element of bool (the_Edges_of G)

P is Relation-like NAT -defined Function-like finite [Graph-like] inducedSubgraph of G,S,G .edgesBetween S

the_Vertices_of P is non empty set

P . VertexSelector is set

the_Edges_of P is set

P . EdgeSelector is set

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

the_Vertices_of P is non empty Element of bool (the_Vertices_of G)

the_Edges_of P is Element of bool (the_Edges_of G)

x is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of G

x .vertices() is finite Element of bool (the_Vertices_of G)

x .vertexSeq() is Relation-like NAT -defined the_Vertices_of G -valued Function-like finite FinSequence-like FinSubsequence-like VertexSeq of G

K426((the_Vertices_of G),(x .vertexSeq())) is finite Element of bool (the_Vertices_of G)

x .edges() is finite Element of bool (the_Edges_of G)

x .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of G

K426((the_Edges_of G),(x .edgeSeq())) is finite Element of bool (the_Edges_of G)

G .edgesBetween (x .vertices()) is Element of bool (the_Edges_of G)

G .edgesInto (x .vertices()) is Element of bool (the_Edges_of G)

G .edgesOutOf (x .vertices()) is Element of bool (the_Edges_of G)

(G .edgesInto (x .vertices())) /\ (G .edgesOutOf (x .vertices())) is Element of bool (the_Edges_of G)

G .edgesBetween (the_Vertices_of P) is Element of bool (the_Edges_of G)

G .edgesInto (the_Vertices_of P) is Element of bool (the_Edges_of G)

G .edgesOutOf (the_Vertices_of P) is Element of bool (the_Edges_of G)

(G .edgesInto (the_Vertices_of P)) /\ (G .edgesOutOf (the_Vertices_of P)) is Element of bool (the_Edges_of G)

G is Relation-like NAT -defined Function-like finite [Graph-like] set

S is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

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

the_Vertices_of S is non empty set

S . VertexSelector is set

the_Edges_of S is set

S . EdgeSelector is set

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

P is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of G

x is Relation-like NAT -defined (the_Vertices_of S) \/ (the_Edges_of S) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of S

len x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

P .first() is Element of the_Vertices_of G

P . 1 is set

P .last() is Element of the_Vertices_of G

len P is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

P . (len P) is set

x .first() is Element of the_Vertices_of S

x . 1 is set

x .last() is Element of the_Vertices_of S

x . (len x) is set

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

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

S is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of G

len S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

P is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

S . P is set

S . x is set

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

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

S is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of G

S .vertices() is finite Element of bool (the_Vertices_of G)

bool (the_Vertices_of G) is non empty set

S .vertexSeq() is Relation-like NAT -defined the_Vertices_of G -valued Function-like finite FinSequence-like FinSubsequence-like VertexSeq of G

K426((the_Vertices_of G),(S .vertexSeq())) is finite Element of bool (the_Vertices_of G)

S .first() is Element of the_Vertices_of G

S . 1 is set

P is set

x is set

x is set

G .walkOf (P,x,x) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of G

(G .walkOf (P,x,x)) .append S is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of G

(G .walkOf (P,x,x)) .last() is Element of the_Vertices_of G

len (G .walkOf (P,x,x)) is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

(G .walkOf (P,x,x)) . (len (G .walkOf (P,x,x))) is set

Seg 3 is non empty finite 3 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of bool NAT

Seg (len (G .walkOf (P,x,x))) is non empty finite len (G .walkOf (P,x,x)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of bool NAT

dom (G .walkOf (P,x,x)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

((G .walkOf (P,x,x)) .append S) . 3 is set

(G .walkOf (P,x,x)) . 3 is set

C is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

y is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

len ((G .walkOf (P,x,x)) .append S) is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

((G .walkOf (P,x,x)) .append S) . y is set

((G .walkOf (P,x,x)) .append S) . C is set

2 * 0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() even V121() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() Element of NAT

(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

((G .walkOf (P,x,x)) .append S) .first() is Element of the_Vertices_of G

((G .walkOf (P,x,x)) .append S) . 1 is set

(G .walkOf (P,x,x)) .first() is Element of the_Vertices_of G

(G .walkOf (P,x,x)) . 1 is set

dom ((G .walkOf (P,x,x)) .append S) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

len S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

C is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len (G .walkOf (P,x,x))) + C is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

b is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

S . b is set

Seg (len ((G .walkOf (P,x,x)) .append S)) is non empty finite len ((G .walkOf (P,x,x)) .append S) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of bool NAT

dom ((G .walkOf (P,x,x)) .append S) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

len S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

C is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len (G .walkOf (P,x,x))) + C is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

b is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

S . (C + 1) is set

v is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len (G .walkOf (P,x,x))) + v is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

n1 is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

n1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

bg is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

v + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

S . (v + 1) is set

y is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

C is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

((G .walkOf (P,x,x)) .append S) . y is set

((G .walkOf (P,x,x)) .append S) . C is set

G is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

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

S is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of G

S .edges() is finite Element of bool (the_Edges_of G)

bool (the_Edges_of G) is non empty set

S .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of G

K426((the_Edges_of G),(S .edgeSeq())) is finite Element of bool (the_Edges_of G)

P is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of G

P .edges() is finite Element of bool (the_Edges_of G)

P .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of G

K426((the_Edges_of G),(P .edgeSeq())) is finite Element of bool (the_Edges_of G)

S .vertices() is finite Element of bool (the_Vertices_of G)

bool (the_Vertices_of G) is non empty set

S .vertexSeq() is Relation-like NAT -defined the_Vertices_of G -valued Function-like finite FinSequence-like FinSubsequence-like VertexSeq of G

K426((the_Vertices_of G),(S .vertexSeq())) is finite Element of bool (the_Vertices_of G)

P .vertices() is finite Element of bool (the_Vertices_of G)

P .vertexSeq() is Relation-like NAT -defined the_Vertices_of G -valued Function-like finite FinSequence-like FinSubsequence-like VertexSeq of G

K426((the_Vertices_of G),(P .vertexSeq())) is finite Element of bool (the_Vertices_of G)

(S .vertices()) /\ (P .vertices()) is finite Element of bool (the_Vertices_of G)

S .first() is Element of the_Vertices_of G

S . 1 is set

S .last() is Element of the_Vertices_of G

len S is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

S . (len S) is set

{(S .first()),(S .last())} is non empty finite Element of bool (the_Vertices_of G)

P .first() is Element of the_Vertices_of G

P . 1 is set

P .last() is Element of the_Vertices_of G

len P is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

P . (len P) is set

S .append P is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Walk of G

(S .append P) .first() is Element of the_Vertices_of G

(S .append P) . 1 is set

x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

dom S is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

(S .append P) . x is set

S . x is set

len (S .append P) is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

dom (S .append P) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of bool NAT

x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

(len (S .append P)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

- 1 is complex V25() integer ext-real non positive set

((len (S .append P)) + 1) + (- 1) is complex V25() integer ext-real set

(len S) + (len P) is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

((len S) + (len P)) + (- 1) is complex V25() integer ext-real set

n is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

x is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

S . x is set

(S .append P) . x is set

S . n is set

(S .append P) . n is set

(S .append P) . x is set

S . x is set

H is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len S) + H is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

C is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even ext-real positive non negative set

(S .append P) . n is set

H + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

P . (H + 1) is set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

2 * 0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V25() integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V100() even V121() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V141() V148() V149() V150() V151() Element of NAT

(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

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

P . C is set

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

(S .append P) . x is set

(S .append P) . n is set

H is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V148() V149() V150() Element of NAT

(len S) + H is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal even ext-real non negative set

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

C is non empty epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal non even V121() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of NAT

C is epsilon-transitive epsilon-connected ordinal natural complex V25() integer finite cardinal V121() ext-real non negative complex-membered