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

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

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

S . x is Element of the carrier of R

S . c

rf . x is Element of the carrier of (Image S)

rf . c

(id T) . x is Element of the carrier of T

S . (S . x) is Element of the carrier of T

(id T) . c

S . (S . c

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

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

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

c

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

("\/" (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

c

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

("/\" (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