:: LEXBFS semantic presentation

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

K216(1,NAT) is M10( NAT )

proj1 G is set
L is set
V is set

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

{V} is non empty trivial finite 1 -element set
[:{L},{V}:] is non empty Relation-like finite set

G +* (L .--> V) is Relation-like Function-like set
proj1 (G +* (L .--> V)) is set
() \/ {L} is non empty set
dom (L .--> V) is trivial finite Element of bool {L}

() \/ (dom (L .--> V)) is set

L is set
V is set

(G | L) " is Relation-like Function-like set
proj1 ((G | L) ") is 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

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

{ } is set
card { } is epsilon-transitive epsilon-connected ordinal cardinal set
{ } is set
card { } is epsilon-transitive epsilon-connected ordinal cardinal set

{ } is set
card { } is epsilon-transitive epsilon-connected ordinal cardinal set

{ } is set
card { } is epsilon-transitive epsilon-connected ordinal cardinal set

{ } is set
vc is set

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

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

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

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

va \/ {(a . ((G + b) + 1))} is non empty finite set

a . P is Element of V
{ } is set
{ } is set
{ } is set

a . vc is Element of V

b is set

{ } is set

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

card { } is epsilon-transitive epsilon-connected ordinal cardinal set

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

V - G is ext-real V55() real V57() set
V - L is ext-real V55() real V57() set
bool () is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

L is Element of bool ()

proj1 G is set

proj1 L is set
() \/ () is set
a is set
G . a is set
L . a is set
(G . a) \/ (L . a) is set

proj1 a is 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

proj1 V is 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

a is set
a is set

((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

b is set

b is set

L is set
L is set

L is set
G . L is finite set
proj1 G is set

proj1 G is set
proj1 G is set

L is finite Element of bool G
V is finite Element of bool 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

a is set

proj1 G is set
L is set

L /\ () is set

proj1 a is set
b is set
proj2 a is set
c is set
a . c is set

proj2 (G +* a) is set

(rng G) \/ () is set

proj1 b is set
() \/ (L /\ ()) is set
c is set

a . c is set

c is set

va is set

proj1 a is set

proj1 b is set
c is 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)

a . (b + 1) is set

a . va is set

a . va is set

a . P is set

a . P is set

a . 1 is set

a . c is set

a . b is set

a . vb is 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

the_Vertices_of G is non empty set

() \/ () is non empty set

L . (len L) is set

a is set
V is set

() .adj V is Element of the_Vertices_of G

the_Vertices_of G is non empty set

() \/ () is non empty set

((2 * ()) + 1) - 1 is ext-real V55() real V57() even set

((2 * ()) + 1) - 1 is ext-real V55() real V57() even set

the_Vertices_of G is non empty set

() \/ () is non empty set

L . (len L) is set

a is set
V is set

() .adj V is Element of the_Vertices_of G

(L .addEdge V) . b is set
L . b is set

L . 0 is set

L . (0 + 1) is set

L . V is set

L . a is set

L . (V + 1) is set

L . (a + 1) is set

L . V is set

G . () is set

G . (() + V) is set

G . (() + (V + 1)) is set

G . (() + 1) is set

G . ((() + V) + 1) is set

G . (() + 0) is set

G . V is set

G . L is set

G . (L + 1) is set

G . () is set

G . V is set

G . (() + a) is set

G . (() + (a + 1)) is set

G . (() + 1) is set

G . ((() + a) + 1) is set

G . (() + 0) is set

G . V is set
G . L is set
G . () is set

the_Vertices_of G is non empty finite set

bool is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

L . V is set

L . V is set
the_Vertices_of G is non empty finite set

bool is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

the_Vertices_of G is non empty finite set

b is set

is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
(() | (Seg c)) " is Relation-like Function-like set

b . c is set

is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
(() | (Seg c)) " is Relation-like Function-like set

(() | (Seg va)) " is Relation-like Function-like set

b . c is set

is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
(() | (Seg c)) " is Relation-like Function-like set

vb is set

bool is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set
vb is set
proj1 (((() | (Seg c)) ") * a) is set
proj1 ((() | (Seg c)) ") is set
rng (() | (Seg c)) is finite Element of bool ()

b . c is set

b . c is set

(() | (Seg c)) " is Relation-like Function-like set

proj2 ((() | (Seg c)) ") is set
proj1 (((() | (Seg c)) ") * a) is set
proj1 ((() | (Seg c)) ") is set
rng (() | (Seg c)) is finite Element of bool ()
card (proj1 (((() | (Seg c)) ") * a)) is epsilon-transitive epsilon-connected ordinal cardinal set

proj2 (() ") is set
vc is set

proj2 (() ~) is set

dom (G,c,vb) is finite Element of bool ()

proj1 (() ") is set

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

c . va is set

c . vb is set

c . (va + 1) is set

c . (vb + 1) is set