REAL is complex-membered ext-real-membered real-membered V30() V33() V34() V36() set
NAT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V31() V33() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
NAT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V31() V33() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
bool NAT is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
COMPLEX is complex-membered V30() set
RAT is complex-membered ext-real-membered real-membered rational-membered V30() set
INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V30() set
{} is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() set
2 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty cup-closed diff-closed preBoolean set
1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
K216(1,NAT) is M10( NAT )
{{},1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered set
3 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
_GraphSelectors is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V33() Element of bool NAT
VertexSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
EdgeSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
SourceSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
TargetSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
4 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT
card {} is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() set
0 is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() V59() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() Element of NAT
proj1 {} is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() set
proj2 {} is empty trivial Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued V72() decreasing non-decreasing non-increasing FinSequence-yielding finite-support V224() Function-yielding V264() set
6 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
5 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G is Relation-like Function-like set
proj1 G is set
L is set
V is set
L .--> V is Relation-like {L} -defined Function-like one-to-one finite finite-support set
{L} is non empty trivial finite 1 -element set
{L} --> V is non empty Relation-like {L} -defined {V} -valued Function-like constant total quasi_total finite finite-support Element of bool [:{L},{V}:]
{V} is non empty trivial finite 1 -element set
[:{L},{V}:] is non empty Relation-like finite set
bool [:{L},{V}:] is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set
G +* (L .--> V) is Relation-like Function-like set
proj1 (G +* (L .--> V)) is set
(proj1 G) \/ {L} is non empty set
dom (L .--> V) is trivial finite Element of bool {L}
bool {L} is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set
(proj1 G) \/ (dom (L .--> V)) is set
G is Relation-like Function-like one-to-one set
L is set
V is set
G | L is Relation-like Function-like set
(G | L) " is Relation-like Function-like set
proj1 ((G | L) ") is set
G | V is Relation-like Function-like set
(G | V) " is Relation-like Function-like set
(G | L) ~ is Relation-like set
(G | V) ~ is Relation-like set
a is set
((G | L) ") . a is set
((G | V) ") . a is set
G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G + L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
V is non empty set
[:NAT,V:] is non empty non trivial Relation-like non finite set
bool [:NAT,V:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
a is Relation-like NAT -defined V -valued Function-like quasi_total Element of bool [:NAT,V:]
{ (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + L ) } is set
card { (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + L ) } is epsilon-transitive epsilon-connected ordinal cardinal set
{ (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + a1 ) } is set
card { (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + a1 ) } is epsilon-transitive epsilon-connected ordinal cardinal set
dom a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool NAT
b is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G + b is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
{ (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + b ) } is set
card { (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + b ) } is epsilon-transitive epsilon-connected ordinal cardinal set
b + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G + (b + 1) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
{ (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + (b + 1) ) } is set
card { (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + (b + 1) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
(b + 1) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G + b) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
{ (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= (G + b) + 1 ) } is set
vc is set
P is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a . P is Element of V
a . ((G + b) + 1) is Element of V
{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V
bool V is non empty cup-closed diff-closed preBoolean V225() set
va is finite set
va \/ {(a . ((G + b) + 1))} is non empty finite set
va is finite set
a . ((G + b) + 1) is Element of V
{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V
bool V is non empty cup-closed diff-closed preBoolean V225() set
va \/ {(a . ((G + b) + 1))} is non empty finite set
va is finite set
a . ((G + b) + 1) is Element of V
{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V
bool V is non empty cup-closed diff-closed preBoolean V225() set
va \/ {(a . ((G + b) + 1))} is non empty finite set
va is finite set
a . ((G + b) + 1) is Element of V
{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V
bool V is non empty cup-closed diff-closed preBoolean V225() set
va \/ {(a . ((G + b) + 1))} is non empty finite set
P is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a . P is Element of V
{ (a . b2) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b2 & b2 <= (G + b) + 1 ) } is set
{ (a . b2) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b2 & b2 <= (G + b) + 1 ) } is set
{ (a . b2) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b2 & b2 <= (G + b) + 1 ) } is set
vc is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a . vc is Element of V
card (va \/ {(a . ((G + b) + 1))}) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
b is set
G + 0 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
{ (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + 0 ) } is set
c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a . c is Element of V
a . G is Element of V
{(a . G)} is non empty trivial finite 1 -element Element of bool V
bool V is non empty cup-closed diff-closed preBoolean V225() set
card { (a . b1) where b1 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT : ( G <= b1 & b1 <= G + 0 ) } is epsilon-transitive epsilon-connected ordinal cardinal set
0 + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L is ext-real V55() real set
G is ext-real V55() real set
V is ext-real V55() real set
V - G is ext-real V55() real set
(V - G) + 1 is ext-real V55() real set
V - L is ext-real V55() real set
(V - L) + 1 is ext-real V55() real set
L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
V -' G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
V -' L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
V - G is ext-real V55() real V57() set
V - L is ext-real V55() real V57() set
bool (bool NAT) is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element Element of bool NAT
{{1}} is non empty trivial finite finite-membered 1 -element Element of bool (bool NAT)
L is Element of bool (bool NAT)
G is Relation-like Function-like set
proj1 G is set
L is Relation-like Function-like set
proj1 L is set
(proj1 G) \/ (proj1 L) is set
a is set
G . a is set
L . a is set
(G . a) \/ (L . a) is set
a is Relation-like Function-like set
proj1 a is set
a is Relation-like Function-like set
proj1 a is set
b is set
a . b is set
G . b is set
L . b is set
(G . b) \/ (L . b) is set
V is Relation-like Function-like set
proj1 V is set
a is Relation-like Function-like set
proj1 a is set
b is set
V . b is set
G . b is set
L . b is set
(G . b) \/ (L . b) is set
a . b is set
G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
Seg V is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite V -element Element of bool NAT
L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
V -' L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
Seg (V -' L) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite V -' L -element Element of bool NAT
(Seg V) \ (Seg (V -' L)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
0 + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
Seg L is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -element Element of bool NAT
L -' G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
Seg (L -' G) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' G -element Element of bool NAT
(Seg L) \ (Seg (L -' G)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
L -' V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
Seg (L -' V) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' V -element Element of bool NAT
(Seg L) \ (Seg (L -' V)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
a is set
a is set
b is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
Seg L is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -element Element of bool NAT
L -' G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
Seg (L -' G) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' G -element Element of bool NAT
(Seg L) \ (Seg (L -' G)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
{(L -' G)} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element Element of bool NAT
((Seg L) \ (Seg (L -' G))) \/ {(L -' G)} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT
G + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L -' (G + 1) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
Seg (L -' (G + 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' (G + 1) -element Element of bool NAT
(Seg L) \ (Seg (L -' (G + 1))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
b is set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
b is set
c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(L -' (G + 1)) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
NAT --> {} is non empty Relation-like NAT -defined RAT -valued INT -valued {{}} -valued Function-like constant total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Function-yielding V264() Element of bool [:NAT,{{}}:]
{{}} is non empty trivial functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element set
[:NAT,{{}}:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,{{}}:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
rng (NAT --> {}) is non empty trivial functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element Element of bool {{}}
bool {{}} is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set
L is set
L is set
G is Relation-like Function-like finite-yielding () set
L is set
G . L is finite set
proj1 G is set
proj2 G is finite-membered set
proj1 G is set
proj1 G is set
G is epsilon-transitive epsilon-connected ordinal set
bool G is non empty cup-closed diff-closed preBoolean set
L is finite Element of bool G
V is finite Element of bool G
(L,1) -bag is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags G
Bags G is non empty set
Bags G is non empty functional Element of bool (Bags G)
bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set
(V,1) -bag is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags G
a is set
((V,1) -bag) . a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 G is set
L is set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
L /\ (proj1 G) is set
a is Relation-like Function-like set
proj1 a is set
b is set
proj2 a is set
c is set
a . c is set
G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G +* a is Relation-like Function-like set
proj2 (G +* a) is set
rng G is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool RAT
bool RAT is non empty cup-closed diff-closed preBoolean set
(rng G) \/ (proj2 a) is set
b is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 b is set
(proj1 G) \/ (L /\ (proj1 G)) is set
c is set
b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a . c is set
G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
c is set
b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
va is set
b . va is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . va is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 a is set
b is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 b is set
c is set
a . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G is epsilon-transitive epsilon-connected ordinal set
Bags G is non empty functional Element of bool (Bags G)
Bags G is non empty set
bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set
[:(Bags G),(Bags G):] is non empty Relation-like set
bool [:(Bags G),(Bags G):] is non empty cup-closed diff-closed preBoolean V225() set
bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set
V is non empty functional finite Element of bool (Bags G)
L is Relation-like Bags G -defined Bags G -valued total reflexive antisymmetric connected transitive Element of bool [:(Bags G),(Bags G):]
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
proj2 a is finite set
len a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
dom a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
b is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
b + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a . (b + 1) is set
va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
a . va is set
vb is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
a . va is set
vb is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
c is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
max (vb,c,L) is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
a . P is set
e1 is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
a . P is set
e1 is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
a . 1 is set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
a . c is set
va is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
b is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
a . b is set
c is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
va is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
vb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
a . vb is set
va is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
a is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
b is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
G is epsilon-transitive epsilon-connected ordinal set
InvLexOrder G is Relation-like Bags G -defined Bags G -valued total reflexive antisymmetric transitive admissible Element of bool [:(Bags G),(Bags G):]
Bags G is non empty functional Element of bool (Bags G)
Bags G is non empty set
bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set
[:(Bags G),(Bags G):] is non empty Relation-like set
bool [:(Bags G),(Bags G):] is non empty cup-closed diff-closed preBoolean V225() set
G is Relation-like NAT -defined Function-like finite finite-support [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
L is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
L .last() is Element of the_Vertices_of G
len L is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
L . (len L) is set
L .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G
len (L .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(L .length()) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
a is set
V is set
L .addEdge V is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
(L .last()) .adj V is Element of the_Vertices_of G
G .walkOf ((L .last()),V,((L .last()) .adj V)) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Trail-like Path-like Walk of G
L .append (G .walkOf ((L .last()),V,((L .last()) .adj V))) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
(L .addEdge V) .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(L .addEdge V) .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G
len ((L .addEdge V) .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
<*V*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set
(L .edgeSeq()) ^ <*V*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len <*V*> is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G is Relation-like NAT -defined Function-like finite finite-support [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
L is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
L .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G
len (L .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L .reverse() is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
(L .reverse()) .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(L .reverse()) .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G
len ((L .reverse()) .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
len L is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
2 * (L .length()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() even Element of NAT
(2 * (L .length())) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
len (L .reverse()) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
((2 * (L .length())) + 1) - 1 is ext-real V55() real V57() even set
2 * ((L .reverse()) .length()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() even Element of NAT
(2 * ((L .reverse()) .length())) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
((2 * ((L .reverse()) .length())) + 1) - 1 is ext-real V55() real V57() even set
G is Relation-like NAT -defined Function-like finite finite-support [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
L is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
L .last() is Element of the_Vertices_of G
len L is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
L . (len L) is set
dom L is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
a is set
V is set
L .addEdge V is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
(L .last()) .adj V is Element of the_Vertices_of G
G .walkOf ((L .last()),V,((L .last()) .adj V)) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Trail-like Path-like Walk of G
L .append (G .walkOf ((L .last()),V,((L .last()) .adj V))) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
dom (L .addEdge V) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
(L .addEdge V) . b is set
L . b is set
(len L) + 2 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
len (L .addEdge V) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT
NAT --> 1 is non empty Relation-like non-zero NAT -defined NAT -valued RAT -valued INT -valued Function-like constant total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element set
[:NAT,{1}:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
L is Relation-like NAT -defined Function-like total set
L . 0 is set
0 + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L . (0 + 1) is set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
L . V is set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
L . a is set
V + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L . (V + 1) is set
a + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L . (a + 1) is set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
L . V is set
G is Relation-like NAT -defined Function-like total set
G .Lifespan() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . (G .Lifespan()) is set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
(G .Lifespan()) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + V) is set
V + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G .Lifespan()) + (V + 1) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + (V + 1)) is set
(G .Lifespan()) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + 1) is set
((G .Lifespan()) + V) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . (((G .Lifespan()) + V) + 1) is set
(G .Lifespan()) + 0 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + 0) is set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
G . V is set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
(G .Lifespan()) + a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G is Relation-like NAT -defined Function-like total set
G is Relation-like NAT -defined Function-like total set
L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
G . L is set
L + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . (L + 1) is set
G is Relation-like NAT -defined Function-like total set
G is Relation-like NAT -defined Function-like total halting () () set
G .Lifespan() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . (G .Lifespan()) is set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
G . V is set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
(G .Lifespan()) + a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + a) is set
a + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G .Lifespan()) + (a + 1) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + (a + 1)) is set
(G .Lifespan()) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + 1) is set
((G .Lifespan()) + a) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . (((G .Lifespan()) + a) + 1) is set
(G .Lifespan()) + 0 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G . ((G .Lifespan()) + 0) is set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
(G .Lifespan()) + a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
G is Relation-like NAT -defined Function-like total halting () () set
G .Lifespan() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
G . V is set
G . L is set
G . (G .Lifespan()) is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set
the_Vertices_of G is non empty finite set
G . VertexSelector is set
[:(the_Vertices_of G),NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(the_Vertices_of G),NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
L is Relation-like NAT -defined Function-like total set
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
L . V is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set
L is Relation-like NAT -defined Function-like total (G)
V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
L . V is set
the_Vertices_of G is non empty finite set
G . VertexSelector is set
[:(the_Vertices_of G),NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(the_Vertices_of G),NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set
the_Vertices_of G is non empty finite set
G . VertexSelector is set
card (the_Vertices_of G) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
canFS (the_Vertices_of G) is non empty Relation-like NAT -defined the_Vertices_of G -valued Function-like one-to-one onto finite FinSequence-like FinSubsequence-like finite-support FinSequence of the_Vertices_of G
[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
a is Relation-like NAT -defined NAT -valued Function-like quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
b is set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT
(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]
[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set
bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set
(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
b is Relation-like NAT -defined Function-like total set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
b . c is set
Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT
(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]
[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set
bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set
(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
Seg va is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite va -element Element of bool NAT
(canFS (the_Vertices_of G)) | (Seg va) is Relation-like NAT -defined Seg va -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]
((canFS (the_Vertices_of G)) | (Seg va)) " is Relation-like Function-like set
(((canFS (the_Vertices_of G)) | (Seg va)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
len (canFS (the_Vertices_of G)) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(canFS (the_Vertices_of G)) " is Relation-like Function-like one-to-one set
((canFS (the_Vertices_of G)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT
Seg (len (canFS (the_Vertices_of G))) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite len (canFS (the_Vertices_of G)) -element Element of bool NAT
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
b . c is set
Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT
(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]
[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set
bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT
(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]
[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set
bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set
(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
vb is set
rng ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool RAT
bool RAT is non empty cup-closed diff-closed preBoolean set
rng a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool NAT
((canFS (the_Vertices_of G)) | (Seg c)) ~ is Relation-like the_Vertices_of G -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
[:(the_Vertices_of G),NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(the_Vertices_of G),NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
vb is set
proj1 ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a) is set
proj1 (((canFS (the_Vertices_of G)) | (Seg c)) ") is set
rng ((canFS (the_Vertices_of G)) | (Seg c)) is finite Element of bool (the_Vertices_of G)
bool (the_Vertices_of G) is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set
b . c is set
dom a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool NAT
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
b . c is set
card (b . c) is epsilon-transitive epsilon-connected ordinal cardinal set
Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT
Seg (len (canFS (the_Vertices_of G))) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite len (canFS (the_Vertices_of G)) -element Element of bool NAT
(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]
((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set
(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
card (Seg c) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT
dom ((canFS (the_Vertices_of G)) | (Seg c)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT
proj2 (((canFS (the_Vertices_of G)) | (Seg c)) ") is set
proj1 ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a) is set
proj1 (((canFS (the_Vertices_of G)) | (Seg c)) ") is set
rng ((canFS (the_Vertices_of G)) | (Seg c)) is finite Element of bool (the_Vertices_of G)
card (proj1 ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a)) is epsilon-transitive epsilon-connected ordinal cardinal set
c is Relation-like NAT -defined Function-like total (G)
vb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
(G,c,va) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
(G,c,vb) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
va + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G,c,(va + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
vb + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
(G,c,(vb + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
card (G,c,vb) is epsilon-transitive epsilon-connected ordinal cardinal set
proj2 ((canFS (the_Vertices_of G)) ") is set
vc is set
(canFS (the_Vertices_of G)) ~ is Relation-like Function-like set
proj2 ((canFS (the_Vertices_of G)) ~) is set
dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT
card (G,c,vb) is epsilon-transitive epsilon-connected ordinal cardinal set
dom (G,c,vb) is finite Element of bool (the_Vertices_of G)
card (dom (G,c,vb)) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
proj1 ((canFS (the_Vertices_of G)) ") is set
card (proj1 ((canFS (the_Vertices_of G)) ")) is epsilon-transitive epsilon-connected ordinal cardinal set
rng (canFS (the_Vertices_of G)) is non empty finite Element of bool (the_Vertices_of G)
card (rng (canFS (the_Vertices_of G))) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT
card (dom (canFS (the_Vertices_of G))) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
c . va is set
vb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set
c . vb is set
va + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
c . (va + 1) is set
vb + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT
c . (vb + 1) is set
(G,c,va) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
(G,c,vb) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
(G,c,(va + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]
(G,c,(vb + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool