:: SGRAPH1 semantic presentation

REAL is set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty cup-closed diff-closed preBoolean set

{} is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

2 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

3 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

4 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

Seg 3 is non empty finite 3 -element Element of bool NAT

{.2,3,.} is non empty finite set

o is set

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Seg VERTICES is finite VERTICES -element Element of bool NAT

p is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is V6() V7() V8() V12() ext-real non negative finite cardinal set

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal set

{ b

One is set

Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

{0} is non empty trivial finite V41() 1 -element set

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} \/ (Seg VERTICES) is non empty finite set

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

0 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} is non empty trivial finite V41() 1 -element set

{0} \/ (Seg VERTICES) is non empty finite set

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

{0} is non empty trivial finite V41() 1 -element set

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} \/ (Seg VERTICES) is non empty finite set

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

{0} is non empty trivial finite V41() 1 -element set

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} \/ (Seg VERTICES) is non empty finite set

o is V6() V7() V8() V12() ext-real non negative finite cardinal set

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal set

(o,VERTICES) is Element of bool NAT

{ b

One is set

Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

{0} is non empty trivial finite V41() 1 -element set

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} \/ (Seg VERTICES) is non empty finite set

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

0 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} is non empty trivial finite V41() 1 -element set

{0} \/ (Seg VERTICES) is non empty finite set

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

{0} is non empty trivial finite V41() 1 -element set

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} \/ (Seg VERTICES) is non empty finite set

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

{0} is non empty trivial finite V41() 1 -element set

Seg VERTICES is finite VERTICES -element Element of bool NAT

{0} \/ (Seg VERTICES) is non empty finite set

p is set

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(o,VERTICES) is finite Element of bool NAT

{ b

Three is set

ONE is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(One,Two) is finite Element of bool NAT

{ b

p is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(o,VERTICES) is finite Element of bool NAT

{ b

One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(1,o) is finite Element of bool NAT

{ b

Seg o is finite o -element Element of bool NAT

VERTICES is set

p is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

VERTICES is set

p is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(o,VERTICES) is finite Element of bool NAT

{ b

Seg VERTICES is finite VERTICES -element Element of bool NAT

p is set

One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Seg o is finite o -element Element of bool NAT

p is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(VERTICES,p) is finite Element of bool NAT

{ b

One is set

(Seg o) /\ (VERTICES,p) is finite Element of bool NAT

Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Three is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(o,VERTICES) is finite Element of bool NAT

{ b

p is set

One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is set

bool o is non empty cup-closed diff-closed preBoolean set

VERTICES is Element of bool o

p is set

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

VERTICES \/ {p} is non empty set

One is set

o is set

bool o is non empty cup-closed diff-closed preBoolean set

{ b

p is set

bool p is non empty cup-closed diff-closed preBoolean set

VERTICES is set

o is set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ b

One is set

Two is finite Element of bool p

card Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

(p) is set

{ b

o is set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ b

VERTICES is set

One is finite Element of bool o

card One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

One is finite Element of bool o

card One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

p is finite Element of bool o

One is finite Element of bool o

card One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

One is set

Two is set

{One,Two} is non empty finite set

Three is set

ONE is set

{Three,ONE} is non empty finite set

p is set

One is set

{p,One} is non empty finite set

p is Element of o

One is Element of o

{p,One} is non empty finite set

Two is finite Element of bool o

card Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Three is finite Element of bool o

card Three is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ b

VERTICES is set

o is set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ b

VERTICES is set

p is set

{VERTICES,p} is non empty finite set

One is set

Two is set

{One,Two} is non empty finite set

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

Three is set

ONE is set

{Three,ONE} is non empty finite set

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

Three is set

ONE is set

{Three,ONE} is non empty finite set

({}) is set

bool {} is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

o is set

VERTICES is set

p is set

{VERTICES,p} is non empty finite set

o is set

VERTICES is set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ b

(VERTICES) is set

bool VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

p is set

One is set

Two is set

{One,Two} is non empty finite set

o is finite set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

o is non empty non trivial set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ b

VERTICES is set

p is non empty non trivial set

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

p \ {VERTICES} is Element of bool p

bool p is non empty cup-closed diff-closed preBoolean set

One is set

{VERTICES,One} is non empty finite set

o is set

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

({o}) is set

bool {o} is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

VERTICES is set

p is set

One is set

{p,One} is non empty finite set

o is set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

{} ({}) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool ({})

bool ({}) is non empty cup-closed diff-closed preBoolean set

({},({} ({}))) is () ()

o is set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

VERTICES is finite Element of bool o

(VERTICES) is set

bool VERTICES is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool (VERTICES) is non empty cup-closed diff-closed preBoolean set

p is finite Element of bool (VERTICES)

(VERTICES,p) is () ()

o is set

(o) is set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

o is set

(o) is non empty set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

p is set

bool p is non empty cup-closed diff-closed preBoolean set

Two is finite Element of bool p

(Two) is set

bool Two is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool (Two) is non empty cup-closed diff-closed preBoolean set

VERTICES is set

o is set

(o) is non empty set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

One is set

Three is finite Element of bool (Two)

(Two,Three) is () ()

(p) is non empty set

{ (b

o is set

VERTICES is () (o)

the carrier of VERTICES is set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

(o) is non empty set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

p is finite Element of bool o

(p) is set

bool p is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool (p) is non empty cup-closed diff-closed preBoolean set

One is finite Element of bool (p)

(p,One) is () ()

o is set

p is set

VERTICES is () (o)

the of VERTICES is Element of bool ( the carrier of VERTICES)

the carrier of VERTICES is set

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

o is set

p is set

One is set

{p,One} is non empty finite set

VERTICES is () (o)

the of VERTICES is Element of bool ( the carrier of VERTICES)

the carrier of VERTICES is set

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

o is set

bool o is non empty cup-closed diff-closed preBoolean set

VERTICES is () (o)

the carrier of VERTICES is set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

(o) is non empty set

{ (b

p is finite Element of bool o

(p) is set

bool p is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool (p) is non empty cup-closed diff-closed preBoolean set

One is finite Element of bool (p)

(p,One) is () ()

o is set

F

(F

bool F

{ (b

o is set

p is finite Element of bool F

(p) is set

bool p is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool (p) is non empty cup-closed diff-closed preBoolean set

One is finite Element of bool (p)

(p,One) is () ()

VERTICES is () (F

the carrier of VERTICES is set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

p is non empty set

Fin p is non empty cup-closed diff-closed preBoolean set

One is finite Element of Fin p

(One) is set

bool One is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

{} (One) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool (One)

bool (One) is non empty cup-closed diff-closed preBoolean set

(One,({} (One))) is () ()

bool p is non empty cup-closed diff-closed preBoolean set

Two is Element of p

ONE is () (F

the carrier of ONE is set

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

the carrier of ONE \/ {Two} is non empty set

(( the carrier of ONE \/ {Two})) is set

bool ( the carrier of ONE \/ {Two}) is non empty cup-closed diff-closed preBoolean set

{ b

{} (( the carrier of ONE \/ {Two})) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool (( the carrier of ONE \/ {Two}))

bool (( the carrier of ONE \/ {Two})) is non empty cup-closed diff-closed preBoolean set

(( the carrier of ONE \/ {Two}),({} (( the carrier of ONE \/ {Two})))) is () ()

One \/ {Two} is non empty finite set

((One \/ {Two})) is set

bool (One \/ {Two}) is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

{} ((One \/ {Two})) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool ((One \/ {Two}))

bool ((One \/ {Two})) is non empty cup-closed diff-closed preBoolean set

((One \/ {Two}),({} ((One \/ {Two})))) is () ()

{}. p is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of Fin p

(({}. p)) is set

bool ({}. p) is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

{} (({}. p)) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool (({}. p))

bool (({}. p)) is non empty cup-closed diff-closed preBoolean set

(({}. p),({} (({}. p)))) is () ()

One is finite Element of Fin p

(One) is set

bool One is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

Fin (One) is non empty cup-closed diff-closed preBoolean set

bool (One) is non empty cup-closed diff-closed preBoolean set

Two is finite Element of Fin (One)

Three is Element of bool (One)

{} (One) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool (One)

(One,Three) is () ()

One is finite Element of Fin p

(One) is set

bool One is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

Two is non empty set

Fin Two is non empty cup-closed diff-closed preBoolean set

bool (One) is non empty cup-closed diff-closed preBoolean set

Three is finite Element of Fin Two

ONE is Element of Two

TWO is Element of bool (One)

(One,TWO) is () ()

pp is () (F

the carrier of pp is set

( the carrier of pp) is set

bool the carrier of pp is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of pp) is non empty cup-closed diff-closed preBoolean set

the of pp is Element of bool ( the carrier of pp)

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

the of pp \/ {ONE} is non empty set

{.ONE.} is non empty trivial finite 1 -element Element of Fin Two

Three \/ {.ONE.} is non empty finite Element of Fin Two

i is Element of bool (One)

(One,i) is () ()

j is Element of bool ( the carrier of pp)

( the carrier of pp,j) is () ()

{}. Two is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of Fin Two

Three is Element of bool (One)

(One,Three) is () ()

{} (One) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool (One)

Fin (One) is non empty cup-closed diff-closed preBoolean set

ONE is Element of bool (One)

Three is finite Element of Fin (One)

(One,ONE) is () ()

One is finite Element of Fin p

(One) is set

bool One is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

Fin ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

One is finite Element of bool F

(One) is set

bool One is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool (One) is non empty cup-closed diff-closed preBoolean set

Two is finite Element of bool (One)

(One,Two) is () ()

o is set

VERTICES is () (o)

the carrier of VERTICES is set

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES, the of VERTICES) is () ()

o is set

bool o is non empty cup-closed diff-closed preBoolean set

(o) is non empty set

{ (b

VERTICES is Element of bool o

(VERTICES) is set

bool VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool (VERTICES) is non empty cup-closed diff-closed preBoolean set

p is Element of bool (VERTICES)

(VERTICES,p) is () ()

One is set

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

VERTICES \/ {One} is non empty set

((VERTICES \/ {One})) is set

bool (VERTICES \/ {One}) is non empty cup-closed diff-closed preBoolean set

{ b

bool ((VERTICES \/ {One})) is non empty cup-closed diff-closed preBoolean set

Two is finite Element of bool ((VERTICES \/ {One}))

((VERTICES \/ {One}),Two) is () ()

ONE is () (o)

the carrier of ONE is set

o is set

bool o is non empty cup-closed diff-closed preBoolean set

(o) is non empty set

{ (b

VERTICES is Element of bool o

(VERTICES) is set

bool VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool (VERTICES) is non empty cup-closed diff-closed preBoolean set

p is Element of bool (VERTICES)

(VERTICES,p) is () ()

One is set

Two is set

{One,Two} is non empty finite set

{{One,Two}} is non empty trivial finite V41() 1 -element set

p \/ {{One,Two}} is non empty set

ONE is () (o)

the of ONE is Element of bool ( the carrier of ONE)

the carrier of ONE is set

( the carrier of ONE) is set

bool the carrier of ONE is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of ONE) is non empty cup-closed diff-closed preBoolean set

TWO is finite Element of bool o

(TWO) is set

bool TWO is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

THREE is set

bool (TWO) is non empty cup-closed diff-closed preBoolean set

THREE is finite Element of bool (TWO)

(TWO,THREE) is () ()

o is set

(o) is non empty set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

VERTICES is Element of bool o

(VERTICES) is set

bool VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool (VERTICES) is non empty cup-closed diff-closed preBoolean set

One is set

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

VERTICES \/ {One} is non empty set

((VERTICES \/ {One})) is set

bool (VERTICES \/ {One}) is non empty cup-closed diff-closed preBoolean set

{ b

bool ((VERTICES \/ {One})) is non empty cup-closed diff-closed preBoolean set

p is Element of bool (VERTICES)

(VERTICES,p) is () ()

Two is finite Element of bool ((VERTICES \/ {One}))

((VERTICES \/ {One}),Two) is () ()

VERTICES is Element of bool o

(VERTICES) is set

bool VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool (VERTICES) is non empty cup-closed diff-closed preBoolean set

p is Element of bool (VERTICES)

(VERTICES,p) is () ()

One is set

Two is set

{One,Two} is non empty finite set

{{One,Two}} is non empty trivial finite V41() 1 -element set

p \/ {{One,Two}} is non empty set

o is set

(o) is non empty set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

VERTICES is set

p is () (o)

the carrier of p is set

One is set

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

the carrier of p \/ {One} is non empty set

(( the carrier of p \/ {One})) is set

bool ( the carrier of p \/ {One}) is non empty cup-closed diff-closed preBoolean set

{ b

{} (( the carrier of p \/ {One})) is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of bool (( the carrier of p \/ {One}))

bool (( the carrier of p \/ {One})) is non empty cup-closed diff-closed preBoolean set

(( the carrier of p \/ {One}),({} (( the carrier of p \/ {One})))) is () ()

p is () (o)

the carrier of p is set

( the carrier of p) is set

bool the carrier of p is non empty cup-closed diff-closed preBoolean set

{ b

the of p is Element of bool ( the carrier of p)

bool ( the carrier of p) is non empty cup-closed diff-closed preBoolean set

One is set

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

the of p \/ {One} is non empty set

ONE is set

TWO is set

{ONE,TWO} is non empty finite set

{{ONE,TWO}} is non empty trivial finite V41() 1 -element set

the of p \/ {{ONE,TWO}} is non empty set

THREE is finite Element of bool ( the carrier of p)

( the carrier of p,THREE) is () ()

p is set

o is set

(o) is non empty set

bool o is non empty cup-closed diff-closed preBoolean set

{ (b

VERTICES is set

p is set

(VERTICES) is non empty set

bool VERTICES is non empty cup-closed diff-closed preBoolean set

{ (b

o is set

VERTICES is () (o)

the carrier of VERTICES is set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

o is set

VERTICES is () (o)

the of VERTICES is Element of bool ( the carrier of VERTICES)

the carrier of VERTICES is set

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

p is set

One is set

Two is set

Two is finite set

card Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Three is set

ONE is set

One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Three is finite set

card Three is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

ONE is finite set

card ONE is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Three is finite set

card Three is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

ONE is finite set

card ONE is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

TWO is set

TWO is set

o is non empty set

VERTICES is () (o)

the carrier of VERTICES is set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

p is set

{ b

(o,VERTICES,p) is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Two is finite set

card Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Three is set

{p,Three} is non empty finite set

ONE is Element of o

{p,ONE} is non empty finite set

bool o is non empty cup-closed diff-closed preBoolean set

Three is set

Three is finite set

card Three is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

{ [b

TWO is set

THREE is set

[TWO,THREE] is non empty V22() set

{TWO,THREE} is non empty finite set

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

{{TWO,THREE},{TWO}} is non empty finite V41() set

pp is set

i is set

[pp,i] is non empty V22() set

{pp,i} is non empty finite set

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

{{pp,i},{pp}} is non empty finite V41() set

j is Element of o

{p,j} is non empty finite set

[j,{p,j}] is non empty V22() set

{j,{p,j}} is non empty finite set

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

{{j,{p,j}},{j}} is non empty finite V41() set

w2 is Element of o

{p,w2} is non empty finite set

[w2,{p,w2}] is non empty V22() set

{w2,{p,w2}} is non empty finite set

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

{{w2,{p,w2}},{w2}} is non empty finite V41() set

[TWO,THREE] `1 is set

[w2,{p,w2}] `1 is set

[w2,{p,w2}] `2 is set

[TWO,THREE] `2 is set

[pp,i] `1 is set

TWO is set

{p,TWO} is non empty finite set

[TWO,{p,TWO}] is non empty V22() set

{TWO,{p,TWO}} is non empty finite set

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

{{TWO,{p,TWO}},{TWO}} is non empty finite V41() set

THREE is Element of o

{p,THREE} is non empty finite set

[THREE,{p,THREE}] is non empty V22() set

{THREE,{p,THREE}} is non empty finite set

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

{{THREE,{p,THREE}},{THREE}} is non empty finite V41() set

[THREE,{p,THREE}] `1 is set

bool o is non empty cup-closed diff-closed preBoolean set

THREE is Element of o

{p,THREE} is non empty finite set

[THREE,{p,THREE}] is non empty V22() set

{THREE,{p,THREE}} is non empty finite set

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

{{THREE,{p,THREE}},{THREE}} is non empty finite V41() set

pp is Element of o

{p,pp} is non empty finite set

[pp,{p,pp}] is non empty V22() set

{pp,{p,pp}} is non empty finite set

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

{{pp,{p,pp}},{pp}} is non empty finite V41() set

TWO is set

THREE is set

pp is set

{THREE,pp} is non empty finite set

{p,pp} is non empty finite set

{p,THREE} is non empty finite set

THREE is set

{p,THREE} is non empty finite set

THREE is set

{p,THREE} is non empty finite set

[THREE,TWO] is non empty V22() set

{THREE,TWO} is non empty finite set

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

{{THREE,TWO},{THREE}} is non empty finite V41() set

TWO is set

{p,TWO} is non empty finite set

[TWO,{p,TWO}] is non empty V22() set

{TWO,{p,TWO}} is non empty finite set

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

{{TWO,{p,TWO}},{TWO}} is non empty finite V41() set

TWO is set

THREE is set

pp is set

i is set

[pp,i] is non empty V22() set

{pp,i} is non empty finite set

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

{{pp,i},{pp}} is non empty finite V41() set

j is set

w2 is set

[j,w2] is non empty V22() set

{j,w2} is non empty finite set

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

{{j,w2},{j}} is non empty finite V41() set

o is non empty set

VERTICES is () (o)

the carrier of VERTICES is set

p is set

(o,VERTICES,p) is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

One is finite set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

{ b

Two is finite set

card Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

{p,p} is non empty finite set

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

Three is Element of o

{p,Three} is non empty finite set

Three is set

ONE is set

{Three,ONE} is non empty finite set

card One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Three is set

ONE is Element of o

{p,ONE} is non empty finite set

0 is V6() V7() V8() V10() V11() V12() functional empty trivial ext-real non positive non negative finite V41() cardinal {} -element FinSequence-membered Element of NAT

o is set

VERTICES is () (o)

the of VERTICES is Element of bool ( the carrier of VERTICES)

the carrier of VERTICES is set

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

One is set

p is set

(o,VERTICES,p) is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Two is finite set

card Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is set

VERTICES is () (o)

the carrier of VERTICES is set

the of VERTICES is Element of bool ( the carrier of VERTICES)

( the carrier of VERTICES) is set

bool the carrier of VERTICES is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set

p is set

(o,VERTICES,p) is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

1 + (o,VERTICES,p) is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

One is finite set

card One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

bool o is non empty cup-closed diff-closed preBoolean set

Three is Element of One

{p,Three} is non empty finite set

Two is non empty set

{ b

ONE is finite set

card ONE is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

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

ONE \/ {p} is non empty finite set

THREE is Element of Two

{p,THREE} is non empty finite set

bool One is non empty cup-closed diff-closed preBoolean finite V41() set

THREE is finite Element of bool One

card THREE is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

THREE is Element of Two

{p,THREE} is non empty finite set

THREE is set

pp is Element of Two

{p,pp} is non empty finite set

TWO is finite set

THREE is set

card TWO is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

1 + (card ONE) is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

o is set

VERTICES is () (o)

the carrier of VERTICES is set

o is set

VERTICES is () (o)

the carrier of VERTICES is set

the carrier of VERTICES * is functional non empty FinSequence-membered M8( the carrier of VERTICES)

p is Element of the carrier of VERTICES

One is Element of the carrier of VERTICES

{ b

bool ( the carrier of VERTICES *) is non empty cup-closed diff-closed preBoolean set

Three is set

ONE is V1() V4( NAT ) V5( the carrier of VERTICES) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of VERTICES *

o is set

VERTICES is () (o)

the carrier of VERTICES is set

Three is set

ONE is () (Three)

the carrier of ONE is set

the carrier of ONE * is functional non empty FinSequence-membered M8( the carrier of ONE)

Two is set

p is Element of the carrier of VERTICES

One is Element of the carrier of VERTICES

(o,VERTICES,p,One) is functional FinSequence-membered Element of bool ( the carrier of VERTICES *)

the carrier of VERTICES * is functional non empty FinSequence-membered M8( the carrier of VERTICES)

bool ( the carrier of VERTICES *) is non empty cup-closed diff-closed preBoolean set

{ b

pp is set

i is V1() V4( NAT ) V5( the carrier of ONE) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of ONE *

TWO is Element of the carrier of ONE

THREE is Element of the carrier of ONE

(Three,ONE,TWO,THREE) is functional FinSequence-membered Element of bool ( the carrier of ONE *)

bool ( the carrier of ONE *) is non empty cup-closed diff-closed preBoolean set

{ b

o is set

VERTICES is () (o)

the carrier of VERTICES is set

the carrier of VERTICES * is functional non empty FinSequence-membered M8( the carrier of VERTICES)

p is Element of the carrier of VERTICES

One is Element of the carrier of VERTICES

Two is V1() V4( NAT ) V5( the carrier of VERTICES) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of VERTICES *

(o,VERTICES,p,One) is functional FinSequence-membered Element of bool ( the carrier of VERTICES *)

bool ( the carrier of VERTICES *) is non empty cup-closed diff-closed preBoolean set

{ b

o is set

VERTICES is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

VERTICES + o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Seg (VERTICES + o) is finite VERTICES + o -element Element of bool NAT

((Seg (VERTICES + o))) is set

bool (Seg (VERTICES + o)) is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool ((Seg (VERTICES + o))) is non empty cup-closed diff-closed preBoolean set

Seg VERTICES is finite VERTICES -element Element of bool NAT

VERTICES + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

((VERTICES + 1),(VERTICES + o)) is finite Element of bool NAT

{ b

{ {b

ONE is set

TWO is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

THREE is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

{TWO,THREE} is non empty finite V41() set

pp is set

(Seg VERTICES) /\ ((VERTICES + 1),(VERTICES + o)) is finite Element of bool NAT

ONE is finite Element of bool ((Seg (VERTICES + o)))

((Seg (VERTICES + o)),ONE) is () ()

(NAT) is non empty set

{ (b

THREE is () ( NAT )

pp is Element of bool ((Seg (VERTICES + o)))

((Seg (VERTICES + o)),pp) is () ()

Two is Element of bool ((Seg (VERTICES + o)))

p is () ( NAT )

((Seg (VERTICES + o)),Two) is () ()

Three is Element of bool ((Seg (VERTICES + o)))

One is () ( NAT )

((Seg (VERTICES + o)),Three) is () ()

o is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Seg o is finite o -element Element of bool NAT

((Seg o)) is set

bool (Seg o) is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool ((Seg o)) is non empty cup-closed diff-closed preBoolean set

{ {b

p is set

One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

{One,Two} is non empty finite V41() set

Three is set

p is finite Element of bool ((Seg o))

((Seg o),p) is () ()

(NAT) is non empty set

{ (b

Two is () ( NAT )

One is finite Element of bool ((Seg o))

VERTICES is () ( NAT )

((Seg o),One) is () ()

Two is finite Element of bool ((Seg o))

p is () ( NAT )

((Seg o),Two) is () ()

(3) is () ( NAT )

() is () ( NAT )

((Seg 3)) is set

bool (Seg 3) is non empty cup-closed diff-closed preBoolean finite V41() set

{ b

bool ((Seg 3)) is non empty cup-closed diff-closed preBoolean set

Fin NAT is non empty cup-closed diff-closed preBoolean set

{.1,2.} is non empty finite V41() Element of Fin NAT

{.2,3.} is non empty finite V41() Element of Fin NAT

{.3,1.} is non empty finite V41() Element of Fin NAT

{.{.1,2.},{.2,3.},{.3,1.}.} is non empty finite Element of Fin (Fin NAT)

Fin (Fin NAT) is non empty cup-closed diff-closed preBoolean set

{ {b

o is finite Element of bool ((Seg 3))

((Seg 3),o) is () ()

VERTICES is set

p is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

{p,One} is non empty finite V41() set

VERTICES is set

{1,2} is non empty finite V41() set

p is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

{p,One} is non empty finite V41() set

p is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

{p,One} is non empty finite V41() set

{2,3} is non empty finite V41() set

p is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

{p,One} is non empty finite V41() set

p is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

{p,One} is non empty finite V41() set

{3,1} is non empty finite V41() set

p is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

{p,One} is non empty finite V41() set

p is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

One is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

{p,One} is non empty finite V41() set

{1,2} is non empty finite V41() set

{2,3} is non empty finite V41() set

{3,1} is non empty finite V41() set

the carrier of () is set

the of () is Element of bool ( the carrier of ())

( the carrier of ()) is set

bool the carrier of () is non empty cup-closed diff-closed preBoolean set

{ b

bool ( the carrier of ()) is non empty cup-closed diff-closed preBoolean set

o is Element of bool ((Seg 3))

((Seg 3),o) is () ()

{1,2} is non empty finite V41() set

{2,3} is non empty finite V41() set

{3,1} is non empty finite V41() set

o is Element of bool ((Seg 3))

((Seg 3),o) is () ()

<*1*> is V1() V4( NAT ) V5( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

<*2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

<*1*> ^ <*2*> is V1() V4( NAT ) V5( NAT ) Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

1 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

<*3*> is V1() V4( NAT ) V5( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

(<*1*> ^ <*2*>) ^ <*3*> is V1() V4( NAT ) V5( NAT ) Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

(1 + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is V1() V4( NAT ) V5( NAT ) Function-like non empty finite ((1 + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

((1 + 1) + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

VERTICES is Element of bool ((Seg 3))

((Seg 3),VERTICES) is () ()

p is Element of bool ((Seg 3))

((Seg 3),p) is () ()

(((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 1 is set

VERTICES is non empty set

ONE is Element of bool ((Seg 3))

((Seg 3),ONE) is () ()

(((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 2 is set

One is Element of VERTICES

<*One*> is V1() V4( NAT ) V5(VERTICES) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of VERTICES

Two is Element of VERTICES

<*Two*> is V1() V4( NAT ) V5(VERTICES) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of VERTICES

Three is Element of VERTICES

<*Three*> is V1() V4( NAT ) V5(VERTICES) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of VERTICES

ONE is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()

TWO is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()

ONE ^ TWO is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()

THREE is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()

(ONE ^ TWO) ^ THREE is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()

((ONE ^ TWO) ^ THREE) ^ ONE is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()

the carrier of () * is functional non empty FinSequence-membered M8( the carrier of ())

(((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 3 is set

(((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 4 is set

i is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

3 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *

pp . i is set

i + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j is Element of bool ((Seg 3))

((Seg 3),j) is () ()

pp is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *

pp . i is set

i + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j is Element of bool ((Seg 3))

((Seg 3),j) is () ()

pp is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *

pp . i is set

i + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j is Element of bool ((Seg 3))

((Seg 3),j) is () ()

pp is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *

pp is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *

i is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

len pp is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

j is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

i + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . i is set

o is Element of the carrier of ()

2 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . j is set

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (j + 1) is set

{(pp . j),(pp . (j + 1))} is non empty finite set

pp . j is set

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (j + 1) is set

{(pp . j),(pp . (j + 1))} is non empty finite set

pp . j is set

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (j + 1) is set

{(pp . j),(pp . (j + 1))} is non empty finite set

pp . j is set

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (j + 1) is set

{(pp . j),(pp . (j + 1))} is non empty finite set

pp . i is set

pp . j is set

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (j + 1) is set

{(pp . j),(pp . (j + 1))} is non empty finite set

pp . i is set

pp . j is set

pp . (i + 1) is set

{(pp . i),(pp . (i + 1))} is non empty finite set

j + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

pp . (j + 1) is set

{(pp . j),(pp . (j + 1))} is non empty finite set

o is Element of the carrier of ()

(NAT,(),o,o) is functional FinSequence-membered Element of bool ( the carrier of () *)

bool ( the carrier of () *) is non empty cup-closed diff-closed preBoolean set

{ b