:: SGRAPH1 semantic presentation

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

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal 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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( o <= b1 & b1 <= VERTICES ) } is set
One is set
Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

is non empty trivial finite V41() 1 -element set
Seg VERTICES is finite VERTICES -element Element of bool NAT
\/ (Seg VERTICES) is non empty finite set

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
is non empty trivial finite V41() 1 -element set
\/ (Seg VERTICES) is non empty finite set

is non empty trivial finite V41() 1 -element set
Seg VERTICES is finite VERTICES -element Element of bool NAT
\/ (Seg VERTICES) is non empty finite set

is non empty trivial finite V41() 1 -element set
Seg VERTICES is finite VERTICES -element Element of bool NAT
\/ (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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( o <= b1 & b1 <= VERTICES ) } is set
One is set
Two is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT

is non empty trivial finite V41() 1 -element set
Seg VERTICES is finite VERTICES -element Element of bool NAT
\/ (Seg VERTICES) is non empty finite set

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
is non empty trivial finite V41() 1 -element set
\/ (Seg VERTICES) is non empty finite set

is non empty trivial finite V41() 1 -element set
Seg VERTICES is finite VERTICES -element Element of bool NAT
\/ (Seg VERTICES) is non empty finite set

is non empty trivial finite V41() 1 -element set
Seg VERTICES is finite VERTICES -element Element of bool NAT
\/ (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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( o <= b1 & b1 <= VERTICES ) } is set
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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( One <= b1 & b1 <= Two ) } 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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( o <= b1 & b1 <= VERTICES ) } is set
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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( 1 <= b1 & b1 <= o ) } is set

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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( o <= b1 & b1 <= VERTICES ) } is set
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

p is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT
(VERTICES,p) is finite Element of bool NAT
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( VERTICES <= b1 & b1 <= p ) } is set
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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( o <= b1 & b1 <= VERTICES ) } is set
p is set
One is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT
o is 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

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
p is set

VERTICES is set
o is set
(o) is set

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool p : card b1 = 2 } is set
o is set
(o) is set

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
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

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
VERTICES is set
o is set
(o) is set

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
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

{ b1 where b1 is finite Element of bool {} : card b1 = 2 } is set
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

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
(VERTICES) is set
bool VERTICES is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of bool VERTICES : card b1 = 2 } is set
p is set
One is set
Two is set
{One,Two} is non empty finite set
o is finite set
(o) is set

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
o is non empty non trivial set
(o) is set

{ b1 where b1 is finite Element of bool o : card b1 = 2 } is set
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

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

{ b1 where b1 is finite Element of bool {o} : card b1 = 2 } is set
VERTICES is set
p is set
One is set
{p,One} is non empty finite set
o is set

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set

({},({} ({}))) is () ()
o is set
(o) is set

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
VERTICES is finite Element of bool o
(VERTICES) is set
bool VERTICES is non empty cup-closed diff-closed preBoolean finite V41() set
{ b1 where b1 is finite Element of bool VERTICES : card b1 = 2 } is set
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

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
o is set
(o) is non empty set

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
p is set

Two is finite Element of bool p
(Two) is set
bool Two is non empty cup-closed diff-closed preBoolean finite V41() set
{ b1 where b1 is finite Element of bool Two : card b1 = 2 } is set
bool (Two) is non empty cup-closed diff-closed preBoolean set
VERTICES is set
o is set
(o) is non empty set

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
One is set
Three is finite Element of bool (Two)
(Two,Three) is () ()
(p) is non empty set
{ (b1,b2) where b1 is finite Element of bool p, b2 is finite Element of bool (b1) : verum } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set
(o) is non empty set

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
p is finite Element of bool o
(p) is set

{ b1 where b1 is finite Element of bool p : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set
(o) is non empty set
{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
p is finite Element of bool o
(p) is set

{ b1 where b1 is finite Element of bool p : card b1 = 2 } is set
bool (p) is non empty cup-closed diff-closed preBoolean set
One is finite Element of bool (p)
(p,One) is () ()
o is set
F1() is set
(F1()) is non empty set
bool F1() is non empty cup-closed diff-closed preBoolean set
{ (b1,b2) where b1 is finite Element of bool F1(), b2 is finite Element of bool (b1) : verum } is set
o is set
p is finite Element of bool F1()
(p) is set

{ b1 where b1 is finite Element of bool p : card b1 = 2 } is set
bool (p) is non empty cup-closed diff-closed preBoolean set
One is finite Element of bool (p)
(p,One) is () ()
VERTICES is () (F1())
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set
p is non empty set

One is finite Element of Fin p
(One) is set
bool One is non empty cup-closed diff-closed preBoolean finite V41() set
{ b1 where b1 is finite Element of bool One : card b1 = 2 } is set
{} (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 () ()

Two is Element of p
ONE is () (F1())
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
{ b1 where b1 is finite Element of bool ( the carrier of ONE \/ {Two}) : card b1 = 2 } is set
{} (( 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
{ b1 where b1 is finite Element of bool (One \/ {Two}) : card b1 = 2 } is set
{} ((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 set
bool ({}. p) is non empty cup-closed diff-closed preBoolean finite V41() set
{ b1 where b1 is finite Element of bool ({}. p) : card b1 = 2 } is set
{} (({}. 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
{ b1 where b1 is finite Element of bool One : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool One : card b1 = 2 } is set
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 () (F1())
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
{ b1 where b1 is finite Element of bool the carrier of pp : card b1 = 2 } is set
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 () ()

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
{ b1 where b1 is finite Element of bool One : card b1 = 2 } 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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
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 F1()
(One) is set
bool One is non empty cup-closed diff-closed preBoolean finite V41() set
{ b1 where b1 is finite Element of bool One : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
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

(o) is non empty set
{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
VERTICES is Element of bool o
(VERTICES) is set
bool VERTICES is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of bool VERTICES : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool (VERTICES \/ {One}) : card b1 = 2 } is set
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

(o) is non empty set
{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
VERTICES is Element of bool o
(VERTICES) is set
bool VERTICES is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of bool VERTICES : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool the carrier of ONE : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool TWO : card b1 = 2 } is set
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

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
VERTICES is Element of bool o
(VERTICES) is set
bool VERTICES is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of bool VERTICES : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool (VERTICES \/ {One}) : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool VERTICES : card b1 = 2 } is set
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

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
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
{ b1 where b1 is finite Element of bool ( the carrier of p \/ {One}) : card b1 = 2 } is set
{} (( 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
{ b1 where b1 is finite Element of bool the carrier of p : card b1 = 2 } is set
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

{ (b1,b2) where b1 is finite Element of bool o, b2 is finite Element of bool (b1) : verum } is set
VERTICES is set
p is set
(VERTICES) is non empty set
bool VERTICES is non empty cup-closed diff-closed preBoolean set
{ (b1,b2) where b1 is finite Element of bool VERTICES, b2 is finite Element of bool (b1) : verum } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set
p is set
{ b1 where b1 is Element of o : ( b1 in the carrier of VERTICES & {p,b1} in the of VERTICES ) } 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
Three is set
{p,Three} is non empty finite set
ONE is Element of o
{p,ONE} is non empty finite set

Three is set
Three is finite set
card Three is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT
{ [b1,{p,b1}] where b1 is Element of o : ( b1 in Three & {p,b1} in Two ) } is set
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

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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
bool ( the carrier of VERTICES) is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is Element of o : ( b1 in One & {p,b1} in the of VERTICES ) } is set
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

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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
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
{ b1 where b1 is finite Element of bool the carrier of VERTICES : card b1 = 2 } is set
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

Three is Element of One
{p,Three} is non empty finite set
Two is non empty set
{ b1 where b1 is Element of Two : ( b1 in One & {p,b1} in the of VERTICES ) } is set
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
{ b1 where b1 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,b1) } is set
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
{ b1 where b1 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,b1) } is set
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
{ b1 where b1 is V1() V4( NAT ) V5( the carrier of ONE) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of ONE * : (Three,ONE,TWO,THREE,b1) } 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
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
{ b1 where b1 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,b1) } is set
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
{ b1 where b1 is finite Element of bool (Seg (VERTICES + o)) : card b1 = 2 } is set
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
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( VERTICES + 1 <= b1 & b1 <= VERTICES + o ) } is set
{ {b1,b2} where b1, b2 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( b1 in Seg VERTICES & b2 in ((VERTICES + 1),(VERTICES + o)) ) } is set
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
{ (b1,b2) where b1 is finite Element of bool NAT, b2 is finite Element of bool (b1) : verum } is set
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 set
bool (Seg o) is non empty cup-closed diff-closed preBoolean finite V41() set
{ b1 where b1 is finite Element of bool (Seg o) : card b1 = 2 } is set
bool ((Seg o)) is non empty cup-closed diff-closed preBoolean set
{ {b1,b2} where b1, b2 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( b1 in Seg o & b2 in Seg o & not b1 = b2 ) } is set
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
{ (b1,b2) where b1 is finite Element of bool NAT, b2 is finite Element of bool (b1) : verum } is set
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
{ b1 where b1 is finite Element of bool (Seg 3) : card b1 = 2 } is set
bool ((Seg 3)) 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 ()

{ {b1,b2} where b1, b2 is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT : ( b1 in Seg 3 & b2 in Seg 3 & not b1 = b2 ) } is set
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
{ b1 where b1 is finite Element of bool the carrier of () : card b1 = 2 } is set
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 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT

(1 + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative finite cardinal Element of NAT
(() ^ <*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 () ()
((() ^ <*3*>) ^ <*1*>) . 1 is set
VERTICES is non empty set
ONE is Element of bool ((Seg 3))
((Seg 3),ONE) is () ()
((() ^ <*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 ())
((() ^ <*3*>) ^ <*1*>) . 3 is set
((() ^ <*3*>) ^ <*1*>) . 4 is set
i is V6() V7() V8() V12() ext-real non negative finite cardinal Element of NAT
len ((() ^ <*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
{ b1 where b1 is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () * : ( NAT ,(),o,o,b1) } is set