:: 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 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)
p is Element of the carrier of (P,S)
(P,S,R) is Element of the carrier of P
(P,S,p) is Element of the carrier of P
(P,S,R) is Element of the carrier of S
(P,S,p) is Element of the carrier of S
[(P,S,R),(P,S,R)] is V15() Element of [: the carrier of P, the carrier of S:]
{(P,S,R),(P,S,R)} is non empty set
{(P,S,R)} is non empty set
{{(P,S,R),(P,S,R)},{(P,S,R)}} 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
[(P,S,p),(P,S,p)] is V15() Element of [: the carrier of P, the carrier of S:]
{(P,S,p),(P,S,p)} is non empty set
{(P,S,p)} is non empty set
{{(P,S,p),(P,S,p)},{(P,S,p)}} 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
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 total reflexive 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 reflexive 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 () ()
R is set
the carrier of (P,S) 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 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 set
p9 is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is non empty set
[:q,q:] is Relation-like non empty set
bool [:q,q:] is non empty set
q9 is Relation-like q -defined q -valued Element of bool [:q,q:]
(q,q,q9) is Element of bool (q \/ q)
q \/ q is non empty set
bool (q \/ q) is non empty set
proj1 q9 is set
proj2 q9 is set
(proj1 q9) \/ (proj2 q9) is 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 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 total reflexive 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 reflexive 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 () ()
R is set
the carrier of (P,S) 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 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 set
p9 is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is non empty set
[:q,q:] is Relation-like non empty set
bool [:q,q:] is non empty set
q9 is Relation-like q -defined q -valued Element of bool [:q,q:]
(q,q,q9) is Element of bool (q \/ q)
q \/ q is non empty set
bool (q \/ q) is non empty set
proj1 q9 is set
proj2 q9 is set
(proj1 q9) \/ (proj2 q9) is set
[p,p] is V15() set
{p,p} is non empty set
{{p,p},{p}} is non empty set
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 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
the of S is Relation-like the carrier of S -defined the carrier of S -valued symmetric 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 symmetric 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 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) is set
[: 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
( the carrier of (P,S), the carrier of (P,S), the of (P,S)) is Element of bool ( the carrier of (P,S) \/ the carrier of (P,S))
the carrier of (P,S) \/ the carrier of (P,S) is set
bool ( the carrier of (P,S) \/ the carrier of (P,S)) is non empty set
proj1 the of (P,S) is set
proj2 the of (P,S) is set
(proj1 the of (P,S)) \/ (proj2 the of (P,S)) is 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
[q,p9] is V15() set
{q,p9} is non empty set
{q} is non empty set
{{q,p9},{q}} is non empty set
P is ()
P is ()
P is ()
P is ()
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),(nabla P)) is () ()
P is set
(P) is ()
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),(nabla P)) is () ()
P is non empty set
(P) is () ()
nabla P is Relation-like P -defined P -valued total reflexive symmetric transitive Element of bool [:P,P:]
[:P,P:] is Relation-like non empty set
bool [:P,P:] is non empty set
(P,(nabla P),(nabla P)) is () ()
P is set
(P) is () ()
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),(nabla P)) is () ()
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) 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 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), the InternalRel 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 InternalRel of (P) is set
proj2 the InternalRel of (P) is set
(proj1 the InternalRel of (P)) \/ (proj2 the InternalRel of (P)) is set
P is set
(P) is total reflexive transitive () () () () ()
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),(nabla P)) is () ()
the carrier of (P) is set
R is Element of the carrier of (P)
p9 is Element of the carrier of (P)
p is Element of the carrier of (P)
q is Element of the carrier of (P)
[p,R] is V15() set
{p,R} is non empty set
{p} is non empty set
{{p,R},{p}} is non empty set
[p,q] is V15() set
{p,q} is non empty set
{{p,q},{p}} is non empty set
the of (P) is Relation-like the carrier of (P) -defined the carrier of (P) -valued total reflexive 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
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,P) is Relation-like P -defined P -valued Element of bool [:P,P:]
(P,(nabla P),({} (P,P))) is () ()
the carrier of (P,(nabla P),({} (P,P))) is set
the InternalRel of (P,(nabla P),({} (P,P))) is Relation-like the carrier of (P,(nabla P),({} (P,P))) -defined the carrier of (P,(nabla P),({} (P,P))) -valued Element of bool [: the carrier of (P,(nabla P),({} (P,P))), the carrier of (P,(nabla P),({} (P,P))):]
[: the carrier of (P,(nabla P),({} (P,P))), the carrier of (P,(nabla P),({} (P,P))):] is Relation-like set
bool [: the carrier of (P,(nabla P),({} (P,P))), the carrier of (P,(nabla P),({} (P,P))):] is non empty set
RelStr(# the carrier of (P,(nabla P),({} (P,P))), the InternalRel of (P,(nabla P),({} (P,P))) #) is strict RelStr
RelStr(# P,(nabla P) #) is strict total reflexive transitive RelStr
the carrier of RelStr(# P,(nabla P) #) is set
the InternalRel of RelStr(# P,(nabla P) #) is Relation-like the carrier of RelStr(# P,(nabla P) #) -defined the carrier of RelStr(# P,(nabla P) #) -valued total reflexive transitive Element of bool [: the carrier of RelStr(# P,(nabla P) #), the carrier of RelStr(# P,(nabla P) #):]
[: the carrier of RelStr(# P,(nabla P) #), the carrier of RelStr(# P,(nabla P) #):] is Relation-like set
bool [: the carrier of RelStr(# P,(nabla P) #), the carrier of RelStr(# P,(nabla P) #):] is non empty set
RelStr(# the carrier of RelStr(# P,(nabla P) #), the InternalRel of RelStr(# P,(nabla P) #) #) is strict total reflexive transitive RelStr
the of (P,(nabla P),({} (P,P))) is Relation-like the carrier of (P,(nabla P),({} (P,P))) -defined the carrier of (P,(nabla P),({} (P,P))) -valued Element of bool [: the carrier of (P,(nabla P),({} (P,P))), the carrier of (P,(nabla P),({} (P,P))):]
( the carrier of (P,(nabla P),({} (P,P))), the of (P,(nabla P),({} (P,P)))) is () ()
(P,({} (P,P))) is () () () ()
the carrier of (P,({} (P,P))) is set
the of (P,({} (P,P))) is Relation-like the carrier of (P,({} (P,P))) -defined the carrier of (P,({} (P,P))) -valued irreflexive symmetric Element of bool [: the carrier of (P,({} (P,P))), the carrier of (P,({} (P,P))):]
[: 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
( the carrier of (P,({} (P,P))), the of (P,({} (P,P)))) is () ()
R is Element of the carrier of (P,(nabla P),({} (P,P)))
p9 is Element of the carrier of (P,(nabla P),({} (P,P)))
p is Element of the carrier of (P,(nabla P),({} (P,P)))
q is Element of the carrier of (P,(nabla P),({} (P,P)))
({{}}) is non empty total reflexive transitive non void () () () () () () ()
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 {{}}),(nabla {{}})) is () ()
P is non empty total reflexive transitive non void () () () () () () ()
the carrier of 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
{} ({{}},{{}}) is Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]
({{}},(nabla {{}}),({} ({{}},{{}}))) is total reflexive transitive () () () () () ()
P is total reflexive transitive () () () () () ()
the carrier of P is set
(0) is total reflexive transitive () () () () () () ()
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),(nabla 0)) is () ()
() is ()
P is set
{P} is non empty set
({P}) is non empty total reflexive transitive non void () () () () () () ()
nabla {P} is Relation-like {P} -defined {P} -valued total reflexive symmetric transitive Element of bool [:{P},{P}:]
[:{P},{P}:] is Relation-like non empty set
bool [:{P},{P}:] is non empty set
({P},(nabla {P}),(nabla {P})) is () ()
P is set
(P) is ()
{P} is non empty set
({P}) is non empty total reflexive transitive non void () () () () () () ()
nabla {P} is Relation-like {P} -defined {P} -valued total reflexive symmetric transitive Element of bool [:{P},{P}:]
[:{P},{P}:] is Relation-like non empty set
bool [:{P},{P}:] is non empty set
({P},(nabla {P}),(nabla {P})) is () ()
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
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
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
P is Relation-like set
S is set
proj2 P is set
P is Relation-like set
S is RelStr
proj2 P is set
S is RelStr
proj2 P is set
S is ()
proj2 P is set
S is ()
proj2 P is set
P is set
S is total reflexive transitive () () () () () ()
P --> S is Relation-like P -defined {S} -valued Function-like constant total V18(P,{S}) 1-sorted-yielding () () () 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
P --> () is Relation-like P -defined {()} -valued Function-like constant total V18(P,{()}) 1-sorted-yielding RelStr-yielding reflexive-yielding () () () () () () () Element of bool [:P,{()}:]
{()} is non empty set
[:P,{()}:] is Relation-like set
bool [:P,{()}:] is non empty set
P is non empty set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
R is Element of P
S . R is set
P is non empty set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding reflexive-yielding () () () () () () set
R is Element of P
S . R is set
R is ()
the carrier of R is set
p is ()
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
p9 is ()
the carrier of p9 is set
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, the carrier of p9:] is Relation-like set
bool [: the carrier of p9, the carrier of p9:] is non empty set
P is RelStr
the carrier of P is set
S is RelStr
the carrier of S 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
the InternalRel 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
R is Element of the carrier of P
p is Element of the carrier of P
p9 is Element of the carrier of S
q 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
[p9,q] is V15() set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
P is ()
the carrier of P is set
S is ()
the carrier of S 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 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
R is Element of the carrier of P
p is Element of the carrier of P
p9 is Element of the carrier of S
q 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
[p9,q] is V15() set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
P is ()
the carrier of P is set
S is ()
the carrier of S is set
R is set
P is set
S is ()
P --> S is Relation-like P -defined {S} -valued Function-like constant total V18(P,{S}) 1-sorted-yielding () 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
p9 is ()
rng (P --> S) is Element of bool {S}
bool {S} is non empty set
p is Relation-like P -defined Function-like total set
the total reflexive transitive () () () () () () is total reflexive transitive () () () () () ()
0 --> the total reflexive transitive () () () () () () is Relation-like non-empty empty-yielding {} -defined 0 -defined { the total reflexive transitive () () () () () ()} -valued Function-like constant empty total total V18( 0 ,{ the total reflexive transitive () () () () () ()}) V25() Function-yielding Relation-yielding 1-sorted-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive RelStr-yielding reflexive-yielding V159() () () () () () () () () Element of bool [:0,{ the total reflexive transitive () () () () () ()}:]
{ the total reflexive transitive () () () () () ()} is non empty set
[:0,{ the total reflexive transitive () () () () () ()}:] is Relation-like set
bool [:0,{ the total reflexive transitive () () () () () ()}:] is non empty set
P is set
the total reflexive transitive () () () () () () is total reflexive transitive () () () () () ()
P --> the total reflexive transitive () () () () () () is Relation-like P -defined { the total reflexive transitive () () () () () ()} -valued Function-like constant total V18(P,{ the total reflexive transitive () () () () () ()}) 1-sorted-yielding RelStr-yielding reflexive-yielding () () () () () () () Element of bool [:P,{ the total reflexive transitive () () () () () ()}:]
{ the total reflexive transitive () () () () () ()} is non empty set
[:P,{ the total reflexive transitive () () () () () ()}:] is Relation-like set
bool [:P,{ the total reflexive transitive () () () () () ()}:] is non empty set
P is set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
Carrier S is Relation-like P -defined Function-like total set
Union (Carrier S) is set
proj2 (Carrier S) is set
union (proj2 (Carrier S)) is set
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
dom (Carrier S) is Element of bool P
bool P is non empty set
[:(Union (Carrier S)),(Union (Carrier S)):] is Relation-like set
b is set
a1 is set
dom (P,S) is Element of bool P
b1 is set
(P,S) . b1 is set
S . b1 is set
p1 is RelStr
the InternalRel of p1 is Relation-like the carrier of p1 -defined the carrier of p1 -valued Element of bool [: the carrier of p1, the carrier of p1:]
the carrier of p1 is set
[: the carrier of p1, the carrier of p1:] is Relation-like set
bool [: the carrier of p1, the carrier of p1:] is non empty set
q1 is set
t is set
[q1,t] is V15() set
{q1,t} is non empty set
{q1} is non empty set
{{q1,t},{q1}} is non empty set
(Carrier S) . b1 is set
e is 1-sorted
the carrier of e is set
bool [:(Union (Carrier S)),(Union (Carrier S)):] is non empty set
a1 is set
b1 is set
dom (P,S) is Element of bool P
p1 is set
(P,S) . p1 is set
S . p1 is set
q1 is ()
the of q1 is Relation-like the carrier of q1 -defined the carrier of q1 -valued Element of bool [: the carrier of q1, the carrier of q1:]
the carrier of q1 is set
[: the carrier of q1, the carrier of q1:] is Relation-like set
bool [: the carrier of q1, the carrier of q1:] 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
(Carrier S) . p1 is set
f is 1-sorted
the carrier of f is set
b is Relation-like Union (Carrier S) -defined Union (Carrier S) -valued Element of bool [:(Union (Carrier S)),(Union (Carrier S)):]
a1 is Relation-like Union (Carrier S) -defined Union (Carrier S) -valued Element of bool [:(Union (Carrier S)),(Union (Carrier S)):]
((Union (Carrier S)),b,a1) is () ()
the carrier of ((Union (Carrier S)),b,a1) is set
the InternalRel of ((Union (Carrier S)),b,a1) is Relation-like the carrier of ((Union (Carrier S)),b,a1) -defined the carrier of ((Union (Carrier S)),b,a1) -valued Element of bool [: the carrier of ((Union (Carrier S)),b,a1), the carrier of ((Union (Carrier S)),b,a1):]
[: the carrier of ((Union (Carrier S)),b,a1), the carrier of ((Union (Carrier S)),b,a1):] is Relation-like set
bool [: the carrier of ((Union (Carrier S)),b,a1), the carrier of ((Union (Carrier S)),b,a1):] is non empty set
the of ((Union (Carrier S)),b,a1) is Relation-like the carrier of ((Union (Carrier S)),b,a1) -defined the carrier of ((Union (Carrier S)),b,a1) -valued Element of bool [: the carrier of ((Union (Carrier S)),b,a1), the carrier of ((Union (Carrier S)),b,a1):]
R is () ()
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
p is () ()
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
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:]
P is set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
(P,S) is () ()
the carrier of (P,S) is set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
dom (P,S) is Element of bool P
bool P is non empty set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
the InternalRel 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
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
q is set
q9 is set
(P,S) . q9 is set
a is non empty set
b is Relation-like a -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
a1 is Element of a
(a,b,a1) is ()
S . q9 is set
b1 is ()
the carrier of b1 is set
the InternalRel of (a,b,a1) is Relation-like the carrier of (a,b,a1) -defined the carrier of (a,b,a1) -valued Element of bool [: the carrier of (a,b,a1), the carrier of (a,b,a1):]
the carrier of (a,b,a1) is set
[: the carrier of (a,b,a1), the carrier of (a,b,a1):] is Relation-like set
bool [: the carrier of (a,b,a1), the carrier of (a,b,a1):] is non empty set
p1 is Element of the carrier of b1
q1 is Element of the carrier of b1
[p1,q1] is V15() set
{p1,q1} is non empty set
{p1} is non empty set
{{p1,q1},{p1}} is non empty set
the InternalRel of b1 is Relation-like the carrier of b1 -defined the carrier of b1 -valued Element of bool [: the carrier of b1, the carrier of b1:]
[: the carrier of b1, the carrier of b1:] is Relation-like set
bool [: the carrier of b1, the carrier of b1:] is non empty set
q9 is ()
the carrier of q9 is set
q is set
S . q is set
a is Element of the carrier of q9
b is Element of the carrier of q9
[a,b] is V15() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
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, the carrier of q9:] is Relation-like set
bool [: the carrier of q9, the carrier of q9:] is non empty set
a1 is non empty set
p1 is Relation-like a1 -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
(a1,p1) is Relation-like a1 -defined Function-like total Relation-yielding set
b1 is Element of a1
(a1,p1) . b1 is set
(a1,p1,b1) is ()
the InternalRel of (a1,p1,b1) is Relation-like the carrier of (a1,p1,b1) -defined the carrier of (a1,p1,b1) -valued Element of bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):]
the carrier of (a1,p1,b1) is set
[: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is Relation-like set
bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is non empty set
proj2 (P,S) is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
Union (P,S) is set
union (proj2 (P,S)) is set
the InternalRel 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 set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
(P,S) is () ()
the carrier of (P,S) is set
R is Element of the carrier of (P,S)
p is Element of the carrier of (P,S)
q is ()
the carrier of q is set
p9 is set
S . p9 is set
q9 is Element of the carrier of q
a is Element of the carrier of q
p9 is Element of P
(P,S,p9) is ()
the carrier of (P,S,p9) is set
q is Element of the carrier of (P,S,p9)
q9 is Element of the carrier of (P,S,p9)
P is set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
(P,S) is () ()
the carrier of (P,S) is set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
dom (P,S) is Element of bool P
bool P is non empty set
[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,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
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
q is set
q9 is set
(P,S) . q9 is set
a is non empty set
b is Relation-like a -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
a1 is Element of a
(a,b,a1) is ()
S . q9 is set
b1 is ()
the carrier of b1 is set
the of (a,b,a1) is Relation-like the carrier of (a,b,a1) -defined the carrier of (a,b,a1) -valued Element of bool [: the carrier of (a,b,a1), the carrier of (a,b,a1):]
the carrier of (a,b,a1) is set
[: the carrier of (a,b,a1), the carrier of (a,b,a1):] is Relation-like set
bool [: the carrier of (a,b,a1), the carrier of (a,b,a1):] is non empty set
p1 is Element of the carrier of b1
q1 is Element of the carrier of b1
[p1,q1] is V15() set
{p1,q1} is non empty set
{p1} is non empty set
{{p1,q1},{p1}} is non empty set
the of b1 is Relation-like the carrier of b1 -defined the carrier of b1 -valued Element of bool [: the carrier of b1, the carrier of b1:]
[: the carrier of b1, the carrier of b1:] is Relation-like set
bool [: the carrier of b1, the carrier of b1:] is non empty set
q9 is ()
the carrier of q9 is set
q is set
S . q is set
a is Element of the carrier of q9
b is Element of the carrier of q9
[a,b] is V15() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
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, the carrier of q9:] is Relation-like set
bool [: the carrier of q9, the carrier of q9:] is non empty set
a1 is non empty set
p1 is Relation-like a1 -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
(a1,p1) is Relation-like a1 -defined Function-like total Relation-yielding set
b1 is Element of a1
(a1,p1) . b1 is set
(a1,p1,b1) is ()
the of (a1,p1,b1) is Relation-like the carrier of (a1,p1,b1) -defined the carrier of (a1,p1,b1) -valued Element of bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):]
the carrier of (a1,p1,b1) is set
[: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is Relation-like set
bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is non empty set
proj2 (P,S) is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
Union (P,S) is set
union (proj2 (P,S)) is 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 set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () set
(P,S) is () ()
the carrier of (P,S) is set
R is Element of the carrier of (P,S)
p is Element of the carrier of (P,S)
q is ()
the carrier of q is set
p9 is set
S . p9 is set
q9 is Element of the carrier of q
a is Element of the carrier of q
p9 is Element of P
(P,S,p9) is ()
the carrier of (P,S,p9) is set
q is Element of the carrier of (P,S,p9)
q9 is Element of the carrier of (P,S,p9)
P is set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding reflexive-yielding () () set
(P,S) is () ()
the InternalRel 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) is set
[: 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
Carrier S is Relation-like P -defined Function-like total set
Union (Carrier S) is set
proj2 (Carrier S) is set
union (proj2 (Carrier S)) is set
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
dom (P,S) is Element of bool P
bool P is non empty set
q9 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
a is set
dom (Carrier S) is Element of bool P
b is set
(Carrier S) . b is set
S . b is set
a1 is non empty set
p1 is Relation-like a1 -defined Function-like total 1-sorted-yielding RelStr-yielding reflexive-yielding () () set
(a1,p1) is Relation-like a1 -defined Function-like total Relation-yielding set
b1 is Element of a1
(a1,p1) . b1 is set
(a1,p1,b1) is total reflexive ()
the InternalRel of (a1,p1,b1) is Relation-like the carrier of (a1,p1,b1) -defined the carrier of (a1,p1,b1) -valued total reflexive Element of bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):]
the carrier of (a1,p1,b1) is set
[: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is Relation-like set
bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is non empty set
q1 is 1-sorted
the carrier of q1 is set
proj2 (a1,p1) is set
P is set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () () set
(P,S) is () ()
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) is set
[: 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
Carrier S is Relation-like P -defined Function-like total set
Union (Carrier S) is set
proj2 (Carrier S) is set
union (proj2 (Carrier S)) is set
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
dom (P,S) is Element of bool P
bool P is non empty set
q9 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
a is set
dom (Carrier S) is Element of bool P
b is set
(Carrier S) . b is set
S . b is set
a1 is non empty set
p1 is Relation-like a1 -defined Function-like total 1-sorted-yielding RelStr-yielding () () () set
(a1,p1) is Relation-like a1 -defined Function-like total Relation-yielding set
b1 is Element of a1
(a1,p1) . b1 is set
(a1,p1,b1) is () () ()
the of (a1,p1,b1) is Relation-like the carrier of (a1,p1,b1) -defined the carrier of (a1,p1,b1) -valued total reflexive Element of bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):]
the carrier of (a1,p1,b1) is set
[: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is Relation-like set
bool [: the carrier of (a1,p1,b1), the carrier of (a1,p1,b1):] is non empty set
q1 is 1-sorted
the carrier of q1 is set
proj2 (a1,p1) is set
P is set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding () () () set
(P,S) is () ()
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) is set
[: 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,S) is Relation-like P -defined Function-like total Relation-yielding set
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) 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
[q9,q] is V15() set
{q9,q} is non empty set
{q9} is non empty set
{{q9,q},{q9}} is non empty set
a is set
dom (P,S) is Element of bool P
bool P is non empty set
b is set
(P,S) . b is set
a1 is non empty set
b1 is Relation-like a1 -defined Function-like total 1-sorted-yielding RelStr-yielding () () () set
(a1,b1) is Relation-like a1 -defined Function-like total Relation-yielding set
p1 is Element of a1
(a1,b1) . p1 is set
(a1,b1,p1) is () ()
the of (a1,b1,p1) is Relation-like the carrier of (a1,b1,p1) -defined the carrier of (a1,b1,p1) -valued symmetric Element of bool [: the carrier of (a1,b1,p1), the carrier of (a1,b1,p1):]
the carrier of (a1,b1,p1) is set
[: the carrier of (a1,b1,p1), the carrier of (a1,b1,p1):] is Relation-like set
bool [: the carrier of (a1,b1,p1), the carrier of (a1,b1,p1):] is non empty set
proj2 (a1,b1) is set
P is set
S is Relation-like P -defined Function-like total 1-sorted-yielding RelStr-yielding reflexive-yielding () () () () () () () set
(P,S) is total reflexive () () () () ()
the InternalRel of (P,S) is Relation-like the carrier of (P,S) -defined the carrier of (P,S) -valued total reflexive Element of bool [: the carrier of (P,S), the carrier of (P,S):]
the carrier of (P,S) is set
[: 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
the of (P,S) is Relation-like the carrier of (P,S) -defined the carrier of (P,S) -valued total reflexive symmetric Element of bool [: the carrier of (P,S), the carrier of (P,S):]
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
(P,S) is Relation-like P -defined Function-like total Relation-yielding set
Union (P,S) is set
proj2 (P,S) is set
union (proj2 (P,S)) is set
dom S is Element of bool P
bool P is non empty set
q9 is set
a is set
b 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
[a,b] is V15() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
[q9,b] is V15() set
{q9,b} is non empty set
{{q9,b},{q9}} is non empty set
a1 is set
dom (P,S) is Element of bool P
b1 is set
(P,S) . b1 is set
p1 is set
q1 is set
(P,S) . q1 is set
t is non empty set
e is Relation-like t -defined Function-like total 1-sorted-yielding RelStr-yielding reflexive-yielding () () () () () () () set
(t,e) is Relation-like t -defined Function-like total Relation-yielding set
f is Element of t
(t,e) . f is set
(t,e,f) is total reflexive transitive () () () () () ()
the InternalRel of (t,e,f) is Relation-like the carrier of (t,e,f) -defined the carrier of (t,e,f) -valued total reflexive transitive Element of bool [: the carrier of (t,e,f), the carrier of (t,e,f):]
the carrier of (t,e,f) is set
[: the carrier of (t,e,f), the carrier of (t,e,f):] is Relation-like set
bool [: the carrier of (t,e,f), the carrier of (t,e,f):] is non empty set
g is Element of t
(t,e) . g is set
(t,e,g) is total reflexive transitive () () () () () ()
the InternalRel of (t,e,g) is Relation-like the carrier of (t,e,g) -defined the carrier of (t,e,g) -valued total reflexive transitive Element of bool [: the carrier of (t,e,g), the carrier of (t,e,g):]
the carrier of (t,e,g) is set
[: the carrier of (t,e,g), the carrier of (t,e,g):] is Relation-like set
bool [: the carrier of (t,e,g), the carrier of (t,e,g):] is non empty set
proj2 e is set
q9 is Element of the carrier of (P,S)
b is Element of the carrier of (P,S)
a is Element of the carrier of (P,S)
a1 is Element of the carrier of (P,S)
[a,q9] is V15() set
{a,q9} is non empty set
{a} is non empty set
{{a,q9},{a}} is non empty set
b1 is set
dom (P,S) is Element of bool P
p1 is set
(P,S) . p1 is set
q1 is non empty set
t is Relation-like q1 -defined Function-like total 1-sorted-yielding RelStr-yielding reflexive-yielding () () () () () () () set
(q1,t) is Relation-like q1 -defined Function-like total Relation-yielding set
e is Element of q1
(q1,t) . e is set
(q1,t,e) is total reflexive transitive () () () () () ()
the of (q1,t,e) is Relation-like the carrier of (q1,t,e) -defined the carrier of (q1,t,e) -valued total reflexive symmetric Element of bool [: the carrier of (q1,t,e), the carrier of (q1,t,e):]
the carrier of (q1,t,e) is set
[: the carrier of (q1,t,e), the carrier of (q1,t,e):] is Relation-like set
bool [: the carrier of (q1,t,e), the carrier of (q1,t,e):] is non empty set
(q1,t) is Relation-like q1 -defined Function-like total Relation-yielding set
(q1,t) . e is set
the InternalRel of (q1,t,e) is Relation-like the carrier of (q1,t,e) -defined the carrier of (q1,t,e) -valued total reflexive transitive Element of bool [: the carrier of (q1,t,e), the carrier of (q1,t,e):]
[a1,b] is V15() set
{a1,b} is non empty set
{a1} is non empty set
{{a1,b},{a1}} is non empty set
proj2 (q1,t) is set
h is set
dom (q1,t) is Element of bool q1
bool q1 is non empty set
P is set
(q1,t) . P is set
Q is Element of q1
(q1,t) . Q is set
(q1,t,Q) is total reflexive transitive () () () () () ()
the of (q1,t,Q) is Relation-like the carrier of (q1,t,Q) -defined the carrier of (q1,t,Q) -valued total reflexive symmetric Element of bool [: the carrier of (q1,t,Q), the carrier of (q1,t,Q):]
the carrier of (q1,t,Q) is set
[: the carrier of (q1,t,Q), the carrier of (q1,t,Q):] is Relation-like set
bool [: the carrier of (q1,t,Q), the carrier of (q1,t,Q):] is non empty set
(q1,t) . Q is set
the InternalRel of (q1,t,Q) is Relation-like the carrier of (q1,t,Q) -defined the carrier of (q1,t,Q) -valued total reflexive transitive Element of bool [: the carrier of (q1,t,Q), the carrier of (q1,t,Q):]
[q9,b] is V15() set
{q9,b} is non empty set
{q9} is non empty set
{{q9,b},{q9}} is non empty set
proj2 (q1,t) is set
c is set
dom (q1,t) is Element of bool q1
e is set
(q1,t) . e is set
g is Element of q1
(q1,t) . g is set
(q1,t,g) is total reflexive transitive () () () () () ()
the of (q1,t,g) is Relation-like the carrier of (q1,t,g) -defined the carrier of (q1,t,g) -valued total reflexive symmetric Element of bool [: the carrier of (q1,t,g), the carrier of (q1,t,g):]
the carrier of (q1,t,g) is set
[: the carrier of (q1,t,g), the carrier of (q1,t,g):] is Relation-like set
bool [: the carrier of (q1,t,g), the carrier of (q1,t,g):] is non empty set
proj2 t is set
the InternalRel of (q1,t,g) is Relation-like the carrier of (q1,t,g) -defined the carrier of (q1,t,g) -valued total reflexive transitive Element of bool [: the carrier of (q1,t,g), the carrier of (q1,t,g):]
f is Element of the carrier of (q1,t,g)
b is Element of the carrier of (q1,t,g)
h is Element of the carrier of (q1,t,g)
d is Element of the carrier of (q1,t,g)
[f,h] is V15() set
{f,h} is non empty set
{f} is non empty set
{{f,h},{f}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
the InternalRel of (q1,t,g) is Relation-like the carrier of (q1,t,g) -defined the carrier of (q1,t,g) -valued total reflexive transitive Element of bool [: the carrier of (q1,t,g), the carrier of (q1,t,g):]
f is Element of the carrier of (q1,t,g)
b is Element of the carrier of (q1,t,g)
h is Element of the carrier of (q1,t,g)
d is Element of the carrier of (q1,t,g)
[f,h] is V15() set
{f,h} is non empty set
{f} is non empty set
{{f,h},{f}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
the InternalRel of (q1,t,g) is Relation-like the carrier of (q1,t,g) -defined the carrier of (q1,t,g) -valued total reflexive transitive Element of bool [: the carrier of (q1,t,g), the carrier of (q1,t,g):]
f is Element of the carrier of (q1,t,Q)
qi is Element of the carrier of (q1,t,Q)
h is Element of the carrier of (q1,t,Q)
a is Element of the carrier of (q1,t,Q)
[f,h] is V15() set
{f,h} is non empty set
{f} is non empty set
{{f,h},{f}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
f is Element of the carrier of (q1,t,Q)
qi is Element of the carrier of (q1,t,Q)
h is Element of the carrier of (q1,t,Q)
a is Element of the carrier of (q1,t,Q)
f is Element of the carrier of (q1,t,e)
qi is Element of the carrier of (q1,t,e)
[f,h] is V15() set
{f,h} is non empty set
{f} is non empty set
{{f,h},{f}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
g is Element of the carrier of (q1,t,e)
f is Element of the carrier of (q1,t,e)
f is Element of the carrier of (q1,t,e)
h is Element of the carrier of (q1,t,e)
qi is Element of the carrier of (q1,t,Q)
a is Element of the carrier of (q1,t,Q)
[g,f] is V15() set
{g,f} is non empty set
{g} is non empty set
{{g,f},{g}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
the InternalRel of (q1,t,g) is Relation-like the carrier of (q1,t,g) -defined the carrier of (q1,t,g) -valued total reflexive transitive Element of bool [: the carrier of (q1,t,g), the carrier of (q1,t,g):]
f is Element of the carrier of (q1,t,g)
d is Element of the carrier of (q1,t,g)
g is Element of the carrier of (q1,t,e)
f is Element of the carrier of (q1,t,e)
h is Element of the carrier of (q1,t,e)
qi is Element of the carrier of (q1,t,e)
[g,h] is V15() set
{g,h} is non empty set
{g} is non empty set
{{g,h},{g}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
P is set
S is set
<%P,S%> is Relation-like K138() -defined Function-like V25() V28() V35(2) V159() set
len <%P,S%> is Element of K138()
proj1 <%P,S%> is V27() set
len <%P,S%> is Element of K138()
proj1 <%P,S%> is V27() set
P is 1-sorted
S is 1-sorted
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) V159() set
R is set
proj1 <%P,S%> is V27() set
<%P,S%> . R is set
dom <%P,S%> is V27() Element of bool K138()
len <%P,S%> is Element of K138()
P is set
S is set
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) V159() set
(0,1) --> (P,S) is set
proj2 <%P,S%> is set
{P,S} is non empty set
P is RelStr
S is RelStr
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding V159() set
R is set
proj2 <%P,S%> is set
{P,S} is non empty set
P is ()
S is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding V159() set
R is set
<%P,S%> . R is set
P is ()
S is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () set
R is set
<%P,S%> . R is set
P is total reflexive ()
S is total reflexive ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
R is RelStr
proj2 <%P,S%> is set
{P,S} is non empty set
P is transitive ()
S is transitive ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
R is RelStr
proj2 <%P,S%> is set
{P,S} is non empty set
P is () () ()
S is () () ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
R is ()
proj2 <%P,S%> is set
{P,S} is non empty set
P is () ()
S is () ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
R is ()
proj2 <%P,S%> is set
{P,S} is non empty set
P is total reflexive transitive () () () () () ()
S is total reflexive transitive () () () () () ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding reflexive-yielding V159() () () () () () set
R is set
<%P,S%> . R is set
P is ()
S is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
({0,1},<%P,S%>) is () ()
P is ()
S is ()
(P,S) is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
({0,1},<%P,S%>) is () ()
the carrier of (P,S) is set
the carrier of P is set
the carrier of S is set
the carrier of P \/ the carrier of S is set
the InternalRel 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
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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 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 P, the carrier of S, the carrier of S, the InternalRel of P, the InternalRel 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 () ()
Carrier <%P,S%> is Relation-like {0,1} -defined Function-like total set
dom (Carrier <%P,S%>) is Element of bool {0,1}
bool {0,1} is non empty set
({0,1},<%P,S%>) is Relation-like {0,1} -defined Function-like total Relation-yielding set
dom ({0,1},<%P,S%>) is Element of bool {0,1}
({0,1},<%P,S%>) is Relation-like {0,1} -defined Function-like total Relation-yielding set
dom ({0,1},<%P,S%>) is Element of bool {0,1}
<%P,S%> . 0 is set
<%P,S%> . 1 is set
the carrier of H₁(P,S) is set
Union (Carrier <%P,S%>) is set
proj2 (Carrier <%P,S%>) is set
union (proj2 (Carrier <%P,S%>)) is set
p9 is set
z is Element of {0,1}
(Carrier <%P,S%>) . z is set
({0,1},<%P,S%>,z) is ()
the carrier of ({0,1},<%P,S%>,z) is set
j is Element of {0,1}
(Carrier <%P,S%>) . j is set
({0,1},<%P,S%>,j) is ()
the carrier of ({0,1},<%P,S%>,j) is set
p9 is set
q is set
q9 is set
(Carrier <%P,S%>) . q9 is set
z is Element of {0,1}
({0,1},<%P,S%>,z) is ()
the carrier of ({0,1},<%P,S%>,z) is set
j is Element of {0,1}
({0,1},<%P,S%>,j) is ()
the carrier of ({0,1},<%P,S%>,j) is set
the InternalRel of H₁(P,S) is Relation-like the carrier of H₁(P,S) -defined the carrier of H₁(P,S) -valued Element of bool [: the carrier of H₁(P,S), the carrier of H₁(P,S):]
[: the carrier of H₁(P,S), the carrier of H₁(P,S):] is Relation-like set
bool [: the carrier of H₁(P,S), the carrier of H₁(P,S):] is non empty set
Union ({0,1},<%P,S%>) is set
proj2 ({0,1},<%P,S%>) is set
union (proj2 ({0,1},<%P,S%>)) is set
p9 is set
z is Element of {0,1}
({0,1},<%P,S%>) . z is set
({0,1},<%P,S%>,z) is ()
the InternalRel of ({0,1},<%P,S%>,z) is Relation-like the carrier of ({0,1},<%P,S%>,z) -defined the carrier of ({0,1},<%P,S%>,z) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):]
the carrier of ({0,1},<%P,S%>,z) is set
[: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is non empty set
j is Element of {0,1}
({0,1},<%P,S%>) . j is set
({0,1},<%P,S%>,j) is ()
the InternalRel of ({0,1},<%P,S%>,j) is Relation-like the carrier of ({0,1},<%P,S%>,j) -defined the carrier of ({0,1},<%P,S%>,j) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):]
the carrier of ({0,1},<%P,S%>,j) is set
[: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is non empty set
p9 is set
q is set
q9 is set
({0,1},<%P,S%>) . q9 is set
z is Element of {0,1}
({0,1},<%P,S%>,z) is ()
the InternalRel of ({0,1},<%P,S%>,z) is Relation-like the carrier of ({0,1},<%P,S%>,z) -defined the carrier of ({0,1},<%P,S%>,z) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):]
the carrier of ({0,1},<%P,S%>,z) is set
[: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is non empty set
j is Element of {0,1}
({0,1},<%P,S%>,j) is ()
the InternalRel of ({0,1},<%P,S%>,j) is Relation-like the carrier of ({0,1},<%P,S%>,j) -defined the carrier of ({0,1},<%P,S%>,j) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):]
the carrier of ({0,1},<%P,S%>,j) is set
[: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is non empty set
the of H₁(P,S) is Relation-like the carrier of H₁(P,S) -defined the carrier of H₁(P,S) -valued Element of bool [: the carrier of H₁(P,S), the carrier of H₁(P,S):]
Union ({0,1},<%P,S%>) is set
proj2 ({0,1},<%P,S%>) is set
union (proj2 ({0,1},<%P,S%>)) is set
p9 is set
z is Element of {0,1}
({0,1},<%P,S%>) . z is set
({0,1},<%P,S%>,z) is ()
the of ({0,1},<%P,S%>,z) is Relation-like the carrier of ({0,1},<%P,S%>,z) -defined the carrier of ({0,1},<%P,S%>,z) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):]
the carrier of ({0,1},<%P,S%>,z) is set
[: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is non empty set
j is Element of {0,1}
({0,1},<%P,S%>) . j is set
({0,1},<%P,S%>,j) is ()
the of ({0,1},<%P,S%>,j) is Relation-like the carrier of ({0,1},<%P,S%>,j) -defined the carrier of ({0,1},<%P,S%>,j) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):]
the carrier of ({0,1},<%P,S%>,j) is set
[: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is non empty set
p9 is set
q is set
q9 is set
({0,1},<%P,S%>) . q9 is set
z is Element of {0,1}
({0,1},<%P,S%>,z) is ()
the of ({0,1},<%P,S%>,z) is Relation-like the carrier of ({0,1},<%P,S%>,z) -defined the carrier of ({0,1},<%P,S%>,z) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):]
the carrier of ({0,1},<%P,S%>,z) is set
[: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,z), the carrier of ({0,1},<%P,S%>,z):] is non empty set
j is Element of {0,1}
({0,1},<%P,S%>,j) is ()
the of ({0,1},<%P,S%>,j) is Relation-like the carrier of ({0,1},<%P,S%>,j) -defined the carrier of ({0,1},<%P,S%>,j) -valued Element of bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):]
the carrier of ({0,1},<%P,S%>,j) is set
[: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is Relation-like set
bool [: the carrier of ({0,1},<%P,S%>,j), the carrier of ({0,1},<%P,S%>,j):] is non empty set
P is ()
S is ()
(P,S) is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
({0,1},<%P,S%>) is () ()
the carrier of P is set
the carrier of S is set
the carrier of P \/ the carrier of S 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 P, the carrier of S, the carrier of S, the InternalRel of P, the InternalRel 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
the InternalRel 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 ()
S is ()
(P,S) is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
({0,1},<%P,S%>) is () ()
the carrier of (P,S) is set
the carrier of P is set
the carrier of S is set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
the InternalRel 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
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
the InternalRel 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 InternalRel of P, the InternalRel 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 is set
[:( 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
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is Element of the carrier of P
q9 is Element of the carrier of P
q is Element of the carrier of S
q9 is Element of the carrier of S
q is Element of the carrier of P
q9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of P
[q,q9] is V15() set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is non empty set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is Element of the carrier of S
q9 is Element of the carrier of S
q is Element of the carrier of S
q9 is Element of the carrier of S
[q,q9] is V15() set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is non empty set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is Element of the carrier of P
q9 is Element of the carrier of P
a is Element of the carrier of S
b is Element of the carrier of S
P is ()
S is ()
(P,S) is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () set
({0,1},<%P,S%>) is () ()
the carrier of (P,S) is set
the carrier of P is set
the carrier of S is set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
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
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 is set
[:( 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
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is Element of the carrier of P
q9 is Element of the carrier of P
q is Element of the carrier of S
q9 is Element of the carrier of S
q is Element of the carrier of P
q9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of P
[q,q9] is V15() set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is non empty set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is Element of the carrier of S
q9 is Element of the carrier of S
q is Element of the carrier of S
q9 is Element of the carrier of S
[q,q9] is V15() set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is non empty set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is Element of the carrier of P
q9 is Element of the carrier of P
a is Element of the carrier of S
b is Element of the carrier of S
P is total reflexive ()
S is total reflexive ()
(P,S) is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding reflexive-yielding V159() () () set
({0,1},<%P,S%>) is total reflexive () ()
P is () () ()
S is () () ()
(P,S) is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () () set
({0,1},<%P,S%>) is () () () ()
P is () ()
S is () ()
(P,S) is ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding V159() () () () set
({0,1},<%P,S%>) is () () ()
P is total reflexive transitive () () () () () ()
S is total reflexive transitive () () () () () ()
(P,S) is total reflexive () () () ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding reflexive-yielding V159() () () () () () () set
({0,1},<%P,S%>) is total reflexive () () () () ()
the InternalRel of (P,S) is Relation-like the carrier of (P,S) -defined the carrier of (P,S) -valued total reflexive Element of bool [: the carrier of (P,S), the carrier of (P,S):]
the carrier of (P,S) is set
[: 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
the carrier of P is set
the carrier of S is set
the carrier of P \/ the carrier of S is set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive transitive 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 InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive transitive 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 InternalRel of P, the InternalRel of S) is Relation-like the carrier of P \/ the carrier of S -defined the carrier of P \/ the carrier of S -valued total reflexive 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 of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive symmetric Element of bool [: the carrier of P, the carrier of P:]
the of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric Element of bool [: the carrier of S, 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 Relation-like the carrier of P \/ the carrier of S -defined the carrier of P \/ the carrier of S -valued total reflexive symmetric 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 P, the carrier of S, the carrier of S, the InternalRel of P, the InternalRel 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 total reflexive transitive () () () () () ()
S is total reflexive transitive () () () () () ()
(P,S) is total reflexive () () () ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding reflexive-yielding V159() () () () () () () set
({0,1},<%P,S%>) is total reflexive () () () () ()
the carrier of P is set
the carrier of S is set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive transitive 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 InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive transitive 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 of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive symmetric Element of bool [: the carrier of P, the carrier of P:]
the of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric Element of bool [: the carrier of S, the carrier of S:]
( the carrier of P, the carrier of P, the carrier of S, the carrier of S, the InternalRel of P, the InternalRel of S) is Relation-like the carrier of P \/ the carrier of S -defined the carrier of P \/ the carrier of S -valued total reflexive 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 is set
[:( 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 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 total reflexive symmetric Element of bool [:( the carrier of P \/ the carrier of S),( the carrier of P \/ the carrier of S):]
the carrier of (P,S) is set
b1 is Element of the carrier of (P,S)
q1 is Element of the carrier of (P,S)
p1 is Element of the carrier of (P,S)
t is Element of the carrier of (P,S)
(( 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 InternalRel of P, the InternalRel 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 () ()
[b1,q1] is V15() set
{b1,q1} is non empty set
{b1} is non empty set
{{b1,q1},{b1}} is non empty set
e is Element of the carrier of P
f is Element of the carrier of P
[p1,b1] is V15() set
{p1,b1} is non empty set
{p1} is non empty set
{{p1,b1},{p1}} is non empty set
[t,q1] is V15() set
{t,q1} is non empty set
{t} is non empty set
{{t,q1},{t}} is non empty set
g is Element of the carrier of P
h is Element of the carrier of P
[g,h] is V15() set
{g,h} is non empty set
{g} is non empty set
{{g,h},{g}} is non empty set
e is Element of the carrier of S
f is Element of the carrier of S
[p1,b1] is V15() set
{p1,b1} is non empty set
{p1} is non empty set
{{p1,b1},{p1}} is non empty set
[t,q1] is V15() set
{t,q1} is non empty set
{t} is non empty set
{{t,q1},{t}} is non empty set
g is Element of the carrier of S
h is Element of the carrier of S
[g,h] is V15() set
{g,h} is non empty set
{g} is non empty set
{{g,h},{g}} is non empty set
P is total reflexive transitive () () () () () ()
S is total reflexive transitive () () () () () ()
(P,S) is total reflexive () () () ()
<%P,S%> is Relation-like K138() -defined {0,1} -defined Function-like total V25() V28() V35(2) 1-sorted-yielding RelStr-yielding reflexive-yielding V159() () () () () () () set
({0,1},<%P,S%>) is total reflexive () () () () ()
the carrier of (P,S) is set
the InternalRel of (P,S) is Relation-like the carrier of (P,S) -defined the carrier of (P,S) -valued total reflexive 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
( the carrier of (P,S), the carrier of (P,S), the InternalRel of (P,S)) is Element of bool ( the carrier of (P,S) \/ the carrier of (P,S))
the carrier of (P,S) \/ the carrier of (P,S) is set
bool ( the carrier of (P,S) \/ the carrier of (P,S)) is non empty set
proj1 the InternalRel of (P,S) is set
proj2 the InternalRel of (P,S) is set
(proj1 the InternalRel of (P,S)) \/ (proj2 the InternalRel of (P,S)) is set
S is set
{S} is non empty set
P is ()
the carrier of P is set
{S} \/ the carrier of P is non empty 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
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:]
[:{S},({S} \/ the carrier of P):] is Relation-like non empty set
[:{S},({S} \/ the carrier of P):] \/ the InternalRel of P is Relation-like non empty set
[:({S} \/ the carrier of P),{S}:] is Relation-like non empty set
[:({S} \/ the carrier of P),{S}:] \/ [:{S},({S} \/ the carrier of P):] is Relation-like non empty set
([:({S} \/ the carrier of P),{S}:] \/ [:{S},({S} \/ the carrier of P):]) \/ the of P is Relation-like non empty set
[:({S} \/ the carrier of P),({S} \/ the carrier of P):] is Relation-like non empty set
bool [:({S} \/ the carrier of P),({S} \/ the carrier of P):] is non empty set
q is Relation-like {S} \/ the carrier of P -defined {S} \/ the carrier of P -valued Element of bool [:({S} \/ the carrier of P),({S} \/ the carrier of P):]
q9 is Relation-like {S} \/ the carrier of P -defined {S} \/ the carrier of P -valued Element of bool [:({S} \/ the carrier of P),({S} \/ the carrier of P):]
(({S} \/ the carrier of P),q,q9) is () ()
the carrier of (({S} \/ the carrier of P),q,q9) is set
the InternalRel of (({S} \/ the carrier of P),q,q9) is Relation-like the carrier of (({S} \/ the carrier of P),q,q9) -defined the carrier of (({S} \/ the carrier of P),q,q9) -valued Element of bool [: the carrier of (({S} \/ the carrier of P),q,q9), the carrier of (({S} \/ the carrier of P),q,q9):]
[: the carrier of (({S} \/ the carrier of P),q,q9), the carrier of (({S} \/ the carrier of P),q,q9):] is Relation-like set
bool [: the carrier of (({S} \/ the carrier of P),q,q9), the carrier of (({S} \/ the carrier of P),q,q9):] is non empty set
[:{S}, the carrier of (({S} \/ the carrier of P),q,q9):] is Relation-like set
[:{S}, the carrier of (({S} \/ the carrier of P),q,q9):] \/ the InternalRel of P is Relation-like set
the of (({S} \/ the carrier of P),q,q9) is Relation-like the carrier of (({S} \/ the carrier of P),q,q9) -defined the carrier of (({S} \/ the carrier of P),q,q9) -valued Element of bool [: the carrier of (({S} \/ the carrier of P),q,q9), the carrier of (({S} \/ the carrier of P),q,q9):]
[: the carrier of (({S} \/ the carrier of P),q,q9),{S}:] is Relation-like set
[:{S}, the carrier of (({S} \/ the carrier of P),q,q9):] \/ [: the carrier of (({S} \/ the carrier of P),q,q9),{S}:] is Relation-like set
([:{S}, the carrier of (({S} \/ the carrier of P),q,q9):] \/ [: the carrier of (({S} \/ the carrier of P),q,q9),{S}:]) \/ the of P is Relation-like set
R is () ()
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
[:{S}, the carrier of R:] is Relation-like set
[:{S}, the carrier of R:] \/ the InternalRel of P is Relation-like set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R,{S}:] is Relation-like set
[:{S}, the carrier of R:] \/ [: the carrier of R,{S}:] is Relation-like set
([:{S}, the carrier of R:] \/ [: the carrier of R,{S}:]) \/ the of P is Relation-like set
p is () ()
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
[:{S}, the carrier of p:] is Relation-like set
[:{S}, the carrier of p:] \/ the InternalRel of P 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,{S}:] is Relation-like set
[:{S}, the carrier of p:] \/ [: the carrier of p,{S}:] is Relation-like set
([:{S}, the carrier of p:] \/ [: the carrier of p,{S}:]) \/ the of P is Relation-like set
P is ()
S is set
(P,S) is () ()
the carrier of (P,S) is set
{S} is non empty set
the carrier of P is set
{S} \/ the carrier of P is non empty set
P is ()
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
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:]
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
the InternalRel 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] 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):]
{S} is non empty set
{S} \/ the carrier of P is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ the InternalRel of P is Relation-like non empty set
[: the carrier of (P,S),{S}:] is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:] is Relation-like non empty set
([:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:]) \/ the of P is Relation-like non empty set
P is ()
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
the InternalRel 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
{S} is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty 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 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
[:{S}, the carrier of (P,S):] \/ the InternalRel of P is Relation-like non empty set
[S,p9] is V15() set
{S,p9} is non empty set
{{S,p9},{S}} is non empty set
[p,p9] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
P is ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
R is Element of the carrier of P
p is Element of the carrier of P
p9 is Element of the carrier of (P,S)
q is Element of the carrier of (P,S)
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} is non empty 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
the InternalRel 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
[p9,q] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
P is ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
R is Element of the carrier of P
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
the InternalRel 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
{S} is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty 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
[:{S}, the carrier of (P,S):] \/ the InternalRel of P is Relation-like non empty set
[p,p9] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
P is ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
R is Element of the carrier of (P,S)
{S} is non empty set
{S} \/ the carrier of P is non empty set
P is ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
R is Element of the carrier of P
p is Element of the carrier of P
p9 is Element of the carrier of (P,S)
q is Element of the carrier of (P,S)
the InternalRel 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
{S} is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty 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
[:{S}, the carrier of (P,S):] \/ the InternalRel of P is Relation-like non empty set
[p9,q] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty 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 is ()
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
{S} is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty set
[: the carrier of (P,S),{S}:] is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{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 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
([:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:]) \/ the of P is Relation-like non empty set
[: the carrier of (P,S),{S}:] \/ the of P is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ ([: the carrier of (P,S),{S}:] \/ the of P) is Relation-like non empty set
[S,p9] is V15() set
{S,p9} is non empty set
{{S,p9},{S}} is non empty set
[p9,S] is V15() set
{p9,S} is non empty set
{p9} is non empty set
{{p9,S},{p9}} is non empty set
[p,p9] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
[p9,p] is V15() Element of the carrier of [:(P,S),(P,S):]
{p9,p} is non empty set
{{p9,p},{p9}} is non empty set
P is ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
R is Element of the carrier of P
p is Element of the carrier of P
p9 is Element of the carrier of (P,S)
q is Element of the carrier of (P,S)
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} is 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 set
bool [: the carrier of P, the carrier of P:] 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
[p9,q] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
P is ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
R is Element of the carrier of P
p is Element of the carrier of P
p9 is Element of the carrier of (P,S)
q is Element of the carrier of (P,S)
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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
{S} is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty set
[: the carrier of (P,S),{S}:] is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{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 set
bool [: the carrier of P, the carrier of P:] is non empty set
([:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:]) \/ the of P is Relation-like non empty set
[p9,q] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty 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 is total reflexive ()
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
{S} is non empty set
the carrier of P is set
{S} \/ the carrier of P is non empty set
the InternalRel 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive 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
[:{S}, the carrier of (P,S):] \/ the InternalRel of P is Relation-like non empty set
p is set
[p,p] is V15() set
{p,p} is non empty set
{p} is non empty set
{{p,p},{p}} is non empty set
P is transitive ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the InternalRel 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) is non empty set
[: the carrier of (P,S), the carrier of (P,S):] is Relation-like non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
{S} is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty 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
[:{S}, the carrier of (P,S):] \/ the InternalRel of P is Relation-like non empty set
p is set
p9 is set
q is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
[p9,q] is V15() set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
[p,q] is V15() set
{p,q} is non empty set
{{p,q},{p}} is non empty set
[S,q] is V15() set
{S,q} is non empty set
{{S,q},{S}} is non empty set
q9 is Element of the carrier of (P,S)
a is Element of the carrier of (P,S)
b is Element of the carrier of (P,S)
a1 is Element of the carrier of P
b1 is Element of the carrier of P
p1 is Element of the carrier of P
P is () () ()
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
{S} is non empty set
the carrier of P is set
{S} \/ the carrier of P 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty set
[: the carrier of (P,S),{S}:] is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:] is Relation-like non empty set
the of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive 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
([:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:]) \/ the of P is Relation-like non empty set
[: the carrier of (P,S),{S}:] \/ the of P is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ ([: the carrier of (P,S),{S}:] \/ the of P) is Relation-like non empty set
p is set
[p,p] is V15() set
{p,p} is non empty set
{p} is non empty set
{{p,p},{p}} is non empty set
P is () ()
S is set
(P,S) is non empty () ()
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) is non empty set
[: the carrier of (P,S), the carrier of (P,S):] is Relation-like non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
{S} is non empty set
[:{S}, the carrier of (P,S):] is Relation-like non empty set
[: the carrier of (P,S),{S}:] is Relation-like non empty set
[:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:] is Relation-like 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 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
([:{S}, the carrier of (P,S):] \/ [: the carrier of (P,S),{S}:]) \/ the of P is Relation-like non empty set
p is set
p9 is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{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 () ()
the carrier of P is set
S is set
(P,S) is non empty () ()
the carrier of (P,S) is non empty set
p is Element of the carrier of (P,S)
q is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
q9 is Element of the carrier of (P,S)
a is Element of the carrier of P
b is Element of the carrier of P
a1 is Element of the carrier of P
b1 is Element of the carrier of P
P is total reflexive transitive () () () () () ()
the carrier of P is set
S is set
(P,S) is non empty total reflexive non void () () () () ()
P is ()
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
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 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 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:] \ the of P is Relation-like set
S 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 InternalRel of P ~),S) is () ()
the carrier of ( the carrier of P,( the InternalRel of P ~),S) is set
the InternalRel of ( the carrier of P,( the InternalRel of P ~),S) is Relation-like the carrier of ( the carrier of P,( the InternalRel of P ~),S) -defined the carrier of ( the carrier of P,( the InternalRel of P ~),S) -valued Element of bool [: the carrier of ( the carrier of P,( the InternalRel of P ~),S), the carrier of ( the carrier of P,( the InternalRel of P ~),S):]
[: the carrier of ( the carrier of P,( the InternalRel of P ~),S), the carrier of ( the carrier of P,( the InternalRel of P ~),S):] is Relation-like set
bool [: the carrier of ( the carrier of P,( the InternalRel of P ~),S), the carrier of ( the carrier of P,( the InternalRel of P ~),S):] is non empty set
the of ( the carrier of P,( the InternalRel of P ~),S) is Relation-like the carrier of ( the carrier of P,( the InternalRel of P ~),S) -defined the carrier of ( the carrier of P,( the InternalRel of P ~),S) -valued Element of bool [: the carrier of ( the carrier of P,( the InternalRel of P ~),S), the carrier of ( the carrier of P,( the InternalRel of P ~),S):]
S is () ()
the carrier of S is set
the InternalRel 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 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:]
R is () ()
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
P is non empty ()
(P) is () ()
the carrier of (P) is set
the carrier of P is non empty set
P is ()
the carrier of P is set
(P) is () ()
the carrier of (P) is set
S is Element of the carrier of P
R is Element of the carrier of P
p9 is Element of the carrier of (P)
q is Element of the carrier of (P)
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
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
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:]
[S,R] is V15() set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} 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
[q,p9] is V15() set
{q,p9} is non empty set
{q} is non empty set
{{q,p9},{q}} is non empty set
[S,R] is V15() set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
P is ()
the carrier of P is set
(P) is () ()
the carrier of (P) is set
S is Element of the carrier of P
R is Element of the carrier of P
p9 is Element of the carrier of (P)
q is Element of the carrier of (P)
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 carrier of P:] 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:]
bool [: the carrier of P, the carrier of P:] is 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:] \ the of P is Relation-like set
[S,R] is V15() set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
[p9,q] is V15() set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
P is non empty ()
the carrier of P is non empty set
(P) is non empty () ()
the carrier of (P) is non empty set
S is Element of the carrier of P
R is Element of the carrier of P
p9 is Element of the carrier of (P)
q is Element of the carrier of (P)
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 carrier of P, the carrier of P:] 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:]
bool [: the carrier of P, the carrier of P:] is 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:] \ the of P is Relation-like set
[p9,q] is V15() Element of the carrier of [:(P),(P):]
[:(P),(P):] is non empty strict RelStr
the carrier of [:(P),(P):] is non empty set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
[S,R] is V15() Element of the carrier of [:P,P:]
[:P,P:] is non empty strict RelStr
the carrier of [:P,P:] is non empty set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
P is total reflexive ()
(P) is () ()
the carrier of (P) is set
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
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive 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 InternalRel of P ~ is Relation-like the carrier of P -defined the carrier of P -valued reflexive Element of bool [: the carrier of P, the carrier of P:]
P is transitive ()
(P) is () ()
the carrier of (P) is set
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
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
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:]
P is () () ()
(P) is () ()
the carrier of (P) is set
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 carrier of P:] is Relation-like set
the of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive Element of bool [: the carrier of P, the carrier of P:]
bool [: the carrier of P, the carrier of P:] is 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:] \ the of P is Relation-like 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
P is () ()
(P) is () ()
the carrier of (P) is set
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 carrier of P:] is Relation-like set
the of P is Relation-like the carrier of P -defined the carrier of P -valued irreflexive Element of bool [: the carrier of P, the carrier of P:]
bool [: the carrier of P, the carrier of P:] is 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:] \ the of P is Relation-like 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
P is () ()
(P) is () ()
the carrier of (P) is set
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 carrier of P:] is Relation-like 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:]
bool [: the carrier of P, the carrier of P:] is 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:] \ the of P is Relation-like 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
P is () ()
(P) is () ()
the carrier of (P) is set
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
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
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 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 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 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:] \ the of P is Relation-like set
R is Element of the carrier of (P)
p9 is Element of the carrier of (P)
p is Element of the carrier of (P)
q is Element of the carrier of (P)
[R,p9] is V15() set
{R,p9} is non empty set
{R} is non empty set
{{R,p9},{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
[q,p9] is V15() set
{q,p9} is non empty set
{q} is non empty set
{{q,p9},{q}} is non empty set
b is Element of the carrier of P
a1 is Element of the carrier of P
[b,a1] is V15() set
{b,a1} is non empty set
{b} is non empty set
{{b,a1},{b}} is non empty set
q9 is Element of the carrier of P
[b,q9] is V15() set
{b,q9} is non empty set
{{b,q9},{b}} is non empty set
a is Element of the carrier of P
[a1,a] is V15() set
{a1,a} is non empty set
{a1} is non empty set
{{a1,a},{a1}} is non empty set
[q9,a] is V15() set
{q9,a} is non empty set
{q9} is non empty set
{{q9,a},{q9}} is non empty set
[p,q] is V15() set
{p,q} is non empty set
{{p,q},{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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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 ()
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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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 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 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 non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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 ()
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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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)
p is Element of the carrier of (P,S)
p9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of S
[p9,q9] is V15() set
{p9,q9} is non empty set
{p9} is non empty set
{{p9,q9},{p9}} is non empty set
a is Element of the carrier of S
[q,a] is V15() set
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} 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
b1 is set
p1 is set
[b1,p1] is V15() set
{b1,p1} is non empty set
{b1} is non empty set
{{b1,p1},{b1}} is non empty set
[b,b1] is V15() set
{b,b1} is non empty set
{{b,b1},{b}} is non empty set
[a1,p1] is V15() set
{a1,p1} is non empty set
{a1} is non empty set
{{a1,p1},{a1}} is non empty set
[p9,q] is V15() set
{p9,q} is non empty set
{{p9,q},{p9}} is non empty set
[q9,a] is V15() set
{q9,a} is non empty set
{q9} is non empty set
{{q9,a},{q9}} is non empty set
[p9,q] is V15() set
{p9,q} is non empty set
{{p9,q},{p9}} is non empty set
[q9,a] is V15() set
{q9,a} is non empty set
{q9} is non empty set
{{q9,a},{q9}} is non empty set
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} is non empty set
the InternalRel 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 ()
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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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)
p is Element of the carrier of (P,S)
p9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of S
[p9,q9] is V15() set
{p9,q9} is non empty set
{p9} is non empty set
{{p9,q9},{p9}} is non empty set
a is Element of the carrier of S
[q,a] is V15() set
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} 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
b1 is set
p1 is set
[b1,p1] is V15() set
{b1,p1} is non empty set
{b1} is non empty set
{{b1,p1},{b1}} is non empty set
[b,b1] is V15() set
{b,b1} is non empty set
{{b,b1},{b}} is non empty set
[a1,p1] is V15() set
{a1,p1} is non empty set
{a1} is non empty set
{{a1,p1},{a1}} is non empty set
P is non empty ()
S is non empty ()
(P,S) is non empty () ()
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 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 non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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 non empty set
R is Element of the carrier of (P,S)
p is Element of the carrier of (P,S)
p9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of S
[p9,q9] is V15() Element of the carrier of [:P,S:]
[:P,S:] is non empty strict RelStr
the carrier of [:P,S:] is non empty set
{p9,q9} is non empty set
{p9} is non empty set
{{p9,q9},{p9}} is non empty set
a is Element of the carrier of S
[q,a] is V15() Element of the carrier of [:P,S:]
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
[p9,q] is V15() Element of the carrier of [:P,P:]
[:P,P:] is non empty strict RelStr
the carrier of [:P,P:] is non empty set
{p9,q} is non empty set
{{p9,q},{p9}} is non empty set
[q9,a] is V15() Element of the carrier of [:S,S:]
[:S,S:] is non empty strict RelStr
the carrier of [:S,S:] is non empty set
{q9,a} is non empty set
{q9} is non empty set
{{q9,a},{q9}} is non empty set
[R,p] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
P is total reflexive ()
S is total reflexive ()
(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 InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive 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 InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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
the InternalRel 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
RelStr(# the carrier of (P,S), the InternalRel of (P,S) #) is strict RelStr
[:P,S:] is strict total reflexive RelStr
P is transitive ()
S is transitive ()
(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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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
the InternalRel 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
RelStr(# the carrier of (P,S), the InternalRel of (P,S) #) is strict RelStr
[:P,S:] is strict transitive RelStr
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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive Element of bool [: the carrier of S, 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 Relation-like [: the carrier of P, the carrier of S:] -defined [: the carrier of P, the carrier of S:] -valued reflexive 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 InternalRel of P, the InternalRel 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
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
( the carrier of (P,S), the of (P,S)) is () ()
(P,S) is () () ()
([: 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 () () ()
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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive Element of bool [: the carrier of P, the carrier of P:]
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 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 reflexive 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 InternalRel of P, the InternalRel 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
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
( the carrier of (P,S), the of (P,S)) is () ()
(P,S) is () () ()
([: 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 () ()
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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 of S is Relation-like the carrier of S -defined the carrier of S -valued symmetric Element of bool [: the carrier of S, 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 Relation-like [: the carrier of P, the carrier of S:] -defined [: the carrier of P, the carrier of S:] -valued symmetric 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 InternalRel of P, the InternalRel 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
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
( the carrier of (P,S), the of (P,S)) is () ()
(P,S) is () ()
([: 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 () ()
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 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
the InternalRel 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 InternalRel of P, the InternalRel 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 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 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 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 InternalRel of P, the InternalRel 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 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) is set
[: 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
q9 is Element of the carrier of (P,S)
b is Element of the carrier of (P,S)
a is Element of the carrier of (P,S)
a1 is Element of the carrier of (P,S)
[q9,b] is V15() set
{q9,b} is non empty set
{q9} is non empty set
{{q9,b},{q9}} is non empty set
b1 is set
p1 is set
[b1,p1] is V15() set
{b1,p1} is non empty set
{b1} is non empty set
{{b1,p1},{b1}} is non empty set
q1 is set
t is set
[q1,t] is V15() set
{q1,t} is non empty set
{q1} is non empty set
{{q1,t},{q1}} is non empty set
[b1,q1] is V15() set
{b1,q1} is non empty set
{{b1,q1},{b1}} is non empty set
[p1,t] is V15() set
{p1,t} is non empty set
{p1} is non empty set
{{p1,t},{p1}} is non empty set
[a,q9] is V15() set
{a,q9} is non empty set
{a} is non empty set
{{a,q9},{a}} is non empty set
the InternalRel 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):]
e is set
f is set
[e,f] is V15() set
{e,f} is non empty set
{e} is non empty set
{{e,f},{e}} is non empty set
[a1,b] is V15() set
{a1,b} is non empty set
{a1} is non empty set
{{a1,b},{a1}} is non empty set
g is set
h is set
[g,h] is V15() set
{g,h} is non empty set
{g} is non empty set
{{g,h},{g}} is non empty set
P is non empty () ()
the carrier of P is non empty set
Q is non empty () ()
the carrier of Q is non empty set
(P,Q) is ()
[: the carrier of P, the carrier of Q:] 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 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, the carrier of Q:] is Relation-like non empty set
bool [: the carrier of Q, the carrier of Q:] is non empty set
( the carrier of P, the carrier of P, the carrier of Q, the carrier of Q, the of P, the of Q) is Relation-like [: the carrier of P, the carrier of Q:] -defined [: the carrier of P, the carrier of Q:] -valued Element of bool [:[: the carrier of P, the carrier of Q:],[: the carrier of P, the carrier of Q:]:]
[:[: the carrier of P, the carrier of Q:],[: the carrier of P, the carrier of Q:]:] is Relation-like non empty set
bool [:[: the carrier of P, the carrier of Q:],[: the carrier of P, the carrier of Q:]:] is non empty set
([: the carrier of P, the carrier of Q:],( the carrier of P, the carrier of P, the carrier of Q, the carrier of Q, the of P, the of Q)) is () ()
a is Element of the carrier of P
b is Element of the carrier of Q
(P,Q,a,b) is V15() Element of the carrier of (P,Q)
the carrier of (P,Q) is set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
c is Element of the carrier of P
d is Element of the carrier of Q
(P,Q,c,d) is V15() Element of the carrier of (P,Q)
{c,d} is non empty set
{c} is non empty set
{{c,d},{c}} is non empty set
(P,Q) is non empty () ()
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 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 InternalRel of P, the InternalRel of Q"] is Relation-like [: the carrier of P, the carrier of Q:] -defined [: the carrier of P, the carrier of Q:] -valued Element of bool [:[: the carrier of P, the carrier of Q:],[: the carrier of P, the carrier of Q:]:]
([: the carrier of P, the carrier of Q:],[" the InternalRel of P, the InternalRel of Q"],( the carrier of P, the carrier of P, the carrier of Q, the carrier of Q, the of P, the of Q)) is () ()
the carrier of (P,Q) is non empty set
the InternalRel of (P,Q) is Relation-like the carrier of (P,Q) -defined the carrier of (P,Q) -valued Element of bool [: the carrier of (P,Q), the carrier of (P,Q):]
[: the carrier of (P,Q), the carrier of (P,Q):] is Relation-like non empty set
bool [: the carrier of (P,Q), the carrier of (P,Q):] is non empty set
RelStr(# the carrier of (P,Q), the InternalRel of (P,Q) #) is non empty strict RelStr
[:P,Q:] is non empty strict RelStr
e is Element of the carrier of P
f is Element of the carrier of Q
[e,f] is V15() Element of the carrier of [:P,Q:]
the carrier of [:P,Q:] is non empty set
{e,f} is non empty set
{e} is non empty set
{{e,f},{e}} is non empty set
[a,b] is V15() Element of the carrier of [:P,Q:]
g is Element of the carrier of P
h is Element of the carrier of Q
[g,h] is V15() Element of the carrier of [:P,Q:]
{g,h} is non empty set
{g} is non empty set
{{g,h},{g}} is non empty set
[c,d] is V15() Element of the carrier of [:P,Q:]
[e,g] is V15() Element of the carrier of [:P,P:]
[:P,P:] is non empty strict RelStr
the carrier of [:P,P:] is non empty set
{e,g} is non empty set
{{e,g},{e}} is non empty set
[f,h] is V15() Element of the carrier of [:Q,Q:]
[:Q,Q:] is non empty strict RelStr
the carrier of [:Q,Q:] is non empty set
{f,h} is non empty set
{f} is non empty set
{{f,h},{f}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
P is ()
(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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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 ()
S is ()
(P,S) is ()
(P) 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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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 non empty ()
S is non empty ()
(P,S) is () ()
(P) is non empty () ()
((P),S) is non empty () ()
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 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 non empty set
bool [: the carrier of (P), the carrier of (P):] is non empty set
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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 ()
S is ()
(P,S) is () ()
(P) 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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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
the carrier of P is set
R is Element of the carrier of (P,S)
p is Element of the carrier of (P,S)
p9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of S
[p9,q9] is V15() set
{p9,q9} is non empty set
{p9} is non empty set
{{p9,q9},{p9}} is non empty set
a is Element of the carrier of S
[q,a] is V15() set
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} is non empty set
b1 is set
p1 is set
[b1,p1] is V15() set
{b1,p1} is non empty set
{b1} is non empty set
{{b1,p1},{b1}} is non empty set
q1 is set
t is set
[q1,t] is V15() set
{q1,t} is non empty set
{q1} is non empty set
{{q1,t},{q1}} is non empty set
[b1,q1] is V15() set
{b1,q1} is non empty set
{{b1,q1},{b1}} is non empty set
[p1,t] is V15() set
{p1,t} is non empty set
{p1} is non empty set
{{p1,t},{p1}} is non empty set
b is Element of the carrier of (P)
a1 is Element of the carrier of (P)
[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 Element of the carrier of (P)
a1 is Element of the carrier of (P)
[b,a1] is V15() set
{b,a1} is non empty set
{b} is non empty set
{{b,a1},{b}} is non empty set
[q9,a] is V15() set
{q9,a} is non empty set
{q9} is non empty set
{{q9,a},{q9}} is non empty set
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} is non empty set
the InternalRel 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 ()
S is ()
(P,S) is () ()
(P) 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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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
the carrier of P is set
R is Element of the carrier of (P,S)
p is Element of the carrier of (P,S)
p9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of S
[p9,q9] is V15() set
{p9,q9} is non empty set
{p9} is non empty set
{{p9,q9},{p9}} is non empty set
a is Element of the carrier of S
[q,a] is V15() set
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
[R,p] is V15() set
{R,p} is non empty set
{R} is non empty set
{{R,p},{R}} 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
b1 is set
p1 is set
[b1,p1] is V15() set
{b1,p1} is non empty set
{b1} is non empty set
{{b1,p1},{b1}} is non empty set
q1 is set
t is set
[q1,t] is V15() set
{q1,t} is non empty set
{q1} is non empty set
{{q1,t},{q1}} is non empty set
[b1,q1] is V15() set
{b1,q1} is non empty set
{{b1,q1},{b1}} is non empty set
[p1,t] is V15() set
{p1,t} is non empty set
{p1} is non empty set
{{p1,t},{p1}} is non empty set
b is Element of the carrier of (P)
a1 is Element of the carrier of (P)
P is non empty ()
S is non empty ()
(P,S) is non empty () ()
(P) is non empty () ()
((P),S) is non empty () ()
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 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 non empty set
bool [: the carrier of (P), the carrier of (P):] is non empty set
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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 non empty set
the carrier of P is non empty set
R is Element of the carrier of (P,S)
p is Element of the carrier of (P,S)
p9 is Element of the carrier of P
q is Element of the carrier of P
q9 is Element of the carrier of S
[p9,q9] is V15() Element of the carrier of [:P,S:]
[:P,S:] is non empty strict RelStr
the carrier of [:P,S:] is non empty set
{p9,q9} is non empty set
{p9} is non empty set
{{p9,q9},{p9}} is non empty set
a is Element of the carrier of S
[q,a] is V15() Element of the carrier of [:P,S:]
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
the carrier of ((P),S) is non empty set
b is Element of the carrier of (P)
[b,q9] is V15() Element of the carrier of [:(P),S:]
[:(P),S:] is non empty strict RelStr
the carrier of [:(P),S:] is non empty set
{b,q9} is non empty set
{b} is non empty set
{{b,q9},{b}} is non empty set
a1 is Element of the carrier of (P)
[a1,a] is V15() Element of the carrier of [:(P),S:]
{a1,a} is non empty set
{a1} is non empty set
{{a1,a},{a1}} is non empty set
b1 is Element of the carrier of ((P),S)
p1 is Element of the carrier of ((P),S)
P is total reflexive ()
S is total reflexive ()
(P,S) is () ()
(P) is total reflexive () ()
((P),S) is total reflexive () ()
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 InternalRel of (P) is Relation-like the carrier of (P) -defined the carrier of (P) -valued total reflexive 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 InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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 transitive ()
S is transitive ()
(P,S) is () ()
(P) is transitive () ()
((P),S) is transitive () ()
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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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 ()
S is () () ()
(P,S) is () ()
(P) 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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive Element of bool [: the carrier of S, 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 Relation-like [: the carrier of (P), the carrier of S:] -defined [: the carrier of (P), the carrier of S:] -valued reflexive 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 InternalRel of (P), the InternalRel 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 () ()
S is ()
(P,S) is () ()
(P) 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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 of (P) is Relation-like the carrier of (P) -defined the carrier of (P) -valued total reflexive Element of bool [: the carrier of (P), the carrier of (P):]
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 (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 reflexive 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 InternalRel of (P), the InternalRel 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 () ()
S is () ()
(P,S) is () ()
(P) 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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 of S is Relation-like the carrier of S -defined the carrier of S -valued symmetric Element of bool [: the carrier of S, 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 Relation-like [: the carrier of (P), the carrier of S:] -defined [: the carrier of (P), the carrier of S:] -valued symmetric 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 InternalRel of (P), the InternalRel 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 () ()
S is () ()
(P,S) is () ()
(P) 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 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
the InternalRel 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 InternalRel of (P), the InternalRel 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 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 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 (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 InternalRel of (P), the InternalRel 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 total reflexive transitive () () () () () ()
S is total reflexive transitive () () () () () ()
(P,S) is total reflexive transitive () () () () () () ()
(P) is total reflexive transitive () () () () () ()
((P),S) is total reflexive transitive () () () () () () ()
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 InternalRel of (P) is Relation-like the carrier of (P) -defined the carrier of (P) -valued total reflexive transitive 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 InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive transitive 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 InternalRel of (P), the InternalRel 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 of (P) is Relation-like the carrier of (P) -defined the carrier of (P) -valued irreflexive symmetric Element of bool [: the carrier of (P), the carrier of (P):]
the of S is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric Element of bool [: the carrier of S, 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 Relation-like [: the carrier of (P), the carrier of S:] -defined [: the carrier of (P), the carrier of S:] -valued reflexive symmetric 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 InternalRel of (P), the InternalRel 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
bool the carrier of P is non empty set
P is ()
the carrier of P is set
bool the carrier of P is non empty set
S is Element of bool the carrier of P
R is Element of the carrier of P
p is Element of the carrier of P
P is ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
P is ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is Element of bool (bool the carrier of P)
R is Element of bool the carrier of P
{} P is Relation-like non-empty empty-yielding empty reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive () () () (P) Element of bool the carrier of P
S is set
P is RelStr
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 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
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
R is Relation-like S -defined S -valued Element of bool [:S,S:]
p is set
p9 is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
q is 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
R is Relation-like S -defined S -valued Element of bool [:S,S:]
p is Relation-like S -defined S -valued Element of bool [:S,S:]
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
q9 is 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
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
q9 is 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
S 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
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
R is Relation-like S -defined S -valued Element of bool [:S,S:]
p is set
p9 is set
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} 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
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
R is Relation-like S -defined S -valued Element of bool [:S,S:]
p is Relation-like S -defined S -valued Element of bool [:S,S:]
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
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
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
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
P is RelStr
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is Element of bool (bool the carrier of P)
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] 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
p9 is Element of the carrier of P
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
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
q9 is Element of the carrier of P
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
p9 is set
q is Element of the carrier of P
q9 is Element of the carrier of P
[p9,q9] is V15() set
{p9,q9} is non empty set
{p9} is non empty set
{{p9,q9},{p9}} is non empty set
P is ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is Element of bool (bool the carrier of P)
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] 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
p9 is Element of the carrier of P
q is Element of the carrier of P
[p9,q] is V15() set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is 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 set
bool [: the carrier of P, the carrier of P:] is 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 set
bool [: the carrier of P, the carrier of P:] 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
q9 is Element of the carrier of P
a is Element of the carrier of P
S is set
P is ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
P is ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
P is ()
S is non empty set
(P,S) is ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like non empty set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
P is ()
the carrier of P is set
S is set
(P,S) is ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
the carrier of (P,S) is set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
[p,p9] is V15() set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
the InternalRel 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
q is Element of the carrier of P
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
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
a is Element of the carrier of P
[q,a] is V15() set
{q,a} is non empty set
{{q,a},{q}} is non empty set
P is ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is non empty Element of bool (bool the carrier of P)
(P,S) is non empty ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like non empty set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
the carrier of (P,S) is non empty set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
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
q is set
q9 is Element of the carrier of P
a is Element of the carrier of P
[q,a] is V15() set
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
[p,p9] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} is non empty set
the InternalRel 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
P is ()
the carrier of P is set
S is set
(P,S) is ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
the carrier of (P,S) is set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
[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,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
q is Element of the carrier of P
q9 is Element of the carrier of P
[q,q9] is V15() set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is 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 set
bool [: the carrier of P, the carrier of P:] is non empty set
P is ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is non empty Element of bool (bool the carrier of P)
(P,S) is non empty ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like non empty set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
the carrier of (P,S) is non empty set
p is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
q is set
q9 is set
a is Element of the carrier of P
b is Element of the carrier of P
[q,q9] is V15() set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is 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 set
bool [: the carrier of P, the carrier of P:] is non empty set
[p,p9] is V15() Element of the carrier of [:(P,S),(P,S):]
[:(P,S),(P,S):] is non empty strict RelStr
the carrier of [:(P,S),(P,S):] is non empty set
{p,p9} is non empty set
{p} is non empty set
{{p,p9},{p}} 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 non empty set
bool [: the carrier of (P,S), the carrier of (P,S):] is non empty set
P is ()
S is set
(P,S) is ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
P is total reflexive ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is Element of bool (bool the carrier of P)
(P,S) is () ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
p is set
the carrier of (P,S) is set
[p,p] is V15() set
{p,p} is non empty set
{p} is non empty set
{{p,p},{p}} is non empty set
the InternalRel 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
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive 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 is set
[p9,p9] is V15() set
{p9,p9} is non empty set
{p9} is non empty set
{{p9,p9},{p9}} is non empty set
( the carrier of P, the carrier of P, the InternalRel 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 InternalRel of P is set
proj2 the InternalRel of P is set
(proj1 the InternalRel of P) \/ (proj2 the InternalRel of P) is set
P is transitive ()
S is set
(P,S) is () ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
the InternalRel 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) is set
[: 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
p9 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
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 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
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
[b,a1] is V15() set
{b,a1} is non empty set
{b} is non empty set
{{b,a1},{b}} is non empty set
[a,a1] is V15() set
{a,a1} is non empty set
{{a,a1},{a}} is non empty set
P is () () ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is (P) Element of bool (bool the carrier of P)
(P,S) is () ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
R is set
the carrier of (P,S) 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 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 Element of bool the carrier of P
p9 is set
q is set
q9 is Element of the carrier of P
a is Element of the carrier of P
[p9,q] is V15() set
{p9,q} is non empty set
{p9} is non empty set
{{p9,q},{p9}} is non empty set
the of P is Relation-like the carrier of P -defined the carrier of P -valued total reflexive 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 carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is Element of bool (bool the carrier of P)
(P,S) is () ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
p is set
the carrier of (P,S) is set
p9 is set
[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,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
[p9,p] is V15() set
{p9,p} is non empty set
{p9} is non empty set
{{p9,p},{p9}} is non empty set
q is set
q9 is set
[q9,q] is V15() set
{q9,q} is non empty set
{q9} is non empty set
{{q9,q},{q9}} 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
b is Element of the carrier of P
a is Element of the carrier of P
[q,q9] is V15() set
{q,q9} is non empty set
{q} is non empty set
{{q,q9},{q}} is non empty set
P is () ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
S is Element of bool (bool the carrier of P)
(P,S) is () ()
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is non empty set
(P,S) is Relation-like S -defined S -valued Element of bool [:S,S:]
(S,(P,S),(P,S)) is () ()
the carrier of (P,S) is set
p is Element of the carrier of (P,S)
q is Element of the carrier of (P,S)
p9 is Element of the carrier of (P,S)
q9 is Element of the carrier of (P,S)
[p9,p] is V15() set
{p9,p} is non empty set
{p9} is non empty set
{{p9,p},{p9}} is non empty set
the InternalRel 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
[q9,q] is V15() set
{q9,q} is non empty set
{q9} is non empty set
{{q9,q},{q9}} is non empty set
a is set
b is set
a1 is Element of the carrier of P
p1 is Element of the carrier of P
b1 is Element of the carrier of P
q1 is Element of the carrier of P
[a,b] is V15() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is 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 set
bool [: the carrier of P, the carrier of P:] is non empty set
[p9,q9] is V15() set
{p9,q9} is non empty set
{{p9,q9},{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):]
P is ()
the carrier of P is set
bool the carrier of P is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
P is ()
the carrier of P is set
bool the carrier of P is non empty set
{} P is Relation-like non-empty empty-yielding empty reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive strongly_connected () () () (P) Element of bool the carrier of P
P is ()
(P) is set
the carrier of P is set
bool the carrier of P is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
S is set
R is Element of bool the carrier of P
P is ()
(P) is set
the carrier of P is set
bool the carrier of P is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
{} P is Relation-like non-empty empty-yielding empty reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive strongly_connected () () () (P) Element of bool the carrier of P
P is ()
(P) is non empty set
the carrier of P is set
bool the carrier of P is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
bool (bool the carrier of P) is non empty set
S is set
P is ()
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
(P) is non empty Element of bool (bool the carrier of P)
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
S is Element of bool the carrier of P
S is Element of bool (bool the carrier of P)
P is ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is ()
(P) is ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is ()
(P) is () ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is total reflexive ()
(P) is non empty () ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty total reflexive non void () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is transitive ()
(P) is non empty () ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty transitive () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is () () ()
(P) is non empty () ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty () () () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is () ()
(P) is non empty () ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty () () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is () ()
(P) is non empty () ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty () () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()
P is total reflexive transitive () () () () () ()
(P) is non empty total reflexive transitive non void () () () () () () ()
(P) is non empty (P) Element of bool (bool the carrier of P)
the carrier of P is set
bool the carrier of P is non empty set
bool (bool the carrier of P) is non empty set
{ b₁ where b₁ is Element of bool the carrier of P : b₁ is (P) } is set
(P,(P)) is non empty total reflexive transitive non void () () () () () () ()
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
[:(P),(P):] is Relation-like non empty set
bool [:(P),(P):] is non empty set
(P,(P)) is Relation-like (P) -defined (P) -valued Element of bool [:(P),(P):]
((P),(P,(P)),(P,(P))) is () ()