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