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