:: PCS_0 semantic presentation

K138() is Element of bool K134()

K134() is set

bool K134() is non empty set

K87() is set

bool K87() is non empty set

bool K138() is non empty set

K183() is set

{} is Relation-like non-empty empty-yielding empty reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive set

the Relation-like non-empty empty-yielding empty reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive set is Relation-like non-empty empty-yielding empty reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive set

{{}} is non empty set

K161({{}}) is M8({{}})

[:K161({{}}),{{}}:] is Relation-like set

bool [:K161({{}}),{{}}:] is non empty set

PFuncs (K161({{}}),{{}}) is functional non empty set

1 is non empty set

2 is non empty set

3 is non empty set

0 is Relation-like non-empty empty-yielding empty reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Element of K138()

{{},1} is non empty set

{0,1} is non empty set

P is set

S is set

[:P,S:] is Relation-like set

bool [:P,S:] is non empty set

R is Relation-like P -defined S -valued Element of bool [:P,S:]

field R is set

proj1 R is set

proj2 R is set

(proj1 R) \/ (proj2 R) is set

P \/ S is set

bool (P \/ S) is non empty set

P is set

S is set

[:P,S:] is Relation-like set

bool [:P,S:] is non empty set

R is set

p is set

[:R,p:] is Relation-like set

bool [:R,p:] is non empty set

p9 is Relation-like P -defined S -valued Element of bool [:P,S:]

q is Relation-like R -defined p -valued Element of bool [:R,p:]

p9 \/ q is Relation-like set

P \/ R is set

S \/ p is set

[:(P \/ R),(S \/ p):] is Relation-like set

bool [:(P \/ R),(S \/ p):] is non empty set

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

P \/ S is set

[:(P \/ S),(P \/ S):] is Relation-like set

bool [:(P \/ S),(P \/ S):] is non empty set

R is Relation-like P -defined P -valued total Element of bool [:P,P:]

p is Relation-like S -defined S -valued total Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like P \/ S -defined P \/ S -valued Element of bool [:(P \/ S),(P \/ S):]

dom (P,P,S,S,R,p) is Element of bool (P \/ S)

bool (P \/ S) is non empty set

dom R is Element of bool P

bool P is non empty set

dom p is Element of bool S

bool S is non empty set

(dom R) \/ (dom p) is set

P \/ (dom p) is set

p9 is Relation-like P \/ S -defined P \/ S -valued Element of bool [:(P \/ S),(P \/ S):]

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

P \/ S is set

[:(P \/ S),(P \/ S):] is Relation-like set

bool [:(P \/ S),(P \/ S):] is non empty set

R is Relation-like P -defined P -valued reflexive Element of bool [:P,P:]

p is Relation-like S -defined S -valued reflexive Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like P \/ S -defined P \/ S -valued reflexive Element of bool [:(P \/ S),(P \/ S):]

p9 is Relation-like P \/ S -defined P \/ S -valued Element of bool [:(P \/ S),(P \/ S):]

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

P \/ S is set

[:(P \/ S),(P \/ S):] is Relation-like set

bool [:(P \/ S),(P \/ S):] is non empty set

R is Relation-like P -defined P -valued symmetric Element of bool [:P,P:]

p is Relation-like S -defined S -valued symmetric Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like P \/ S -defined P \/ S -valued symmetric Element of bool [:(P \/ S),(P \/ S):]

p9 is Relation-like P \/ S -defined P \/ S -valued Element of bool [:(P \/ S),(P \/ S):]

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

p9 is set

q is set

[p9,q] is V15() set

{p9,q} is non empty set

{p9} is non empty set

{{p9,q},{p9}} is non empty set

R is Relation-like P -defined P -valued Element of bool [:P,P:]

p is Relation-like S -defined S -valued Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like P \/ S -defined P \/ S -valued Element of bool [:(P \/ S),(P \/ S):]

P \/ S is set

[:(P \/ S),(P \/ S):] is Relation-like set

bool [:(P \/ S),(P \/ S):] is non empty set

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

R is Relation-like P -defined P -valued transitive Element of bool [:P,P:]

p is Relation-like S -defined S -valued transitive Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like P \/ S -defined P \/ S -valued Element of bool [:(P \/ S),(P \/ S):]

P \/ S is set

[:(P \/ S),(P \/ S):] is Relation-like set

bool [:(P \/ S),(P \/ S):] is non empty set

p9 is set

field (P,P,S,S,R,p) is set

proj1 (P,P,S,S,R,p) is set

proj2 (P,P,S,S,R,p) is set

(proj1 (P,P,S,S,R,p)) \/ (proj2 (P,P,S,S,R,p)) is set

q is set

q9 is set

[p9,q] is V15() set

{p9,q} is non empty set

{p9} is non empty set

{{p9,q},{p9}} is non empty set

[q,q9] is V15() set

{q,q9} is non empty set

{q} is non empty set

{{q,q9},{q}} is non empty set

[p9,q9] is V15() set

{p9,q9} is non empty set

{{p9,q9},{p9}} is non empty set

((P \/ S),(P \/ S),(P,P,S,S,R,p)) is Element of bool ((P \/ S) \/ (P \/ S))

(P \/ S) \/ (P \/ S) is set

bool ((P \/ S) \/ (P \/ S)) is non empty set

P is non empty set

S is Relation-like P -defined Function-like total 1-sorted-yielding set

Carrier S is Relation-like P -defined Function-like total set

R is Relation-like P -defined Function-like total set

p is Element of P

R . p is set

S . p is 1-sorted

the carrier of (S . p) is set

p9 is 1-sorted

the carrier of p9 is set

p is set

S . p is set

R . p is set

p9 is Element of P

S . p9 is 1-sorted

the carrier of (S . p9) is set

P is set

S is set

[:P,S:] is Relation-like set

bool [:P,S:] is non empty set

R is set

p is set

[:R,p:] is Relation-like set

bool [:R,p:] is non empty set

p9 is Relation-like P -defined S -valued Element of bool [:P,S:]

q is Relation-like R -defined p -valued Element of bool [:R,p:]

[:P,R:] is Relation-like set

[:S,p:] is Relation-like set

[:[:P,R:],[:S,p:]:] is Relation-like set

bool [:[:P,R:],[:S,p:]:] is non empty set

q9 is Relation-like [:P,R:] -defined [:S,p:] -valued Element of bool [:[:P,R:],[:S,p:]:]

a is set

b is set

[a,b] is V15() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

a1 is set

b1 is set

[a1,b1] is V15() set

{a1,b1} is non empty set

{a1} is non empty set

{{a1,b1},{a1}} is non empty set

p1 is set

q1 is set

[p1,q1] is V15() set

{p1,q1} is non empty set

{p1} is non empty set

{{p1,q1},{p1}} is non empty set

[a1,p1] is V15() set

{a1,p1} is non empty set

{{a1,p1},{a1}} is non empty set

[b1,q1] is V15() set

{b1,q1} is non empty set

{b1} is non empty set

{{b1,q1},{b1}} is non empty set

q9 is Relation-like [:P,R:] -defined [:S,p:] -valued Element of bool [:[:P,R:],[:S,p:]:]

a is Relation-like [:P,R:] -defined [:S,p:] -valued Element of bool [:[:P,R:],[:S,p:]:]

P is non empty set

S is non empty set

[:P,S:] is Relation-like non empty set

bool [:P,S:] is non empty set

R is non empty set

p is non empty set

[:R,p:] is Relation-like non empty set

bool [:R,p:] is non empty set

[:P,R:] is Relation-like non empty set

[:S,p:] is Relation-like non empty set

[:[:P,R:],[:S,p:]:] is Relation-like non empty set

bool [:[:P,R:],[:S,p:]:] is non empty set

p9 is Relation-like P -defined S -valued Element of bool [:P,S:]

q is Relation-like R -defined p -valued Element of bool [:R,p:]

(P,S,R,p,p9,q) is Relation-like [:P,R:] -defined [:S,p:] -valued Element of bool [:[:P,R:],[:S,p:]:]

q9 is Relation-like [:P,R:] -defined [:S,p:] -valued Element of bool [:[:P,R:],[:S,p:]:]

a is Element of P

b is Element of S

[a,b] is V15() Element of [:P,S:]

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

a1 is Element of R

[a,a1] is V15() Element of [:P,R:]

{a,a1} is non empty set

{{a,a1},{a}} is non empty set

b1 is Element of p

[b,b1] is V15() Element of [:S,p:]

{b,b1} is non empty set

{b} is non empty set

{{b,b1},{b}} is non empty set

[[a,a1],[b,b1]] is V15() Element of [:[:P,R:],[:S,p:]:]

{[a,a1],[b,b1]} is Relation-like non empty set

{[a,a1]} is Relation-like non empty set

{{[a,a1],[b,b1]},{[a,a1]}} is non empty set

[a1,b1] is V15() Element of [:R,p:]

{a1,b1} is non empty set

{a1} is non empty set

{{a1,b1},{a1}} is non empty set

p1 is set

q1 is set

[p1,q1] is V15() set

{p1,q1} is non empty set

{p1} is non empty set

{{p1,q1},{p1}} is non empty set

t is set

e is set

[t,e] is V15() set

{t,e} is non empty set

{t} is non empty set

{{t,e},{t}} is non empty set

[p1,t] is V15() set

{p1,t} is non empty set

{{p1,t},{p1}} is non empty set

[q1,e] is V15() set

{q1,e} is non empty set

{q1} is non empty set

{{q1,e},{q1}} is non empty set

a is set

b is set

[a,b] is V15() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

dom q9 is Relation-like P -defined R -valued Element of bool [:P,R:]

bool [:P,R:] is non empty set

a1 is set

b1 is set

[a1,b1] is V15() set

{a1,b1} is non empty set

{a1} is non empty set

{{a1,b1},{a1}} is non empty set

rng q9 is Relation-like S -defined p -valued Element of bool [:S,p:]

bool [:S,p:] is non empty set

p1 is set

q1 is set

[p1,q1] is V15() set

{p1,q1} is non empty set

{p1} is non empty set

{{p1,q1},{p1}} is non empty set

[a1,p1] is V15() set

{a1,p1} is non empty set

{{a1,p1},{a1}} is non empty set

[b1,q1] is V15() set

{b1,q1} is non empty set

{b1} is non empty set

{{b1,q1},{b1}} is non empty set

a1 is set

b1 is set

[a1,b1] is V15() set

{a1,b1} is non empty set

{a1} is non empty set

{{a1,b1},{a1}} is non empty set

p1 is set

q1 is set

[p1,q1] is V15() set

{p1,q1} is non empty set

{p1} is non empty set

{{p1,q1},{p1}} is non empty set

[a1,p1] is V15() set

{a1,p1} is non empty set

{{a1,p1},{a1}} is non empty set

[b1,q1] is V15() set

{b1,q1} is non empty set

{b1} is non empty set

{{b1,q1},{b1}} is non empty set

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

[:P,S:] is Relation-like set

R is Relation-like P -defined P -valued total Element of bool [:P,P:]

p is Relation-like S -defined S -valued total Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like [:P,S:] -defined [:P,S:] -valued Element of bool [:[:P,S:],[:P,S:]:]

[:[:P,S:],[:P,S:]:] is Relation-like set

bool [:[:P,S:],[:P,S:]:] is non empty set

dom (P,P,S,S,R,p) is Relation-like P -defined S -valued Element of bool [:P,S:]

bool [:P,S:] is non empty set

p9 is set

q is set

q9 is set

[q,q9] is V15() set

{q,q9} is non empty set

{q} is non empty set

{{q,q9},{q}} is non empty set

dom R is Element of bool P

bool P is non empty set

a is set

[q,a] is V15() set

{q,a} is non empty set

{{q,a},{q}} is non empty set

dom p is Element of bool S

bool S is non empty set

b is set

[q9,b] is V15() set

{q9,b} is non empty set

{q9} is non empty set

{{q9,b},{q9}} is non empty set

[a,b] is V15() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

[[q,q9],[a,b]] is V15() set

{[q,q9],[a,b]} is Relation-like non empty set

{[q,q9]} is Relation-like non empty set

{{[q,q9],[a,b]},{[q,q9]}} is non empty set

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

R is Relation-like P -defined P -valued reflexive Element of bool [:P,P:]

p is Relation-like S -defined S -valued reflexive Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like [:P,S:] -defined [:P,S:] -valued Element of bool [:[:P,S:],[:P,S:]:]

[:P,S:] is Relation-like set

[:[:P,S:],[:P,S:]:] is Relation-like set

bool [:[:P,S:],[:P,S:]:] is non empty set

p9 is set

field (P,P,S,S,R,p) is set

proj1 (P,P,S,S,R,p) is Relation-like set

proj2 (P,P,S,S,R,p) is Relation-like set

(proj1 (P,P,S,S,R,p)) \/ (proj2 (P,P,S,S,R,p)) is Relation-like set

[p9,p9] is V15() set

{p9,p9} is non empty set

{p9} is non empty set

{{p9,p9},{p9}} is non empty set

([:P,S:],[:P,S:],(P,P,S,S,R,p)) is Relation-like Element of bool ([:P,S:] \/ [:P,S:])

[:P,S:] \/ [:P,S:] is Relation-like set

bool ([:P,S:] \/ [:P,S:]) is non empty set

(P,P,R) is Element of bool (P \/ P)

P \/ P is set

bool (P \/ P) is non empty set

proj1 R is set

proj2 R is set

(proj1 R) \/ (proj2 R) is set

(S,S,p) is Element of bool (S \/ S)

S \/ S is set

bool (S \/ S) is non empty set

proj1 p is set

proj2 p is set

(proj1 p) \/ (proj2 p) is set

dom (P,P,S,S,R,p) is Relation-like P -defined S -valued Element of bool [:P,S:]

bool [:P,S:] is non empty set

q is set

[p9,q] is V15() set

{p9,q} is non empty set

{{p9,q},{p9}} is non empty set

q9 is set

a is set

[q9,a] is V15() set

{q9,a} is non empty set

{q9} is non empty set

{{q9,a},{q9}} is non empty set

b is set

a1 is set

[b,a1] is V15() set

{b,a1} is non empty set

{b} is non empty set

{{b,a1},{b}} is non empty set

[q9,b] is V15() set

{q9,b} is non empty set

{{q9,b},{q9}} is non empty set

[a,a1] is V15() set

{a,a1} is non empty set

{a} is non empty set

{{a,a1},{a}} is non empty set

[q9,q9] is V15() set

{q9,q9} is non empty set

{{q9,q9},{q9}} is non empty set

[a,a] is V15() set

{a,a} is non empty set

{{a,a},{a}} is non empty set

rng (P,P,S,S,R,p) is Relation-like P -defined S -valued Element of bool [:P,S:]

bool [:P,S:] is non empty set

q is set

[q,p9] is V15() set

{q,p9} is non empty set

{q} is non empty set

{{q,p9},{q}} is non empty set

q9 is set

a is set

[q9,a] is V15() set

{q9,a} is non empty set

{q9} is non empty set

{{q9,a},{q9}} is non empty set

b is set

a1 is set

[b,a1] is V15() set

{b,a1} is non empty set

{b} is non empty set

{{b,a1},{b}} is non empty set

[q9,b] is V15() set

{q9,b} is non empty set

{{q9,b},{q9}} is non empty set

[a,a1] is V15() set

{a,a1} is non empty set

{a} is non empty set

{{a,a1},{a}} is non empty set

[b,b] is V15() set

{b,b} is non empty set

{{b,b},{b}} is non empty set

[a1,a1] is V15() set

{a1,a1} is non empty set

{a1} is non empty set

{{a1,a1},{a1}} is non empty set

dom (P,P,S,S,R,p) is Relation-like P -defined S -valued Element of bool [:P,S:]

bool [:P,S:] is non empty set

rng (P,P,S,S,R,p) is Relation-like P -defined S -valued Element of bool [:P,S:]

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

R is Relation-like P -defined P -valued Element of bool [:P,P:]

p is Relation-like S -defined S -valued total reflexive Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like [:P,S:] -defined [:P,S:] -valued Element of bool [:[:P,S:],[:P,S:]:]

[:P,S:] is Relation-like set

[:[:P,S:],[:P,S:]:] is Relation-like set

bool [:[:P,S:],[:P,S:]:] is non empty set

p9 is set

field (P,P,S,S,R,p) is set

proj1 (P,P,S,S,R,p) is Relation-like set

proj2 (P,P,S,S,R,p) is Relation-like set

(proj1 (P,P,S,S,R,p)) \/ (proj2 (P,P,S,S,R,p)) is Relation-like set

[p9,p9] is V15() set

{p9,p9} is non empty set

{p9} is non empty set

{{p9,p9},{p9}} is non empty set

([:P,S:],[:P,S:],(P,P,S,S,R,p)) is Relation-like Element of bool ([:P,S:] \/ [:P,S:])

[:P,S:] \/ [:P,S:] is Relation-like set

bool ([:P,S:] \/ [:P,S:]) is non empty set

q is set

q9 is set

[q,q9] is V15() set

{q,q9} is non empty set

{q} is non empty set

{{q,q9},{q}} is non empty set

(S,S,p) is Element of bool (S \/ S)

S \/ S is set

bool (S \/ S) is non empty set

proj1 p is set

proj2 p is set

(proj1 p) \/ (proj2 p) is set

[q9,q9] is V15() set

{q9,q9} is non empty set

{q9} is non empty set

{{q9,q9},{q9}} is non empty set

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

R is Relation-like P -defined P -valued total reflexive Element of bool [:P,P:]

p is Relation-like S -defined S -valued Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like [:P,S:] -defined [:P,S:] -valued Element of bool [:[:P,S:],[:P,S:]:]

[:P,S:] is Relation-like set

[:[:P,S:],[:P,S:]:] is Relation-like set

bool [:[:P,S:],[:P,S:]:] is non empty set

p9 is set

field (P,P,S,S,R,p) is set

proj1 (P,P,S,S,R,p) is Relation-like set

proj2 (P,P,S,S,R,p) is Relation-like set

(proj1 (P,P,S,S,R,p)) \/ (proj2 (P,P,S,S,R,p)) is Relation-like set

[p9,p9] is V15() set

{p9,p9} is non empty set

{p9} is non empty set

{{p9,p9},{p9}} is non empty set

([:P,S:],[:P,S:],(P,P,S,S,R,p)) is Relation-like Element of bool ([:P,S:] \/ [:P,S:])

[:P,S:] \/ [:P,S:] is Relation-like set

bool ([:P,S:] \/ [:P,S:]) is non empty set

q is set

q9 is set

[q,q9] is V15() set

{q,q9} is non empty set

{q} is non empty set

{{q,q9},{q}} is non empty set

(P,P,R) is Element of bool (P \/ P)

P \/ P is set

bool (P \/ P) is non empty set

proj1 R is set

proj2 R is set

(proj1 R) \/ (proj2 R) is set

[q,q] is V15() set

{q,q} is non empty set

{{q,q},{q}} is non empty set

P is set

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

S is set

[:S,S:] is Relation-like set

bool [:S,S:] is non empty set

R is Relation-like P -defined P -valued symmetric Element of bool [:P,P:]

p is Relation-like S -defined S -valued symmetric Element of bool [:S,S:]

(P,P,S,S,R,p) is Relation-like [:P,S:] -defined [:P,S:] -valued Element of bool [:[:P,S:],[:P,S:]:]

[:P,S:] is Relation-like set

[:[:P,S:],[:P,S:]:] is Relation-like set

bool [:[:P,S:],[:P,S:]:] is non empty set

p9 is set

field (P,P,S,S,R,p) is set

proj1 (P,P,S,S,R,p) is Relation-like set

proj2 (P,P,S,S,R,p) is Relation-like set

(proj1 (P,P,S,S,R,p)) \/ (proj2 (P,P,S,S,R,p)) is Relation-like set

q is set

[p9,q] is V15() set

{p9,q} is non empty set

{p9} is non empty set

{{p9,q},{p9}} is non empty set

[q,p9] is V15() set

{q,p9} is non empty set

{q} is non empty set

{{q,p9},{q}} is non empty set

([:P,S:],[:P,S:],(P,P,S,S,R,p)) is Relation-like Element of bool ([:P,S:] \/ [:P,S:])

[:P,S:] \/ [:P,S:] is Relation-like set

bool ([:P,S:] \/ [:P,S:]) is non empty set

q9 is set

a is set

[q9,a] is V15() set

{q9,a} is non empty set

{q9} is non empty set

{{q9,a},{q9}} is non empty set

b is set

a1 is set

[b,a1] is V15() set

{b,a1} is non empty set

{b} is non empty set

{{b,a1},{b}} is non empty set

[q9,b] is V15() set

{q9,b} is non empty set

{{q9,b},{q9}} is non empty set

[a,a1] is V15() set

{a,a1} is non empty set

{a} is non empty set

{{a,a1},{a}} is non empty set

(P,P,R) is Element of bool (P \/ P)

P \/ P is set

bool (P \/ P) is non empty set

proj1 R is set

proj2 R is set

(proj1 R) \/ (proj2 R) is set

(S,S,p) is Element of bool (S \/ S)

S \/ S is set

bool (S \/ S) is non empty set

proj1 p is set

proj2 p is set

(proj1 p) \/ (proj2 p) is set

[b,q9] is V15() set

{b,q9} is non empty set

{{b,q9},{b}} is non empty set

[a1,a] is V15() set

{a1,a} is non empty set

{a1} is non empty set

{{a1,a},{a1}} is non empty set

P is RelStr

the carrier of P is set

the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

dom the InternalRel of P is Element of bool the carrier of P

bool the carrier of P is non empty set

P is Relation-like set

S is RelStr

proj2 P is set

the Relation-like non-empty empty-yielding 0 -defined Function-like empty total V25() Function-yielding Relation-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive RelStr-yielding reflexive-yielding Poset-yielding V159() () set is Relation-like non-empty empty-yielding 0 -defined Function-like empty total V25() Function-yielding Relation-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive RelStr-yielding reflexive-yielding Poset-yielding V159() () set

P is set

the Relation-like P -defined Function-like total RelStr-yielding reflexive-yielding Poset-yielding () set is Relation-like P -defined Function-like total RelStr-yielding reflexive-yielding Poset-yielding () set

P is set

S is Relation-like P -defined Function-like total RelStr-yielding set

R is set

S . R is set

p is non empty set

p9 is Relation-like p -defined Function-like total RelStr-yielding set

q is Element of p

p9 . q is RelStr

the InternalRel of (p9 . q) is Relation-like the carrier of (p9 . q) -defined the carrier of (p9 . q) -valued Element of bool [: the carrier of (p9 . q), the carrier of (p9 . q):]

the carrier of (p9 . q) is set

[: the carrier of (p9 . q), the carrier of (p9 . q):] is Relation-like set

bool [: the carrier of (p9 . q), the carrier of (p9 . q):] is non empty set

R is Relation-like Function-like set

proj1 R is set

R is Relation-like P -defined Function-like total set

p is Relation-like P -defined Function-like total set

p9 is set

R . p9 is set

p . p9 is set

S . p9 is set

q is RelStr

the InternalRel of q is Relation-like the carrier of q -defined the carrier of q -valued Element of bool [: the carrier of q, the carrier of q:]

the carrier of q is set

[: the carrier of q, the carrier of q:] is Relation-like set

bool [: the carrier of q, the carrier of q:] is non empty set

q9 is RelStr

the InternalRel of q9 is Relation-like the carrier of q9 -defined the carrier of q9 -valued Element of bool [: the carrier of q9, the carrier of q9:]

the carrier of q9 is set

[: the carrier of q9, the carrier of q9:] is Relation-like set

bool [: the carrier of q9, the carrier of q9:] is non empty set

P is non empty set

S is Relation-like P -defined Function-like total RelStr-yielding set

(P,S) is Relation-like P -defined Function-like total set

R is Relation-like P -defined Function-like total set

p is Element of P

R . p is set

S . p is RelStr

the InternalRel of (S . p) is Relation-like the carrier of (S . p) -defined the carrier of (S . p) -valued Element of bool [: the carrier of (S . p), the carrier of (S . p):]

the carrier of (S . p) is set

[: the carrier of (S . p), the carrier of (S . p):] is Relation-like set

bool [: the carrier of (S . p), the carrier of (S . p):] is non empty set

p9 is RelStr

the InternalRel of p9 is Relation-like the carrier of p9 -defined the carrier of p9 -valued Element of bool [: the carrier of p9, the carrier of p9:]

the carrier of p9 is set

[: the carrier of p9, the carrier of p9:] is Relation-like set

bool [: the carrier of p9, the carrier of p9:] is non empty set

p is set

S . p is set

R . p is set

p9 is Element of P

S . p9 is RelStr

the InternalRel of (S . p9) is Relation-like the carrier of (S . p9) -defined the carrier of (S . p9) -valued Element of bool [: the carrier of (S . p9), the carrier of (S . p9):]

the carrier of (S . p9) is set

[: the carrier of (S . p9), the carrier of (S . p9):] is Relation-like set

bool [: the carrier of (S . p9), the carrier of (S . p9):] is non empty set

P is set

S is Relation-like P -defined Function-like total RelStr-yielding set

(P,S) is Relation-like P -defined Function-like total set

p is set

proj1 (P,S) is set

(P,S) . p is set

dom (P,S) is Element of bool P

bool P is non empty set

S . p is set

p9 is RelStr

the InternalRel of p9 is Relation-like the carrier of p9 -defined the carrier of p9 -valued Element of bool [: the carrier of p9, the carrier of p9:]

the carrier of p9 is set

[: the carrier of p9, the carrier of p9:] is Relation-like set

bool [: the carrier of p9, the carrier of p9:] is non empty set

P is non empty set

S is Relation-like P -defined Function-like total RelStr-yielding () set

R is Element of P

S . R is RelStr

dom S is Element of bool P

bool P is non empty set

proj2 S is set

p is RelStr

P is ()

the carrier of P is set

{} ({},{}) is Relation-like non-empty empty-yielding {} -defined {} -valued empty total reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Element of bool [:{},{}:]

[:{},{}:] is Relation-like set

bool [:{},{}:] is non empty set

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

() is ()

P is ()

the carrier of P is set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

( the carrier of P, the of P) is () ()

P is ()

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

the carrier of P is set

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

dom the of P is Element of bool the carrier of P

bool the carrier of P is non empty set

P is ()

the carrier of P is set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

( the carrier of P, the of P) is () ()

( the carrier of P, the carrier of P, the of P) is Element of bool ( the carrier of P \/ the carrier of P)

the carrier of P \/ the carrier of P is set

bool ( the carrier of P \/ the carrier of P) is non empty set

proj1 the of P is set

proj2 the of P is set

(proj1 the of P) \/ (proj2 the of P) is set

P is () ()

the carrier of P is set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

P is () () ()

the of P is Relation-like the carrier of P -defined the carrier of P -valued total Element of bool [: the carrier of P, the carrier of P:]

the carrier of P is set

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

( the carrier of P, the carrier of P, the of P) is Element of bool ( the carrier of P \/ the carrier of P)

the carrier of P \/ the carrier of P is set

bool ( the carrier of P \/ the carrier of P) is non empty set

proj1 the of P is set

proj2 the of P is set

(proj1 the of P) \/ (proj2 the of P) is set

P is () ()

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

the carrier of P is set

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

R is set

field the of P is set

proj1 the of P is set

proj2 the of P is set

(proj1 the of P) \/ (proj2 the of P) is set

[R,R] is V15() set

{R,R} is non empty set

{R} is non empty set

{{R,R},{R}} is non empty set

( the carrier of P, the carrier of P, the of P) is Element of bool ( the carrier of P \/ the carrier of P)

the carrier of P \/ the carrier of P is set

bool ( the carrier of P \/ the carrier of P) is non empty set

dom the of P is Element of bool the carrier of P

bool the carrier of P is non empty set

P is () ()

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

the carrier of P is set

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

R is set

field the of P is set

proj1 the of P is set

proj2 the of P is set

(proj1 the of P) \/ (proj2 the of P) is set

p is set

[R,p] is V15() set

{R,p} is non empty set

{R} is non empty set

{{R,p},{R}} is non empty set

[p,R] is V15() set

{p,R} is non empty set

{p} is non empty set

{{p,R},{p}} is non empty set

( the carrier of P, the carrier of P, the of P) is Element of bool ( the carrier of P \/ the carrier of P)

the carrier of P \/ the carrier of P is set

bool ( the carrier of P \/ the carrier of P) is non empty set

dom the of P is Element of bool the carrier of P

bool the carrier of P is non empty set

rng the of P is Element of bool the carrier of P

P is () ()

the carrier of P is set

the of P is Relation-like the carrier of P -defined the carrier of P -valued total Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

( the carrier of P, the of P) is () ()

P is () ()

the carrier of P is set

p is Element of the carrier of P

p9 is Element of the carrier of P

[p,p9] is V15() set

{p,p9} is non empty set

{p} is non empty set

{{p,p9},{p}} is non empty set

the of P is Relation-like the carrier of P -defined the carrier of P -valued symmetric Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

[p9,p] is V15() set

{p9,p} is non empty set

{p9} is non empty set

{{p9,p},{p9}} is non empty set

P is set

nabla P is Relation-like P -defined P -valued total reflexive symmetric transitive Element of bool [:P,P:]

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

(P,(nabla P)) is () ()

the of (P,(nabla P)) is Relation-like the carrier of (P,(nabla P)) -defined the carrier of (P,(nabla P)) -valued Element of bool [: the carrier of (P,(nabla P)), the carrier of (P,(nabla P)):]

the carrier of (P,(nabla P)) is set

[: the carrier of (P,(nabla P)), the carrier of (P,(nabla P)):] is Relation-like set

bool [: the carrier of (P,(nabla P)), the carrier of (P,(nabla P)):] is non empty set

( the carrier of (P,(nabla P)), the carrier of (P,(nabla P)), the of (P,(nabla P))) is Element of bool ( the carrier of (P,(nabla P)) \/ the carrier of (P,(nabla P)))

the carrier of (P,(nabla P)) \/ the carrier of (P,(nabla P)) is set

bool ( the carrier of (P,(nabla P)) \/ the carrier of (P,(nabla P))) is non empty set

proj1 the of (P,(nabla P)) is set

proj2 the of (P,(nabla P)) is set

(proj1 the of (P,(nabla P))) \/ (proj2 the of (P,(nabla P))) is set

P is set

{} (P,P) is Relation-like P -defined P -valued Element of bool [:P,P:]

[:P,P:] is Relation-like set

bool [:P,P:] is non empty set

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

the of (P,({} (P,P))) is Relation-like the carrier of (P,({} (P,P))) -defined the carrier of (P,({} (P,P))) -valued Element of bool [: the carrier of (P,({} (P,P))), the carrier of (P,({} (P,P))):]

the carrier of (P,({} (P,P))) is set

[: the carrier of (P,({} (P,P))), the carrier of (P,({} (P,P))):] is Relation-like set

bool [: the carrier of (P,({} (P,P))), the carrier of (P,({} (P,P))):] is non empty set

R is set

[R,R] is V15() set

{R,R} is non empty set

{R} is non empty set

{{R,R},{R}} is non empty set

R is set

p is set

[R,p] is V15() set

{R,p} is non empty set

{R} is non empty set

{{R,p},{R}} is non empty set

[p,R] is V15() set

{p,R} is non empty set

{p} is non empty set

{{p,R},{p}} is non empty set

nabla {{}} is Relation-like {{}} -defined {{}} -valued total reflexive symmetric transitive Element of bool [:{{}},{{}}:]

[:{{}},{{}}:] is Relation-like non empty set

bool [:{{}},{{}}:] is non empty set

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

P is () () () () ()

the carrier of P is set

{} ({{}},{{}}) is Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]

[:{{}},{{}}:] is Relation-like non empty set

bool [:{{}},{{}}:] is non empty set

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

P is () () () ()

the carrier of P is set

P is Relation-like Function-like set

proj1 P is set

S is set

P . S is set

proj2 P is set

S is set

R is set

P . R is set

P is set

S is Relation-like P -defined Function-like total set

dom S is Element of bool P

bool P is non empty set

R is set

S . R is set

P is Relation-like set

S is set

proj2 P is set

S is set

proj2 P is set

S is set

proj2 P is set

P is set

S is ()

P --> S is Relation-like P -defined {S} -valued Function-like constant total V18(P,{S}) Element of bool [:P,{S}:]

{S} is non empty set

[:P,{S}:] is Relation-like set

bool [:P,{S}:] is non empty set

R is set

(P --> S) . R is set

R is Relation-like P -defined Function-like total set

P is set

S is () () ()

P --> S is Relation-like P -defined {S} -valued Function-like constant total V18(P,{S}) () Element of bool [:P,{S}:]

{S} is non empty set

[:P,{S}:] is Relation-like set

bool [:P,{S}:] is non empty set

p is ()

proj2 (P --> S) is set

rng (P --> S) is Element of bool {S}

bool {S} is non empty set

p is Relation-like P -defined Function-like total set

P is set

S is () ()

P --> S is Relation-like P -defined {S} -valued Function-like constant total V18(P,{S}) () Element of bool [:P,{S}:]

{S} is non empty set

[:P,{S}:] is Relation-like set

bool [:P,{S}:] is non empty set

p is ()

proj2 (P --> S) is set

rng (P --> S) is Element of bool {S}

bool {S} is non empty set

p is Relation-like P -defined Function-like total set

P is set

S is () ()

P --> S is Relation-like P -defined {S} -valued Function-like constant total V18(P,{S}) () Element of bool [:P,{S}:]

{S} is non empty set

[:P,{S}:] is Relation-like set

bool [:P,{S}:] is non empty set

p is ()

proj2 (P --> S) is set

rng (P --> S) is Element of bool {S}

bool {S} is non empty set

p is Relation-like P -defined Function-like total set

P is Relation-like Function-like set

S is set

proj1 P is set

P . S is set

P is set

nabla 0 is Relation-like non-empty empty-yielding 0 -defined 0 -valued empty total reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive () () () Element of bool [:0,0:]

[:0,0:] is Relation-like set

bool [:0,0:] is non empty set

(0,(nabla 0)) is () () () () ()

P --> (0,(nabla 0)) is Relation-like P -defined {(0,(nabla 0))} -valued Function-like constant total V18(P,{(0,(nabla 0))}) 1-sorted-yielding () () () Element of bool [:P,{(0,(nabla 0))}:]

{(0,(nabla 0))} is non empty set

[:P,{(0,(nabla 0))}:] is Relation-like set

bool [:P,{(0,(nabla 0))}:] is non empty set

P is set

{} (0,0) is Relation-like non-empty empty-yielding 0 -defined 0 -valued empty total reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive () () () Element of bool [:0,0:]

[:0,0:] is Relation-like set

bool [:0,0:] is non empty set

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

P --> (0,({} (0,0))) is Relation-like P -defined {(0,({} (0,0)))} -valued Function-like constant total V18(P,{(0,({} (0,0)))}) 1-sorted-yielding () () () Element of bool [:P,{(0,({} (0,0)))}:]

{(0,({} (0,0)))} is non empty set

[:P,{(0,({} (0,0)))}:] is Relation-like set

bool [:P,{(0,({} (0,0)))}:] is non empty set

P is set

the () is ()

P --> the () is Relation-like P -defined { the ()} -valued Function-like constant total V18(P,{ the ()}) 1-sorted-yielding () Element of bool [:P,{ the ()}:]

{ the ()} is non empty set

[:P,{ the ()}:] is Relation-like set

bool [:P,{ the ()}:] is non empty set

P is non empty set

S is Relation-like P -defined Function-like total 1-sorted-yielding () set

R is Element of P

S . R is set

dom S is Element of bool P

bool P is non empty set

P is set

S is Relation-like P -defined Function-like total 1-sorted-yielding () set

R is set

S . R is set

p is non empty set

p9 is Relation-like p -defined Function-like total 1-sorted-yielding () set

q is Element of p

(p,p9,q) is ()

the of (p,p9,q) is Relation-like the carrier of (p,p9,q) -defined the carrier of (p,p9,q) -valued Element of bool [: the carrier of (p,p9,q), the carrier of (p,p9,q):]

the carrier of (p,p9,q) is set

[: the carrier of (p,p9,q), the carrier of (p,p9,q):] is Relation-like set

bool [: the carrier of (p,p9,q), the carrier of (p,p9,q):] is non empty set

R is Relation-like Function-like set

proj1 R is set

R is Relation-like P -defined Function-like total set

p is Relation-like P -defined Function-like total set

p9 is set

R . p9 is set

p . p9 is set

S . p9 is set

q is ()

the of q is Relation-like the carrier of q -defined the carrier of q -valued Element of bool [: the carrier of q, the carrier of q:]

the carrier of q is set

[: the carrier of q, the carrier of q:] is Relation-like set

bool [: the carrier of q, the carrier of q:] is non empty set

q9 is ()

the of q9 is Relation-like the carrier of q9 -defined the carrier of q9 -valued Element of bool [: the carrier of q9, the carrier of q9:]

the carrier of q9 is set

[: the carrier of q9, the carrier of q9:] is Relation-like set

bool [: the carrier of q9, the carrier of q9:] is non empty set

P is non empty set

S is Relation-like P -defined Function-like total 1-sorted-yielding () set

(P,S) is Relation-like P -defined Function-like total set

R is Relation-like P -defined Function-like total set

p is Element of P

R . p is set

(P,S,p) is ()

the of (P,S,p) is Relation-like the carrier of (P,S,p) -defined the carrier of (P,S,p) -valued Element of bool [: the carrier of (P,S,p), the carrier of (P,S,p):]

the carrier of (P,S,p) is set

[: the carrier of (P,S,p), the carrier of (P,S,p):] is Relation-like set

bool [: the carrier of (P,S,p), the carrier of (P,S,p):] is non empty set

p9 is ()

the of p9 is Relation-like the carrier of p9 -defined the carrier of p9 -valued Element of bool [: the carrier of p9, the carrier of p9:]

the carrier of p9 is set

[: the carrier of p9, the carrier of p9:] is Relation-like set

bool [: the carrier of p9, the carrier of p9:] is non empty set

p is set

S . p is set

R . p is set

p9 is Element of P

(P,S,p9) is ()

the of (P,S,p9) is Relation-like the carrier of (P,S,p9) -defined the carrier of (P,S,p9) -valued Element of bool [: the carrier of (P,S,p9), the carrier of (P,S,p9):]

the carrier of (P,S,p9) is set

[: the carrier of (P,S,p9), the carrier of (P,S,p9):] is Relation-like set

bool [: the carrier of (P,S,p9), the carrier of (P,S,p9):] is non empty set

P is set

S is Relation-like P -defined Function-like total 1-sorted-yielding () set

(P,S) is Relation-like P -defined Function-like total set

p is set

proj1 (P,S) is set

(P,S) . p is set

dom (P,S) is Element of bool P

bool P is non empty set

S . p is set

p9 is ()

the of p9 is Relation-like the carrier of p9 -defined the carrier of p9 -valued Element of bool [: the carrier of p9, the carrier of p9:]

the carrier of p9 is set

[: the carrier of p9, the carrier of p9:] is Relation-like set

bool [: the carrier of p9, the carrier of p9:] is non empty set

P is non empty set

S is Relation-like P -defined Function-like total 1-sorted-yielding () () set

R is Element of P

(P,S,R) is ()

dom S is Element of bool P

bool P is non empty set

proj2 S is set

p is ()

P is non empty set

S is Relation-like P -defined Function-like total 1-sorted-yielding () () set

R is Element of P

(P,S,R) is ()

dom S is Element of bool P

bool P is non empty set

proj2 S is set

p is ()

P is non empty set

S is Relation-like P -defined Function-like total 1-sorted-yielding () () set

R is Element of P

(P,S,R) is ()

dom S is Element of bool P

bool P is non empty set

proj2 S is set

p is ()

P is ()

the carrier of P is set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

( the carrier of P, the of P) is () ()

S is ()

the carrier of S is set

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:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of S, the of S) is () ()

R is set

[R,R] is V15() set

{R,R} is non empty set

{R} is non empty set

{{R,R},{R}} is non empty set

P is ()

the carrier of P is set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

( the carrier of P, the of P) is () ()

S is ()

the carrier of S is set

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:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of S, the of S) is () ()

R is set

[R,R] is V15() set

{R,R} is non empty set

{R} is non empty set

{{R,R},{R}} is non empty set

P is ()

the carrier of P is set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

( the carrier of P, the of P) is () ()

S is ()

the carrier of S is set

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:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of S, the of S) is () ()

R is set

p is set

[R,p] is V15() set

{R,p} is non empty set

{R} is non empty set

{{R,p},{R}} is non empty set

[p,R] is V15() set

{p,R} is non empty set

{p} is non empty set

{{p,R},{p}} is non empty set

P is ()

the carrier of P is set

S is ()

the carrier of S is set

[: the carrier of P, the carrier of S:] is Relation-like set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

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:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S) is Relation-like [: the carrier of P, the carrier of S:] -defined [: the carrier of P, the carrier of S:] -valued Element of bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:]

[:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is Relation-like set

bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is non empty set

([: the carrier of P, the carrier of S:],( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S)) is () ()

P is ()

the carrier of P is set

S is ()

the carrier of S is set

P is non empty ()

the carrier of P is non empty set

S is non empty ()

the carrier of S is non empty set

R is Element of the carrier of P

p is Element of the carrier of S

[R,p] is V15() set

{R,p} is non empty set

{R} is non empty set

{{R,p},{R}} is non empty set

(P,S) is ()

[: the carrier of P, the carrier of S:] is Relation-like non empty set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like non empty set

bool [: the carrier of P, the carrier of P:] is non empty set

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:] is Relation-like non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S) is Relation-like [: the carrier of P, the carrier of S:] -defined [: the carrier of P, the carrier of S:] -valued Element of bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:]

[:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is Relation-like non empty set

bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is non empty set

([: the carrier of P, the carrier of S:],( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S)) is () ()

the carrier of (P,S) is set

[R,p] is V15() Element of [: the carrier of P, the carrier of S:]

P is ()

S is ()

(P,S) is ()

the carrier of P is set

the carrier of S is set

[: the carrier of P, the carrier of S:] is Relation-like set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like set

bool [: the carrier of P, the carrier of P:] is non empty set

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:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S) is Relation-like [: the carrier of P, the carrier of S:] -defined [: the carrier of P, the carrier of S:] -valued Element of bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:]

[:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is Relation-like set

bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is non empty set

([: the carrier of P, the carrier of S:],( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S)) is () ()

the carrier of (P,S) is set

P is non empty ()

S is non empty ()

(P,S) is ()

the carrier of P is non empty set

the carrier of S is non empty set

[: the carrier of P, the carrier of S:] is Relation-like non empty set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like non empty set

bool [: the carrier of P, the carrier of P:] is non empty set

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:] is Relation-like non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S) is Relation-like [: the carrier of P, the carrier of S:] -defined [: the carrier of P, the carrier of S:] -valued Element of bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:]

[:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is Relation-like non empty set

bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is non empty set

([: the carrier of P, the carrier of S:],( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S)) is () ()

the carrier of (P,S) is set

R is Element of the carrier of (P,S)

R `1 is set

R `2 is set

P is non empty ()

the carrier of P is non empty set

S is non empty ()

the carrier of S is non empty set

(P,S) is ()

[: the carrier of P, the carrier of S:] is Relation-like non empty set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like non empty set

bool [: the carrier of P, the carrier of P:] is non empty set

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:] is Relation-like non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S) is Relation-like [: the carrier of P, the carrier of S:] -defined [: the carrier of P, the carrier of S:] -valued Element of bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:]

[:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is Relation-like non empty set

bool [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:] is non empty set

([: the carrier of P, the carrier of S:],( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the of P, the of S)) is () ()

R is Element of the carrier of P

p is Element of the carrier of P

p9 is Element of the carrier of S

(P,S,R,p9) is V15() Element of the carrier of (P,S)

the carrier of (P,S) is set

{R,p9} is non empty set

{R} is non empty set

{{R,p9},{R}} is non empty set

q is Element of the carrier of S

(P,S,p,q) is V15() Element of the carrier of (P,S)

{p,q} is non empty set

{p} is non empty set

{{p,q},{p}} is non empty set

[R,p9] is V15() Element of [: the carrier of P, the carrier of S:]

[p,q] is V15() Element of [: the carrier of P, the carrier of S:]

[[R,p9],[p,q]] is V15() Element of [:[: the carrier of P, the carrier of S:],[: the carrier of P, the carrier of S:]:]

{[R,p9],[p,q]} is Relation-like non empty set

{[R,p9]} is Relation-like non empty set

{{[R,p9],[p,q]},{[R,p9]}} is non empty set

the of (P,S) is Relation-like the carrier of (P,S) -defined the carrier of (P,S) -valued Element of bool [: the carrier of (P,S), the carrier of (P,S):]

[: the carrier of (P,S), the carrier of (P,S):] is Relation-like set

bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set

[R,p] is V15() Element of [: the carrier of P, the carrier of P:]

{R,p} is non empty set

{{R,p},{R}} is non empty set

[p9,q] is V15() Element of [: the carrier of S, the carrier of S:]

{p9,q} is non empty set

{p9} is non empty set

{{p9,q},{p9}} is non empty set

[[R,p9],[p,q]] `1 is Element of [: the carrier of P, the carrier of S:]

([[R,p9],[p,q]] `1) `1 is Element of the carrier of P

[[R,p9],[p,q]] `2 is Element of [: the carrier of P, the carrier of S:]

([[R,p9],[p,q]] `2) `1 is Element of the carrier of P

[(([[R,p9],[p,q]] `1) `1),(([[R,p9],[p,q]] `2) `1)] is V15() Element of [: the carrier of P, the carrier of P:]

{(([[R,p9],[p,q]] `1) `1),(([[R,p9],[p,q]] `2) `1)} is non empty set

{(([[R,p9],[p,q]] `1) `1)} is non empty set

{{(([[R,p9],[p,q]] `1) `1),(([[R,p9],[p,q]] `2) `1)},{(([[R,p9],[p,q]] `1) `1)}} is non empty set

([[R,p9],[p,q]] `1) `2 is Element of the carrier of S

([[R,p9],[p,q]] `2) `2 is Element of the carrier of S

[(([[R,p9],[p,q]] `1) `2),(([[R,p9],[p,q]] `2) `2)] is V15() Element of [: the carrier of S, the carrier of S:]

{(([[R,p9],[p,q]] `1) `2),(([[R,p9],[p,q]] `2) `2)} is non empty set

{(([[R,p9],[p,q]] `1) `2)} is non empty set

{{(([[R,p9],[p,q]] `1) `2),(([[R,p9],[p,q]] `2) `2)},{(([[R,p9],[p,q]] `1) `2)}} is non empty set

the of (P,S) is Relation-like the carrier of (P,S) -defined the carrier of (P,S) -valued Element of bool [: the carrier of (P,S), the carrier of (P,S):]

[: the carrier of (P,S), the carrier of (P,S):] is Relation-like set

bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set

P is non empty ()

S is non empty ()

(P,S) is ()

the carrier of P is non empty set

the carrier of S is non empty set

[: the carrier of P, the carrier of S:] is Relation-like non empty set

the of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]

[: the carrier of P, the carrier of P:] is Relation-like non empty set

bool [: the carrier of P, the carrier of P:] is non empty set

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:] is Relation-like non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of P, the