:: YELLOW16 semantic presentation

K99() is Element of bool K95()
K95() is set
bool K95() is set
K54() is set
bool K54() is set
bool K99() is set

the carrier of I[01] is non empty set
K96() is set
K97() is set
K98() is set
[:K95(),K95():] is Relation-like set
bool [:K95(),K95():] is set
K404() is non empty V111() L9()
the carrier of K404() is non empty set
K409() is non empty V111() V133() V134() V135() V137() V187() V188() V189() V190() V191() V192() L9()
K410() is non empty V111() V135() V137() V190() V191() V192() M22(K409())
K411() is non empty V111() V133() V135() V137() V190() V191() V192() V193() M25(K409(),K410())
K413() is non empty V111() V133() V135() V137() L9()
K414() is non empty V111() V133() V135() V137() V193() M22(K413())

1 is non empty set
{{},1} is non empty set
K653() is set

K375() is M19()

K39(K375(),) is set

RelStr(# ,() #) is non empty trivial V60() 1 -element strict RelStr
{1} is non empty set

{0,1} is non empty set
{{},{1},{0,1}} is set
R is set
T is non empty RelStr
the carrier of T is non empty set
[:R, the carrier of T:] is Relation-like set
bool [:R, the carrier of T:] is set
S is non empty SubRelStr of T
the carrier of S is non empty set
[:R, the carrier of S:] is Relation-like set
bool [:R, the carrier of S:] is set
S is Relation-like R -defined the carrier of S -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of S:]
f is Relation-like R -defined the carrier of S -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of S:]
S is Relation-like R -defined the carrier of T -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of T:]
rf is Relation-like R -defined the carrier of T -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of T:]
x is set
S . x is set
rf . x is set
S . x is set
f . x is set
c9 is Element of the carrier of S
b is Element of the carrier of S
Xx is Element of the carrier of T
Xy is Element of the carrier of T
a9 is Element of the carrier of S
b9 is Element of the carrier of S
R is set
T is non empty RelStr
the carrier of T is non empty set
[:R, the carrier of T:] is Relation-like set
bool [:R, the carrier of T:] is set
S is non empty full SubRelStr of T
the carrier of S is non empty set
[:R, the carrier of S:] is Relation-like set
bool [:R, the carrier of S:] is set
S is Relation-like R -defined the carrier of S -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of S:]
f is Relation-like R -defined the carrier of S -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of S:]
S is Relation-like R -defined the carrier of T -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of T:]
rf is Relation-like R -defined the carrier of T -valued Function-like V24(R) quasi_total Element of bool [:R, the carrier of T:]
x is set
S . x is set
f . x is set
c9 is Element of the carrier of S
b is Element of the carrier of S
Xx is Element of the carrier of T
Xy is Element of the carrier of T
R is non empty RelStr
the carrier of R is non empty set
T is non empty reflexive antisymmetric RelStr
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
the Element of the carrier of T is Element of the carrier of T
R --> the Element of the carrier of T is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
the carrier of R --> the Element of the carrier of T is Relation-like the carrier of R -defined the carrier of T -valued Function-like constant non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
bool the carrier of R is set
f is Element of bool the carrier of R
S .: f is Element of bool the carrier of T
bool the carrier of T is set
{ the Element of the carrier of T} is non empty set
the Element of f is Element of f
dom S is non empty Element of bool the carrier of R
S . the Element of f is set
"\/" ((S .: f),T) is Element of the carrier of T
"\/" (f,R) is Element of the carrier of R
S . ("\/" (f,R)) is Element of the carrier of T
f is Element of the carrier of R
S is Element of the carrier of R
S . f is Element of the carrier of T
S . S is Element of the carrier of T

rng T is set
rng R is set
dom R is set

S is set
dom T is set
T . S is set
(T * R) . S is set
R . (T . S) is set
S is set
R . S is set
dom (T * R) is set
R is 1-sorted
the carrier of R is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id R is Relation-like the carrier of R -defined the carrier of R -valued Function-like V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
T is Relation-like the carrier of R -defined the carrier of R -valued Function-like V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
T * T is Relation-like the carrier of R -defined the carrier of R -valued Function-like V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

the carrier of T is non empty set
bool the carrier of T is set
the carrier of R is non empty set
bool the carrier of R is set
S is non empty directed Element of bool the carrier of T
S is non empty directed Element of bool the carrier of R

the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
T is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

rng T is non empty Element of bool the carrier of R
bool the carrier of R is set

the Element of the carrier of R is Element of the carrier of R
the carrier of (subrelstr (rng T)) is non empty set
bool the carrier of (subrelstr (rng T)) is set
S is directed Element of bool the carrier of (subrelstr (rng T))
"\/" (S,R) is Element of the carrier of R

the carrier of f is non empty set
bool the carrier of f is set
rf is non empty directed Element of bool the carrier of R
T .: rf is Element of bool the carrier of R
"\/" ((T .: rf),R) is Element of the carrier of R
"\/" (rf,R) is Element of the carrier of R
T . ("\/" (rf,R)) is Element of the carrier of R
R is non empty RelStr
the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
T is non empty SubRelStr of R
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
incl (T,R) is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total idempotent monotone isomorphic projection Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
S * (incl (T,R)) is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
(incl (T,R)) * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S * S is Relation-like the carrier of R -defined the carrier of T -valued Function-like Element of bool [: the carrier of R, the carrier of T:]
(id the carrier of T) * S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
dom S is non empty Element of bool the carrier of R
bool the carrier of R is set
rng S is non empty Element of bool the carrier of T
bool the carrier of T is set

incl (R,T) is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set

[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

(incl (R,T)) * S is Relation-like the carrier of R -defined Function-like set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set

(id the carrier of R) * S is Relation-like the carrier of R -defined Function-like set

the carrier of T is non empty set
the carrier of R is non empty set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set

[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
incl (R,T) is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of T:]

the carrier of R is non empty set

rng S is set
the carrier of T is non empty set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set
incl (R,T) is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
S * (incl (R,T)) is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set

id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

the carrier of R is non empty set

rng S is set
the carrier of T is non empty set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set

[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
f is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of T:]

the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set

the carrier of R is non empty set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set
incl (R,T) is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
(incl (R,T)) * S is Relation-like the carrier of R -defined Function-like set

[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set

the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the carrier of () is non empty set

the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set

S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
S | (rng S) is Relation-like the carrier of R -defined rng S -defined the carrier of R -defined the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
(S | (rng S)) * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
S | the carrier of T is Relation-like the carrier of R -defined the carrier of T -defined the carrier of R -defined the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
(S | the carrier of T) * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]

[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
(id T) * S is Relation-like the carrier of R -defined the carrier of T -valued Function-like Element of bool [: the carrier of R, the carrier of T:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of T:]
(id the carrier of T) * S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
incl (T,R) is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set
R is non empty reflexive transitive RelStr
the carrier of R is non empty set
T is non empty reflexive transitive RelStr
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set

[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]

S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
f is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
rng S is non empty Element of bool the carrier of T
bool the carrier of T is set
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
S * S is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
S * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
S * S is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
S * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set

[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone Element of bool [: the carrier of R, the carrier of T:]

f is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
rf is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone Element of bool [: the carrier of R, the carrier of T:]
rng S is non empty Element of bool the carrier of T
bool the carrier of T is set
x is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
S * x is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
x * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone Element of bool [: the carrier of R, the carrier of T:]
S * S is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
S * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
rng S is non empty Element of bool the carrier of T

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set

[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
id the carrier of R is Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone Element of bool [: the carrier of R, the carrier of T:]
S * S is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
S * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]

the carrier of R is non empty set

the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set

[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone Element of bool [: the carrier of R, the carrier of T:]
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone Element of bool [: the carrier of T, the carrier of R:]
S * S is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
S * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
(S * S) * (S * S) is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
(S * S) * S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
((S * S) * S) * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S * (id T) is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of R:]
(S * (id T)) * S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
dom S is non empty Element of bool the carrier of T
bool the carrier of T is set
rng S is non empty Element of bool the carrier of T
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone projection Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the carrier of () is non empty set
[: the carrier of T, the carrier of ():] is Relation-like set
bool [: the carrier of T, the carrier of ():] is set
corestr S is Relation-like the carrier of T -defined the carrier of () -valued Function-like non empty V24( the carrier of T) quasi_total onto monotone Element of bool [: the carrier of T, the carrier of ():]

rng S is non empty Element of bool the carrier of R

the carrier of () is non empty set
[: the carrier of T, the carrier of ():] is Relation-like set
bool [: the carrier of T, the carrier of ():] is set
the carrier of () |` S is Relation-like the carrier of T -defined the carrier of R -valued the carrier of () -valued the carrier of R -valued Function-like Element of bool [: the carrier of T, the carrier of R:]
rf is Relation-like the carrier of T -defined the carrier of () -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of ():]
x is Element of the carrier of T
c9 is Element of the carrier of T
S . x is Element of the carrier of R
S . c9 is Element of the carrier of R
rf . x is Element of the carrier of ()
rf . c9 is Element of the carrier of ()
(id T) . x is Element of the carrier of T
S . (S . x) is Element of the carrier of T
(id T) . c9 is Element of the carrier of T
S . (S . c9) is Element of the carrier of T
rng rf is non empty Element of bool the carrier of ()
bool the carrier of () is set
S | the carrier of () is Relation-like the carrier of R -defined the carrier of () -defined the carrier of R -defined the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]

[: the carrier of (), the carrier of ():] is Relation-like set
bool [: the carrier of (), the carrier of ():] is set
id the carrier of () is Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
inclusion S is Relation-like the carrier of () -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of ()) quasi_total monotone Element of bool [: the carrier of (), the carrier of R:]
[: the carrier of (), the carrier of R:] is Relation-like set
bool [: the carrier of (), the carrier of R:] is set
S * () is Relation-like the carrier of () -defined the carrier of R -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of R:]
corestr S is Relation-like the carrier of R -defined the carrier of () -valued Function-like non empty V24( the carrier of R) quasi_total onto monotone Element of bool [: the carrier of R, the carrier of ():]
[: the carrier of R, the carrier of ():] is Relation-like set
bool [: the carrier of R, the carrier of ():] is set
the carrier of () |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of () -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
() * () is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]

the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set

the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
[: the carrier of T, the carrier of R:] is Relation-like set
bool [: the carrier of T, the carrier of R:] is set

[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
S is Relation-like the carrier of T -defined the carrier of R -valued Function-like non empty V24( the carrier of T) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of T, the carrier of R:]

f is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of T:]
S * f is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone projection Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the carrier of () is non empty set
S | the carrier of () is Relation-like the carrier of R -defined the carrier of () -defined the carrier of R -defined the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]

[: the carrier of (), the carrier of ():] is Relation-like set
bool [: the carrier of (), the carrier of ():] is set
id the carrier of () is Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one non empty V24( the carrier of ()) quasi_total Element of bool [: the carrier of (), the carrier of ():]
rf is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of R, the carrier of R:]

rng rf is non empty Element of bool the carrier of R

the carrier of (Image rf) is non empty set
corestr rf is Relation-like the carrier of R -defined the carrier of (Image rf) -valued Function-like non empty V24( the carrier of R) quasi_total onto monotone Element of bool [: the carrier of R, the carrier of (Image rf):]
[: the carrier of R, the carrier of (Image rf):] is Relation-like set
bool [: the carrier of R, the carrier of (Image rf):] is set
the carrier of (Image rf) |` rf is Relation-like the carrier of R -defined the carrier of R -valued the carrier of (Image rf) -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]

the carrier of x is non empty set
[: the carrier of R, the carrier of x:] is Relation-like set
bool [: the carrier of R, the carrier of x:] is set

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the carrier of () is non empty set
corestr S is Relation-like the carrier of R -defined the carrier of () -valued Function-like non empty V24( the carrier of R) quasi_total onto monotone Element of bool [: the carrier of R, the carrier of ():]
[: the carrier of R, the carrier of ():] is Relation-like set
bool [: the carrier of R, the carrier of ():] is set
the carrier of () |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of () -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the carrier of () is non empty set
corestr S is Relation-like the carrier of R -defined the carrier of () -valued Function-like non empty V24( the carrier of R) quasi_total onto monotone Element of bool [: the carrier of R, the carrier of ():]
[: the carrier of R, the carrier of ():] is Relation-like set
bool [: the carrier of R, the carrier of ():] is set
the carrier of () |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of () -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]

the carrier of R is non empty set
the carrier of T is non empty set
[: the carrier of R, the carrier of T:] is Relation-like set
bool [: the carrier of R, the carrier of T:] is set
S is Relation-like the carrier of R -defined the carrier of T -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
S is Relation-like the carrier of R -defined the carrier of R -valued Function-like non empty V24( the carrier of R) quasi_total idempotent monotone directed-sups-preserving projection Element of bool [: the carrier of R, the carrier of R:]

rng S is non empty Element of bool the carrier of R
bool the carrier of R is set

the carrier of () is non empty set
corestr S is Relation-like the carrier of R -defined the carrier of () -valued Function-like non empty V24( the carrier of R) quasi_total onto monotone Element of bool [: the carrier of R, the carrier of ():]
[: the carrier of R, the carrier of ():] is Relation-like set
bool [: the carrier of R, the carrier of ():] is set
the carrier of () |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of () -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
R is RelStr
T is full SubRelStr of R
S is SubRelStr of T
the carrier of S is set
the carrier of T is set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is set
the InternalRel of T |_2 the carrier of S is Relation-like set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is set
the InternalRel of R |_2 the carrier of T is Relation-like set
( the InternalRel of R |_2 the carrier of T) |_2 the carrier of S is Relation-like set
S is SubRelStr of R
the carrier of S is set
the InternalRel of R |_2 the carrier of S is Relation-like set
the InternalRel of R |_2 the carrier of S is Relation-like set
R is non empty transitive RelStr

S is non empty directed-sups-inheriting SubRelStr of T
S is SubRelStr of R
the carrier of S is set
bool the carrier of S is set
f is directed Element of bool the carrier of S
"\/" (f,R) is Element of the carrier of R
the carrier of R is non empty set
the carrier of T is non empty set
bool the carrier of T is set
S is directed Element of bool the carrier of T
"\/" (S,T) is Element of the carrier of T

S is SubRelStr of S
the carrier of S is set
bool the carrier of S is set
f is directed Element of bool the carrier of S
"\/" (f,S) is Element of the carrier of S
the carrier of S is non empty set
the carrier of T is non empty set
bool the carrier of T is set
bool the carrier of S is set
S is non empty directed Element of bool the carrier of T
the carrier of R is non empty set
bool the carrier of R is set
x is non empty directed Element of bool the carrier of R
"\/" (x,R) is Element of the carrier of R
"\/" (S,T) is Element of the carrier of T
rf is non empty directed Element of bool the carrier of S
"\/" (rf,S) is Element of the carrier of S

rng R is set
T is set
T is RelStr
R is non empty set
T is non empty RelStr
T |^ R is non empty strict RelStr

{T} is non empty set

bool [:R,{T}:] is set
product (R --> T) is non empty V177() strict RelStr
the carrier of (T |^ R) is non empty set
bool the carrier of (T |^ R) is set
S is Element of R
S is Element of bool the carrier of (T |^ R)
pi (S,S) is set
the carrier of T is non empty set
bool the carrier of T is set
the carrier of (product (R --> T)) is non empty set
bool the carrier of (product (R --> T)) is set
f is Element of bool the carrier of (product (R --> T))
pi (f,S) is Element of bool the carrier of ((R --> T) . S)
(R --> T) . S is non empty RelStr
the carrier of ((R --> T) . S) is non empty set
bool the carrier of ((R --> T) . S) is set
R is set

{T} is non empty set

bool [:R,{T}:] is set
S is set
rng (R --> T) is trivial set
rng (R --> T) is trivial Element of bool {T}
bool {T} is set
R is set

R --> the non empty reflexive transitive antisymmetric RelStr is Relation-like R -defined {} -valued Function-like constant V24(R) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:R,{}:]
{} is non empty set
[:R,{}:] is Relation-like set
bool [:R,{}:] is set
R is non empty set

product T is non empty V177() strict reflexive RelStr
dom T is Element of bool R
bool R is set
S is Element of R
T . S is non empty reflexive RelStr
rng T is set
S is Element of R
T . S is non empty reflexive RelStr
S is Element of R
T . S is non empty reflexive RelStr
R is non empty set

S is Element of R
T . S is set
dom T is Element of bool R
bool R is set
T . S is non empty reflexive RelStr
rng T is set
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Element of bool the carrier of ()

f is Element of R
S . f is set
T . f is non empty reflexive RelStr
pi (S,f) is Element of bool the carrier of (T . f)
the carrier of (T . f) is non empty set
bool the carrier of (T . f) is set
"\/" ((pi (S,f)),(T . f)) is Element of the carrier of (T . f)
(R,T,f) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,f) is non empty set
dom S is Element of bool R
bool R is set
f is Relation-like Function-like Element of the carrier of ()
S is Relation-like Function-like Element of the carrier of ()
rf is Element of R
S . rf is Element of the carrier of (T . rf)
T . rf is non empty reflexive RelStr
the carrier of (T . rf) is non empty set
pi (S,rf) is Element of bool the carrier of (T . rf)
bool the carrier of (T . rf) is set
"\/" ((pi (S,rf)),(T . rf)) is Element of the carrier of (T . rf)
rf is Relation-like Function-like Element of the carrier of ()
x is Element of R
S . x is Element of the carrier of (T . x)
T . x is non empty reflexive RelStr
the carrier of (T . x) is non empty set
pi (S,x) is Element of bool the carrier of (T . x)
bool the carrier of (T . x) is set
"\/" ((pi (S,x)),(T . x)) is Element of the carrier of (T . x)
rf . x is Element of the carrier of (T . x)
(R,T,x) is non empty reflexive transitive antisymmetric RelStr
rf is Relation-like Function-like Element of the carrier of ()
x is Element of R
(R,T,x) is non empty reflexive transitive antisymmetric RelStr
pi (S,x) is Element of bool the carrier of (T . x)
T . x is non empty reflexive RelStr
the carrier of (T . x) is non empty set
bool the carrier of (T . x) is set
rf . x is Element of the carrier of (T . x)
the carrier of (R,T,x) is non empty set
c9 is Element of the carrier of (R,T,x)

b . x is set
Xx is Relation-like Function-like Element of the carrier of ()
S . x is Element of the carrier of (T . x)
"\/" ((pi (S,x)),(T . x)) is Element of the carrier of (T . x)
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Element of bool the carrier of ()

f is Element of R
S . f is set
T . f is non empty reflexive RelStr
pi (S,f) is Element of bool the carrier of (T . f)
the carrier of (T . f) is non empty set
bool the carrier of (T . f) is set
"/\" ((pi (S,f)),(T . f)) is Element of the carrier of (T . f)
(R,T,f) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,f) is non empty set
dom S is Element of bool R
bool R is set
f is Relation-like Function-like Element of the carrier of ()
S is Relation-like Function-like Element of the carrier of ()
rf is Element of R
S . rf is Element of the carrier of (T . rf)
T . rf is non empty reflexive RelStr
the carrier of (T . rf) is non empty set
pi (S,rf) is Element of bool the carrier of (T . rf)
bool the carrier of (T . rf) is set
"/\" ((pi (S,rf)),(T . rf)) is Element of the carrier of (T . rf)
rf is Relation-like Function-like Element of the carrier of ()
x is Element of R
S . x is Element of the carrier of (T . x)
T . x is non empty reflexive RelStr
the carrier of (T . x) is non empty set
pi (S,x) is Element of bool the carrier of (T . x)
bool the carrier of (T . x) is set
"/\" ((pi (S,x)),(T . x)) is Element of the carrier of (T . x)
rf . x is Element of the carrier of (T . x)
(R,T,x) is non empty reflexive transitive antisymmetric RelStr
rf is Relation-like Function-like Element of the carrier of ()
x is Element of R
(R,T,x) is non empty reflexive transitive antisymmetric RelStr
pi (S,x) is Element of bool the carrier of (T . x)
T . x is non empty reflexive RelStr
the carrier of (T . x) is non empty set
bool the carrier of (T . x) is set
rf . x is Element of the carrier of (T . x)
the carrier of (R,T,x) is non empty set
c9 is Element of the carrier of (R,T,x)

b . x is set
Xx is Relation-like Function-like Element of the carrier of ()
S . x is Element of the carrier of (T . x)
"/\" ((pi (S,x)),(T . x)) is Element of the carrier of (T . x)
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Relation-like Function-like Element of the carrier of ()
S is Element of bool the carrier of ()
f is Element of R
T . f is non empty reflexive RelStr
pi (S,f) is Element of bool the carrier of (T . f)
the carrier of (T . f) is non empty set
bool the carrier of (T . f) is set
S . f is Element of the carrier of (T . f)
(R,T,f) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,f) is non empty set
S is Element of the carrier of (R,T,f)

rf . f is set
x is Relation-like Function-like Element of the carrier of ()
f is Relation-like Function-like Element of the carrier of ()
S is Element of R
T . S is non empty reflexive RelStr
pi (S,S) is Element of bool the carrier of (T . S)
the carrier of (T . S) is non empty set
bool the carrier of (T . S) is set
S . S is Element of the carrier of (T . S)
f . S is Element of the carrier of (T . S)
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Relation-like Function-like Element of the carrier of ()
S is Element of bool the carrier of ()
f is Element of R
T . f is non empty reflexive RelStr
pi (S,f) is Element of bool the carrier of (T . f)
the carrier of (T . f) is non empty set
bool the carrier of (T . f) is set
S . f is Element of the carrier of (T . f)
(R,T,f) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,f) is non empty set
S is Element of the carrier of (R,T,f)

rf . f is set
x is Relation-like Function-like Element of the carrier of ()
f is Relation-like Function-like Element of the carrier of ()
S is Element of R
T . S is non empty reflexive RelStr
pi (S,S) is Element of bool the carrier of (T . S)
the carrier of (T . S) is non empty set
bool the carrier of (T . S) is set
S . S is Element of the carrier of (T . S)
f . S is Element of the carrier of (T . S)
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Element of bool the carrier of ()
"\/" (S,()) is Relation-like Function-like Element of the carrier of ()
f is Element of R
(R,T,f) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,f) is non empty set
pi (S,f) is Element of bool the carrier of (T . f)
T . f is non empty reflexive RelStr
the carrier of (T . f) is non empty set
bool the carrier of (T . f) is set
S is Element of the carrier of (R,T,f)
("\/" (S,())) +* (f,S) is Relation-like Function-like set
dom (("\/" (S,())) +* (f,S)) is set
dom ("\/" (S,())) is set
(("\/" (S,())) +* (f,S)) . f is set
x is Element of R
(("\/" (S,())) +* (f,S)) . x is set
("\/" (S,())) . x is Element of the carrier of (T . x)
T . x is non empty reflexive RelStr
the carrier of (T . x) is non empty set
(R,T,x) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,x) is non empty set
x is Relation-like Function-like Element of the carrier of ()
c9 is Relation-like Function-like Element of the carrier of ()
c9 . f is Element of the carrier of (T . f)
b is Element of R
x . b is Element of the carrier of (T . b)
T . b is non empty reflexive RelStr
the carrier of (T . b) is non empty set
("\/" (S,())) . b is Element of the carrier of (T . b)
c9 . b is Element of the carrier of (T . b)
("\/" (S,())) . f is Element of the carrier of (T . f)
S is Relation-like Function-like Element of the carrier of ()
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Element of bool the carrier of ()
"/\" (S,()) is Relation-like Function-like Element of the carrier of ()
f is Element of R
(R,T,f) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,f) is non empty set
S is Element of the carrier of (R,T,f)
("/\" (S,())) +* (f,S) is Relation-like Function-like set
dom (("/\" (S,())) +* (f,S)) is set
dom ("/\" (S,())) is set
(("/\" (S,())) +* (f,S)) . f is set
x is Element of R
(("/\" (S,())) +* (f,S)) . x is set
("/\" (S,())) . x is Element of the carrier of (T . x)
T . x is non empty reflexive RelStr
the carrier of (T . x) is non empty set
(R,T,x) is non empty reflexive transitive antisymmetric RelStr
the carrier of (R,T,x) is non empty set
pi (S,f) is Element of bool the carrier of (T . f)
T . f is non empty reflexive RelStr
the carrier of (T . f) is non empty set
bool the carrier of (T . f) is set
x is Relation-like Function-like Element of the carrier of ()
c9 is Relation-like Function-like Element of the carrier of ()
c9 . f is Element of the carrier of (T . f)
b is Element of R
x . b is Element of the carrier of (T . b)
T . b is non empty reflexive RelStr
the carrier of (T . b) is non empty set
("/\" (S,())) . b is Element of the carrier of (T . b)
c9 . b is Element of the carrier of (T . b)
("/\" (S,())) . f is Element of the carrier of (T . f)
S is Relation-like Function-like Element of the carrier of ()
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Element of bool the carrier of ()
"\/" (S,()) is Relation-like Function-like Element of the carrier of ()
S is Element of R
(R,T,S) is non empty reflexive transitive antisymmetric RelStr
pi (S,S) is Element of bool the carrier of (T . S)
T . S is non empty reflexive RelStr
the carrier of (T . S) is non empty set
bool the carrier of (T . S) is set
S is Relation-like Function-like Element of the carrier of ()
f is Element of R
("\/" (S,())) . f is Element of the carrier of (T . f)
T . f is non empty reflexive RelStr
the carrier of (T . f) is non empty set
pi (S,f) is Element of bool the carrier of (T . f)
bool the carrier of (T . f) is set
"\/" ((pi (S,f)),(T . f)) is Element of the carrier of (T . f)
R is non empty set

the carrier of () is non empty set
bool the carrier of () is set
S is Element of bool the carrier of ()
"/\" (S,()) is Relation-like Function-like Element of the carrier of ()
S is Element of R
(R,T,S) is non empty reflexive transitive antisymmetric RelStr
pi (S,S) is Element of bool the carrier of (T . S)
T . S is non empty reflexive RelStr
the carrier of (T . S) is non empty set
bool the carrier of (T . S) is set
S is Relation-like Function-like Element of the carrier of ()
f is Element of R
("/\" (S,())) . f is Element of the carrier of (T . f)
T . f is non empty reflexive RelStr
the carrier of (T . f