:: 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

1 is non empty set
{{},1} is non empty set
bool K219() is non empty set
F1() is non empty set
{ F2(b1,b2) where b1, b2 is Element of F1() : P1[b1,b2] } is set
bool F1() is non empty set
f is set
f is Element of F1()
c3 is Element of F1()
F2(f,c3) is set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set

downarrow f is Element of bool the carrier of f
c3 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
c3 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
c3 is Relation-like f -defined f -valued Element of bool [:f,f:]
proj1 c3 is set
proj2 c3 is set
[:(proj1 c3),(proj2 c3):] 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
c3 is set
[f,c3] is V1() set
{f,c3} is non empty set
{f} is non empty set
{{f,c3},{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,c3],[y1,C2]] is V1() set
{[f,c3],[y1,C2]} is non empty Relation-like set
{[f,c3]} is non empty Relation-like set
{{[f,c3],[y1,C2]},{[f,c3]}} 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

the carrier of f is non empty set
f is Element of the carrier of f
y1 is Element of the carrier of f
c3 is Element of the carrier of f
C2 is Element of the carrier of f
f "/\" c3 is Element of the carrier of f
y1 "/\" C2 is Element of the carrier of f
{f,c3} 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

the carrier of f is non empty set
f is Element of the carrier of f
y1 is Element of the carrier of f
c3 is Element of the carrier of f
C2 is Element of the carrier of f
f "\/" c3 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

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
c3 is Element of the carrier of f
("\/" (f,f)) "/\" c3 is Element of the carrier of f

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
c3 is Element of the carrier of f
("/\" (f,f)) "\/" c3 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
c3 is Element of bool the carrier of f
downarrow f is Element of bool the carrier of f
downarrow c3 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
c3 is Element of bool the carrier of f
uparrow f is Element of bool the carrier of f
uparrow c3 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

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
bool [: the carrier of f, the carrier of f:] is non empty set
c3 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
c3 . (y1 "/\" C2) is Element of the carrier of f
c3 . y1 is Element of the carrier of f
c3 . C2 is Element of the carrier of f
(c3 . y1) "/\" (c3 . C2) is Element of the carrier of f
dom c3 is Element of bool the carrier of f
"/\" ({y1,C2},f) is Element of the carrier of f
c3 . ("/\" ({y1,C2},f)) is Element of the carrier of f
c3 .: {y1,C2} is Element of bool the carrier of f
bool the carrier of f is non empty set
"/\" ((c3 .: {y1,C2}),f) is Element of the carrier of f
{(c3 . y1),(c3 . C2)} is non empty Element of bool the carrier of f
"/\" ({(c3 . y1),(c3 . C2)},f) is Element of the carrier of f

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
bool [: the carrier of f, the carrier of f:] is non empty set
c3 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
c3 . (y1 "\/" C2) is Element of the carrier of f
c3 . y1 is Element of the carrier of f
c3 . C2 is Element of the carrier of f
(c3 . y1) "\/" (c3 . C2) is Element of the carrier of f
dom c3 is Element of bool the carrier of f
"\/" ({y1,C2},f) is Element of the carrier of f
c3 . ("\/" ({y1,C2},f)) is Element of the carrier of f
c3 .: {y1,C2} is Element of bool the carrier of f
bool the carrier of f is non empty set
"\/" ((c3 .: {y1,C2}),f) is Element of the carrier of f
{(c3 . y1),(c3 . C2)} is non empty Element of bool the carrier of f
"\/" ({(c3 . y1),(c3 . C2)},f) is Element of the carrier of f

the carrier of F1() is non empty set
bool the carrier of F1() is non empty set
{ b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"/\" ((union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } ),F1()) is Element of the carrier of F1()
{ ("/\" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"/\" ( { ("/\" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } ,F1()) is Element of the carrier of F1()
f is Element of the carrier of F1()
f is Element of bool the carrier of F1()
"/\" (f,F1()) is Element of the carrier of F1()

the carrier of F1() is non empty set
bool the carrier of F1() is non empty set
{ ("/\" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"/\" ( { ("/\" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } ,F1()) is Element of the carrier of F1()
{ b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"/\" ((union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } ),F1()) is Element of the carrier of F1()
f is Element of the carrier of F1()
f is set
c3 is Element of bool the carrier of F1()
"/\" (c3,F1()) is Element of the carrier of F1()

the carrier of F1() is non empty set
bool the carrier of F1() is non empty set
{ ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"\/" ( { ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } ,F1()) is Element of the carrier of F1()
{ b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"\/" ((union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } ),F1()) is Element of the carrier of F1()
f is Element of the carrier of F1()
f is Element of bool the carrier of F1()
"\/" (f,F1()) is Element of the carrier of F1()

the carrier of F1() is non empty set
bool the carrier of F1() is non empty set
{ ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"\/" ( { ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : P1[b1] } ,F1()) is Element of the carrier of F1()
{ b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } is set
"\/" ((union { b1 where b1 is Element of bool the carrier of F1() : P1[b1] } ),F1()) is Element of the carrier of F1()
f is Element of the carrier of F1()
f is set
c3 is Element of bool the carrier of F1()
"\/" (c3,F1()) is Element of the carrier of F1()

proj1 f is set
proj1 f is set
[:(),():] is Relation-like set
proj2 f is set
proj2 f is set
[:(),():] is Relation-like set
c3 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
c3 is Relation-like set
y1 is Relation-like set

(f,f) is Relation-like set
c3 is set
c3 `1 is set
(c3 `1) `1 is set
c3 `2 is set
(c3 `2) `1 is set
[((c3 `1) `1),((c3 `2) `1)] is V1() set
{((c3 `1) `1),((c3 `2) `1)} is non empty set
{((c3 `1) `1)} is non empty set
{{((c3 `1) `1),((c3 `2) `1)},{((c3 `1) `1)}} is non empty set
(c3 `1) `2 is set
(c3 `2) `2 is set
[((c3 `1) `2),((c3 `2) `2)] is V1() set
{((c3 `1) `2),((c3 `2) `2)} is non empty set
{((c3 `1) `2)} is non empty set
{{((c3 `1) `2),((c3 `2) `2)},{((c3 `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,((c3 `2) `1)] is V1() set
{y1,((c3 `2) `1)} is non empty set
{{y1,((c3 `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,((c3 `2) `2)] is V1() set
{C2,((c3 `2) `2)} is non empty set
{C2} is non empty set
{{C2,((c3 `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
c3 is set
y1 is set
[:c3,y1:] is Relation-like set
bool [:c3,y1:] is non empty set
C2 is Relation-like f -defined f -valued Element of bool [:f,f:]
q is Relation-like c3 -defined y1 -valued Element of bool [:c3,y1:]
(C2,q) is Relation-like set
[:f,c3:] is Relation-like set
[:f,y1:] is Relation-like set
[:[:f,c3:],[:f,y1:]:] is Relation-like set
bool [:[:f,c3:],[: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
c3 is strict RelStr
the carrier of c3 is set
the InternalRel of c3 is Relation-like the carrier of c3 -defined the carrier of c3 -valued Element of bool [: the carrier of c3, the carrier of c3:]
[: the carrier of c3, the carrier of c3:] is Relation-like set
bool [: the carrier of c3, the carrier of c3:] 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
c3 is Element of bool the carrier of (f,f)
proj1 c3 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 c3 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
c3 is Element of bool the carrier of f
y1 is Element of bool the carrier of f
[:c3,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
[:c3,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
c3 is Element of the carrier of f
y1 is Element of the carrier of f
[c3,y1] is V1() set
{c3,y1} is non empty set
{c3} is non empty set
{{c3,y1},{c3}} 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
c3 is Element of the carrier of (f,f)
c3 `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
c3 `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
c3 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,c3,C2) is V1() Element of the carrier of (f,f)
the carrier of (f,f) is set
{c3,C2} is non empty set
{c3} is non empty set
{{c3,C2},{c3}} 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,c3,C2),(f,f,y1,q)] is V1() set
{(f,f,c3,C2),(f,f,y1,q)} is non empty Relation-like set
{(f,f,c3,C2)} is non empty Relation-like set
{{(f,f,c3,C2),(f,f,y1,q)},{(f,f,c3,C2)}} is non empty set
[(f,f,c3,C2),(f,f,y1,q)] `1 is set
([(f,f,c3,C2),(f,f,y1,q)] `1) `1 is set
[(f,f,c3,C2),(f,f,y1,q)] `2 is set
([(f,f,c3,C2),(f,f,y1,q)] `2) `1 is set
([(f,f,c3,C2),(f,f,y1,q)] `1) `2 is set
([(f,f,c3,C2),(f,f,y1,q)] `2) `2 is set
[(([(f,f,c3,C2),(f,f,y1,q)] `1) `1),(([(f,f,c3,C2),(f,f,y1,q)] `2) `1)] is V1() set
{(([(f,f,c3,C2),(f,f,y1,q)] `1) `1),(([(f,f,c3,C2),(f,f,y1,q)] `2) `1)} is non empty set
{(([(f,f,c3,C2),(f,f,y1,q)] `1) `1)} is non empty set
{{(([(f,f,c3,C2),(f,f,y1,q)] `1) `1),(([(f,f,c3,C2),(f,f,y1,q)] `2) `1)},{(([(f,f,c3,C2),(f,f,y1,q)] `1) `1)}} is non empty set
[(([(f,f,c3,C2),(f,f,y1,q)] `1) `2),(([(f,f,c3,C2),(f,f,y1,q)] `2) `2)] is V1() set
{(([(f,f,c3,C2),(f,f,y1,q)] `1) `2),(([(f,f,c3,C2),(f,f,y1,q)] `2) `2)} is non empty set
{(([(f,f,c3,C2),(f,f,y1,q)] `1) `2)} is non empty set
{{(([(f,f,c3,C2),(f,f,y1,q)] `1) `2),(([(f,f,c3,C2),(f,f,y1,q)] `2) `2)},{(([(f,f,c3,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,c3,y1) is V1() Element of the carrier of (f,f)
(f,f) is strict RelStr
the carrier of (f,f) is set
{c3,y1} is non empty set
{{c3,y1},{c3}} 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
c3 is Element of the carrier of (f,f)
y1 is Element of the carrier of (f,f)
(f,f,c3) 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,c3) 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,c3),(f,f,c3)) is V1() Element of the carrier of (f,f)
{(f,f,c3),(f,f,c3)} is non empty set
{(f,f,c3)} is non empty set
{{(f,f,c3),(f,f,c3)},{(f,f,c3)}} 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
c3 is non empty RelStr
the carrier of c3 is non empty set
[: the carrier of (f,f), the carrier of c3:] is Relation-like set
bool [: the carrier of (f,f), the carrier of c3:] is non empty set
y1 is Relation-like the carrier of (f,f) -defined the carrier of c3 -valued V12() V18( the carrier of (f,f), the carrier of c3) Element of bool [: the carrier of (f,f), the carrier of c3:]
C2 is Relation-like the carrier of (f,f) -defined the carrier of c3 -valued V12() V18( the carrier of (f,f), the carrier of c3) Element of bool [: the carrier of (f,f), the carrier of c3:]
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
c3 is set
the carrier of (f,f) is set
[c3,c3] is V1() set
{c3,c3} is non empty set
{c3} is non empty set
{{c3,c3},{c3}} 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,f) is strict RelStr
c3 is set
the carrier of (f,f) is set
y1 is set
[c3,y1] is V1() set
{c3,y1} is non empty set
{c3} is non empty set
{{c3,y1},{c3}} 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,c3] is V1() set
{y1,c3} is non empty set
{y1} is non empty set
{{y1,c3},{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,c3] `1 is set
([y1,c3] `1) `1 is set
[y1,c3] `2 is set
([y1,c3] `2) `1 is set
[(([y1,c3] `1) `1),(([y1,c3] `2) `1)] is V1() set
{(([y1,c3] `1) `1),(([y1,c3] `2) `1)} is non empty set
{(([y1,c3] `1) `1)} is non empty set
{{(([y1,c3] `1) `1),(([y1,c3] `2) `1)},{(([y1,c3] `1) `1)}} is non empty set
y1 `1 is set
[(y1 `1),(([y1,c3] `2) `1)] is V1() set
{(y1 `1),(([y1,c3] `2) `1)} is non empty set
{(y1 `1)} is non empty set
{{(y1 `1),(([y1,c3] `2) `1)},{(y1 `1)}} is non empty set
c3 `1 is set
[(y1 `1),(c3 `1)] is V1() set
{(y1 `1),(c3 `1)} is non empty set
{{(y1 `1),(c3 `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,c3] `1) `2 is set
([y1,c3] `2) `2 is set
[(([y1,c3] `1) `2),(([y1,c3] `2) `2)] is V1() set
{(([y1,c3] `1) `2),(([y1,c3] `2) `2)} is non empty set
{(([y1,c3] `1) `2)} is non empty set
{{(([y1,c3] `1) `2),(([y1,c3] `2) `2)},{(([y1,c3] `1) `2)}} is non empty set
y1 `2 is set
[(y1 `2),(([y1,c3] `2) `2)] is V1() set
{(y1 `2),(([y1,c3] `2) `2)} is non empty set
{(y1 `2)} is non empty set
{{(y1 `2),(([y1,c3] `2) `2)},{(y1 `2)}} is non empty set
c3 `2 is set
[(y1 `2),(c3 `2)] is V1() set
{(y1 `2),(c3 `2)} is non empty set
{{(y1 `2),(c3 `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
[c3,y1] `1 is set
([c3,y1] `1) `2 is set
[c3,y1] `2 is set
([c3,y1] `2) `2 is set
[(([c3,y1] `1) `2),(([c3,y1] `2) `2)] is V1() set
{(([c3,y1] `1) `2),(([c3,y1] `2) `2)} is non empty set
{(([c3,y1] `1) `2)} is non empty set
{{(([c3,y1] `1) `2),(([c3,y1] `2) `2)},{(([c3,y1] `1) `2)}} is non empty set
[(c3 `2),(([c3,y1] `2) `2)] is V1() set
{(c3 `2),(([c3,y1] `2) `2)} is non empty set
{(c3 `2)} is non empty set
{{(c3 `2),(([c3,y1] `2) `2)},{(c3 `2)}} is non empty set
[(c3 `2),(y1 `2)] is V1() set
{(c3 `2),(y1 `2)} is non empty set
{{(c3 `2),(y1 `2)},{(c3 `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
([c3,y1] `1) `1 is set
([c3,y1] `2) `1 is set
[(([c3,y1] `1) `1),(([c3,y1] `2) `1)] is V1() set
{(([c3,y1] `1) `1),(([c3,y1] `2) `1)} is non empty set
{(([c3,y1] `1) `1)} is non empty set
{{(([c3,y1] `1) `1),(([c3,y1] `2) `1)},{(([c3,y1] `1) `1)}} is non empty set
[(c3 `1),(([c3,y1] `2) `1)] is V1() set
{(c3 `1),(([c3,y1] `2) `1)} is non empty set
{(c3 `1)} is non empty set
{{(c3 `1),(([c3,y1] `2) `1)},{(c3 `1)}} is non empty set
[(c3 `1),(y1 `1)] is V1() set
{(c3 `1),(y1 `1)} is non empty set
{{(c3 `1),(y1 `1)},{(c3 `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,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
c3 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
c3 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,c3, the Element of the carrier of f) is V1() Element of the carrier of (f,f)
{c3, the Element of the carrier of f} is non