:: 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
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
c₉ 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
c₉ 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
c<sub>9</sub> is Element of the carrier of T
S . x is Element of the carrier of R
S . c<sub>9</sub> is Element of the carrier of R
rf . x is Element of the carrier of (Image S)
rf . c<sub>9</sub> 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) . c<sub>9</sub> is Element of the carrier of T
S . (S . c<sub>9</sub>) 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
c₉ 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
c₉ 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)
c₉ is Relation-like Function-like Element of the carrier of (product T)
c₉ . 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)
c₉ . 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)
c₉ is Relation-like Function-like Element of the carrier of (product T)
c₉ . 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)
c₉ . 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) 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 RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is directed Element of bool 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
f is Element of the carrier of (T . S)
S is Element of the carrier of (T . S)
rf is Relation-like Function-like set
rf . S is set
x is Relation-like Function-like set
x . S is set
c₉ is Relation-like Function-like Element of the carrier of (product T)
b is Relation-like Function-like Element of the carrier of (product T)
Xx is Relation-like Function-like Element of the carrier of (product T)
Xx . S is Element of the carrier of (T . S)
R is non empty set
S is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty set
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty set
product S is non empty V177() strict RelStr
product T is non empty V177() strict RelStr
S is set
f is Element of R
T . f is non empty RelStr
Carrier T is Relation-like R -defined Function-like V24(R) set
(Carrier T) . f is set
S . f is non empty RelStr
Carrier S is Relation-like R -defined Function-like V24(R) set
(Carrier S) . f is set
(Carrier S) . S is set
(Carrier T) . S is set
S is 1-sorted
the carrier of S is set
rf is 1-sorted
the carrier of rf is set
dom (Carrier S) is Element of bool R
bool R is set
dom (Carrier T) is Element of bool R
the carrier of (product T) is non empty set
product (Carrier T) is set
the carrier of (product S) is non empty set
product (Carrier S) is set
the InternalRel of (product S) is Relation-like the carrier of (product S) -defined the carrier of (product S) -valued Element of bool [: the carrier of (product S), the carrier of (product S):]
[: the carrier of (product S), the carrier of (product S):] is Relation-like set
bool [: the carrier of (product S), the carrier of (product S):] is set
the InternalRel of (product T) is Relation-like the carrier of (product T) -defined the carrier of (product T) -valued Element of bool [: the carrier of (product T), the carrier of (product T):]
[: the carrier of (product T), the carrier of (product T):] is Relation-like set
bool [: the carrier of (product T), the carrier of (product T):] is set
S is set
f is set
[S,f] is set
{S,f} is non empty set
{S} is non empty set
{{S,f},{S}} is non empty set
S is Relation-like Function-like Element of the carrier of (product S)
rf is Relation-like Function-like Element of the carrier of (product S)
b is Element of R
S . b is non empty RelStr
S . b is Element of the carrier of (S . b)
the carrier of (S . b) is non empty set
rf . b is Element of the carrier of (S . b)
T . b is non empty RelStr
x is Relation-like Function-like Element of the carrier of (product T)
x . b is Element of the carrier of (T . b)
the carrier of (T . b) is non empty set
c₉ is Relation-like Function-like Element of the carrier of (product T)
c₉ . b is Element of the carrier of (T . b)
R is non empty set
S is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty set
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty set
product S is non empty V177() strict RelStr
product T is non empty V177() strict RelStr
S is Element of R
S . S is non empty RelStr
T . S is non empty RelStr
the InternalRel of (product T) is Relation-like the carrier of (product T) -defined the carrier of (product T) -valued Element of bool [: the carrier of (product T), the carrier of (product T):]
the carrier of (product T) is non empty set
[: the carrier of (product T), the carrier of (product T):] is Relation-like set
bool [: the carrier of (product T), the carrier of (product T):] is set
S is non empty SubRelStr of product T
the carrier of S is non empty set
the InternalRel of (product T) |_2 the carrier of S is Relation-like set
[: the carrier of S, the carrier of S:] is Relation-like set
the InternalRel of (product T) /\ [: the carrier of S, the carrier of S:] is Relation-like the carrier of (product T) -defined the carrier of (product T) -valued Element of bool [: the carrier of (product T), the carrier of (product T):]
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:]
bool [: the carrier of S, the carrier of S:] is set
K43( the InternalRel of (product T), the carrier 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:]
f is set
S is set
[f,S] is set
{f,S} is non empty set
{f} is non empty set
{{f,S},{f}} is non empty set
rf is Element of the carrier of S
x is Element of the carrier of S
the carrier of (product S) is non empty set
c₉ is Relation-like Function-like Element of the carrier of (product T)
b is Relation-like Function-like Element of the carrier of (product T)
a9 is Element of R
S . a9 is non empty RelStr
T . a9 is non empty RelStr
c₉ . a9 is Element of the carrier of (T . a9)
the carrier of (T . a9) is non empty set
b . a9 is Element of the carrier of (T . a9)
Xx is Relation-like Function-like Element of the carrier of (product S)
Xx . a9 is Element of the carrier of (S . a9)
the carrier of (S . a9) is non empty set
Xy is Relation-like Function-like Element of the carrier of (product S)
Xy . a9 is Element of the carrier of (S . a9)
R is non empty RelStr
T is non empty SubRelStr of R
S is set
T |^ S is non empty strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{T}:]
{T} is non empty set
[:S,{T}:] is Relation-like set
bool [:S,{T}:] is set
product (S --> T) is non empty V177() strict RelStr
R |^ S is non empty strict RelStr
S --> R is Relation-like S -defined {R} -valued Function-like constant V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{R}:]
{R} is non empty set
[:S,{R}:] is Relation-like set
bool [:S,{R}:] is set
product (S --> R) is non empty V177() strict RelStr
S is non empty set
S --> R is Relation-like S -defined {R} -valued Function-like constant non empty V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{R}:]
[:S,{R}:] is Relation-like set
bool [:S,{R}:] is set
f is Element of S
(S --> R) . f is non empty RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant non empty V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{T}:]
[:S,{T}:] is Relation-like set
bool [:S,{T}:] is set
(S --> T) . f is non empty RelStr
R is non empty RelStr
T is non empty full SubRelStr of R
S is set
T |^ S is non empty strict RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{T}:]
{T} is non empty set
[:S,{T}:] is Relation-like set
bool [:S,{T}:] is set
product (S --> T) is non empty V177() strict RelStr
R |^ S is non empty strict RelStr
S --> R is Relation-like S -defined {R} -valued Function-like constant V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{R}:]
{R} is non empty set
[:S,{R}:] is Relation-like set
bool [:S,{R}:] is set
product (S --> R) is non empty V177() strict RelStr
S is non empty set
S --> R is Relation-like S -defined {R} -valued Function-like constant non empty V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{R}:]
[:S,{R}:] is Relation-like set
bool [:S,{R}:] is set
f is Element of S
(S --> R) . f is non empty RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant non empty V24(S) quasi_total V361() RelStr-yielding non-Empty Element of bool [:S,{T}:]
[:S,{T}:] is Relation-like set
bool [:S,{T}:] is set
(S --> T) . f is non empty RelStr
R is non empty transitive RelStr
T is non empty transitive full SubRelStr of R
the carrier of T is non empty set
bool the carrier of T is set
S is Element of bool the carrier of T
"\/" (S,T) is Element of the carrier of T
"\/" (S,R) is Element of the carrier of R
the carrier of R is non empty set
R is non empty transitive RelStr
T is non empty transitive full SubRelStr of R
the carrier of T is non empty set
bool the carrier of T is set
S is Element of bool the carrier of T
"/\" (S,T) is Element of the carrier of T
"/\" (S,R) is Element of the carrier of R
the carrier of R is non empty set
F₁() is non empty set
F₃() is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
product F₃() is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product F₃()) is non empty set
bool the carrier of (product F₃()) is set
F₂() is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
product F₂() is non empty V177() strict reflexive transitive antisymmetric RelStr
R is Element of bool the carrier of (product F₃())
"\/" (R,(product F₂())) is Relation-like Function-like Element of the carrier of (product F₂())
the carrier of (product F₂()) is non empty set
bool the carrier of (product F₂()) is set
S is Element of F₁()
(F₁(),F₂(),S) is non empty reflexive transitive antisymmetric RelStr
T is Element of bool the carrier of (product F₂())
pi (T,S) is Element of bool the carrier of (F₂() . S)
F₂() . S is non empty reflexive RelStr
the carrier of (F₂() . S) is non empty set
bool the carrier of (F₂() . S) is set
(F₁(),F₃(),S) is non empty reflexive transitive antisymmetric RelStr
pi (R,S) is Element of bool the carrier of (F₃() . S)
F₃() . S is non empty reflexive RelStr
the carrier of (F₃() . S) is non empty set
bool the carrier of (F₃() . S) is set
"\/" ((pi (T,S)),(F₂() . S)) is Element of the carrier of (F₂() . S)
the carrier of (F₁(),F₃(),S) is non empty set
("\/" (R,(product F₂()))) . S is Element of the carrier of (F₂() . S)
dom ("\/" (R,(product F₂()))) is set
F₂() is non empty reflexive transitive antisymmetric RelStr
F₁() is non empty set
F₃() is non empty reflexive transitive antisymmetric full SubRelStr of F₂()
F₃() |^ F₁() is non empty strict reflexive transitive antisymmetric RelStr
F₁() --> F₃() is Relation-like F₁() -defined {F₃()} -valued Function-like constant non empty V24(F₁()) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:F₁(),{F₃()}:]
{F₃()} is non empty set
[:F₁(),{F₃()}:] is Relation-like set
bool [:F₁(),{F₃()}:] is set
product (F₁() --> F₃()) is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (F₃() |^ F₁()) is non empty set
bool the carrier of (F₃() |^ F₁()) is set
the carrier of F₃() is non empty set
bool the carrier of F₃() is set
F₂() |^ F₁() is non empty strict reflexive transitive antisymmetric RelStr
F₁() --> F₂() is Relation-like F₁() -defined {F₂()} -valued Function-like constant non empty V24(F₁()) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:F₁(),{F₂()}:]
{F₂()} is non empty set
[:F₁(),{F₂()}:] is Relation-like set
bool [:F₁(),{F₂()}:] is set
product (F₁() --> F₂()) is non empty V177() strict reflexive transitive antisymmetric RelStr
R is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
product R is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product R) is non empty set
bool the carrier of (product R) is set
S is Element of bool the carrier of (product R)
S is Element of F₁()
(F₁(),R,S) is non empty reflexive transitive antisymmetric RelStr
pi (S,S) is Element of bool the carrier of (R . S)
R . S is non empty reflexive RelStr
the carrier of (R . S) is non empty set
bool the carrier of (R . S) is set
S is Element of F₁()
(F₁(),R,S) is non empty reflexive transitive antisymmetric RelStr
the carrier of (F₁(),R,S) is non empty set
bool the carrier of (F₁(),R,S) is set
S is Element of bool the carrier of (F₁(),R,S)
T is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
(F₁(),T,S) is non empty reflexive transitive antisymmetric RelStr
S is Element of F₁()
(F₁(),T,S) is non empty reflexive transitive antisymmetric RelStr
(F₁(),R,S) is non empty reflexive transitive antisymmetric RelStr
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
S is Element of bool the carrier of (F₃() |^ F₁())
F₁() is non empty set
F₃() is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
product F₃() is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product F₃()) is non empty set
bool the carrier of (product F₃()) is set
F₂() is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
product F₂() is non empty V177() strict reflexive transitive antisymmetric RelStr
R is Element of bool the carrier of (product F₃())
"/\" (R,(product F₂())) is Relation-like Function-like Element of the carrier of (product F₂())
the carrier of (product F₂()) is non empty set
bool the carrier of (product F₂()) is set
S is Element of F₁()
(F₁(),F₂(),S) is non empty reflexive transitive antisymmetric RelStr
T is Element of bool the carrier of (product F₂())
pi (T,S) is Element of bool the carrier of (F₂() . S)
F₂() . S is non empty reflexive RelStr
the carrier of (F₂() . S) is non empty set
bool the carrier of (F₂() . S) is set
(F₁(),F₃(),S) is non empty reflexive transitive antisymmetric RelStr
pi (R,S) is Element of bool the carrier of (F₃() . S)
F₃() . S is non empty reflexive RelStr
the carrier of (F₃() . S) is non empty set
bool the carrier of (F₃() . S) is set
"/\" ((pi (T,S)),(F₂() . S)) is Element of the carrier of (F₂() . S)
the carrier of (F₁(),F₃(),S) is non empty set
("/\" (R,(product F₂()))) . S is Element of the carrier of (F₂() . S)
dom ("/\" (R,(product F₂()))) is set
F₂() is non empty reflexive transitive antisymmetric RelStr
F₁() is non empty set
F₃() is non empty reflexive transitive antisymmetric full SubRelStr of F₂()
F₃() |^ F₁() is non empty strict reflexive transitive antisymmetric RelStr
F₁() --> F₃() is Relation-like F₁() -defined {F₃()} -valued Function-like constant non empty V24(F₁()) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:F₁(),{F₃()}:]
{F₃()} is non empty set
[:F₁(),{F₃()}:] is Relation-like set
bool [:F₁(),{F₃()}:] is set
product (F₁() --> F₃()) is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (F₃() |^ F₁()) is non empty set
bool the carrier of (F₃() |^ F₁()) is set
the carrier of F₃() is non empty set
bool the carrier of F₃() is set
F₂() |^ F₁() is non empty strict reflexive transitive antisymmetric RelStr
F₁() --> F₂() is Relation-like F₁() -defined {F₂()} -valued Function-like constant non empty V24(F₁()) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:F₁(),{F₂()}:]
{F₂()} is non empty set
[:F₁(),{F₂()}:] is Relation-like set
bool [:F₁(),{F₂()}:] is set
product (F₁() --> F₂()) is non empty V177() strict reflexive transitive antisymmetric RelStr
R is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
product R is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (product R) is non empty set
bool the carrier of (product R) is set
S is Element of bool the carrier of (product R)
S is Element of F₁()
(F₁(),R,S) is non empty reflexive transitive antisymmetric RelStr
pi (S,S) is Element of bool the carrier of (R . S)
R . S is non empty reflexive RelStr
the carrier of (R . S) is non empty set
bool the carrier of (R . S) is set
S is Element of F₁()
(F₁(),R,S) is non empty reflexive transitive antisymmetric RelStr
the carrier of (F₁(),R,S) is non empty set
bool the carrier of (F₁(),R,S) is set
S is Element of bool the carrier of (F₁(),R,S)
T is Relation-like F₁() -defined Function-like V24(F₁()) V361() RelStr-yielding non-Empty reflexive-yielding () set
(F₁(),T,S) is non empty reflexive transitive antisymmetric RelStr
S is Element of F₁()
(F₁(),T,S) is non empty reflexive transitive antisymmetric RelStr
(F₁(),R,S) is non empty reflexive transitive antisymmetric RelStr
product T is non empty V177() strict reflexive transitive antisymmetric RelStr
S is Element of bool the carrier of (F₃() |^ F₁())
R is 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 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 set
S is non empty Element of bool the carrier of (T |^ R)
pi (S,S) is set
the carrier of (product (R --> T)) is non empty set
bool the carrier of (product (R --> T)) is set
f is non empty Element of bool the carrier of (product (R --> T))
the Element of f is Element of f
rf is Relation-like Function-like set
rf . S is set
R is non empty reflexive transitive antisymmetric RelStr
T is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of R
S is non empty set
T |^ S is non empty strict reflexive transitive antisymmetric RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant non empty V24(S) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:S,{T}:]
{T} is non empty set
[:S,{T}:] is Relation-like set
bool [:S,{T}:] is set
product (S --> T) is non empty V177() strict reflexive transitive antisymmetric RelStr
R |^ S is non empty strict reflexive transitive antisymmetric RelStr
S --> R is Relation-like S -defined {R} -valued Function-like constant non empty V24(S) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:S,{R}:]
{R} is non empty set
[:S,{R}:] is Relation-like set
bool [:S,{R}:] is set
product (S --> R) is non empty V177() strict reflexive transitive antisymmetric RelStr
the carrier of (T |^ S) is non empty set
bool the carrier of (T |^ S) is set
f is Element of bool the carrier of (T |^ S)
rf is Element of S
(S,(S --> T),rf) is non empty reflexive transitive antisymmetric RelStr
S is non empty directed Element of bool the carrier of (T |^ S)
(S,T,rf,S) is non empty Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is set
(S,T,rf,f) is Element of bool the carrier of T
f is Element of bool the carrier of T
"\/" (f,T) is Element of the carrier of T
"\/" (f,R) is Element of the carrier of R
the carrier of R is non empty set
S is non empty reflexive transitive antisymmetric full SubRelStr of R |^ S
the carrier of S is non empty set
bool the carrier of S is set
f is directed Element of bool the carrier of S
"\/" (f,(R |^ S)) is Element of the carrier of (R |^ S)
the carrier of (R |^ S) is non empty set
R is non empty set
T is Relation-like R -defined Function-like V24(R) V361() RelStr-yielding non-Empty set
product T is non empty V177() strict RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is set
S is set
S is non empty Element of bool the carrier of (product T)
pi (S,S) is set
the Element of S is Element of S
S is Relation-like Function-like set
S . S is set
R is non empty set
T is non empty reflexive transitive antisymmetric up-complete RelStr
T |^ R is non empty strict reflexive transitive antisymmetric RelStr
R --> T is Relation-like R -defined {T} -valued Function-like constant non empty V24(R) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () 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 reflexive transitive antisymmetric RelStr
the carrier of (T |^ R) is non empty set
bool the carrier of (T |^ R) is set
the carrier of (product (R --> T)) is non empty set
bool the carrier of (product (R --> T)) is set
S is non empty directed Element of bool the carrier of (T |^ R)
f is Element of R
(R,(R --> T),f) is non empty reflexive transitive antisymmetric RelStr
(R --> T) . f is non empty reflexive RelStr
S is non empty directed Element of bool the carrier of (product (R --> T))
pi (S,f) is non empty Element of bool the carrier of ((R --> T) . f)
the carrier of ((R --> T) . f) is non empty set
bool the carrier of ((R --> T) . f) is set
(R,T,f,S) is non empty Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is set
T is non empty set
R is non empty reflexive transitive antisymmetric up-complete RelStr
R |^ T is non empty strict reflexive transitive antisymmetric RelStr
T --> R is Relation-like T -defined {R} -valued Function-like constant non empty V24(T) quasi_total V361() RelStr-yielding non-Empty reflexive-yielding () Element of bool [:T,{R}:]
{R} is non empty set
[:T,{R}:] is Relation-like set
bool [:T,{R}:] is set
product (T --> R) is non empty V177() strict reflexive transitive antisymmetric RelStr
R is non empty TopSpace-like TopStruct
the carrier of R is non empty set
T is non empty TopSpace-like SubSpace 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 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:]
rng S is non empty Element of bool the carrier of T
bool the carrier of T is set
S is set
[#] T is non empty non proper open closed Element of bool the carrier of T
[#] R is non empty non proper open closed Element of bool the carrier of R
bool the carrier of R is set
dom S is non empty Element of bool the carrier of R
S . S is set
R is non empty TopSpace-like TopStruct
the carrier of R is non empty set
T is non empty TopSpace-like SubSpace 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
[#] T is non empty non proper open closed Element of bool the carrier of T
bool 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 continuous Element of bool [: the carrier of R, the carrier of T:]
rng S is non empty Element of bool the carrier of T
dom S is non empty Element of bool the carrier of R
bool the carrier of R is set
[#] R is non empty non proper open closed Element of bool the carrier of R
S is set
S . S is set
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:]
(S * S) . S is set
S . (S . S) is set
dom (S * S) is Element of bool the carrier of R
the carrier of Sierpinski_Space is non empty set
R is non empty TopSpace-like TopStruct
the carrier of R is non empty set
bool the carrier of R is set
[: the carrier of R, the carrier of Sierpinski_Space:] is Relation-like set
bool [: the carrier of R, the carrier of Sierpinski_Space:] is set
T is open Element of bool the carrier of R
chi (T, the carrier of R) is Relation-like the carrier of R -defined {{},1} -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R,{{},1}:]
[: the carrier of R,{{},1}:] is Relation-like set
bool [: the carrier of R,{{},1}:] is set
S is Relation-like the carrier of R -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of Sierpinski_Space:]
S " {0,1} is Element of bool the carrier of R
[#] R is non empty non proper open closed Element of bool the carrier of R
S " {1} is Element of bool the carrier of R
chi ((S " {1}), the carrier of R) is Relation-like the carrier of R -defined {{},1} -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R,{{},1}:]
S " {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V40() open closed Element of bool the carrier of R
{} R is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V40() open closed Element of bool the carrier of R
bool the carrier of Sierpinski_Space is set
S is Element of bool the carrier of Sierpinski_Space
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
bool (bool the carrier of Sierpinski_Space) is set
S " S is Element of bool the carrier of R
[#] Sierpinski_Space is non empty non proper open closed Element of bool the carrier of Sierpinski_Space
R is non empty TopSpace-like TopStruct
the carrier of R is non empty set
bool the carrier of R is set
[: the carrier of Sierpinski_Space, the carrier of R:] is Relation-like set
bool [: the carrier of Sierpinski_Space, the carrier of R:] is set
S is Element of the carrier of R
T is Element of the carrier of R
(0,1) --> (S,T) is Relation-like {0,1} -defined the carrier of R -valued Function-like non empty V24({0,1}) quasi_total Element of bool [:{0,1}, the carrier of R:]
[:{0,1}, the carrier of R:] is Relation-like set
bool [:{0,1}, the carrier of R:] is set
S is Relation-like the carrier of Sierpinski_Space -defined the carrier of R -valued Function-like non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of R:]
S . 1 is set
{0} is functional non empty set
S . 0 is set
f is Element of bool the carrier of R
S " f is Element of bool the carrier of Sierpinski_Space
bool the carrier of Sierpinski_Space is set
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
bool (bool the carrier of Sierpinski_Space) is set
[#] R is non empty non proper open closed Element of bool the carrier of R
id Sierpinski_Space is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of Sierpinski_Space) quasi_total continuous open Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
[: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:] is Relation-like set
bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:] is set
id the carrier of Sierpinski_Space is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued Function-like one-to-one non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
R is non empty TopSpace-like TopStruct
the carrier of R is non empty set
bool the carrier of R is set
T is Element of the carrier of R
S is Element of the carrier of R
(0,1) --> (S,T) is Relation-like {0,1} -defined the carrier of R -valued Function-like non empty V24({0,1}) quasi_total Element of bool [:{0,1}, the carrier of R:]
[:{0,1}, the carrier of R:] is Relation-like set
bool [:{0,1}, the carrier of R:] is set
S is open Element of bool the carrier of R
chi (S, the carrier of R) is Relation-like the carrier of R -defined {{},1} -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R,{{},1}:]
[: the carrier of R,{{},1}:] is Relation-like set
bool [: the carrier of R,{{},1}:] is set
(chi (S, the carrier of R)) * ((0,1) --> (S,T)) is Relation-like {0,1} -defined {{},1} -valued Function-like non empty V24({0,1}) quasi_total Element of bool [:{0,1},{{},1}:]
[:{0,1},{{},1}:] is Relation-like set
bool [:{0,1},{{},1}:] is set
[: the carrier of R, the carrier of Sierpinski_Space:] is Relation-like set
bool [: the carrier of R, the carrier of Sierpinski_Space:] is set
f is Relation-like the carrier of R -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of Sierpinski_Space:]
f . T is Element of the carrier of Sierpinski_Space
[: the carrier of Sierpinski_Space, the carrier of R:] is Relation-like set
bool [: the carrier of Sierpinski_Space, the carrier of R:] is set
S is Relation-like the carrier of Sierpinski_Space -defined the carrier of R -valued Function-like non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of R:]
S . 1 is set
f . S is Element of the carrier of Sierpinski_Space
S . 0 is set
f * S is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
rf is Element of the carrier of Sierpinski_Space
(f * S) . rf is Element of the carrier of Sierpinski_Space
(id Sierpinski_Space) . rf is Element of the carrier of Sierpinski_Space
BoolePoset 1 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V305() up-complete /\-complete distributive V381() complemented Boolean RelStr
BooleLatt 1 is non empty V205() V212() V219() complete L17()
LattPOSet (BooleLatt 1) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V305() up-complete /\-complete RelStr
the carrier of (BooleLatt 1) is non empty set
K454((BooleLatt 1)) is Relation-like the carrier of (BooleLatt 1) -defined the carrier of (BooleLatt 1) -valued V16() V19() V23() V24( the carrier of (BooleLatt 1)) quasi_total Element of bool [: the carrier of (BooleLatt 1), the carrier of (BooleLatt 1):]
[: the carrier of (BooleLatt 1), the carrier of (BooleLatt 1):] is Relation-like set
bool [: the carrier of (BooleLatt 1), the carrier of (BooleLatt 1):] is set
RelStr(# the carrier of (BooleLatt 1),K454((BooleLatt 1)) #) is strict RelStr
R is non empty 1-sorted
the carrier of R is non empty set
bool the carrier of R is set
T is Element of bool the carrier of R
chi (T, the carrier of R) is Relation-like the carrier of R -defined {{},1} -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R,{{},1}:]
[: the carrier of R,{{},1}:] is Relation-like set
bool [: the carrier of R,{{},1}:] is set
S is Element of bool the carrier of R
chi (S, the carrier of R) is Relation-like the carrier of R -defined {{},1} -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R,{{},1}:]
S is TopAugmentation of BoolePoset 1
the carrier of S is set
[: the carrier of R, the carrier of S:] is Relation-like set
bool [: the carrier of R, the carrier of S:] is set
f is Relation-like the carrier of R -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of R, the carrier of S:]
S is Relation-like the carrier of R -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of R, the carrier of S:]
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
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
rf is set
the carrier of (BoolePoset 1) is non empty set
x is Element of the carrier of R
f . x is Element of the carrier of S
S . x is Element of the carrier of S
c₉ is Element of the carrier of (BoolePoset 1)
b is Element of the carrier of (BoolePoset 1)
f . rf is set
S . rf is set
rf is set
x is Element of the carrier of R
S . x is Element of the carrier of S
f . x is Element of the carrier of S
c₉ is Element of the carrier of (BoolePoset 1)
b is Element of the carrier of (BoolePoset 1)
Xx is Element of the carrier of S
Xy is Element of the carrier of S
R is non empty RelStr
the carrier of R is non empty set
T is non empty set
R |^ T is non empty strict RelStr
T --> R is Relation-like T -defined {R} -valued Function-like constant non empty V24(T) quasi_total V361() RelStr-yielding non-Empty Element of bool [:T,{R}:]
{R} is non empty set
[:T,{R}:] is Relation-like set
bool [:T,{R}:] is set
product (T --> R) is non empty V177() strict RelStr
S is Relation-like the carrier of R -defined Function-like V24( the carrier of R) set
S is non empty full SubRelStr of R |^ T
the carrier of S is non empty set
rng S is set
f is set
dom S is Element of bool the carrier of R
bool the carrier of R is set
S is set
S . S is set
rf is Element of the carrier of R
T --> rf is Relation-like T -defined the carrier of R -valued Function-like constant non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
[:T, the carrier of R:] is Relation-like set
bool [:T, the carrier of R:] is set
dom S is Element of bool the carrier of R
bool the carrier of R is set
[: the carrier of R, the carrier of S:] is Relation-like set
bool [: the carrier of R, the carrier of S:] is set
f is Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of S:]
S is Element of the carrier of R
f . S is Element of the carrier of S
rf is Element of the carrier of R
f . rf is Element of the carrier of S
T --> rf is Relation-like T -defined the carrier of R -valued Function-like constant non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
[:T, the carrier of R:] is Relation-like set
bool [:T, the carrier of R:] is set
{rf} is non empty set
[:T,{rf}:] is Relation-like set
T --> S is Relation-like T -defined the carrier of R -valued Function-like constant non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
{S} is non empty set
[:T,{S}:] is Relation-like set
the Element of T is Element of T
the carrier of (R |^ T) is non empty set
rf is Element of the carrier of R
f . rf is Element of the carrier of S
x is Element of the carrier of R
f . x is Element of the carrier of S
[:T, the carrier of R:] is Relation-like set
bool [:T, the carrier of R:] is set
T --> rf is Relation-like T -defined the carrier of R -valued Function-like constant non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
T --> x is Relation-like T -defined the carrier of R -valued Function-like constant non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
the carrier of (product (T --> R)) is non empty set
c₉ is Element of the carrier of (R |^ T)
b is Element of the carrier of (R |^ T)
(T --> R) . the Element of T is non empty RelStr
Xx is Relation-like T -defined the carrier of R -valued Function-like non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
Xy is Relation-like T -defined the carrier of R -valued Function-like non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
i is set
Xx . i is set
Xy . i is set
(T --> x) . i is set
(T --> rf) . i is set
a9 is Relation-like Function-like Element of the carrier of (product (T --> R))
a9 . the Element of T is Element of the carrier of ((T --> R) . the Element of T)
the carrier of ((T --> R) . the Element of T) is non empty set
b9 is Relation-like Function-like Element of the carrier of (product (T --> R))
b9 . the Element of T is Element of the carrier of ((T --> R) . the Element of T)
Xy . the Element of T is Element of the carrier of R
rng f is non empty Element of bool the carrier of S
bool the carrier of S is set
S is set
rf is Element of the carrier of S
x is Element of the carrier of R
T --> x is Relation-like T -defined the carrier of R -valued Function-like constant non empty V24(T) quasi_total Element of bool [:T, the carrier of R:]
f . x is Element of the carrier of S
R is non empty TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
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 non empty V24( the carrier of T) quasi_total continuous open 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 non empty V24( the carrier of R) quasi_total continuous open 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 continuous 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
[#] T is non empty non proper open closed Element of bool 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 continuous 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 continuous 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
[#] R is non empty non proper open closed Element of bool 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 continuous Element of bool [: the carrier of T, the carrier of R:]
S * rf is Relation-like the carrier of T -defined the carrier of T -defined the carrier of T -valued the carrier of T -valued Function-like non empty V24( the carrier of T) V24( the carrier of T) quasi_total quasi_total continuous Element of bool [: the carrier of T, the carrier of T:]
rf * S is Relation-like the carrier of R -defined the carrier of R -defined the carrier of R -valued the carrier of R -valued Function-like non empty V24( the carrier of R) V24( the carrier of R) quasi_total quasi_total continuous 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 continuous 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 continuous 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 -defined the carrier of T -valued the carrier of T -valued Function-like non empty V24( the carrier of T) V24( the carrier of T) quasi_total quasi_total continuous 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 -defined the carrier of R -valued the carrier of R -valued Function-like non empty V24( the carrier of R) V24( the carrier of R) quasi_total quasi_total continuous Element of bool [: the carrier of R, the carrier of R:]
rng S is non empty Element of bool the carrier of T
dom S is non empty Element of bool the carrier of R
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:]
R is non empty TopSpace-like TopStruct
the carrier of R is non empty set
T is non empty TopSpace-like TopStruct
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
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of T, the carrier of S:] is Relation-like set
bool [: the carrier of T, the carrier of S:] is set
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total continuous open 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 S is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous open 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
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
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:]
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:]
S * f 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 is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
S " is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is Relation-like set
bool [: the carrier of S, the carrier of T:] is set
f * (S ") is Relation-like the carrier of S -defined the carrier of R -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of R:]
[: the carrier of S, the carrier of R:] is Relation-like set
bool [: the carrier of S, the carrier of R:] is set
S * S is Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of S:]
[: the carrier of R, the carrier of S:] is Relation-like set
bool [: the carrier of R, the carrier of S:] is set
(S * S) * (f * (S ")) is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
rng S is non empty Element of bool the carrier of S
bool the carrier of S is set
[#] S is non empty non proper open closed Element of bool the carrier of S
(S * S) * f is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
((S * S) * f) * (S ") is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
S * (id the carrier of T) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
(S * (id the carrier of T)) * (S ") is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
S * (S ") is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
T is non empty TopSpace-like TopStruct
R is non empty TopSpace-like TopStruct
S is non empty TopSpace-like TopStruct
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 T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total continuous open 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 continuous 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 continuous Element of bool [: the carrier of R, the carrier of T:]
f * S is Relation-like the carrier of T -defined the carrier of T -defined the carrier of T -valued the carrier of T -valued Function-like non empty V24( the carrier of T) V24( the carrier of T) quasi_total quasi_total continuous Element of bool [: the carrier of T, the carrier of T:]
the carrier of S is non empty set
[: the carrier of T, the carrier of S:] is Relation-like set
bool [: the carrier of T, the carrier of S:] is set
S is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V24( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
S " is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is Relation-like set
bool [: the carrier of S, the carrier of T:] is set
[: the carrier of S, the carrier of R:] is Relation-like set
bool [: the carrier of S, the carrier of R:] is set
S * (S ") is Relation-like the carrier of S -defined the carrier of R -valued Function-like non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of R:]
[: the carrier of R, the carrier of S:] is Relation-like set
bool [: the carrier of R, the carrier of S:] is set
S * f is Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty V24( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of S:]
rf is Relation-like the carrier of S -defined the carrier of R -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of R:]
id S is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V24( the carrier of S) quasi_total continuous open 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
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
x is Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty V24( the carrier of R) quasi_total continuous Element of bool [: the carrier of R, the carrier of S:]
x * rf is Relation-like the carrier of S -defined the carrier of S -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of S) V24( the carrier of S) quasi_total quasi_total continuous Element of bool [: the carrier of S, the carrier of S:]
R is non empty TopSpace-like TopStruct
T is non empty TopSpace-like SubSpace of R
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 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
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total continuous open 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:]
R is non empty TopSpace-like TopStruct
the carrier of R is non empty set
T is non empty TopSpace-like SubSpace 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 non empty V24( the carrier of T) quasi_total continuous open 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 continuous 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:]
[#] T is non empty non proper open closed Element of bool the carrier of T
bool the carrier of T is set
[#] R is non empty non proper open closed Element of bool the carrier of R
bool the carrier of R is set
S is Element of the carrier of T
(S * (incl (T,R))) . S is Element of the carrier of T
(incl (T,R)) . S is Element of the carrier of R
S . ((incl (T,R)) . S) is Element of the carrier of T
S . S is set
f is Element of the carrier of R
(id T) . S is Element of the carrier of T
R is non empty TopSpace-like TopStruct
T is non empty TopSpace-like SubSpace of R
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
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 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 continuous 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 continuous Element of bool [: the carrier of T, the carrier of R:]
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V24( the carrier of T) quasi_total continuous open 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 * S is Relation-like the carrier of T -defined the carrier of T -defined the carrier of T -valued the carrier of T -valued Function-like non empty V24( the carrier of T) V24( the carrier of T) quasi_total quasi_total continuous Element of bool [: the carrier of T, the carrier of T:]
R is non empty TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
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 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 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:]
Image S is non empty TopSpace-like SubSpace of T
the carrier of (Image S) is non empty 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 Element of bool [: the carrier of T, the carrier of (Image S):]
[: 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
S is non empty TopSpace-like SubSpace of T
the carrier of S is non empty set
[: the carrier of T, the carrier of S:] is Relation-like set
bool [: the carrier of T, the carrier of S:] is set
[#] T is non empty non proper open closed Element of bool the carrier of T
bool the carrier of T is set
S is non empty TopSpace-like SubSpace of T
[#] S is non empty non proper open closed Element of bool the carrier of S
the carrier of S is non empty set
bool the carrier of S is set
f is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V24( the carrier of T) quasi_total continuous Element of bool [: the carrier of T, the carrier of S:]
rng f is non empty Element of bool the carrier of S
bool the carrier of S is set
x is Element of the carrier of T
rf is Element of bool the carrier of T
T | rf is strict TopSpace-like SubSpace of T
[#] (T | rf) is non proper open closed Element of bool the carrier of (T | rf)
the carrier of (T | rf) is set
bool the carrier of (T | rf) is set
dom f is non empty Element of bool the carrier of T
f . x is Element of the carrier of S
c₉ is set
f . c₉ is set
S is non empty TopSpace-like SubSpace of T