:: YELLOW_3 semantic presentation

K219() is Element of bool K215()
K215() is set
bool K215() is non empty set
K113() is set
bool K113() is non empty set
{} is empty Relation-like non-empty empty-yielding set
1 is non empty set
{{},1} is non empty set
bool K219() is non empty set
F₁() is non empty set
{ F₂(b₁,b₂) where b₁, b₂ is Element of F₁() : P₁[b₁,b₂] } is set
bool F₁() is non empty set
f is set
f is Element of F₁()
c₃ is Element of F₁()
F₂(f,c₃) is set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is empty Relation-like non-empty empty-yielding strongly_connected directed filtered Element of bool the carrier of f
downarrow f is Element of bool the carrier of f
c₃ is set
y1 is Element of the carrier of f
C2 is Element of the carrier of f
uparrow f is Element of bool the carrier of f
c₃ is set
y1 is Element of the carrier of f
C2 is Element of the carrier of f
f is set
f is set
[:f,f:] is Relation-like set
bool [:f,f:] is non empty set
c₃ is Relation-like f -defined f -valued Element of bool [:f,f:]
proj1 c₃ is set
proj2 c₃ is set
[:(proj1 c₃),(proj2 c₃):] is Relation-like set
y1 is set
C2 is set
q is set
[C2,q] is V1() set
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
f is set
f is set
c₃ is set
[f,c₃] is V1() set
{f,c₃} is non empty set
{f} is non empty set
{{f,c₃},{f}} is non empty set
y1 is set
C2 is set
[y1,C2] is V1() set
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
[[f,c₃],[y1,C2]] is V1() set
{[f,c₃],[y1,C2]} is non empty Relation-like set
{[f,c₃]} is non empty Relation-like set
{{[f,c₃],[y1,C2]},{[f,c₃]}} is non empty set
f `1 is set
(f `1) `1 is set
(f `1) `2 is set
f `2 is set
(f `2) `1 is set
(f `2) `2 is set
f is non empty transitive antisymmetric with_infima RelStr
the carrier of f is non empty set
f is Element of the carrier of f
y1 is Element of the carrier of f
c₃ is Element of the carrier of f
C2 is Element of the carrier of f
f "/\" c₃ is Element of the carrier of f
y1 "/\" C2 is Element of the carrier of f
{f,c₃} is non empty Element of bool the carrier of f
bool the carrier of f is non empty set
q is Element of the carrier of f
f is non empty transitive antisymmetric with_suprema RelStr
the carrier of f is non empty set
f is Element of the carrier of f
y1 is Element of the carrier of f
c₃ is Element of the carrier of f
C2 is Element of the carrier of f
f "\/" c₃ is Element of the carrier of f
y1 "\/" C2 is Element of the carrier of f
{y1,C2} is non empty Element of bool the carrier of f
bool the carrier of f is non empty set
q is Element of the carrier of f
f is non empty V55() reflexive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() up-complete /\-complete RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is Element of bool the carrier of f
"\/" (f,f) is Element of the carrier of f
c₃ is Element of the carrier of f
("\/" (f,f)) "/\" c₃ is Element of the carrier of f
f is non empty V55() reflexive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() up-complete /\-complete RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is Element of bool the carrier of f
"/\" (f,f) is Element of the carrier of f
c₃ is Element of the carrier of f
("/\" (f,f)) "\/" c₃ is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is Element of bool the carrier of f
c₃ is Element of bool the carrier of f
downarrow f is Element of bool the carrier of f
downarrow c₃ is Element of bool the carrier of f
y1 is set
C2 is Element of the carrier of f
q is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is Element of bool the carrier of f
c₃ is Element of bool the carrier of f
uparrow f is Element of bool the carrier of f
uparrow c₃ is Element of bool the carrier of f
y1 is set
C2 is Element of the carrier of f
q is Element of the carrier of f
f is non empty V55() reflexive transitive antisymmetric with_infima RelStr
the carrier of f is non empty set
f is non empty V55() reflexive transitive antisymmetric with_infima RelStr
the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
c₃ is Relation-like the carrier of f -defined the carrier of f -valued V12() V18( the carrier of f, the carrier of f) Element of bool [: the carrier of f, the carrier of f:]
y1 is Element of the carrier of f
C2 is Element of the carrier of f
{y1,C2} is non empty Element of bool the carrier of f
bool the carrier of f is non empty set
y1 "/\" C2 is Element of the carrier of f
c₃ . (y1 "/\" C2) is Element of the carrier of f
c₃ . y1 is Element of the carrier of f
c₃ . C2 is Element of the carrier of f
(c₃ . y1) "/\" (c₃ . C2) is Element of the carrier of f
dom c₃ is Element of bool the carrier of f
"/\" ({y1,C2},f) is Element of the carrier of f
c₃ . ("/\" ({y1,C2},f)) is Element of the carrier of f
c₃ .: {y1,C2} is Element of bool the carrier of f
bool the carrier of f is non empty set
"/\" ((c₃ .: {y1,C2}),f) is Element of the carrier of f
{(c₃ . y1),(c₃ . C2)} is non empty Element of bool the carrier of f
"/\" ({(c₃ . y1),(c₃ . C2)},f) is Element of the carrier of f
f is non empty V55() reflexive transitive antisymmetric with_suprema RelStr
the carrier of f is non empty set
f is non empty V55() reflexive transitive antisymmetric with_suprema RelStr
the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
c₃ is Relation-like the carrier of f -defined the carrier of f -valued V12() V18( the carrier of f, the carrier of f) Element of bool [: the carrier of f, the carrier of f:]
y1 is Element of the carrier of f
C2 is Element of the carrier of f
{y1,C2} is non empty Element of bool the carrier of f
bool the carrier of f is non empty set
y1 "\/" C2 is Element of the carrier of f
c₃ . (y1 "\/" C2) is Element of the carrier of f
c₃ . y1 is Element of the carrier of f
c₃ . C2 is Element of the carrier of f
(c₃ . y1) "\/" (c₃ . C2) is Element of the carrier of f
dom c₃ is Element of bool the carrier of f
"\/" ({y1,C2},f) is Element of the carrier of f
c₃ . ("\/" ({y1,C2},f)) is Element of the carrier of f
c₃ .: {y1,C2} is Element of bool the carrier of f
bool the carrier of f is non empty set
"\/" ((c₃ .: {y1,C2}),f) is Element of the carrier of f
{(c₃ . y1),(c₃ . C2)} is non empty Element of bool the carrier of f
"\/" ({(c₃ . y1),(c₃ . C2)},f) is Element of the carrier of f
F₁() is non empty antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() RelStr
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
{ b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"/\" ((union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ),F₁()) is Element of the carrier of F₁()
{ ("/\" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"/\" ( { ("/\" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ,F₁()) is Element of the carrier of F₁()
f is Element of the carrier of F₁()
f is Element of bool the carrier of F₁()
"/\" (f,F₁()) is Element of the carrier of F₁()
F₁() is non empty V55() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() up-complete /\-complete RelStr
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
{ ("/\" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"/\" ( { ("/\" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ,F₁()) is Element of the carrier of F₁()
{ b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"/\" ((union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ),F₁()) is Element of the carrier of F₁()
f is Element of the carrier of F₁()
f is set
c₃ is Element of bool the carrier of F₁()
"/\" (c₃,F₁()) is Element of the carrier of F₁()
F₁() is non empty antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() RelStr
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
{ ("\/" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"\/" ( { ("\/" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ,F₁()) is Element of the carrier of F₁()
{ b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"\/" ((union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ),F₁()) is Element of the carrier of F₁()
f is Element of the carrier of F₁()
f is Element of bool the carrier of F₁()
"\/" (f,F₁()) is Element of the carrier of F₁()
F₁() is non empty V55() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() up-complete /\-complete RelStr
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
{ ("\/" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"\/" ( { ("\/" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ,F₁()) is Element of the carrier of F₁()
{ b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
"\/" ((union { b₁ where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ),F₁()) is Element of the carrier of F₁()
f is Element of the carrier of F₁()
f is set
c₃ is Element of bool the carrier of F₁()
"\/" (c₃,F₁()) is Element of the carrier of F₁()
f is Relation-like set
f is Relation-like set
proj1 f is set
proj1 f is set
[:(proj1 f),(proj1 f):] is Relation-like set
proj2 f is set
proj2 f is set
[:(proj2 f),(proj2 f):] is Relation-like set
c₃ is Relation-like set
y1 is set
C2 is set
[y1,C2] is V1() set
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
q is set
D1 is set
[q,D1] is V1() set
{q,D1} is non empty set
{q} is non empty set
{{q,D1},{q}} is non empty set
D9 is set
D2 is set
[D9,D2] is V1() set
{D9,D2} is non empty set
{D9} is non empty set
{{D9,D2},{D9}} is non empty set
[q,D9] is V1() set
{q,D9} is non empty set
{{q,D9},{q}} is non empty set
[D1,D2] is V1() set
{D1,D2} is non empty set
{D1} is non empty set
{{D1,D2},{D1}} is non empty set
D2 is set
D1 is set
[D2,D1] is V1() set
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
d is set
e is set
[d,e] is V1() set
{d,e} is non empty set
{d} is non empty set
{{d,e},{d}} is non empty set
[D2,d] is V1() set
{D2,d} is non empty set
{{D2,d},{D2}} is non empty set
[D1,e] is V1() set
{D1,e} is non empty set
{D1} is non empty set
{{D1,e},{D1}} is non empty set
q is set
D9 is set
[q,D9] is V1() set
{q,D9} is non empty set
{q} is non empty set
{{q,D9},{q}} is non empty set
D1 is set
D2 is set
[D1,D2] is V1() set
{D1,D2} is non empty set
{D1} is non empty set
{{D1,D2},{D1}} is non empty set
[q,D1] is V1() set
{q,D1} is non empty set
{{q,D1},{q}} is non empty set
[D9,D2] is V1() set
{D9,D2} is non empty set
{D9} is non empty set
{{D9,D2},{D9}} is non empty set
c₃ is Relation-like set
y1 is Relation-like set
f is Relation-like set
f is Relation-like set
(f,f) is Relation-like set
c₃ is set
c₃ `1 is set
(c<sub>3</sub> `1) `1 is set
c<sub>3</sub> `2 is set
(c₃ `2) `1 is set
[((c₃ `1) `1),((c₃ `2) `1)] is V1() set
{((c₃ `1) `1),((c₃ `2) `1)} is non empty set
{((c₃ `1) `1)} is non empty set
{{((c₃ `1) `1),((c₃ `2) `1)},{((c₃ `1) `1)}} is non empty set
(c₃ `1) `2 is set
(c₃ `2) `2 is set
[((c₃ `1) `2),((c₃ `2) `2)] is V1() set
{((c₃ `1) `2),((c₃ `2) `2)} is non empty set
{((c₃ `1) `2)} is non empty set
{{((c₃ `1) `2),((c₃ `2) `2)},{((c₃ `1) `2)}} is non empty set
y1 is set
C2 is set
[y1,C2] is V1() set
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
q is set
D9 is set
[q,D9] is V1() set
{q,D9} is non empty set
{q} is non empty set
{{q,D9},{q}} is non empty set
D1 is set
D2 is set
[D1,D2] is V1() set
{D1,D2} is non empty set
{D1} is non empty set
{{D1,D2},{D1}} is non empty set
[q,D1] is V1() set
{q,D1} is non empty set
{{q,D1},{q}} is non empty set
[D9,D2] is V1() set
{D9,D2} is non empty set
{D9} is non empty set
{{D9,D2},{D9}} is non empty set
y1 is set
C2 is set
[y1,C2] is V1() set
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
y1 is set
C2 is set
[y1,C2] is V1() set
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
q is set
D9 is set
[q,D9] is V1() set
{q,D9} is non empty set
{q} is non empty set
{{q,D9},{q}} is non empty set
q is set
D9 is set
[q,D9] is V1() set
{q,D9} is non empty set
{q} is non empty set
{{q,D9},{q}} is non empty set
[y1,((c₃ `2) `1)] is V1() set
{y1,((c₃ `2) `1)} is non empty set
{{y1,((c₃ `2) `1)},{y1}} is non empty set
[y1,q] is V1() set
{y1,q} is non empty set
{{y1,q},{y1}} is non empty set
D1 is set
D2 is set
[D1,D2] is V1() set
{D1,D2} is non empty set
{D1} is non empty set
{{D1,D2},{D1}} is non empty set
D1 is set
D2 is set
[D1,D2] is V1() set
{D1,D2} is non empty set
{D1} is non empty set
{{D1,D2},{D1}} is non empty set
[C2,((c₃ `2) `2)] is V1() set
{C2,((c₃ `2) `2)} is non empty set
{C2} is non empty set
{{C2,((c₃ `2) `2)},{C2}} is non empty set
[C2,D9] is V1() set
{C2,D9} is non empty set
{{C2,D9},{C2}} is non empty set
f is set
f is set
[:f,f:] is Relation-like set
bool [:f,f:] is non empty set
c₃ is set
y1 is set
[:c₃,y1:] is Relation-like set
bool [:c₃,y1:] is non empty set
C2 is Relation-like f -defined f -valued Element of bool [:f,f:]
q is Relation-like c₃ -defined y1 -valued Element of bool [:c₃,y1:]
(C2,q) is Relation-like set
[:f,c₃:] is Relation-like set
[:f,y1:] is Relation-like set
[:[:f,c₃:],[:f,y1:]:] is Relation-like set
bool [:[:f,c₃:],[:f,y1:]:] is non empty set
D9 is set
D1 is set
D2 is set
[D1,D2] is V1() set
{D1,D2} is non empty set
{D1} is non empty set
{{D1,D2},{D1}} is non empty set
D9 `1 is set
(D9 `1) `2 is set
D9 `2 is set
(D9 `2) `2 is set
[((D9 `1) `2),((D9 `2) `2)] is V1() set
{((D9 `1) `2),((D9 `2) `2)} is non empty set
{((D9 `1) `2)} is non empty set
{{((D9 `1) `2),((D9 `2) `2)},{((D9 `1) `2)}} is non empty set
D2 is set
D1 is set
[D2,D1] is V1() set
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
d is set
e is set
[d,e] is V1() set
{d,e} is non empty set
{d} is non empty set
{{d,e},{d}} is non empty set
(D9 `1) `1 is set
(D9 `2) `1 is set
[((D9 `1) `1),((D9 `2) `1)] is V1() set
{((D9 `1) `1),((D9 `2) `1)} is non empty set
{((D9 `1) `1)} is non empty set
{{((D9 `1) `1),((D9 `2) `1)},{((D9 `1) `1)}} is non empty set
y is set
x is set
[y,x] is V1() set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
y is set
e is set
[y,e] is V1() set
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
D2 `2 is set
D1 `2 is set
D2 `1 is set
D1 `1 is set
f is RelStr
the carrier of f is set
f is RelStr
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]
[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set
bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty set
RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) is strict RelStr
the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) is set
the InternalRel of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) is Relation-like the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) -defined the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) -valued Element of bool [: the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #), the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #):]
[: the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #), the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #):] is Relation-like set
bool [: the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #), the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #):] is non empty set
c₃ is strict RelStr
the carrier of c₃ is set
the InternalRel of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Element of bool [: the carrier of c₃, the carrier of c₃:]
[: the carrier of c₃, the carrier of c₃:] is Relation-like set
bool [: the carrier of c₃, the carrier of c₃:] is non empty set
y1 is strict RelStr
the carrier of y1 is set
the InternalRel of y1 is Relation-like the carrier of y1 -defined the carrier of y1 -valued Element of bool [: the carrier of y1, the carrier of y1:]
[: the carrier of y1, the carrier of y1:] is Relation-like set
bool [: the carrier of y1, the carrier of y1:] is non empty set
f is RelStr
f is RelStr
(f,f) is strict RelStr
the carrier of (f,f) is set
bool the carrier of (f,f) is non empty set
c₃ is Element of bool the carrier of (f,f)
proj1 c₃ is set
the carrier of f is set
bool the carrier of f is non empty set
y1 is set
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
C2 is set
[y1,C2] is V1() set
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
proj2 c₃ is set
the carrier of f is set
bool the carrier of f is non empty set
y1 is set
[: the carrier of f, the carrier of f:] is Relation-like set
C2 is set
[C2,y1] is V1() set
{C2,y1} is non empty set
{C2} is non empty set
{{C2,y1},{C2}} is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
c₃ is Element of bool the carrier of f
y1 is Element of bool the carrier of f
[:c₃,y1:] is Relation-like set
(f,f) is strict RelStr
the carrier of (f,f) is set
bool the carrier of (f,f) is non empty set
[:c₃,y1:] is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
f is non empty RelStr
the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
c₃ is Element of the carrier of f
y1 is Element of the carrier of f
[c₃,y1] is V1() set
{c₃,y1} is non empty set
{c₃} is non empty set
{{c₃,y1},{c₃}} is non empty set
(f,f) is strict RelStr
the carrier of (f,f) is set
q is Element of the carrier of f
C2 is Element of the carrier of f
[q,C2] is V1() Element of [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty Relation-like set
{q,C2} is non empty set
{q} is non empty set
{{q,C2},{q}} is non empty set
f is non empty RelStr
f is non empty RelStr
(f,f) is strict RelStr
the carrier of (f,f) is set
c₃ is Element of the carrier of (f,f)
c₃ `1 is set
the carrier of f is non empty set
the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
c<sub>3</sub> `2 is set
the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
f is non empty RelStr
the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
(f,f) is strict RelStr
c₃ is Element of the carrier of f
y1 is Element of the carrier of f
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,c₃,C2) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is set
{c₃,C2} is non empty set
{c₃} is non empty set
{{c₃,C2},{c₃}} is non empty set
(f,f,y1,q) is V1() Element of the carrier of (f,f)
{y1,q} is non empty set
{y1} is non empty set
{{y1,q},{y1}} is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
[(f,f,c₃,C2),(f,f,y1,q)] is V1() set
{(f,f,c₃,C2),(f,f,y1,q)} is non empty Relation-like set
{(f,f,c₃,C2)} is non empty Relation-like set
{{(f,f,c₃,C2),(f,f,y1,q)},{(f,f,c₃,C2)}} is non empty set
[(f,f,c₃,C2),(f,f,y1,q)] `1 is set
([(f,f,c<sub>3</sub>,C2),(f,f,y1,q)] `1) `1 is set
[(f,f,c<sub>3</sub>,C2),(f,f,y1,q)] `2 is set
([(f,f,c₃,C2),(f,f,y1,q)] `2) `1 is set
([(f,f,c₃,C2),(f,f,y1,q)] `1) `2 is set
([(f,f,c₃,C2),(f,f,y1,q)] `2) `2 is set
[(([(f,f,c₃,C2),(f,f,y1,q)] `1) `1),(([(f,f,c₃,C2),(f,f,y1,q)] `2) `1)] is V1() set
{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `1),(([(f,f,c₃,C2),(f,f,y1,q)] `2) `1)} is non empty set
{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `1)} is non empty set
{{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `1),(([(f,f,c₃,C2),(f,f,y1,q)] `2) `1)},{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `1)}} is non empty set
[(([(f,f,c₃,C2),(f,f,y1,q)] `1) `2),(([(f,f,c₃,C2),(f,f,y1,q)] `2) `2)] is V1() set
{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `2),(([(f,f,c₃,C2),(f,f,y1,q)] `2) `2)} is non empty set
{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `2)} is non empty set
{{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `2),(([(f,f,c₃,C2),(f,f,y1,q)] `2) `2)},{(([(f,f,c₃,C2),(f,f,y1,q)] `1) `2)}} is non empty set
( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]
[: the carrier of f, the carrier of f:] is non empty Relation-like set
[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty Relation-like set
bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty set
the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]
[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set
bool [: the carrier of (f,f), the carrier of (f,f):] is non empty set
the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]
[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set
bool [: the carrier of (f,f), the carrier of (f,f):] is non empty set
( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]
[: the carrier of f, the carrier of f:] is non empty Relation-like set
[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty Relation-like set
bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty set
(f,f,c₃,y1) is V1() Element of the carrier of (f,f)
(f,f) is strict RelStr
the carrier of (f,f) is set
{c₃,y1} is non empty set
{{c₃,y1},{c₃}} is non empty set
(f,f,C2,q) is V1() Element of the carrier of (f,f)
(f,f) is strict RelStr
the carrier of (f,f) is set
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
f is non empty RelStr
f is non empty RelStr
(f,f) is strict RelStr
the carrier of (f,f) is set
c₃ is Element of the carrier of (f,f)
y1 is Element of the carrier of (f,f)
(f,f,c₃) is Element of the carrier of f
the carrier of f is non empty set
(f,f,y1) is Element of the carrier of f
(f,f,c₃) is Element of the carrier of f
the carrier of f is non empty set
(f,f,y1) is Element of the carrier of f
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,(f,f,y1),(f,f,y1)) is V1() Element of the carrier of (f,f)
{(f,f,y1),(f,f,y1)} is non empty set
{(f,f,y1)} is non empty set
{{(f,f,y1),(f,f,y1)},{(f,f,y1)}} is non empty set
C2 is set
q is set
[C2,q] is V1() set
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
(f,f,(f,f,c₃),(f,f,c₃)) is V1() Element of the carrier of (f,f)
{(f,f,c₃),(f,f,c₃)} is non empty set
{(f,f,c₃)} is non empty set
{{(f,f,c₃),(f,f,c₃)},{(f,f,c₃)}} is non empty set
C2 is set
q is set
[C2,q] is V1() set
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
f is RelStr
f is RelStr
(f,f) is strict RelStr
the carrier of (f,f) is set
the carrier of f is set
the carrier of f is set
c₃ is non empty RelStr
the carrier of c₃ is non empty set
[: the carrier of (f,f), the carrier of c₃:] is Relation-like set
bool [: the carrier of (f,f), the carrier of c₃:] is non empty set
y1 is Relation-like the carrier of (f,f) -defined the carrier of c₃ -valued V12() V18( the carrier of (f,f), the carrier of c₃) Element of bool [: the carrier of (f,f), the carrier of c₃:]
C2 is Relation-like the carrier of (f,f) -defined the carrier of c₃ -valued V12() V18( the carrier of (f,f), the carrier of c₃) Element of bool [: the carrier of (f,f), the carrier of c₃:]
q is set
D9 is set
y1 . (q,D9) is set
C2 . (q,D9) is set
[: the carrier of f, the carrier of f:] is Relation-like set
f is non empty RelStr
f is non empty RelStr
(f,f) is strict RelStr
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
(f,f, the Element of the carrier of f, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is set
{ the Element of the carrier of f, the Element of the carrier of f} is non empty set
{ the Element of the carrier of f} is non empty set
{{ the Element of the carrier of f, the Element of the carrier of f},{ the Element of the carrier of f}} is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
f is V55() reflexive RelStr
f is V55() reflexive RelStr
(f,f) is strict RelStr
c₃ is set
the carrier of (f,f) is set
[c₃,c₃] is V1() set
{c₃,c₃} is non empty set
{c₃} is non empty set
{{c₃,c₃},{c₃}} is non empty set
the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]
[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set
bool [: the carrier of (f,f), the carrier of (f,f):] is non empty set
the carrier of f is set
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
y1 is set
C2 is set
[y1,C2] is V1() set
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V17( the carrier of f) reflexive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
[y1,y1] is V1() set
{y1,y1} is non empty set
{{y1,y1},{y1}} is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V17( the carrier of f) reflexive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
[C2,C2] is V1() set
{C2,C2} is non empty set
{C2} is non empty set
{{C2,C2},{C2}} is non empty set
[[y1,C2],[y1,C2]] is V1() set
{[y1,C2],[y1,C2]} is non empty Relation-like set
{[y1,C2]} is non empty Relation-like set
{{[y1,C2],[y1,C2]},{[y1,C2]}} is non empty set
[[y1,C2],[y1,C2]] `1 is set
[[y1,C2],[y1,C2]] `2 is set
([[y1,C2],[y1,C2]] `1) `1 is set
([[y1,C2],[y1,C2]] `1) `2 is set
( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]
[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set
bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty set
f is antisymmetric RelStr
f is antisymmetric RelStr
(f,f) is strict RelStr
c₃ is set
the carrier of (f,f) is set
y1 is set
[c₃,y1] is V1() set
{c₃,y1} is non empty set
{c₃} is non empty set
{{c₃,y1},{c₃}} is non empty set
the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]
[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set
bool [: the carrier of (f,f), the carrier of (f,f):] is non empty set
[y1,c₃] is V1() set
{y1,c₃} is non empty set
{y1} is non empty set
{{y1,c₃},{y1}} is non empty set
the carrier of f is set
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
C2 is set
q is set
[C2,q] is V1() set
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
D9 is set
D1 is set
[D9,D1] is V1() set
{D9,D1} is non empty set
{D9} is non empty set
{{D9,D1},{D9}} is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]
[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set
bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty set
[y1,c₃] `1 is set
([y1,c<sub>3</sub>] `1) `1 is set
[y1,c<sub>3</sub>] `2 is set
([y1,c₃] `2) `1 is set
[(([y1,c₃] `1) `1),(([y1,c₃] `2) `1)] is V1() set
{(([y1,c₃] `1) `1),(([y1,c₃] `2) `1)} is non empty set
{(([y1,c₃] `1) `1)} is non empty set
{{(([y1,c₃] `1) `1),(([y1,c₃] `2) `1)},{(([y1,c₃] `1) `1)}} is non empty set
y1 `1 is set
[(y1 `1),(([y1,c₃] `2) `1)] is V1() set
{(y1 `1),(([y1,c<sub>3</sub>] `2) `1)} is non empty set
{(y1 `1)} is non empty set
{{(y1 `1),(([y1,c<sub>3</sub>] `2) `1)},{(y1 `1)}} is non empty set
c₃ `1 is set
[(y1 `1),(c₃ `1)] is V1() set
{(y1 `1),(c₃ `1)} is non empty set
{{(y1 `1),(c₃ `1)},{(y1 `1)}} is non empty set
[C2,q] `1 is set
[D9,([C2,q] `1)] is V1() set
{D9,([C2,q] `1)} is non empty set
{{D9,([C2,q] `1)},{D9}} is non empty set
[D9,C2] is V1() set
{D9,C2} is non empty set
{{D9,C2},{D9}} is non empty set
([y1,c₃] `1) `2 is set
([y1,c₃] `2) `2 is set
[(([y1,c₃] `1) `2),(([y1,c₃] `2) `2)] is V1() set
{(([y1,c₃] `1) `2),(([y1,c₃] `2) `2)} is non empty set
{(([y1,c₃] `1) `2)} is non empty set
{{(([y1,c₃] `1) `2),(([y1,c₃] `2) `2)},{(([y1,c₃] `1) `2)}} is non empty set
y1 `2 is set
[(y1 `2),(([y1,c₃] `2) `2)] is V1() set
{(y1 `2),(([y1,c<sub>3</sub>] `2) `2)} is non empty set
{(y1 `2)} is non empty set
{{(y1 `2),(([y1,c<sub>3</sub>] `2) `2)},{(y1 `2)}} is non empty set
c₃ `2 is set
[(y1 `2),(c₃ `2)] is V1() set
{(y1 `2),(c₃ `2)} is non empty set
{{(y1 `2),(c₃ `2)},{(y1 `2)}} is non empty set
[C2,q] `2 is set
[D1,([C2,q] `2)] is V1() set
{D1,([C2,q] `2)} is non empty set
{D1} is non empty set
{{D1,([C2,q] `2)},{D1}} is non empty set
[D1,q] is V1() set
{D1,q} is non empty set
{{D1,q},{D1}} is non empty set
[c₃,y1] `1 is set
([c<sub>3</sub>,y1] `1) `2 is set
[c<sub>3</sub>,y1] `2 is set
([c₃,y1] `2) `2 is set
[(([c₃,y1] `1) `2),(([c₃,y1] `2) `2)] is V1() set
{(([c₃,y1] `1) `2),(([c₃,y1] `2) `2)} is non empty set
{(([c₃,y1] `1) `2)} is non empty set
{{(([c₃,y1] `1) `2),(([c₃,y1] `2) `2)},{(([c₃,y1] `1) `2)}} is non empty set
[(c₃ `2),(([c<sub>3</sub>,y1] `2) `2)] is V1() set
{(c<sub>3</sub> `2),(([c₃,y1] `2) `2)} is non empty set
{(c₃ `2)} is non empty set
{{(c<sub>3</sub> `2),(([c₃,y1] `2) `2)},{(c₃ `2)}} is non empty set
[(c<sub>3</sub> `2),(y1 `2)] is V1() set
{(c<sub>3</sub> `2),(y1 `2)} is non empty set
{{(c<sub>3</sub> `2),(y1 `2)},{(c<sub>3</sub> `2)}} is non empty set
[D9,D1] `2 is set
[q,([D9,D1] `2)] is V1() set
{q,([D9,D1] `2)} is non empty set
{q} is non empty set
{{q,([D9,D1] `2)},{q}} is non empty set
[q,D1] is V1() set
{q,D1} is non empty set
{{q,D1},{q}} is non empty set
([c₃,y1] `1) `1 is set
([c₃,y1] `2) `1 is set
[(([c₃,y1] `1) `1),(([c₃,y1] `2) `1)] is V1() set
{(([c₃,y1] `1) `1),(([c₃,y1] `2) `1)} is non empty set
{(([c₃,y1] `1) `1)} is non empty set
{{(([c₃,y1] `1) `1),(([c₃,y1] `2) `1)},{(([c₃,y1] `1) `1)}} is non empty set
[(c₃ `1),(([c<sub>3</sub>,y1] `2) `1)] is V1() set
{(c<sub>3</sub> `1),(([c₃,y1] `2) `1)} is non empty set
{(c₃ `1)} is non empty set
{{(c<sub>3</sub> `1),(([c₃,y1] `2) `1)},{(c₃ `1)}} is non empty set
[(c<sub>3</sub> `1),(y1 `1)] is V1() set
{(c<sub>3</sub> `1),(y1 `1)} is non empty set
{{(c<sub>3</sub> `1),(y1 `1)},{(c<sub>3</sub> `1)}} is non empty set
[D9,D1] `1 is set
[C2,([D9,D1] `1)] is V1() set
{C2,([D9,D1] `1)} is non empty set
{{C2,([D9,D1] `1)},{C2}} is non empty set
[C2,D9] is V1() set
{C2,D9} is non empty set
{{C2,D9},{C2}} is non empty set
f is transitive RelStr
f is transitive RelStr
(f,f) is strict RelStr
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
C2 is set
the carrier of (f,f) is set
q is set
D9 is set
[C2,q] is V1() set
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]
[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set
bool [: the carrier of (f,f), the carrier of (f,f):] is non empty set
[q,D9] is V1() set
{q,D9} is non empty set
{q} is non empty set
{{q,D9},{q}} is non empty set
[C2,D9] is V1() set
{C2,D9} is non empty set
{{C2,D9},{C2}} is non empty set
[: the carrier of f, the carrier of f:] is Relation-like set
D1 is set
D2 is set
[D1,D2] is V1() set
{D1,D2} is non empty set
{D1} is non empty set
{{D1,D2},{D1}} is non empty set
D2 is set
D1 is set
[D2,D1] is V1() set
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]
[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set
bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is non empty set
[q,D9] `1 is set
([q,D9] `1) `1 is set
[q,D9] `2 is set
([q,D9] `2) `1 is set
[(([q,D9] `1) `1),(([q,D9] `2) `1)] is V1() set
{(([q,D9] `1) `1),(([q,D9] `2) `1)} is non empty set
{(([q,D9] `1) `1)} is non empty set
{{(([q,D9] `1) `1),(([q,D9] `2) `1)},{(([q,D9] `1) `1)}} is non empty set
q `1 is set
[(q `1),(([q,D9] `2) `1)] is V1() set
{(q `1),(([q,D9] `2) `1)} is non empty set
{(q `1)} is non empty set
{{(q `1),(([q,D9] `2) `1)},{(q `1)}} is non empty set
D9 `1 is set
[(q `1),(D9 `1)] is V1() set
{(q `1),(D9 `1)} is non empty set
{{(q `1),(D9 `1)},{(q `1)}} is non empty set
[D1,(D9 `1)] is V1() set
{D1,(D9 `1)} is non empty set
{{D1,(D9 `1)},{D1}} is non empty set
[D1,D2] is V1() set
{D1,D2} is non empty set
{{D1,D2},{D1}} is non empty set
d is set
e is set
[d,e] is V1() set
{d,e} is non empty set
{d} is non empty set
{{d,e},{d}} is non empty set
[C2,q] `1 is set
([C2,q] `1) `1 is set
[C2,q] `2 is set
([C2,q] `2) `1 is set
[(([C2,q] `1) `1),(([C2,q] `2) `1)] is V1() set
{(([C2,q] `1) `1),(([C2,q] `2) `1)} is non empty set
{(([C2,q] `1) `1)} is non empty set
{{(([C2,q] `1) `1),(([C2,q] `2) `1)},{(([C2,q] `1) `1)}} is non empty set
C2 `1 is set
[(C2 `1),(([C2,q] `2) `1)] is V1() set
{(C2 `1),(([C2,q] `2) `1)} is non empty set
{(C2 `1)} is non empty set
{{(C2 `1),(([C2,q] `2) `1)},{(C2 `1)}} is non empty set
[(C2 `1),(q `1)] is V1() set
{(C2 `1),(q `1)} is non empty set
{{(C2 `1),(q `1)},{(C2 `1)}} is non empty set
[d,(q `1)] is V1() set
{d,(q `1)} is non empty set
{{d,(q `1)},{d}} is non empty set
[d,D1] is V1() set
{d,D1} is non empty set
{{d,D1},{d}} is non empty set
[d,D2] is V1() set
{d,D2} is non empty set
{{d,D2},{d}} is non empty set
[d,(D9 `1)] is V1() set
{d,(D9 `1)} is non empty set
{{d,(D9 `1)},{d}} is non empty set
[(C2 `1),(D9 `1)] is V1() set
{(C2 `1),(D9 `1)} is non empty set
{{(C2 `1),(D9 `1)},{(C2 `1)}} is non empty set
([q,D9] `1) `2 is set
([q,D9] `2) `2 is set
[(([q,D9] `1) `2),(([q,D9] `2) `2)] is V1() set
{(([q,D9] `1) `2),(([q,D9] `2) `2)} is non empty set
{(([q,D9] `1) `2)} is non empty set
{{(([q,D9] `1) `2),(([q,D9] `2) `2)},{(([q,D9] `1) `2)}} is non empty set
q `2 is set
[(q `2),(([q,D9] `2) `2)] is V1() set
{(q `2),(([q,D9] `2) `2)} is non empty set
{(q `2)} is non empty set
{{(q `2),(([q,D9] `2) `2)},{(q `2)}} is non empty set
D9 `2 is set
[(q `2),(D9 `2)] is V1() set
{(q `2),(D9 `2)} is non empty set
{{(q `2),(D9 `2)},{(q `2)}} is non empty set
[D2,(D9 `2)] is V1() set
{D2,(D9 `2)} is non empty set
{D2} is non empty set
{{D2,(D9 `2)},{D2}} is non empty set
[D2,D1] is V1() set
{D2,D1} is non empty set
{{D2,D1},{D2}} is non empty set
([C2,q] `1) `2 is set
([C2,q] `2) `2 is set
[(([C2,q] `1) `2),(([C2,q] `2) `2)] is V1() set
{(([C2,q] `1) `2),(([C2,q] `2) `2)} is non empty set
{(([C2,q] `1) `2)} is non empty set
{{(([C2,q] `1) `2),(([C2,q] `2) `2)},{(([C2,q] `1) `2)}} is non empty set
C2 `2 is set
[(C2 `2),(([C2,q] `2) `2)] is V1() set
{(C2 `2),(([C2,q] `2) `2)} is non empty set
{(C2 `2)} is non empty set
{{(C2 `2),(([C2,q] `2) `2)},{(C2 `2)}} is non empty set
[(C2 `2),(q `2)] is V1() set
{(C2 `2),(q `2)} is non empty set
{{(C2 `2),(q `2)},{(C2 `2)}} is non empty set
[e,(q `2)] is V1() set
{e,(q `2)} is non empty set
{e} is non empty set
{{e,(q `2)},{e}} is non empty set
[e,D2] is V1() set
{e,D2} is non empty set
{{e,D2},{e}} is non empty set
[e,D1] is V1() set
{e,D1} is non empty set
{{e,D1},{e}} is non empty set
[e,(D9 `2)] is V1() set
{e,(D9 `2)} is non empty set
{{e,(D9 `2)},{e}} is non empty set
[(C2 `2),(D9 `2)] is V1() set
{(C2 `2),(D9 `2)} is non empty set
{{(C2 `2),(D9 `2)},{(C2 `2)}} is non empty set
[C2,D9] `1 is set
[C2,D9] `2 is set
f is non empty with_suprema RelStr
f is non empty with_suprema RelStr
(f,f) is non empty strict RelStr
the carrier of (f,f) is non empty set
y1 is Element of the carrier of (f,f)
C2 is Element of the carrier of (f,f)
the carrier of f is non empty set
(f,f,y1) is Element of the carrier of f
(f,f,C2) is Element of the carrier of f
q is Element of the carrier of f
the carrier of f is non empty set
(f,f,y1) is Element of the carrier of f
(f,f,C2) is Element of the carrier of f
D9 is Element of the carrier of f
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,q,D9) is V1() Element of the carrier of (f,f)
{q,D9} is non empty set
{q} is non empty set
{{q,D9},{q}} is non empty set
D1 is V1() Element of the carrier of (f,f)
(f,f,(f,f,y1),(f,f,y1)) is V1() Element of the carrier of (f,f)
{(f,f,y1),(f,f,y1)} is non empty set
{(f,f,y1)} is non empty set
{{(f,f,y1),(f,f,y1)},{(f,f,y1)}} is non empty set
(f,f,(f,f,C2),(f,f,C2)) is V1() Element of the carrier of (f,f)
{(f,f,C2),(f,f,C2)} is non empty set
{(f,f,C2)} is non empty set
{{(f,f,C2),(f,f,C2)},{(f,f,C2)}} is non empty set
D2 is set
D2 is set
[D2,D2] is V1() set
{D2,D2} is non empty set
{D2} is non empty set
{{D2,D2},{D2}} is non empty set
D1 is set
d is set
[D1,d] is V1() set
{D1,d} is non empty set
{D1} is non empty set
{{D1,d},{D1}} is non empty set
D2 is Element of the carrier of (f,f)
(f,f,D2) is Element of the carrier of f
(f,f,D2) is Element of the carrier of f
(f,f,(f,f,D2),(f,f,D2)) is V1() Element of the carrier of (f,f)
{(f,f,D2),(f,f,D2)} is non empty set
{(f,f,D2)} is non empty set
{{(f,f,D2),(f,f,D2)},{(f,f,D2)}} is non empty set
D2 is set
D1 is set
[D2,D1] is V1() set
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
f is non empty with_infima RelStr
f is non empty with_infima RelStr
(f,f) is non empty strict RelStr
the carrier of (f,f) is non empty set
y1 is Element of the carrier of (f,f)
C2 is Element of the carrier of (f,f)
the carrier of f is non empty set
(f,f,y1) is Element of the carrier of f
(f,f,C2) is Element of the carrier of f
q is Element of the carrier of f
the carrier of f is non empty set
(f,f,y1) is Element of the carrier of f
(f,f,C2) is Element of the carrier of f
D9 is Element of the carrier of f
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,q,D9) is V1() Element of the carrier of (f,f)
{q,D9} is non empty set
{q} is non empty set
{{q,D9},{q}} is non empty set
D1 is V1() Element of the carrier of (f,f)
(f,f,(f,f,y1),(f,f,y1)) is V1() Element of the carrier of (f,f)
{(f,f,y1),(f,f,y1)} is non empty set
{(f,f,y1)} is non empty set
{{(f,f,y1),(f,f,y1)},{(f,f,y1)}} is non empty set
(f,f,(f,f,C2),(f,f,C2)) is V1() Element of the carrier of (f,f)
{(f,f,C2),(f,f,C2)} is non empty set
{(f,f,C2)} is non empty set
{{(f,f,C2),(f,f,C2)},{(f,f,C2)}} is non empty set
D2 is set
D2 is set
[D2,D2] is V1() set
{D2,D2} is non empty set
{D2} is non empty set
{{D2,D2},{D2}} is non empty set
D1 is set
d is set
[D1,d] is V1() set
{D1,d} is non empty set
{D1} is non empty set
{{D1,d},{D1}} is non empty set
D2 is Element of the carrier of (f,f)
(f,f,D2) is Element of the carrier of f
(f,f,D2) is Element of the carrier of f
(f,f,(f,f,D2),(f,f,D2)) is V1() Element of the carrier of (f,f)
{(f,f,D2),(f,f,D2)} is non empty set
{(f,f,D2)} is non empty set
{{(f,f,D2),(f,f,D2)},{(f,f,D2)}} is non empty set
D2 is set
D1 is set
[D2,D1] is V1() set
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
f is RelStr
f is RelStr
(f,f) is strict RelStr
the carrier of (f,f) is set
the carrier of f is set
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
c₃ is set
f is non empty RelStr
f is non empty RelStr
(f,f) is non empty strict RelStr
the carrier of f is non empty set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
y1 is Element of the carrier of f
(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is non empty set
{y1, the Element of the carrier of f} is non empty set
{y1} is non empty set
{{y1, the Element of the carrier of f},{y1}} is non empty set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
y1 is Element of the carrier of f
(f,f, the Element of the carrier of f,y1) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is non empty set
{ the Element of the carrier of f,y1} is non empty set
{ the Element of the carrier of f} is non empty set
{{ the Element of the carrier of f,y1},{ the Element of the carrier of f}} is non empty set
f is non empty V55() reflexive RelStr
f is non empty V55() reflexive RelStr
(f,f) is non empty strict V55() reflexive RelStr
the carrier of f is non empty set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
y1 is Element of the carrier of f
C2 is Element of the carrier of f
(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is non empty set
{y1, the Element of the carrier of f} is non empty set
{y1} is non empty set
{{y1, the Element of the carrier of f},{y1}} is non empty set
(f,f,C2, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{C2, the Element of the carrier of f} is non empty set
{C2} is non empty set
{{C2, the Element of the carrier of f},{C2}} is non empty set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
y1 is Element of the carrier of f
C2 is Element of the carrier of f
(f,f, the Element of the carrier of f,y1) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is non empty set
{ the Element of the carrier of f,y1} is non empty set
{ the Element of the carrier of f} is non empty set
{{ the Element of the carrier of f,y1},{ the Element of the carrier of f}} is non empty set
(f,f, the Element of the carrier of f,C2) is V1() Element of the carrier of (f,f)
{ the Element of the carrier of f,C2} is non empty set
{{ the Element of the carrier of f,C2},{ the Element of the carrier of f}} is non empty set
f is non empty V55() reflexive RelStr
f is non empty V55() reflexive RelStr
(f,f) is non empty strict V55() reflexive RelStr
the carrier of f is non empty set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
y1 is Element of the carrier of f
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is non empty set
{y1, the Element of the carrier of f} is non empty set
{y1} is non empty set
{{y1, the Element of the carrier of f},{y1}} is non empty set
(f,f,C2, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{C2, the Element of the carrier of f} is non empty set
{C2} is non empty set
{{C2, the Element of the carrier of f},{C2}} is non empty set
(f,f,q, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{q, the Element of the carrier of f} is non empty set
{q} is non empty set
{{q, the Element of the carrier of f},{q}} is non empty set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
y1 is Element of the carrier of f
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f, the Element of the carrier of f,y1) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is non empty set
{ the Element of the carrier of f,y1} is non empty set
{ the Element of the carrier of f} is non empty set
{{ the Element of the carrier of f,y1},{ the Element of the carrier of f}} is non empty set
(f,f, the Element of the carrier of f,C2) is V1() Element of the carrier of (f,f)
{ the Element of the carrier of f,C2} is non empty set
{{ the Element of the carrier of f,C2},{ the Element of the carrier of f}} is non empty set
(f,f, the Element of the carrier of f,q) is V1() Element of the carrier of (f,f)
{ the Element of the carrier of f,q} is non empty set
{{ the Element of the carrier of f,q},{ the Element of the carrier of f}} is non empty set
f is non empty V55() reflexive RelStr
f is non empty V55() reflexive RelStr
(f,f) is non empty strict V55() reflexive RelStr
the carrier of (f,f) is non empty set
the carrier of f is non empty set
the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
c₃ is Element of the carrier of f
y1 is Element of the carrier of f
the Element of the carrier of f is Element of the carrier of f
(f,f,c₃, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{c₃, the Element of the carrier of f} is non