:: PETRI semantic presentation

K162() is Element of bool K158()
K158() is set
bool K158() is non empty set
K120() is set
bool K120() is non empty set
bool K162() is non empty set
K237() is set
{} is empty Relation-like non-empty empty-yielding V55() V58() V61() set
the empty Relation-like non-empty empty-yielding V55() V58() V61() set is empty Relation-like non-empty empty-yielding V55() V58() V61() set
1 is non empty set
PTN is non empty set
t is non empty set
[:PTN,t:] is non empty Relation-like set
bool [:PTN,t:] is non empty set
S0 is non empty Relation-like PTN -defined t -valued Element of bool [:PTN,t:]
s is Element of S0
{{}} is non empty set
[#] ({{}},{{}}) is non empty Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is non empty Relation-like set
bool [:{{}},{{}}:] is non empty set
({{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}}))) is () ()
() is ()
the of () is Relation-like the carrier of () -defined the carrier' of () -valued Element of bool [: the carrier of (), the carrier' of ():]
the carrier of () is set
the carrier' of () is set
[: the carrier of (), the carrier' of ():] is Relation-like set
bool [: the carrier of (), the carrier' of ():] is non empty set
the of () is Relation-like the carrier' of () -defined the carrier of () -valued Element of bool [: the carrier' of (), the carrier of ():]
[: the carrier' of (), the carrier of ():] is Relation-like set
bool [: the carrier' of (), the carrier of ():] is non empty set
PTN is () ()
the of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the carrier of PTN is set
the carrier' of PTN is set
[: the carrier of PTN, the carrier' of PTN:] is Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
PTN is () ()
the of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
the carrier' of PTN is set
the carrier of PTN is set
[: the carrier' of PTN, the carrier of PTN:] is Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
t is ( the carrier of PTN, the carrier' of PTN, the of PTN)
t `1 is set
t `1 is Element of the carrier of PTN
t `2 is set
t `2 is Element of the carrier' of PTN
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
t is ( the carrier' of PTN, the carrier of PTN, the of PTN)
t `1 is set
t `1 is Element of the carrier' of PTN
t `2 is set
t `2 is Element of the carrier of PTN
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
t is Element of bool the carrier of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : S₁[b₁] } is set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
{ b₁ where b₁ is Element of the carrier' of PTN : S₁[b₁] } is set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
{ (PTN,b₁) where b₁ is ( the carrier' of PTN, the carrier of PTN, the of PTN) : (PTN,b₁) in t } is set
S0 is set
s is Element of the carrier' of PTN
t0 is Element of the carrier of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
t0 is Element of the carrier of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
(PTN,f) is Element of the carrier' of PTN
(PTN,f) is Element of the carrier of PTN
S0 is set
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
(PTN,s) is Element of the carrier' of PTN
(PTN,s) is Element of the carrier of PTN
[(PTN,s),(PTN,s)] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{(PTN,s),(PTN,s)} is non empty set
{(PTN,s)} is non empty set
{{(PTN,s),(PTN,s)},{(PTN,s)}} is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
S0 is set
s is Element of the carrier' of PTN
t0 is Element of the carrier of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
t0 is Element of the carrier of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
[S0,t0] is V9() set
{S0,t0} is non empty set
{S0} is non empty set
{{S0,t0},{S0}} is non empty set
f is Element of the carrier of PTN
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[S0,f] is V9() set
{S0,f} is non empty set
{S0} is non empty set
{{S0,f},{S0}} is non empty set
(PTN,s) is Element of the carrier' of PTN
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
{ (PTN,b₁) where b₁ is ( the carrier of PTN, the carrier' of PTN, the of PTN) : (PTN,b₁) in t } is set
S0 is set
s is Element of the carrier' of PTN
t0 is Element of the carrier of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
t0 is Element of the carrier of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
(PTN,f) is Element of the carrier of PTN
(PTN,f) is Element of the carrier' of PTN
S0 is set
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
(PTN,s) is Element of the carrier' of PTN
(PTN,s) is Element of the carrier of PTN
[(PTN,s),(PTN,s)] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{(PTN,s),(PTN,s)} is non empty set
{(PTN,s)} is non empty set
{{(PTN,s),(PTN,s)},{(PTN,s)}} is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
S0 is set
s is Element of the carrier' of PTN
t0 is Element of the carrier of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
t0 is Element of the carrier of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
[t0,S0] is V9() set
{t0,S0} is non empty set
{{t0,S0},{t0}} is non empty set
f is Element of the carrier of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[f,S0] is V9() set
{f,S0} is non empty set
{f} is non empty set
{{f,S0},{f}} is non empty set
(PTN,s) is Element of the carrier' of PTN
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
t is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
bool the carrier of PTN is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : S₁[b₁] } is set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
{ b₁ where b₁ is Element of the carrier of PTN : S₁[b₁] } is set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
t is Element of bool the carrier' of PTN
(PTN,t) is Element of bool the carrier of PTN
bool the carrier of PTN is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
{ (PTN,b₁) where b₁ is ( the carrier of PTN, the carrier' of PTN, the of PTN) : (PTN,b₁) in t } is set
S0 is set
s is Element of the carrier of PTN
t0 is Element of the carrier' of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
t0 is Element of the carrier' of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
(PTN,f) is Element of the carrier of PTN
(PTN,f) is Element of the carrier' of PTN
S0 is set
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
(PTN,s) is Element of the carrier of PTN
(PTN,s) is Element of the carrier' of PTN
[(PTN,s),(PTN,s)] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{(PTN,s),(PTN,s)} is non empty set
{(PTN,s)} is non empty set
{{(PTN,s),(PTN,s)},{(PTN,s)}} is non empty set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
t is Element of bool the carrier' of PTN
(PTN,t) is Element of bool the carrier of PTN
bool the carrier of PTN is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
S0 is set
s is Element of the carrier of PTN
t0 is Element of the carrier' of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
t0 is Element of the carrier' of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
[S0,t0] is V9() set
{S0,t0} is non empty set
{S0} is non empty set
{{S0,t0},{S0}} is non empty set
f is Element of the carrier' of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[S0,f] is V9() set
{S0,f} is non empty set
{S0} is non empty set
{{S0,f},{S0}} is non empty set
(PTN,s) is Element of the carrier of PTN
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
t is Element of bool the carrier' of PTN
(PTN,t) is Element of bool the carrier of PTN
bool the carrier of PTN is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
{ (PTN,b₁) where b₁ is ( the carrier' of PTN, the carrier of PTN, the of PTN) : (PTN,b₁) in t } is set
S0 is set
s is Element of the carrier of PTN
t0 is Element of the carrier' of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
t0 is Element of the carrier' of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
(PTN,f) is Element of the carrier' of PTN
(PTN,f) is Element of the carrier of PTN
S0 is set
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
(PTN,s) is Element of the carrier of PTN
(PTN,s) is Element of the carrier' of PTN
[(PTN,s),(PTN,s)] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{(PTN,s),(PTN,s)} is non empty set
{(PTN,s)} is non empty set
{{(PTN,s),(PTN,s)},{(PTN,s)}} is non empty set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
t is Element of bool the carrier' of PTN
(PTN,t) is Element of bool the carrier of PTN
bool the carrier of PTN is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
S0 is set
s is Element of the carrier of PTN
t0 is Element of the carrier' of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
t0 is Element of the carrier' of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set
[t0,S0] is V9() set
{t0,S0} is non empty set
{{t0,S0},{t0}} is non empty set
f is Element of the carrier' of PTN
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[f,S0] is V9() set
{f,S0} is non empty set
{f} is non empty set
{{f,S0},{f}} is non empty set
(PTN,s) is Element of the carrier of PTN
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
{} the carrier of PTN is empty proper Relation-like non-empty empty-yielding V55() V58() V61() Element of bool the carrier of PTN
bool the carrier of PTN is non empty set
(PTN,({} the carrier of PTN)) is Element of bool the carrier' of PTN
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in {} the carrier of PTN & b₂ = [b₁,b₃] ) } is set
the Element of (PTN,({} the carrier of PTN)) is Element of (PTN,({} the carrier of PTN))
S0 is Element of the carrier' of PTN
f is Element of the carrier of PTN
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[S0,f] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{S0,f} is non empty set
{S0} is non empty set
{{S0,f},{S0}} is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
{} the carrier of PTN is empty proper Relation-like non-empty empty-yielding V55() V58() V61() Element of bool the carrier of PTN
bool the carrier of PTN is non empty set
(PTN,({} the carrier of PTN)) is Element of bool the carrier' of PTN
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in {} the carrier of PTN & b₂ = [b₃,b₁] ) } is set
the Element of (PTN,({} the carrier of PTN)) is Element of (PTN,({} the carrier of PTN))
S0 is Element of the carrier' of PTN
f is Element of the carrier of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[f,S0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{f,S0} is non empty set
{f} is non empty set
{{f,S0},{f}} is non empty set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
{} the carrier' of PTN is empty proper Relation-like non-empty empty-yielding V55() V58() V61() Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
(PTN,({} the carrier' of PTN)) is Element of bool the carrier of PTN
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in {} the carrier' of PTN & b₂ = [b₁,b₃] ) } is set
the Element of (PTN,({} the carrier' of PTN)) is Element of (PTN,({} the carrier' of PTN))
S0 is Element of the carrier of PTN
f is Element of the carrier' of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[S0,f] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{S0,f} is non empty set
{S0} is non empty set
{{S0,f},{S0}} is non empty set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
{} the carrier' of PTN is empty proper Relation-like non-empty empty-yielding V55() V58() V61() Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
(PTN,({} the carrier' of PTN)) is Element of bool the carrier of PTN
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in {} the carrier' of PTN & b₂ = [b₃,b₁] ) } is set
the Element of (PTN,({} the carrier' of PTN)) is Element of (PTN,({} the carrier' of PTN))
S0 is Element of the carrier of PTN
f is Element of the carrier' of PTN
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[f,S0] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{f,S0} is non empty set
{f} is non empty set
{{f,S0},{f}} is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
PTN is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
[{},{}] is V9() set
{{},{}} is non empty set
{{{},{}},{{}}} is non empty set
{[{},{}]} is non empty Relation-like set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
bool the carrier of PTN is non empty set
t0 is Element of bool the carrier of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
S0 is Element of the carrier' of PTN
t is Element of the carrier of PTN
[S0,t] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{S0,t} is non empty set
{S0} is non empty set
{{S0,t},{S0}} is non empty set
(PTN,t0) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t0 & b₂ = [b₁,b₃] ) } is set
{S0} is non empty Element of bool the carrier' of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[t,S0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{t,S0} is non empty set
{t} is non empty set
{{t,S0},{t}} is non empty set
(PTN,t0) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t0 & b₂ = [b₃,b₁] ) } is set
bool (PTN,t0) is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
PTN is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
[{},{}] is V9() set
{{},{}} is non empty set
{{{},{}},{{}}} is non empty set
{[{},{}]} is non empty Relation-like set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
bool the carrier of PTN is non empty set
t0 is Element of bool the carrier of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
t is Element of the carrier of PTN
S0 is Element of the carrier' of PTN
[t,S0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{t,S0} is non empty set
{t} is non empty set
{{t,S0},{t}} is non empty set
(PTN,t0) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t0 & b₂ = [b₃,b₁] ) } is set
{S0} is non empty Element of bool the carrier' of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[S0,t] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{S0,t} is non empty set
{S0} is non empty set
{{S0,t},{S0}} is non empty set
(PTN,t0) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t0 & b₂ = [b₁,b₃] ) } is set
bool (PTN,t0) is non empty set
PTN is non empty set
t is non empty set
[:PTN,t:] is non empty Relation-like set
bool [:PTN,t:] is non empty set
S0 is non empty Relation-like PTN -defined t -valued Element of bool [:PTN,t:]
S0 ~ is Relation-like set
[:t,PTN:] is non empty Relation-like set
bool [:t,PTN:] is non empty set
the (PTN,t,S0) is (PTN,t,S0)
f is set
t0 is set
[f,t0] is V9() set
{f,t0} is non empty set
{f} is non empty set
{{f,t0},{f}} is non empty set
[t0,f] is V9() set
{t0,f} is non empty set
{t0} is non empty set
{{t0,f},{t0}} is non empty set
S0 ~ is Relation-like t -defined PTN -valued Element of bool [:t,PTN:]
PTN is ()
the carrier of PTN is set
the carrier' of PTN is set
the of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
PTN is non empty non void V49() () () ()
(PTN) is () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
( the carrier' of PTN, the carrier of PTN, the of PTN) is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of (PTN) is Relation-like the carrier of (PTN) -defined the carrier' of (PTN) -valued Element of bool [: the carrier of (PTN), the carrier' of (PTN):]
the carrier of (PTN) is set
the carrier' of (PTN) is set
[: the carrier of (PTN), the carrier' of (PTN):] is Relation-like set
bool [: the carrier of (PTN), the carrier' of (PTN):] is non empty set
( the carrier of PTN, the carrier' of PTN, the of PTN) is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
the of (PTN) is Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
[: the carrier' of (PTN), the carrier of (PTN):] is Relation-like set
bool [: the carrier' of (PTN), the carrier of (PTN):] is non empty set
PTN is non empty non void V49() () () ()
(PTN) is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
((PTN)) is non empty non void V49() () () () ()
the carrier of (PTN) is non empty set
the carrier' of (PTN) is non empty set
the of (PTN) is non empty Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
[: the carrier' of (PTN), the carrier of (PTN):] is non empty Relation-like set
bool [: the carrier' of (PTN), the carrier of (PTN):] is non empty set
the of (PTN) ~ is Relation-like the carrier of (PTN) -defined the carrier' of (PTN) -valued Element of bool [: the carrier of (PTN), the carrier' of (PTN):]
[: the carrier of (PTN), the carrier' of (PTN):] is non empty Relation-like set
bool [: the carrier of (PTN), the carrier' of (PTN):] is non empty set
the of (PTN) is non empty Relation-like the carrier of (PTN) -defined the carrier' of (PTN) -valued Element of bool [: the carrier of (PTN), the carrier' of (PTN):]
the of (PTN) ~ is Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
( the carrier of (PTN), the carrier' of (PTN),( the of (PTN) ~),( the of (PTN) ~)) is () ()
( the carrier of PTN, the carrier' of PTN, the of PTN, the of PTN) is () ()
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
(PTN) is non empty non void V49() () () () ()
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier of (PTN) is non empty set
t is non empty non void V49() () () ()
the carrier' of t is non empty set
(t) is non empty non void V49() () () () ()
the carrier of t is non empty set
the of t is non empty Relation-like the carrier' of t -defined the carrier of t -valued Element of bool [: the carrier' of t, the carrier of t:]
[: the carrier' of t, the carrier of t:] is non empty Relation-like set
bool [: the carrier' of t, the carrier of t:] is non empty set
the of t ~ is Relation-like the carrier of t -defined the carrier' of t -valued Element of bool [: the carrier of t, the carrier' of t:]
[: the carrier of t, the carrier' of t:] is non empty Relation-like set
bool [: the carrier of t, the carrier' of t:] is non empty set
the of t is non empty Relation-like the carrier of t -defined the carrier' of t -valued Element of bool [: the carrier of t, the carrier' of t:]
the of t ~ is Relation-like the carrier' of t -defined the carrier of t -valued Element of bool [: the carrier' of t, the carrier of t:]
( the carrier of t, the carrier' of t,( the of t ~),( the of t ~)) is () ()
the carrier' of (t) is non empty set
S0 is non empty non void V49() () () ()
the carrier of S0 is non empty set
the carrier' of S0 is non empty set
the of S0 is non empty Relation-like the carrier of S0 -defined the carrier' of S0 -valued Element of bool [: the carrier of S0, the carrier' of S0:]
[: the carrier of S0, the carrier' of S0:] is non empty Relation-like set
bool [: the carrier of S0, the carrier' of S0:] is non empty set
( the carrier of S0, the carrier' of S0, the of S0) is non empty Relation-like the carrier' of S0 -defined the carrier of S0 -valued Element of bool [: the carrier' of S0, the carrier of S0:]
[: the carrier' of S0, the carrier of S0:] is non empty Relation-like set
bool [: the carrier' of S0, the carrier of S0:] is non empty set
(S0) is non empty non void V49() () () () ()
the of S0 is non empty Relation-like the carrier' of S0 -defined the carrier of S0 -valued Element of bool [: the carrier' of S0, the carrier of S0:]
the of S0 ~ is Relation-like the carrier of S0 -defined the carrier' of S0 -valued Element of bool [: the carrier of S0, the carrier' of S0:]
the of S0 ~ is Relation-like the carrier' of S0 -defined the carrier of S0 -valued Element of bool [: the carrier' of S0, the carrier of S0:]
( the carrier of S0, the carrier' of S0,( the of S0 ~),( the of S0 ~)) is () ()
the of (S0) is non empty Relation-like the carrier' of (S0) -defined the carrier of (S0) -valued Element of bool [: the carrier' of (S0), the carrier of (S0):]
the carrier' of (S0) is non empty set
the carrier of (S0) is non empty set
[: the carrier' of (S0), the carrier of (S0):] is non empty Relation-like set
bool [: the carrier' of (S0), the carrier of (S0):] is non empty set
s is non empty non void V49() () () ()
the carrier' of s is non empty set
the carrier of s is non empty set
the of s is non empty Relation-like the carrier' of s -defined the carrier of s -valued Element of bool [: the carrier' of s, the carrier of s:]
[: the carrier' of s, the carrier of s:] is non empty Relation-like set
bool [: the carrier' of s, the carrier of s:] is non empty set
( the carrier' of s, the carrier of s, the of s) is non empty Relation-like the carrier of s -defined the carrier' of s -valued Element of bool [: the carrier of s, the carrier' of s:]
[: the carrier of s, the carrier' of s:] is non empty Relation-like set
bool [: the carrier of s, the carrier' of s:] is non empty set
(s) is non empty non void V49() () () () ()
the of s ~ is Relation-like the carrier of s -defined the carrier' of s -valued Element of bool [: the carrier of s, the carrier' of s:]
the of s is non empty Relation-like the carrier of s -defined the carrier' of s -valued Element of bool [: the carrier of s, the carrier' of s:]
the of s ~ is Relation-like the carrier' of s -defined the carrier of s -valued Element of bool [: the carrier' of s, the carrier of s:]
( the carrier of s, the carrier' of s,( the of s ~),( the of s ~)) is () ()
the of (s) is non empty Relation-like the carrier of (s) -defined the carrier' of (s) -valued Element of bool [: the carrier of (s), the carrier' of (s):]
the carrier of (s) is non empty set
the carrier' of (s) is non empty set
[: the carrier of (s), the carrier' of (s):] is non empty Relation-like set
bool [: the carrier of (s), the carrier' of (s):] is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
t is Element of bool the carrier of PTN
(PTN) is non empty non void V49() () () () ()
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier of (PTN) is non empty set
bool the carrier of (PTN) is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
t is Element of the carrier of PTN
(PTN) is non empty non void V49() () () () ()
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier of (PTN) is non empty set
PTN is non empty non void V49() () () ()
(PTN) is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier of (PTN) is non empty set
bool the carrier of (PTN) is non empty set
t is Element of bool the carrier of (PTN)
bool the carrier of PTN is non empty set
PTN is non empty non void V49() () () ()
(PTN) is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier of (PTN) is non empty set
t is Element of the carrier of (PTN)
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
bool the carrier' of PTN is non empty set
t is Element of bool the carrier' of PTN
(PTN) is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier' of (PTN) is non empty set
bool the carrier' of (PTN) is non empty set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
t is Element of the carrier' of PTN
(PTN) is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier' of (PTN) is non empty set
PTN is non empty non void V49() () () ()
(PTN) is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier' of (PTN) is non empty set
bool the carrier' of (PTN) is non empty set
t is Element of bool the carrier' of (PTN)
bool the carrier' of PTN is non empty set
PTN is non empty non void V49() () () ()
(PTN) is non empty non void V49() () () () ()
the carrier of PTN is non empty set
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
the carrier' of (PTN) is non empty set
t is Element of the carrier' of (PTN)
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
(PTN) is non empty non void V49() () () () ()
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier of (PTN)
the carrier of (PTN) is non empty set
bool the carrier of (PTN) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the carrier' of (PTN) is non empty set
bool the carrier' of (PTN) is non empty set
the of (PTN) is non empty Relation-like the carrier of (PTN) -defined the carrier' of (PTN) -valued Element of bool [: the carrier of (PTN), the carrier' of (PTN):]
[: the carrier of (PTN), the carrier' of (PTN):] is non empty Relation-like set
bool [: the carrier of (PTN), the carrier' of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier of (PTN), the carrier' of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₃,b₁] ) } is set
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
S0 is set
f is Element of the carrier of (PTN)
s is ( the carrier of (PTN), the carrier' of (PTN), the of (PTN))
[f,S0] is V9() set
{f,S0} is non empty set
{f} is non empty set
{{f,S0},{f}} is non empty set
(PTN,f) is Element of the carrier of PTN
[S0,(PTN,f)] is V9() set
{S0,(PTN,f)} is non empty set
{S0} is non empty set
{{S0,(PTN,f)},{S0}} is non empty set
S0 is set
f is Element of the carrier of PTN
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[S0,f] is V9() set
{S0,f} is non empty set
{S0} is non empty set
{{S0,f},{S0}} is non empty set
(PTN,f) is Element of the carrier of (PTN)
[(PTN,f),S0] is V9() set
{(PTN,f),S0} is non empty set
{(PTN,f)} is non empty set
{{(PTN,f),S0},{(PTN,f)}} is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
(PTN) is non empty non void V49() () () () ()
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier of (PTN)
the carrier of (PTN) is non empty set
bool the carrier of (PTN) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the carrier' of (PTN) is non empty set
bool the carrier' of (PTN) is non empty set
the of (PTN) is non empty Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
[: the carrier' of (PTN), the carrier of (PTN):] is non empty Relation-like set
bool [: the carrier' of (PTN), the carrier of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier' of (PTN), the carrier of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₁,b₃] ) } is set
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
S0 is set
f is Element of the carrier of (PTN)
s is ( the carrier' of (PTN), the carrier of (PTN), the of (PTN))
[S0,f] is V9() set
{S0,f} is non empty set
{S0} is non empty set
{{S0,f},{S0}} is non empty set
(PTN,f) is Element of the carrier of PTN
[(PTN,f),S0] is V9() set
{(PTN,f),S0} is non empty set
{(PTN,f)} is non empty set
{{(PTN,f),S0},{(PTN,f)}} is non empty set
S0 is set
f is Element of the carrier of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[f,S0] is V9() set
{f,S0} is non empty set
{f} is non empty set
{{f,S0},{f}} is non empty set
(PTN,f) is Element of the carrier of (PTN)
[S0,(PTN,f)] is V9() set
{S0,(PTN,f)} is non empty set
{S0} is non empty set
{{S0,(PTN,f)},{S0}} is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
(PTN) is non empty non void V49() () () () ()
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier of (PTN)
the carrier of (PTN) is non empty set
bool the carrier of (PTN) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the carrier' of (PTN) is non empty set
bool the carrier' of (PTN) is non empty set
the of (PTN) is non empty Relation-like the carrier of (PTN) -defined the carrier' of (PTN) -valued Element of bool [: the carrier of (PTN), the carrier' of (PTN):]
[: the carrier of (PTN), the carrier' of (PTN):] is non empty Relation-like set
bool [: the carrier of (PTN), the carrier' of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier of (PTN), the carrier' of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₃,b₁] ) } is set
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
(PTN,t) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
bool (PTN,t) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the of (PTN) is non empty Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
[: the carrier' of (PTN), the carrier of (PTN):] is non empty Relation-like set
bool [: the carrier' of (PTN), the carrier of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier' of (PTN), the carrier of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₁,b₃] ) } is set
bool ((PTN),(PTN,t)) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the of (PTN) is non empty Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
[: the carrier' of (PTN), the carrier of (PTN):] is non empty Relation-like set
bool [: the carrier' of (PTN), the carrier of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier' of (PTN), the carrier of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₁,b₃] ) } is set
bool ((PTN),(PTN,t)) is non empty set
(PTN,t) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
bool (PTN,t) is non empty set
PTN is non empty non void V49() () () ()
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
(PTN) is non empty non void V49() () () () ()
the carrier' of PTN is non empty set
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
the of PTN ~ is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
the of PTN ~ is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
( the carrier of PTN, the carrier' of PTN,( the of PTN ~),( the of PTN ~)) is () ()
t is Element of bool the carrier of PTN
(PTN,t) is Element of bool the carrier of (PTN)
the carrier of (PTN) is non empty set
bool the carrier of (PTN) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the carrier' of (PTN) is non empty set
bool the carrier' of (PTN) is non empty set
the of (PTN) is non empty Relation-like the carrier of (PTN) -defined the carrier' of (PTN) -valued Element of bool [: the carrier of (PTN), the carrier' of (PTN):]
[: the carrier of (PTN), the carrier' of (PTN):] is non empty Relation-like set
bool [: the carrier of (PTN), the carrier' of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier of (PTN), the carrier' of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₃,b₁] ) } is set
(PTN,t) is Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₁,b₃] ) } is set
(PTN,t) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
bool (PTN,t) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the of (PTN) is non empty Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
[: the carrier' of (PTN), the carrier of (PTN):] is non empty Relation-like set
bool [: the carrier' of (PTN), the carrier of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier' of (PTN), the carrier of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₁,b₃] ) } is set
bool ((PTN),(PTN,t)) is non empty set
((PTN),(PTN,t)) is Element of bool the carrier' of (PTN)
the of (PTN) is non empty Relation-like the carrier' of (PTN) -defined the carrier of (PTN) -valued Element of bool [: the carrier' of (PTN), the carrier of (PTN):]
[: the carrier' of (PTN), the carrier of (PTN):] is non empty Relation-like set
bool [: the carrier' of (PTN), the carrier of (PTN):] is non empty set
{ b₁ where b₁ is Element of the carrier' of (PTN) : ex b₂ being ( the carrier' of (PTN), the carrier of (PTN), the of (PTN)) ex b₃ being Element of the carrier of (PTN) st
( b₃ in (PTN,t) & b₂ = [b₁,b₃] ) } is set
bool ((PTN),(PTN,t)) is non empty set
(PTN,t) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in t & b₂ = [b₃,b₁] ) } is set
bool (PTN,t) is non empty set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
t is Element of the carrier' of PTN
{t} is non empty Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
(PTN,{t}) is Element of bool the carrier of PTN
the of PTN is non empty Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of bool [: the carrier of PTN, the carrier' of PTN:]
[: the carrier of PTN, the carrier' of PTN:] is non empty Relation-like set
bool [: the carrier of PTN, the carrier' of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in {t} & b₂ = [b₁,b₃] ) } is set
S0 is Element of bool the carrier of PTN
(PTN,S0) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier of PTN, the carrier' of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in S0 & b₂ = [b₃,b₁] ) } is set
f is Element of the carrier of PTN
s is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[f,t] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{f,t} is non empty set
{f} is non empty set
{{f,t},{f}} is non empty set
(PTN,{t}) /\ S0 is Element of bool the carrier of PTN
(PTN,{t}) /\ S0 is Element of bool the carrier of PTN
s is Element of the carrier of PTN
t0 is Element of the carrier' of PTN
f is ( the carrier of PTN, the carrier' of PTN, the of PTN)
[s,t0] is V9() Element of [: the carrier of PTN, the carrier' of PTN:]
{s,t0} is non empty set
{s} is non empty set
{{s,t0},{s}} is non empty set
PTN is non empty non void V49() () () ()
the carrier' of PTN is non empty set
the carrier of PTN is non empty set
bool the carrier of PTN is non empty set
t is Element of the carrier' of PTN
{t} is non empty Element of bool the carrier' of PTN
bool the carrier' of PTN is non empty set
(PTN,{t}) is Element of bool the carrier of PTN
the of PTN is non empty Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of bool [: the carrier' of PTN, the carrier of PTN:]
[: the carrier' of PTN, the carrier of PTN:] is non empty Relation-like set
bool [: the carrier' of PTN, the carrier of PTN:] is non empty set
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier' of PTN st
( b₃ in {t} & b₂ = [b₃,b₁] ) } is set
S0 is Element of bool the carrier of PTN
(PTN,S0) is Element of bool the carrier' of PTN
{ b₁ where b₁ is Element of the carrier' of PTN : ex b₂ being ( the carrier' of PTN, the carrier of PTN, the of PTN) ex b₃ being Element of the carrier of PTN st
( b₃ in S0 & b₂ = [b₁,b₃] ) } is set
f is Element of the carrier of PTN
s is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[t,f] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{t,f} is non empty set
{t} is non empty set
{{t,f},{t}} is non empty set
(PTN,{t}) /\ S0 is Element of bool the carrier of PTN
(PTN,{t}) /\ S0 is Element of bool the carrier of PTN
s is Element of the carrier of PTN
t0 is Element of the carrier' of PTN
f is ( the carrier' of PTN, the carrier of PTN, the of PTN)
[t0,s] is V9() Element of [: the carrier' of PTN, the carrier of PTN:]
{t0,s} is non empty set
{t0} is non empty set
{{t0,s},{t0}} is non empty set