:: 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 empty set
{c₃} is non empty set
{{c₃, the Element of the carrier of f},{c₃}} is non empty set
(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{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
q is Element of the carrier of (f,f)
(f,f,q) is Element of the carrier of f
(f,f,q) is Element of the carrier of f
(f,f,(f,f,q),(f,f,q)) is V1() Element of the carrier of (f,f)
{(f,f,q),(f,f,q)} is non empty set
{(f,f,q)} is non empty set
{{(f,f,q),(f,f,q)},{(f,f,q)}} is non empty set
D9 is Element of the carrier of f
(f,f,D9, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{D9, the Element of the carrier of f} is non empty set
{D9} is non empty set
{{D9, the Element of the carrier of f},{D9}} 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 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
q is Element of the carrier of (f,f)
(f,f,q) is Element of the carrier of f
(f,f,q) is Element of the carrier of f
(f,f,(f,f,q),(f,f,q)) is V1() Element of the carrier of (f,f)
{(f,f,q),(f,f,q)} is non empty set
{(f,f,q)} is non empty set
{{(f,f,q),(f,f,q)},{(f,f,q)}} is non empty set
D9 is Element of the carrier of f
(f,f, the Element of the carrier of f,D9) is V1() Element of the carrier of (f,f)
{ the Element of the carrier of f,D9} is non empty set
{{ the Element of the carrier of f,D9},{ 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 empty set
{c₃} is non empty set
{{c₃, the Element of the carrier of f},{c₃}} is non empty set
(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{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
q is Element of the carrier of (f,f)
(f,f,q) is Element of the carrier of f
(f,f,q) is Element of the carrier of f
(f,f,(f,f,q),(f,f,q)) is V1() Element of the carrier of (f,f)
{(f,f,q),(f,f,q)} is non empty set
{(f,f,q)} is non empty set
{{(f,f,q),(f,f,q)},{(f,f,q)}} is non empty set
D9 is Element of the carrier of f
(f,f,D9, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{D9, the Element of the carrier of f} is non empty set
{D9} is non empty set
{{D9, the Element of the carrier of f},{D9}} 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 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
q is Element of the carrier of (f,f)
(f,f,q) is Element of the carrier of f
(f,f,q) is Element of the carrier of f
(f,f,(f,f,q),(f,f,q)) is V1() Element of the carrier of (f,f)
{(f,f,q),(f,f,q)} is non empty set
{(f,f,q)} is non empty set
{{(f,f,q),(f,f,q)},{(f,f,q)}} is non empty set
D9 is Element of the carrier of f
(f,f, the Element of the carrier of f,D9) is V1() Element of the carrier of (f,f)
{ the Element of the carrier of f,D9} is non empty set
{{ the Element of the carrier of f,D9},{ the Element of 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
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
c₃ is directed Element of bool the carrier of f
y1 is directed 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
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
q is Element of the carrier of (f,f)
D9 is Element of the carrier of (f,f)
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
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
y is Element of the carrier of f
x is Element of the carrier of f
y is Element of the carrier of f
e is Element of the carrier of f
x is Element of the carrier of f
d is Element of the carrier of f
D2 is non empty RelStr
the carrier of D2 is non empty set
D1 is non empty RelStr
the carrier of D1 is non empty set
z1 is Element of the carrier of D1
z is Element of the carrier of D2
(D1,D2,z1,z) is V1() Element of the carrier of (D1,D2)
(D1,D2) is non empty strict RelStr
the carrier of (D1,D2) is non empty set
{z1,z} is non empty set
{z1} is non empty set
{{z1,z},{z1}} is non empty set
[d,y] is V1() set
{d,y} is non empty set
{d} is non empty set
{{d,y},{d}} is non empty set
z2 is Element of the carrier of (f,f)
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
the Element of y1 is Element of y1
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,q, the Element of y1) is V1() Element of the carrier of (f,f)
{q, the Element of y1} is non empty set
{q} is non empty set
{{q, the Element of y1},{q}} is non empty set
(f,f,D9, the Element of y1) is V1() Element of the carrier of (f,f)
{D9, the Element of y1} is non empty set
{D9} is non empty set
{{D9, the Element of y1},{D9}} is non empty set
D1 is Element of the carrier of (f,f)
(f,f,D1) is Element of the carrier of f
(f,f,D1) is Element of the carrier of f
D2 is Element of c₃
D2 is Element of y1
(f,f,D2,D2) is V1() Element of the carrier of (f,f)
{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
the Element of c₃ is Element of c₃
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f, the Element of c₃,q) is V1() Element of the carrier of (f,f)
{ the Element of c₃,q} is non empty set
{ the Element of c₃} is non empty set
{{ the Element of c₃,q},{ the Element of c₃}} is non empty set
(f,f, the Element of c₃,D9) is V1() Element of the carrier of (f,f)
{ the Element of c₃,D9} is non empty set
{{ the Element of c₃,D9},{ the Element of c₃}} is non empty set
D1 is Element of the carrier of (f,f)
(f,f,D1) is Element of the carrier of f
(f,f,D1) is Element of the carrier of f
D2 is Element of y1
D2 is Element of c₃
(f,f,D2,D2) is V1() Element of the carrier of (f,f)
{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
f is non empty RelStr
f is non empty RelStr
(f,f) is non empty strict RelStr
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
c₃ is non empty Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool 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
y1 is non empty Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
proj1 y1 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
bool the carrier of (f,f) is non empty set
c₃ is non empty directed Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
q is Element of the carrier of f
D9 is Element of the carrier of f
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
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
D2 is non empty Element of bool the carrier of f
e is Element of D2
(f,f,q,e) is V1() Element of the carrier of (f,f)
{q,e} is non empty set
{{q,e},{q}} is non empty set
d is Element of D2
(f,f,D9,d) is V1() Element of the carrier of (f,f)
{D9,d} is non empty set
{{D9,d},{D9}} is non empty set
y is Element of the carrier of (f,f)
(f,f,y) is Element of the carrier of f
D2 is non empty Element of bool the carrier of f
(f,f,y) is Element of the carrier of f
y is Element of D2
x is Element of D2
(f,f,y,x) is V1() Element of the carrier of (f,f)
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
e is set
x is set
[e,x] is V1() set
{e,x} is non empty set
{e} is non empty set
{{e,x},{e}} is non empty set
q is Element of the carrier of f
D9 is Element of the carrier of f
D1 is set
[D1,D9] is V1() set
{D1,D9} is non empty set
{D1} is non empty set
{{D1,D9},{D1}} is non empty set
D1 is set
[D1,q] is V1() set
{D1,q} is non empty set
{D1} is non empty set
{{D1,q},{D1}} is non empty set
D2 is non empty Element of bool the carrier of f
e is Element of D2
(f,f,e,q) is V1() Element of the carrier of (f,f)
{e,q} is non empty set
{e} is non empty set
{{e,q},{e}} is non empty set
d is Element of D2
(f,f,d,D9) is V1() Element of the carrier of (f,f)
{d,D9} is non empty set
{d} is non empty set
{{d,D9},{d}} is non empty set
y is Element of the carrier of (f,f)
(f,f,y) is Element of the carrier of f
D2 is non empty Element of bool the carrier of f
(f,f,y) is Element of the carrier of f
y is Element of D2
x is Element of D2
(f,f,x,y) is V1() Element of the carrier of (f,f)
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
e is set
x is set
[e,x] is V1() set
{e,x} is non empty set
{e} is non empty set
{{e,x},{e}} 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 filtered Element of bool the carrier of f
y1 is filtered 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
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
q is Element of the carrier of (f,f)
D9 is Element of the carrier of (f,f)
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
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
y is Element of the carrier of f
x is Element of the carrier of f
y is Element of the carrier of f
e is Element of the carrier of f
x is Element of the carrier of f
d is Element of the carrier of f
D2 is non empty RelStr
the carrier of D2 is non empty set
D1 is non empty RelStr
the carrier of D1 is non empty set
z1 is Element of the carrier of D1
z is Element of the carrier of D2
(D1,D2,z1,z) is V1() Element of the carrier of (D1,D2)
(D1,D2) is non empty strict RelStr
the carrier of (D1,D2) is non empty set
{z1,z} is non empty set
{z1} is non empty set
{{z1,z},{z1}} is non empty set
[d,y] is V1() set
{d,y} is non empty set
{d} is non empty set
{{d,y},{d}} is non empty set
z2 is Element of the carrier of (f,f)
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
the Element of y1 is Element of y1
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,q, the Element of y1) is V1() Element of the carrier of (f,f)
{q, the Element of y1} is non empty set
{q} is non empty set
{{q, the Element of y1},{q}} is non empty set
(f,f,D9, the Element of y1) is V1() Element of the carrier of (f,f)
{D9, the Element of y1} is non empty set
{D9} is non empty set
{{D9, the Element of y1},{D9}} is non empty set
D1 is Element of the carrier of (f,f)
(f,f,D1) is Element of the carrier of f
(f,f,D1) is Element of the carrier of f
D2 is Element of c₃
D2 is Element of y1
(f,f,D2,D2) is V1() Element of the carrier of (f,f)
{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
the Element of c₃ is Element of c₃
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f, the Element of c₃,q) is V1() Element of the carrier of (f,f)
{ the Element of c₃,q} is non empty set
{ the Element of c₃} is non empty set
{{ the Element of c₃,q},{ the Element of c₃}} is non empty set
(f,f, the Element of c₃,D9) is V1() Element of the carrier of (f,f)
{ the Element of c₃,D9} is non empty set
{{ the Element of c₃,D9},{ the Element of c₃}} is non empty set
D1 is Element of the carrier of (f,f)
(f,f,D1) is Element of the carrier of f
(f,f,D1) is Element of the carrier of f
D2 is Element of y1
D2 is Element of c₃
(f,f,D2,D2) is V1() Element of the carrier of (f,f)
{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
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
bool the carrier of (f,f) is non empty set
c₃ is non empty filtered Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
q is Element of the carrier of f
D9 is Element of the carrier of f
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
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
D2 is non empty Element of bool the carrier of f
e is Element of D2
(f,f,q,e) is V1() Element of the carrier of (f,f)
{q,e} is non empty set
{{q,e},{q}} is non empty set
d is Element of D2
(f,f,D9,d) is V1() Element of the carrier of (f,f)
{D9,d} is non empty set
{{D9,d},{D9}} is non empty set
y is Element of the carrier of (f,f)
(f,f,y) is Element of the carrier of f
D2 is non empty Element of bool the carrier of f
(f,f,y) is Element of the carrier of f
y is Element of D2
x is Element of D2
(f,f,y,x) is V1() Element of the carrier of (f,f)
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
e is set
x is set
[e,x] is V1() set
{e,x} is non empty set
{e} is non empty set
{{e,x},{e}} is non empty set
q is Element of the carrier of f
D9 is Element of the carrier of f
D1 is set
[D1,D9] is V1() set
{D1,D9} is non empty set
{D1} is non empty set
{{D1,D9},{D1}} is non empty set
D1 is set
[D1,q] is V1() set
{D1,q} is non empty set
{D1} is non empty set
{{D1,q},{D1}} is non empty set
D2 is non empty Element of bool the carrier of f
e is Element of D2
(f,f,e,q) is V1() Element of the carrier of (f,f)
{e,q} is non empty set
{e} is non empty set
{{e,q},{e}} is non empty set
d is Element of D2
(f,f,d,D9) is V1() Element of the carrier of (f,f)
{d,D9} is non empty set
{d} is non empty set
{{d,D9},{d}} is non empty set
y is Element of the carrier of (f,f)
(f,f,y) is Element of the carrier of f
D2 is non empty Element of bool the carrier of f
(f,f,y) is Element of the carrier of f
y is Element of D2
x is Element of D2
(f,f,x,y) is V1() Element of the carrier of (f,f)
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
e is set
x is set
[e,x] is V1() set
{e,x} is non empty set
{e} is non empty set
{{e,x},{e}} 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 upper Element of bool the carrier of f
y1 is upper 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
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
q is Element of the carrier of (f,f)
D9 is Element of the carrier of (f,f)
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 non empty RelStr
the carrier of D2 is non empty set
D1 is non empty RelStr
the carrier of D1 is non empty set
[: the carrier of D2, the carrier of D1:] is non empty Relation-like 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 Element of the carrier of D1
e is Element of the carrier of D1
x is Element of the carrier of D2
d is Element of the carrier of D2
f is non empty V55() reflexive RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty V55() reflexive RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict V55() reflexive RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
the Element of y1 is Element of y1
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,q, the Element of y1) is V1() Element of the carrier of (f,f)
{q, the Element of y1} is non empty set
{q} is non empty set
{{q, the Element of y1},{q}} is non empty set
(f,f,D9, the Element of y1) is V1() Element of the carrier of (f,f)
{D9, the Element of y1} is non empty set
{D9} is non empty set
{{D9, the Element of y1},{D9}} is non empty set
the Element of c₃ is Element of c₃
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f, the Element of c₃,q) is V1() Element of the carrier of (f,f)
{ the Element of c₃,q} is non empty set
{ the Element of c₃} is non empty set
{{ the Element of c₃,q},{ the Element of c₃}} is non empty set
(f,f, the Element of c₃,D9) is V1() Element of the carrier of (f,f)
{ the Element of c₃,D9} is non empty set
{{ the Element of c₃,D9},{ the Element of c₃}} 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
bool the carrier of (f,f) is non empty set
c₃ is non empty upper Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
D1 is Element of the carrier of f
D2 is Element of the carrier of f
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 is non empty Element of bool the carrier of f
D1 is Element of D9
(f,f,D1,D1) is V1() Element of the carrier of (f,f)
{D1,D1} is non empty set
{{D1,D1},{D1}} is non empty set
(f,f,D2,D1) is V1() Element of the carrier of (f,f)
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
D9 is Element of the carrier of f
D1 is Element of the carrier of f
D2 is set
[D2,D9] is V1() set
{D2,D9} is non empty set
{D2} is non empty set
{{D2,D9},{D2}} is non empty set
q is non empty Element of bool the carrier of f
D2 is Element of q
(f,f,D2,D9) is V1() Element of the carrier of (f,f)
{D2,D9} is non empty set
{D2} is non empty set
{{D2,D9},{D2}} is non empty set
(f,f,D2,D1) is V1() Element of the carrier of (f,f)
{D2,D1} is non empty set
{{D2,D1},{D2}} 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 lower Element of bool the carrier of f
y1 is lower 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
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
q is Element of the carrier of (f,f)
D9 is Element of the carrier of (f,f)
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 non empty RelStr
the carrier of D2 is non empty set
D1 is non empty RelStr
the carrier of D1 is non empty set
[: the carrier of D2, the carrier of D1:] is non empty Relation-like 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
e is Element of the carrier of D1
y is Element of the carrier of D1
d is Element of the carrier of D2
x is Element of the carrier of D2
f is non empty V55() reflexive RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty V55() reflexive RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict V55() reflexive RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
the Element of y1 is Element of y1
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,q, the Element of y1) is V1() Element of the carrier of (f,f)
{q, the Element of y1} is non empty set
{q} is non empty set
{{q, the Element of y1},{q}} is non empty set
(f,f,D9, the Element of y1) is V1() Element of the carrier of (f,f)
{D9, the Element of y1} is non empty set
{D9} is non empty set
{{D9, the Element of y1},{D9}} is non empty set
the Element of c₃ is Element of c₃
q is Element of the carrier of f
D9 is Element of the carrier of f
(f,f, the Element of c₃,q) is V1() Element of the carrier of (f,f)
{ the Element of c₃,q} is non empty set
{ the Element of c₃} is non empty set
{{ the Element of c₃,q},{ the Element of c₃}} is non empty set
(f,f, the Element of c₃,D9) is V1() Element of the carrier of (f,f)
{ the Element of c₃,D9} is non empty set
{{ the Element of c₃,D9},{ the Element of c₃}} 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
bool the carrier of (f,f) is non empty set
c₃ is non empty lower Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
D1 is Element of the carrier of f
D2 is Element of the carrier of f
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 is non empty Element of bool the carrier of f
D1 is Element of D9
(f,f,D2,D1) is V1() Element of the carrier of (f,f)
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
(f,f,D1,D1) is V1() Element of the carrier of (f,f)
{D1,D1} is non empty set
{{D1,D1},{D1}} is non empty set
D9 is Element of the carrier of f
D1 is Element of the carrier of f
D2 is set
[D2,D9] is V1() set
{D2,D9} is non empty set
{D2} is non empty set
{{D2,D9},{D2}} is non empty set
q is non empty Element of bool the carrier of f
D2 is Element of q
(f,f,D2,D1) is V1() Element of the carrier of (f,f)
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
(f,f,D2,D9) is V1() Element of the carrier of (f,f)
{D2,D9} is non empty set
{{D2,D9},{D2}} is non empty set
f is RelStr
f is empty trivial V46() V51( {} ) RelStr
the InternalRel of f is empty Relation-like non-empty empty-yielding 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 empty trivial Relation-like non-empty empty-yielding V31() 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
the non empty strict V55() reflexive transitive antisymmetric RelStr is non empty strict V55() reflexive transitive antisymmetric RelStr
the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr is non empty set
the InternalRel of the non empty strict V55() reflexive transitive antisymmetric RelStr is Relation-like the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr -defined the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr -valued V17( the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr ) reflexive antisymmetric transitive Element of bool [: the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr , the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr :]
[: the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr , the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr :] is non empty Relation-like set
bool [: the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr , the carrier of the non empty strict V55() reflexive transitive antisymmetric RelStr :] is non empty set
f is set
f is RelStr
f is RelStr
f is non empty V55() reflexive RelStr
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 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 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 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
c₃ is set
f is non empty () 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 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
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
the Element of y1 is Element of y1
D1 is Element of the carrier of f
(f,f,D1, the Element of y1) is V1() Element of the carrier of (f,f)
{D1, the Element of y1} is non empty set
{D1} is non empty set
{{D1, the Element of y1},{D1}} is non empty set
the Element of c₃ is Element of c₃
D1 is Element of the carrier of f
(f,f, the Element of c₃,D1) is V1() Element of the carrier of (f,f)
{ the Element of c₃,D1} is non empty set
{ the Element of c₃} is non empty set
{{ the Element of c₃,D1},{ the Element of c₃}} is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict RelStr
c₃ is Element of bool the carrier of f
y1 is Element of bool the carrier of f
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
D9 is Element of the carrier of (f,f)
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 Element of the carrier of f
D2 is Element of the carrier of f
f is non empty RelStr
f is non empty RelStr
(f,f) is non empty strict RelStr
the carrier of (f,f) is non empty set
bool 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
c₃ is Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
bool the carrier of f is non empty set
y1 is Element of the carrier of f
C2 is Element of the carrier of f
(f,f,y1,C2) is V1() Element of the carrier of (f,f)
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
D1 is Element of the carrier of f
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 non empty Element of bool the carrier of f
D1 is Element of D2
(f,f,D1,D1) is V1() Element of the carrier of (f,f)
{D1,D1} is non empty set
{{D1,D1},{D1}} is non empty set
D1 is Element of the carrier of f
D2 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
D2 is non empty Element of bool the carrier of f
D1 is Element of D2
(f,f,D1,D1) is V1() Element of the carrier of (f,f)
{D1,D1} is non empty set
{D1} is non empty set
{{D1,D1},{D1}} is non empty set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
[: 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
bool the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
the Element of y1 is Element of y1
D1 is Element of the carrier of f
(f,f,D1, the Element of y1) is V1() Element of the carrier of (f,f)
{D1, the Element of y1} is non empty set
{D1} is non empty set
{{D1, the Element of y1},{D1}} is non empty set
the Element of c₃ is Element of c₃
D1 is Element of the carrier of f
(f,f, the Element of c₃,D1) is V1() Element of the carrier of (f,f)
{ the Element of c₃,D1} is non empty set
{ the Element of c₃} is non empty set
{{ the Element of c₃,D1},{ the Element of c₃}} is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict RelStr
c₃ is Element of bool the carrier of f
y1 is Element of bool the carrier of f
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
D9 is Element of the carrier of (f,f)
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 Element of the carrier of f
D2 is Element of the carrier of f
f is non empty RelStr
f is non empty RelStr
(f,f) is non empty strict RelStr
the carrier of (f,f) is non empty set
bool 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
c₃ is Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
bool the carrier of f is non empty set
y1 is Element of the carrier of f
C2 is Element of the carrier of f
(f,f,y1,C2) is V1() Element of the carrier of (f,f)
{y1,C2} is non empty set
{y1} is non empty set
{{y1,C2},{y1}} is non empty set
D1 is Element of the carrier of f
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 non empty Element of bool the carrier of f
D1 is Element of D2
(f,f,D1,D1) is V1() Element of the carrier of (f,f)
{D1,D1} is non empty set
{{D1,D1},{D1}} is non empty set
D1 is Element of the carrier of f
D2 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
D2 is non empty Element of bool the carrier of f
D1 is Element of D2
(f,f,D1,D1) is V1() Element of the carrier of (f,f)
{D1,D1} is non empty set
{D1} is non empty set
{{D1,D1},{D1}} is non empty set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
[: the carrier of f, the carrier of f:] is non empty Relation-like set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
c₃ is Element of bool the carrier of f
y1 is Element of bool the carrier of f
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
"\/" (y1,f) is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,D9,("\/" (y1,f))) is V1() Element of the carrier of (f,f)
{D9,("\/" (y1,f))} is non empty set
{D9} is non empty set
{{D9,("\/" (y1,f))},{D9}} is non empty set
"\/" (c₃,f) is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,("\/" (c₃,f)),D9) is V1() Element of the carrier of (f,f)
{("\/" (c₃,f)),D9} is non empty set
{("\/" (c₃,f))} is non empty set
{{("\/" (c₃,f)),D9},{("\/" (c₃,f))}} is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
c₃ is Element of bool the carrier of f
y1 is Element of bool the carrier of f
(f,f,c₃,y1) is Relation-like Element of bool the carrier of (f,f)
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
"/\" (y1,f) is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,D9,("/\" (y1,f))) is V1() Element of the carrier of (f,f)
{D9,("/\" (y1,f))} is non empty set
{D9} is non empty set
{{D9,("/\" (y1,f))},{D9}} is non empty set
"/\" (c₃,f) is Element of the carrier of f
D9 is Element of the carrier of f
(f,f,("/\" (c₃,f)),D9) is V1() Element of the carrier of (f,f)
{("/\" (c₃,f)),D9} is non empty set
{("/\" (c₃,f))} is non empty set
{{("/\" (c₃,f)),D9},{("/\" (c₃,f))}} is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
D9 is Element of the carrier of (f,f)
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,D9) is Element of the carrier of f
(f,f,D9) is Element of the carrier of f
(f,f,(f,f,D9),(f,f,D9)) is V1() Element of the carrier of (f,f)
{(f,f,D9),(f,f,D9)} is non empty set
{(f,f,D9)} is non empty set
{{(f,f,D9),(f,f,D9)},{(f,f,D9)}} 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
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,C2,q) is V1() Element of the carrier of (f,f)
{C2,q} is non empty set
{C2} is non empty set
{{C2,q},{C2}} is non empty set
D9 is Element of the carrier of (f,f)
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,D9) is Element of the carrier of f
(f,f,D9) is Element of the carrier of f
(f,f,(f,f,D9),(f,f,D9)) is V1() Element of the carrier of (f,f)
{(f,f,D9),(f,f,D9)} is non empty set
{(f,f,D9)} is non empty set
{{(f,f,D9),(f,f,D9)},{(f,f,D9)}} 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
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,q,C2) is V1() Element of the carrier of (f,f)
{q,C2} is non empty set
{q} is non empty set
{{q,C2},{q}} is non empty set
D9 is V1() Element of the carrier of (f,f)
D1 is Element of the carrier of (f,f)
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,D1) is Element of the carrier of f
(f,f,D1) is Element of the carrier of f
(f,f,(f,f,D1),(f,f,D1)) is V1() Element of the carrier of (f,f)
{(f,f,D1),(f,f,D1)} is non empty set
{(f,f,D1)} is non empty set
{{(f,f,D1),(f,f,D1)},{(f,f,D1)}} is non empty set
D9 is Element of the carrier of (f,f)
C2 is Element of the carrier of (f,f)
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,C2) is Element of the carrier of f
(f,f,C2) is Element of the carrier of f
(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
q is Element of the carrier of f
(f,f,q,(f,f,C2)) is V1() Element of the carrier of (f,f)
{q,(f,f,C2)} is non empty set
{q} is non empty set
{{q,(f,f,C2)},{q}} is non empty set
q is Element of the carrier of f
(f,f,(f,f,C2),q) is V1() Element of the carrier of (f,f)
{(f,f,C2),q} is non empty set
{{(f,f,C2),q},{(f,f,C2)}} is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
c₃ is non empty Element of bool the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
C2 is Element of the carrier of f
q is Element of the carrier of f
(f,f,q,C2) is V1() Element of the carrier of (f,f)
{q,C2} is non empty set
{q} is non empty set
{{q,C2},{q}} is non empty set
D9 is V1() Element of the carrier of (f,f)
D1 is Element of the carrier of (f,f)
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,D1) is Element of the carrier of f
(f,f,D1) is Element of the carrier of f
(f,f,(f,f,D1),(f,f,D1)) is V1() Element of the carrier of (f,f)
{(f,f,D1),(f,f,D1)} is non empty set
{(f,f,D1)} is non empty set
{{(f,f,D1),(f,f,D1)},{(f,f,D1)}} is non empty set
D9 is Element of the carrier of (f,f)
C2 is Element of the carrier of (f,f)
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,C2) is Element of the carrier of f
(f,f,C2) is Element of the carrier of f
(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
q is Element of the carrier of f
(f,f,q,(f,f,C2)) is V1() Element of the carrier of (f,f)
{q,(f,f,C2)} is non empty set
{q} is non empty set
{{q,(f,f,C2)},{q}} is non empty set
q is Element of the carrier of f
(f,f,(f,f,C2),q) is V1() Element of the carrier of (f,f)
{(f,f,C2),q} is non empty set
{{(f,f,C2),q},{(f,f,C2)}} is non empty set
f is non empty antisymmetric RelStr
f is non empty antisymmetric RelStr
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
c₃ is Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
y1 is Element of the carrier of f
C2 is Element of the carrier of f
(f,f,C2,y1) is V1() Element of the carrier of (f,f)
{C2,y1} is non empty set
{C2} is non empty set
{{C2,y1},{C2}} is non empty set
q is V1() Element of the carrier of (f,f)
D9 is Element of the carrier of (f,f)
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 Element of the carrier of f
D2 is Element of the carrier of f
D9 is Element of the carrier of (f,f)
(f,f,D9) is Element of the carrier of f
(f,f,D9) is Element of the carrier of f
(f,f,(f,f,D9),(f,f,D9)) is V1() Element of the carrier of (f,f)
{(f,f,D9),(f,f,D9)} is non empty set
{(f,f,D9)} is non empty set
{{(f,f,D9),(f,f,D9)},{(f,f,D9)}} is non empty set
y1 is Element of the carrier of (f,f)
y1 is Element of the carrier of (f,f)
(f,f,y1) is Element of the carrier of f
(f,f,y1) is Element of the carrier of 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
C2 is Element of the carrier of f
(f,f,C2,(f,f,y1)) is V1() Element of the carrier of (f,f)
{C2,(f,f,y1)} is non empty set
{C2} is non empty set
{{C2,(f,f,y1)},{C2}} is non empty set
C2 is Element of the carrier of f
(f,f,(f,f,y1),C2) is V1() Element of the carrier of (f,f)
{(f,f,y1),C2} is non empty set
{{(f,f,y1),C2},{(f,f,y1)}} is non empty set
f is non empty antisymmetric RelStr
f is non empty antisymmetric RelStr
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
c₃ is Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
y1 is Element of the carrier of f
C2 is Element of the carrier of f
(f,f,C2,y1) is V1() Element of the carrier of (f,f)
{C2,y1} is non empty set
{C2} is non empty set
{{C2,y1},{C2}} is non empty set
q is V1() Element of the carrier of (f,f)
D9 is Element of the carrier of (f,f)
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 Element of the carrier of f
D2 is Element of the carrier of f
D9 is Element of the carrier of (f,f)
(f,f,D9) is Element of the carrier of f
(f,f,D9) is Element of the carrier of f
(f,f,(f,f,D9),(f,f,D9)) is V1() Element of the carrier of (f,f)
{(f,f,D9),(f,f,D9)} is non empty set
{(f,f,D9)} is non empty set
{{(f,f,D9),(f,f,D9)},{(f,f,D9)}} is non empty set
y1 is Element of the carrier of (f,f)
y1 is Element of the carrier of (f,f)
(f,f,y1) is Element of the carrier of f
(f,f,y1) is Element of the carrier of 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
C2 is Element of the carrier of f
(f,f,C2,(f,f,y1)) is V1() Element of the carrier of (f,f)
{C2,(f,f,y1)} is non empty set
{C2} is non empty set
{{C2,(f,f,y1)},{C2}} is non empty set
C2 is Element of the carrier of f
(f,f,(f,f,y1),C2) is V1() Element of the carrier of (f,f)
{(f,f,y1),C2} is non empty set
{{(f,f,y1),C2},{(f,f,y1)}} is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
c₃ is non empty Element of bool the carrier of f
"\/" (c₃,f) is Element of the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
"\/" ((f,f,c₃,y1),(f,f)) is Element of the carrier of (f,f)
"\/" (y1,f) is Element of the carrier of f
(f,f,("\/" (c₃,f)),("\/" (y1,f))) is V1() Element of the carrier of (f,f)
{("\/" (c₃,f)),("\/" (y1,f))} is non empty set
{("\/" (c₃,f))} is non empty set
{{("\/" (c₃,f)),("\/" (y1,f))},{("\/" (c₃,f))}} is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like 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
D2 is Element of the carrier of f
D1 is Element of the carrier of f
(f,f,D2,D1) is V1() Element of the carrier of (f,f)
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
D2 is Element of the carrier of (f,f)
D2 is Element of the carrier of f
D2 is Element of the carrier of f
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f) is non empty strict antisymmetric RelStr
c₃ is non empty Element of bool the carrier of f
"/\" (c₃,f) is Element of the carrier of f
y1 is non empty Element of bool the carrier of f
(f,f,c₃,y1) is non empty Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
"/\" ((f,f,c₃,y1),(f,f)) is Element of the carrier of (f,f)
"/\" (y1,f) is Element of the carrier of f
(f,f,("/\" (c₃,f)),("/\" (y1,f))) is V1() Element of the carrier of (f,f)
{("/\" (c₃,f)),("/\" (y1,f))} is non empty set
{("/\" (c₃,f))} is non empty set
{{("/\" (c₃,f)),("/\" (y1,f))},{("/\" (c₃,f))}} is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like 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
D2 is Element of the carrier of f
D1 is Element of the carrier of f
(f,f,D2,D1) is V1() Element of the carrier of (f,f)
{D2,D1} is non empty set
{D2} is non empty set
{{D2,D1},{D2}} is non empty set
D2 is Element of the carrier of (f,f)
D2 is Element of the carrier of f
D2 is Element of the carrier of f
f is non empty antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() RelStr
f is non empty antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() RelStr
(f,f) is non empty strict antisymmetric with_suprema with_infima RelStr
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
y1 is Element of bool the carrier of (f,f)
(f,f,y1) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,y1) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty antisymmetric lower-bounded RelStr
f is non empty antisymmetric lower-bounded RelStr
(f,f) is non empty strict antisymmetric RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
c₃ is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
the non empty Element of bool the carrier of f is non empty Element of bool the carrier of f
(f,f,c₃, the non empty Element of bool the carrier of f) is Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
the carrier of f is non empty set
bool the carrier of f is non empty set
c₃ is Element of bool the carrier of f
the non empty Element of bool the carrier of f is non empty Element of bool the carrier of f
(f,f, the non empty Element of bool the carrier of f,c₃) is Relation-like Element of bool the carrier of (f,f)
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
f is non empty antisymmetric RelStr
f is non empty antisymmetric RelStr
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
c₃ is non empty Element of bool the carrier of (f,f)
"\/" (c₃,(f,f)) is Element of the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
"\/" ((f,f,c₃),f) is Element of the carrier of f
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
"\/" ((f,f,c₃),f) is Element of the carrier of f
(f,f,("\/" ((f,f,c₃),f)),("\/" ((f,f,c₃),f))) is V1() Element of the carrier of (f,f)
{("\/" ((f,f,c₃),f)),("\/" ((f,f,c₃),f))} is non empty set
{("\/" ((f,f,c₃),f))} is non empty set
{{("\/" ((f,f,c₃),f)),("\/" ((f,f,c₃),f))},{("\/" ((f,f,c₃),f))}} is non empty set
y1 is non empty set
C2 is non empty set
[:y1,C2:] is non empty Relation-like 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
bool [:y1,C2:] is non empty set
D2 is non empty Relation-like y1 -defined C2 -valued Element of bool [:y1,C2:]
proj1 D2 is non empty set
proj2 D2 is non empty set
D2 is non empty Element of bool the carrier of f
D1 is non empty Element of bool the carrier of f
(f,f,D2,D1) is non empty Relation-like Element of bool the carrier of (f,f)
"\/" ((f,f,D2,D1),(f,f)) is Element of the carrier of (f,f)
d is Element of the carrier of f
e is Element of the carrier of f
y 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
x is Element of D2
D1 is Element of the carrier of f
(f,f,D1,d) is V1() Element of the carrier of (f,f)
{D1,d} is non empty set
{D1} is non empty set
{{D1,d},{D1}} is non empty set
y is Element of the carrier of f
(f,f,y,e) is V1() Element of the carrier of (f,f)
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
"\/" (D1,f) is Element of the carrier of f
D1 is Element of the carrier of f
e is Element of the carrier of f
y is set
[e,y] is V1() set
{e,y} is non empty set
{e} is non empty set
{{e,y},{e}} is non empty set
x is Element of D1
(f,f,D1,d) is V1() Element of the carrier of (f,f)
{D1,d} is non empty set
{D1} is non empty set
{{D1,d},{D1}} is non empty set
y is Element of the carrier of f
(f,f,e,y) is V1() Element of the carrier of (f,f)
{e,y} is non empty set
{{e,y},{e}} is non empty set
"\/" (D2,f) is Element of the carrier of f
(f,f,("\/" (D2,f)),("\/" (D1,f))) is V1() Element of the carrier of (f,f)
{("\/" (D2,f)),("\/" (D1,f))} is non empty set
{("\/" (D2,f))} is non empty set
{{("\/" (D2,f)),("\/" (D1,f))},{("\/" (D2,f))}} is non empty set
f is non empty antisymmetric RelStr
f is non empty antisymmetric RelStr
(f,f) is non empty strict antisymmetric RelStr
the carrier of (f,f) is non empty set
bool the carrier of (f,f) is non empty set
c₃ is non empty Element of bool the carrier of (f,f)
"/\" (c₃,(f,f)) is Element of the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
"/\" ((f,f,c₃),f) is Element of the carrier of f
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
"/\" ((f,f,c₃),f) is Element of the carrier of f
(f,f,("/\" ((f,f,c₃),f)),("/\" ((f,f,c₃),f))) is V1() Element of the carrier of (f,f)
{("/\" ((f,f,c₃),f)),("/\" ((f,f,c₃),f))} is non empty set
{("/\" ((f,f,c₃),f))} is non empty set
{{("/\" ((f,f,c₃),f)),("/\" ((f,f,c₃),f))},{("/\" ((f,f,c₃),f))}} is non empty set
y1 is non empty set
C2 is non empty set
[:y1,C2:] is non empty Relation-like 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
bool [:y1,C2:] is non empty set
D2 is non empty Relation-like y1 -defined C2 -valued Element of bool [:y1,C2:]
proj1 D2 is non empty set
proj2 D2 is non empty set
D2 is non empty Element of bool the carrier of f
D1 is non empty Element of bool the carrier of f
(f,f,D2,D1) is non empty Relation-like Element of bool the carrier of (f,f)
"/\" ((f,f,D2,D1),(f,f)) is Element of the carrier of (f,f)
d is Element of the carrier of f
e is Element of the carrier of f
y 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
x is Element of D2
D1 is Element of the carrier of f
(f,f,D1,d) is V1() Element of the carrier of (f,f)
{D1,d} is non empty set
{D1} is non empty set
{{D1,d},{D1}} is non empty set
y is Element of the carrier of f
(f,f,y,e) is V1() Element of the carrier of (f,f)
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
"/\" (D1,f) is Element of the carrier of f
D1 is Element of the carrier of f
e is Element of the carrier of f
y is set
[e,y] is V1() set
{e,y} is non empty set
{e} is non empty set
{{e,y},{e}} is non empty set
x is Element of D1
(f,f,D1,d) is V1() Element of the carrier of (f,f)
{D1,d} is non empty set
{D1} is non empty set
{{D1,d},{D1}} is non empty set
y is Element of the carrier of f
(f,f,e,y) is V1() Element of the carrier of (f,f)
{e,y} is non empty set
{{e,y},{e}} is non empty set
"/\" (D2,f) is Element of the carrier of f
(f,f,("/\" (D2,f)),("/\" (D1,f))) is V1() Element of the carrier of (f,f)
{("/\" (D2,f)),("/\" (D1,f))} is non empty set
{("/\" (D2,f))} is non empty set
{{("/\" (D2,f)),("/\" (D1,f))},{("/\" (D2,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
bool the carrier of (f,f) is non empty set
c₃ is non empty directed Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
downarrow c₃ is non empty Element of bool the carrier of (f,f)
q is set
y1 is non empty set
C2 is non empty set
[:y1,C2:] is non empty Relation-like set
bool [:y1,C2:] is non empty set
{ b₁ where b₁ is Element of the carrier of (f,f) : ex b₂ being Element of the carrier of (f,f) st
( b₁ <= b₂ & b₂ in c₃ ) } is set
D9 is non empty Relation-like y1 -defined C2 -valued Element of bool [:y1,C2:]
proj2 D9 is non empty set
proj1 D9 is non empty set
D1 is non empty Element of bool the carrier of f
D2 is non empty Element of bool the carrier of f
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
y is set
[d,y] is V1() set
{d,y} is non empty set
{{d,y},{d}} is non empty set
x is set
[x,e] is V1() set
{x,e} is non empty set
{x} is non empty set
{{x,e},{x}} is non empty set
d is Element of D1
y is Element of D2
(f,f,d,y) is V1() Element of the carrier of (f,f)
{d,y} is non empty set
{d} is non empty set
{{d,y},{d}} is non empty set
x is Element of D1
e is Element of D2
(f,f,x,e) is V1() Element of the carrier of (f,f)
{x,e} is non empty set
{x} is non empty set
{{x,e},{x}} is non empty set
z is Element of the carrier of (f,f)
z1 is set
z2 is set
[z1,z2] is V1() set
{z1,z2} is non empty set
{z1} is non empty set
{{z1,z2},{z1}} is non empty set
z1 is Element of D1
z2 is Element of D2
(f,f,d,e) is V1() Element of the carrier of (f,f)
{d,e} is non empty set
{{d,e},{d}} is non empty set
(f,f,z1,z2) is V1() Element of the carrier of (f,f)
{z1,z2} is non empty set
{z1} is non empty set
{{z1,z2},{z1}} 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
bool the carrier of (f,f) is non empty set
c₃ is non empty filtered Element of bool the carrier of (f,f)
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,c₃) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f,f,(f,f,c₃),(f,f,c₃)) is Relation-like Element of bool the carrier of (f,f)
uparrow c₃ is non empty Element of bool the carrier of (f,f)
q is set
y1 is non empty set
C2 is non empty set
[:y1,C2:] is non empty Relation-like set
bool [:y1,C2:] is non empty set
{ b₁ where b₁ is Element of the carrier of (f,f) : ex b₂ being Element of the carrier of (f,f) st
( b₂ <= b₁ & b₂ in c₃ ) } is set
D9 is non empty Relation-like y1 -defined C2 -valued Element of bool [:y1,C2:]
proj2 D9 is non empty set
proj1 D9 is non empty set
D1 is non empty Element of bool the carrier of f
D2 is non empty Element of bool the carrier of f
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
y is set
[d,y] is V1() set
{d,y} is non empty set
{{d,y},{d}} is non empty set
x is set
[x,e] is V1() set
{x,e} is non empty set
{x} is non empty set
{{x,e},{x}} is non empty set
d is Element of D1
y is Element of D2
(f,f,d,y) is V1() Element of the carrier of (f,f)
{d,y} is non empty set
{d} is non empty set
{{d,y},{d}} is non empty set
x is Element of D1
e is Element of D2
(f,f,x,e) is V1() Element of the carrier of (f,f)
{x,e} is non empty set
{x} is non empty set
{{x,e},{x}} is non empty set
z is Element of the carrier of (f,f)
z1 is set
z2 is set
[z1,z2] is V1() set
{z1,z2} is non empty set
{z1} is non empty set
{{z1,z2},{z1}} is non empty set
z1 is Element of D1
z2 is Element of D2
(f,f,z1,z2) is V1() Element of the carrier of (f,f)
{z1,z2} is non empty set
{z1} is non empty set
{{z1,z2},{z1}} is non empty set
(f,f,d,e) is V1() Element of the carrier of (f,f)
{d,e} is non empty set
{{d,e},{d}} 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
F₃() is non empty RelStr
the carrier of F₃() is non empty set
(F₁(),F₂()) is non empty strict RelStr
the carrier of (F₁(),F₂()) is non empty set
[: the carrier of (F₁(),F₂()), the carrier of F₃():] is non empty Relation-like set
bool [: the carrier of (F₁(),F₂()), the carrier of F₃():] is non empty set
f is Element of the carrier of F₁()
f is Element of the carrier of F₂()
F₄(f,f) is set
c₃ is Element of the carrier of F₁()
y1 is Element of the carrier of F₂()
F₄(c₃,y1) is set
[: 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₃():] is non empty Relation-like set
bool [:[: the carrier of F₁(), the carrier of F₂():], the carrier of F₃():] is non empty set
f is Relation-like [: the carrier of F₁(), the carrier of F₂():] -defined the carrier of F₃() -valued V12() V18([: the carrier of F₁(), the carrier of F₂():], the carrier of F₃()) Element of bool [:[: the carrier of F₁(), the carrier of F₂():], the carrier of F₃():]
f is Relation-like the carrier of (F₁(),F₂()) -defined the carrier of F₃() -valued V12() V18( the carrier of (F₁(),F₂()), the carrier of F₃()) Element of bool [: the carrier of (F₁(),F₂()), the carrier of F₃():]
c₃ is Element of the carrier of F₁()
y1 is Element of the carrier of F₂()
f . (c₃,y1) is set
F₄(c₃,y1) is set