K99() is Element of bool K95()
K95() is set
bool K95() is set
K54() is set
bool K54() is set
bool K99() is set
I[01] is non empty strict TopSpace-like TopStruct
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())
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V40() set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V40() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V40() set
1 is non empty set
{{},1} is non empty set
K653() is set
{{}} is functional non empty set
K375({{}}) is M19({{}})
[:K375({{}}),{{}}:] is Relation-like set
bool [:K375({{}}),{{}}:] is set
K39(K375({{}}),{{}}) is set
id {{}} is Relation-like {{}} -defined {{}} -valued Function-like one-to-one non empty V24({{}}) quasi_total Function-yielding V40() Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is Relation-like set
bool [:{{}},{{}}:] is set
RelStr(# {{}},(id {{}}) #) is non empty trivial V60() 1 -element strict RelStr
{1} is non empty set
Sierpinski_Space is non empty strict TopSpace-like T_0 V372() TopStruct
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V40() Element of K99()
{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
R is Relation-like Function-like set
T is Relation-like Function-like set
rng T is set
rng R is set
dom R is set
T * R is Relation-like Function-like set
R * R is Relation-like Function-like 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:]
R is non empty reflexive transitive antisymmetric up-complete RelStr
T is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr 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
R is non empty reflexive transitive antisymmetric up-complete 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 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:]
Image T is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng T is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng T) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
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
f is non empty reflexive transitive antisymmetric full SubRelStr 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
R is non empty reflexive transitive antisymmetric RelStr
T is non empty reflexive transitive antisymmetric RelStr
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
id 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
S is Relation-like Function-like set
(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
S | the carrier of R is Relation-like Function-like set
(id the carrier of R) * S is Relation-like the carrier of R -defined Function-like set
R is non empty reflexive transitive antisymmetric RelStr
T is non empty reflexive transitive antisymmetric up-complete RelStr
S is Relation-like 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
id 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
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:]
S * S is Relation-like the carrier of R -defined Function-like set
R is non empty reflexive transitive antisymmetric RelStr
T is non empty reflexive transitive antisymmetric RelStr
the carrier of R is non empty set
S is Relation-like Function-like 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 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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 non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
R is non empty reflexive transitive antisymmetric RelStr
T is non empty reflexive transitive antisymmetric RelStr
the carrier of R is non empty set
S is Relation-like Function-like 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
id 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
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:]
f * S is Relation-like the carrier of R -defined Function-like set
R is non empty reflexive transitive antisymmetric RelStr
T is non empty reflexive transitive antisymmetric RelStr
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
S is Relation-like Function-like 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
id 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
R is non empty reflexive transitive antisymmetric 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 reflexive transitive antisymmetric RelStr
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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
the carrier of (Image S) is non empty set
R is non empty reflexive transitive antisymmetric up-complete 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 reflexive transitive antisymmetric 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:]
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:]
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 infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
(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
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 infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
id 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
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 Function-like 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:]
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:]
R is non empty reflexive transitive antisymmetric RelStr
T is non empty reflexive transitive antisymmetric 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
[: 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 infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
id 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
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:]
S " is Relation-like Function-like set
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
S " is Relation-like Function-like set
R is non empty reflexive transitive antisymmetric up-complete RelStr
T is non empty reflexive transitive antisymmetric up-complete 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
[: 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 infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
id 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 idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
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:]
R is non empty reflexive transitive antisymmetric RelStr
the carrier of R is non empty set
T is non empty reflexive transitive 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 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 infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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:]
[: 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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
the carrier of (Image S) is non empty set
[: the carrier of T, the carrier of (Image S):] is Relation-like set
bool [: the carrier of T, the carrier of (Image S):] is set
corestr S is Relation-like the carrier of T -defined the carrier of (Image S) -valued Function-like non empty V24( the carrier of T) quasi_total onto monotone Element of bool [: the carrier of T, the carrier of (Image S):]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
the carrier of (Image S) is non empty set
[: the carrier of T, the carrier of (Image S):] is Relation-like set
bool [: the carrier of T, the carrier of (Image S):] is set
the carrier of (Image S) |` S is Relation-like the carrier of T -defined the carrier of R -valued the carrier of (Image S) -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 (Image S) -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of (Image S):]
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 (Image S)
rf . c9 is Element of the carrier of (Image S)
(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 (Image S)
bool the carrier of (Image S) is set
S | the carrier of (Image S) is Relation-like the carrier of R -defined the carrier of (Image 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:]
id (Image S) is Relation-like the carrier of (Image S) -defined the carrier of (Image S) -valued Function-like one-to-one non empty V24( the carrier of (Image S)) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (Image S), the carrier of (Image S):]
[: the carrier of (Image S), the carrier of (Image S):] is Relation-like set
bool [: the carrier of (Image S), the carrier of (Image S):] is set
id the carrier of (Image S) is Relation-like the carrier of (Image S) -defined the carrier of (Image S) -valued Function-like one-to-one non empty V24( the carrier of (Image S)) quasi_total Element of bool [: the carrier of (Image S), the carrier of (Image S):]
inclusion S is Relation-like the carrier of (Image S) -defined the carrier of R -valued Function-like one-to-one non empty V24( the carrier of (Image S)) quasi_total monotone Element of bool [: the carrier of (Image S), the carrier of R:]
[: the carrier of (Image S), the carrier of R:] is Relation-like set
bool [: the carrier of (Image S), the carrier of R:] is set
S * (inclusion S) is Relation-like the carrier of (Image S) -defined the carrier of R -valued Function-like non empty V24( the carrier of (Image S)) quasi_total Element of bool [: the carrier of (Image S), the carrier of R:]
corestr S is Relation-like the carrier of R -defined the carrier of (Image S) -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 S):]
[: the carrier of R, the carrier of (Image S):] is Relation-like set
bool [: the carrier of R, the carrier of (Image S):] is set
the carrier of (Image S) |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of (Image S) -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
(corestr S) * (inclusion S) is Relation-like the carrier of (Image S) -defined the carrier of (Image S) -valued Function-like non empty V24( the carrier of (Image S)) quasi_total Element of bool [: the carrier of (Image S), the carrier of (Image S):]
R is non empty reflexive transitive antisymmetric up-complete 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 reflexive transitive antisymmetric RelStr
S is Relation-like Function-like 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
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 infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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 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:]
S * S is Relation-like the carrier of T -defined Function-like set
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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
the carrier of (Image S) is non empty set
S | the carrier of (Image S) is Relation-like the carrier of R -defined the carrier of (Image 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:]
id (Image S) is Relation-like the carrier of (Image S) -defined the carrier of (Image S) -valued Function-like one-to-one non empty V24( the carrier of (Image S)) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (Image S), the carrier of (Image S):]
[: the carrier of (Image S), the carrier of (Image S):] is Relation-like set
bool [: the carrier of (Image S), the carrier of (Image S):] is set
id the carrier of (Image S) is Relation-like the carrier of (Image S) -defined the carrier of (Image S) -valued Function-like one-to-one non empty V24( the carrier of (Image S)) quasi_total Element of bool [: the carrier of (Image S), the carrier of (Image S):]
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:]
Image rf is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng rf is non empty Element of bool the carrier of R
subrelstr (rng rf) is non empty strict reflexive transitive antisymmetric full SubRelStr 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:]
x is non empty reflexive transitive antisymmetric RelStr
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
R is non empty reflexive transitive antisymmetric up-complete RelStr
T is non empty reflexive transitive antisymmetric 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:]
R is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V305() up-complete /\-complete RelStr
T is non empty reflexive transitive antisymmetric 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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
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
R is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V305() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
T is non empty reflexive transitive antisymmetric 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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
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
R is non empty reflexive transitive antisymmetric up-complete RelStr
T is non empty reflexive transitive antisymmetric 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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
the carrier of (Image S) is non empty set
corestr S is Relation-like the carrier of R -defined the carrier of (Image S) -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 S):]
[: the carrier of R, the carrier of (Image S):] is Relation-like set
bool [: the carrier of R, the carrier of (Image S):] is set
the carrier of (Image S) |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of (Image S) -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
R is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V305() up-complete /\-complete RelStr
T is non empty reflexive transitive antisymmetric 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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
the carrier of (Image S) is non empty set
corestr S is Relation-like the carrier of R -defined the carrier of (Image S) -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 S):]
[: the carrier of R, the carrier of (Image S):] is Relation-like set
bool [: the carrier of R, the carrier of (Image S):] is set
the carrier of (Image S) |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of (Image S) -valued the carrier of R -valued Function-like Element of bool [: the carrier of R, the carrier of R:]
R is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V305() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
T is non empty reflexive transitive antisymmetric 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:]
Image S is non empty strict reflexive transitive antisymmetric full SubRelStr of R
rng S is non empty Element of bool the carrier of R
bool the carrier of R is set
subrelstr (rng S) is non empty strict reflexive transitive antisymmetric full SubRelStr of R
the carrier of (Image S) is non empty set
corestr S is Relation-like the carrier of R -defined the carrier of (Image S) -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 S):]
[: the carrier of R, the carrier of (Image S):] is Relation-like set
bool [: the carrier of R, the carrier of (Image S):] is set
the carrier of (Image S) |` S is Relation-like the carrier of R -defined the carrier of R -valued the carrier of (Image S) -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
T is non empty transitive full directed-sups-inheriting SubRelStr of R
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
R is non empty reflexive transitive antisymmetric up-complete RelStr
T is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of R
S is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of R
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
R is Relation-like set
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
R --> T is Relation-like R -defined {T} -valued Function-like constant non empty V24(R) quasi_total V361() RelStr-yielding non-Empty Element of bool [:R,{T}:]
{T} is non empty set
[:R,{T}:] is Relation-like 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 reflexive transitive antisymmetric RelStr
R --> T is Relation-like R -defined {T} -valued Function-like constant V24(R) quasi_total V361() RelStr-yielding reflexive-yielding Element of bool [:R,{T}:]
{T} is non empty set
[:R,{T}:] is Relation-like 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
the non empty reflexive transitive antisymmetric RelStr is non empty reflexive transitive antisymmetric RelStr
R --> the non empty reflexive transitive antisymmetric RelStr is Relation-like R -defined { the non empty reflexive transitive antisymmetric RelStr } -valued Function-like constant V24(R) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:R,{ the non empty reflexive transitive antisymmetric RelStr }:]
{ the non empty reflexive transitive antisymmetric RelStr } is non empty set
[:R,{ the non empty reflexive transitive antisymmetric RelStr }:] is Relation-like set
bool [:R,{ the non empty reflexive transitive antisymmetric RelStr }:] is set
R is non empty set
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () 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
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () 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
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Element of bool the carrier of (product T)
S is Relation-like R -defined Function-like V24(R) set
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 (product T)
S is Relation-like Function-like Element of the carrier of (product T)
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 (product T)
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 (product T)
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 is Relation-like Function-like set
b . x is set
Xx is Relation-like Function-like Element of the carrier of (product T)
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
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Element of bool the carrier of (product T)
S is Relation-like R -defined Function-like V24(R) set
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 (product T)
S is Relation-like Function-like Element of the carrier of (product T)
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 (product T)
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 (product T)
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 is Relation-like Function-like set
b . x is set
Xx is Relation-like Function-like Element of the carrier of (product T)
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
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Relation-like Function-like Element of the carrier of (product T)
S is Element of bool the carrier of (product T)
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 is Relation-like Function-like set
rf . f is set
x is Relation-like Function-like Element of the carrier of (product T)
f is Relation-like Function-like Element of the carrier of (product T)
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
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Relation-like Function-like Element of the carrier of (product T)
S is Element of bool the carrier of (product T)
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 is Relation-like Function-like set
rf . f is set
x is Relation-like Function-like Element of the carrier of (product T)
f is Relation-like Function-like Element of the carrier of (product T)
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
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Element of bool the carrier of (product T)
"\/" (S,(product T)) is Relation-like Function-like Element of the carrier of (product T)
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,(product T))) +* (f,S) is Relation-like Function-like set
dom (("\/" (S,(product T))) +* (f,S)) is set
dom ("\/" (S,(product T))) is set
(("\/" (S,(product T))) +* (f,S)) . f is set
x is Element of R
(("\/" (S,(product T))) +* (f,S)) . x is set
("\/" (S,(product T))) . 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 (product T)
c9 is Relation-like Function-like Element of the carrier of (product T)
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,(product T))) . b is Element of the carrier of (T . b)
c9 . b is Element of the carrier of (T . b)
("\/" (S,(product T))) . f is Element of the carrier of (T . f)
S is Relation-like Function-like Element of the carrier of (product T)
R is non empty set
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Element of bool the carrier of (product T)
"/\" (S,(product T)) is Relation-like Function-like Element of the carrier of (product T)
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,(product T))) +* (f,S) is Relation-like Function-like set
dom (("/\" (S,(product T))) +* (f,S)) is set
dom ("/\" (S,(product T))) is set
(("/\" (S,(product T))) +* (f,S)) . f is set
x is Element of R
(("/\" (S,(product T))) +* (f,S)) . x is set
("/\" (S,(product T))) . 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 (product T)
c9 is Relation-like Function-like Element of the carrier of (product T)
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,(product T))) . b is Element of the carrier of (T . b)
c9 . b is Element of the carrier of (T . b)
("/\" (S,(product T))) . f is Element of the carrier of (T . f)
S is Relation-like Function-like Element of the carrier of (product T)
R is non empty set
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Element of bool the carrier of (product T)
"\/" (S,(product T)) is Relation-like Function-like Element of the carrier of (product T)
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 (product T)
f is Element of R
("\/" (S,(product T))) . 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
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty reflexive-yielding () set
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is Element of bool the carrier of (product T)
"/\" (S,(product T)) is Relation-like Function-like Element of the carrier of (product T)
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 (product T)
f is Element of R
("/\" (S,(product T))) . f is Element of the carrier of (T . f)
T . f is non empty reflexive RelStr
the carrier of (T . f