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

( b

bool the carrier' of PTN is non empty set

{ b

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

( b

{ b

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

( b

{ (PTN,b

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

( b

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

( b

{ (PTN,b

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

( b

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

( b

bool the carrier of PTN is non empty set

{ b

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

( b

{ b

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

( b

{ (PTN,b

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

( b

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

( b

{ (PTN,b

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

( b

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

( b

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

( b

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

( b

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

( b

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

( b

{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

( b

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

( b

{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

( b

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

( b

(PTN,t) is Element of bool the carrier' of PTN

bool the carrier' of PTN is non empty set

{ b

( b

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

( b

(PTN,t) is Element of bool the carrier' of PTN

bool the carrier' of PTN is non empty set

{ b

( b

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

( b

(PTN,t) is Element of bool the carrier' of PTN

bool the carrier' of PTN is non empty set

{ b

( b

(PTN,t) is Element of bool the carrier' of PTN

{ b

( b

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

( b

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

( b

bool ((PTN),(PTN,t)) is non empty set

(PTN,t) is Element of bool the carrier' of PTN

{ b

( b

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

( b

(PTN,t) is Element of bool the carrier' of PTN

bool the carrier' of PTN is non empty set

{ b

( b

(PTN,t) is Element of bool the carrier' of PTN

{ b

( b

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

( b

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

( b

bool ((PTN),(PTN,t)) is non empty set

(PTN,t) is Element of bool the carrier' of PTN

{ b

( b

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

( b

S0 is Element of bool the carrier of PTN

(PTN,S0) is Element of bool the carrier' of PTN

{ b

( b

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

( b

S0 is Element of bool the carrier of PTN

(PTN,S0) is Element of bool the carrier' of PTN

{ b

( b

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