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