:: WAYBEL10 semantic presentation

K222() is Element of bool K218()

K218() is set

bool K218() is set

K141() is set

bool K141() is set

K184() is L6()

the carrier of K184() is set

bool K222() is set

K267() is set

{} is set

the Function-like functional empty set is Function-like functional empty set

{{}} is set

K245({{}}) is M15({{}})

[:K245({{}}),{{}}:] is set

bool [:K245({{}}),{{}}:] is set

K39(K245({{}}),{{}}) is set

1 is non empty set

{{},1} is set

F

F

the carrier of F

L is set

f is set

bool the carrier of F

f is non empty Element of bool the carrier of F

subrelstr f is non empty strict full SubRelStr of F

the carrier of (subrelstr f) is non empty set

c

F

the carrier of F

F

the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

RelStr(# the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

RelStr(# the carrier of F

g is set

c

g is set

c

g is set

c

[g,c

{g,c

{g} is set

{{g,c

f9 is Element of the carrier of F

h is Element of the carrier of F

x is Element of the carrier of F

y is Element of the carrier of F

f9 is Element of the carrier of F

h is Element of the carrier of F

x is Element of the carrier of F

y is Element of the carrier of F

F

F

the carrier of F

F

the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

RelStr(# the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

RelStr(# the carrier of F

L is set

f is set

the InternalRel of F

the carrier of F

[: the carrier of F

bool [: the carrier of F

L is Element of the carrier of F

f is Element of the carrier of F

g is Element of the carrier of F

c

[g,c

{g,c

{g} is set

{{g,c

[L,f] is set

{L,f} is set

{L} is set

{{L,f},{L}} is set

L is Element of the carrier of F

f is Element of the carrier of F

g is Element of the carrier of F

c

[g,c

{g,c

{g} is set

{{g,c

[L,f] is set

{L,f} is set

{L} is set

{{L,f},{L}} is set

L is set

f is set

F

the carrier of F

F

the carrier of F

F

the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

RelStr(# the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

RelStr(# the carrier of F

L is set

L is set

L is Relation-like set

f is Relation-like set

L ~ is Relation-like set

f ~ is Relation-like set

(f ~) ~ is Relation-like set

(L ~) ~ is Relation-like set

f is RelStr

L is RelStr

f ~ is strict RelStr

the carrier of f is set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is set

bool [: the carrier of f, the carrier of f:] is set

the InternalRel of f ~ is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

RelStr(# the carrier of f,( the InternalRel of f ~) #) is strict RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (f ~) is set

the carrier of (L ~) is set

the InternalRel of (f ~) is Relation-like the carrier of (f ~) -defined the carrier of (f ~) -valued Element of bool [: the carrier of (f ~), the carrier of (f ~):]

[: the carrier of (f ~), the carrier of (f ~):] is set

bool [: the carrier of (f ~), the carrier of (f ~):] is set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of bool [: the carrier of (L ~), the carrier of (L ~):]

[: the carrier of (L ~), the carrier of (L ~):] is set

bool [: the carrier of (L ~), the carrier of (L ~):] is set

the carrier of (f ~) is set

the carrier of (L ~) is set

the InternalRel of (f ~) is Relation-like the carrier of (f ~) -defined the carrier of (f ~) -valued Element of bool [: the carrier of (f ~), the carrier of (f ~):]

[: the carrier of (f ~), the carrier of (f ~):] is set

bool [: the carrier of (f ~), the carrier of (f ~):] is set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of bool [: the carrier of (L ~), the carrier of (L ~):]

[: the carrier of (L ~), the carrier of (L ~):] is set

bool [: the carrier of (L ~), the carrier of (L ~):] is set

the carrier of (f ~) is set

the InternalRel of (f ~) is Relation-like the carrier of (f ~) -defined the carrier of (f ~) -valued Element of bool [: the carrier of (f ~), the carrier of (f ~):]

[: the carrier of (f ~), the carrier of (f ~):] is set

bool [: the carrier of (f ~), the carrier of (f ~):] is set

the carrier of (L ~) is set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of bool [: the carrier of (L ~), the carrier of (L ~):]

[: the carrier of (L ~), the carrier of (L ~):] is set

bool [: the carrier of (L ~), the carrier of (L ~):] is set

the carrier of (L ~) is set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of bool [: the carrier of (L ~), the carrier of (L ~):]

[: the carrier of (L ~), the carrier of (L ~):] is set

bool [: the carrier of (L ~), the carrier of (L ~):] is set

the carrier of (f ~) is set

the InternalRel of (f ~) is Relation-like the carrier of (f ~) -defined the carrier of (f ~) -valued Element of bool [: the carrier of (f ~), the carrier of (f ~):]

[: the carrier of (f ~), the carrier of (f ~):] is set

bool [: the carrier of (f ~), the carrier of (f ~):] is set

f is RelStr

L is RelStr

f ~ is strict RelStr

the carrier of f is set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is set

bool [: the carrier of f, the carrier of f:] is set

the InternalRel of f ~ is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

RelStr(# the carrier of f,( the InternalRel of f ~) #) is strict RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the InternalRel of L |_2 the carrier of f is Relation-like set

( the InternalRel of L |_2 the carrier of f) ~ is Relation-like set

( the InternalRel of L ~) |_2 the carrier of f is Relation-like set

(( the InternalRel of L ~) |_2 the carrier of f) ~ is Relation-like set

( the InternalRel of L ~) ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

(( the InternalRel of L ~) ~) |_2 the carrier of f is Relation-like set

the InternalRel of (f ~) is Relation-like the carrier of (f ~) -defined the carrier of (f ~) -valued Element of bool [: the carrier of (f ~), the carrier of (f ~):]

the carrier of (f ~) is set

[: the carrier of (f ~), the carrier of (f ~):] is set

bool [: the carrier of (f ~), the carrier of (f ~):] is set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of bool [: the carrier of (L ~), the carrier of (L ~):]

the carrier of (L ~) is set

[: the carrier of (L ~), the carrier of (L ~):] is set

bool [: the carrier of (L ~), the carrier of (L ~):] is set

the InternalRel of (L ~) |_2 the carrier of f is Relation-like set

L is RelStr

f is full SubRelStr of L

f ~ is strict RelStr

the carrier of f is set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is set

bool [: the carrier of f, the carrier of f:] is set

the InternalRel of f ~ is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

RelStr(# the carrier of f,( the InternalRel of f ~) #) is strict RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is set

f is non empty RelStr

L --> f is Relation-like L -defined {f} -valued Function-like constant V24(L) quasi_total V104() RelStr-yielding Element of bool [:L,{f}:]

{f} is set

[:L,{f}:] is set

bool [:L,{f}:] is set

g is 1-sorted

rng (L --> f) is trivial set

rng (L --> f) is trivial Element of bool {f}

bool {f} is set

L is RelStr

the carrier of L is set

f is non empty reflexive RelStr

the carrier of f is non empty set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

the Element of the carrier of f is Element of the carrier of f

L --> the Element of the carrier of f is Relation-like the carrier of L -defined the carrier of f -valued Function-like V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of f:]

the carrier of L --> the Element of the carrier of f is Relation-like the carrier of L -defined the carrier of f -valued Function-like constant V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of f:]

c

f9 is Element of the carrier of L

h is Element of the carrier of L

c

c

[f9,h] is set

{f9,h} is set

{f9} is set

{{f9,h},{f9}} is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

x is Element of the carrier of f

y is Element of the carrier of f

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

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

L is non empty reflexive RelStr

the carrier of L is non empty set

f is non empty reflexive RelStr

the carrier of f is non empty set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

g is Relation-like the carrier of L -defined the carrier of f -valued Function-like non empty V24( the carrier of L) quasi_total monotone Element of bool [: the carrier of L, the carrier of f:]

Image g is non empty strict reflexive full SubRelStr of f

rng g is Element of bool the carrier of f

bool the carrier of f is set

subrelstr (rng g) is strict reflexive full SubRelStr of f

corestr g is Relation-like the carrier of L -defined the carrier of (Image g) -valued Function-like non empty V24( the carrier of L) quasi_total onto Element of bool [: the carrier of L, the carrier of (Image g):]

the carrier of (Image g) is non empty set

[: the carrier of L, the carrier of (Image g):] is set

bool [: the carrier of L, the carrier of (Image g):] is set

the carrier of (Image g) |` g is Relation-like the carrier of L -defined the carrier of f -valued Function-like Element of bool [: the carrier of L, the carrier of f:]

c

f9 is Element of the carrier of L

(corestr g) . c

(corestr g) . f9 is Element of the carrier of (Image g)

g . f9 is Element of the carrier of f

g . c

L is non empty reflexive RelStr

id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V24( the carrier of L) quasi_total idempotent monotone isomorphic projection closure kernel Element of bool [: the carrier of L, the carrier of L:]

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

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

bool the carrier of L is set

f is Element of bool the carrier of L

"\/" (f,L) is Element of the carrier of L

(id L) . ("\/" (f,L)) is Element of the carrier of L

(id L) .: f is Element of bool the carrier of L

"\/" (((id L) .: f),L) is Element of the carrier of L

bool the carrier of L is set

f is Element of bool the carrier of L

"/\" (f,L) is Element of the carrier of L

(id L) . ("/\" (f,L)) is Element of the carrier of L

(id L) .: f is Element of bool the carrier of L

"/\" (((id L) .: f),L) is Element of the carrier of L

L is RelStr

the carrier of L is set

bool the carrier of L is set

f is Element of bool the carrier of L

id f is Relation-like Function-like one-to-one set

subrelstr f is strict full SubRelStr of L

the carrier of (subrelstr f) is set

[: the carrier of (subrelstr f), the carrier of L:] is set

bool [: the carrier of (subrelstr f), the carrier of L:] is set

rng (id f) is set

dom (id f) is set

g is Relation-like the carrier of (subrelstr f) -defined the carrier of L -valued Function-like quasi_total Element of bool [: the carrier of (subrelstr f), the carrier of L:]

c

f9 is Element of the carrier of (subrelstr f)

g . c

g . f9 is set

[c

{c

{c

{{c

the InternalRel of (subrelstr f) is Relation-like the carrier of (subrelstr f) -defined the carrier of (subrelstr f) -valued Element of bool [: the carrier of (subrelstr f), the carrier of (subrelstr f):]

[: the carrier of (subrelstr f), the carrier of (subrelstr f):] is set

bool [: the carrier of (subrelstr f), the carrier of (subrelstr f):] is set

h is Element of the carrier of L

x is Element of the carrier of L

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

[h,x] is set

{h,x} is set

{h} is set

{{h,x},{h}} is set

L is non empty reflexive RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V24( the carrier of L) 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 L, the carrier of L:]

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

L is non empty reflexive RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

f is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

g is Element of the carrier of L

f . g is Element of the carrier of L

id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V24( the carrier of L) 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 L, the carrier of L:]

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

(id L) . g is Element of the carrier of L

L is RelStr

the carrier of L is set

f is RelStr

the carrier of f is set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

g is SubRelStr of L

the carrier of g is set

c

c

[: the carrier of g, the carrier of f:] is set

bool [: the carrier of g, the carrier of f:] is set

c

f9 is set

(c

c

L is RelStr

the carrier of L is set

f is RelStr

the carrier of f is set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

g is Relation-like the carrier of L -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of f:]

c

g | c

the carrier of c

[: the carrier of c

bool [: the carrier of c

g | the carrier of c

L is non empty reflexive RelStr

the carrier of L is non empty set

f is non empty reflexive RelStr

the carrier of f is non empty set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

c

g is Relation-like the carrier of L -defined the carrier of f -valued Function-like non empty V24( the carrier of L) quasi_total monotone Element of bool [: the carrier of L, the carrier of f:]

g | c

the carrier of c

[: the carrier of c

bool [: the carrier of c

f9 is Element of the carrier of c

h is Element of the carrier of c

(g | c

(g | c

[f9,h] is set

{f9,h} is set

{f9} is set

{{f9,h},{f9}} is set

the InternalRel of c

[: the carrier of c

bool [: the carrier of c

x is Element of the carrier of L

y is Element of the carrier of L

g . y is Element of the carrier of f

g . x is Element of the carrier of f

a is Element of the carrier of f

b is Element of the carrier of f

L is non empty RelStr

the carrier of L is non empty set

f is non empty RelStr

the carrier of f is non empty set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

[: the carrier of f, the carrier of L:] is set

bool [: the carrier of f, the carrier of L:] is set

g is non empty SubRelStr of L

the carrier of g is non empty set

c

c

c

[: the carrier of g, the carrier of f:] is set

bool [: the carrier of g, the carrier of f:] is set

Image (c

rng (c

bool the carrier of f is set

subrelstr (rng (c

the carrier of (Image (c

[: the carrier of (Image (c

bool [: the carrier of (Image (c

(c

f9 is Relation-like the carrier of f -defined the carrier of L -valued Function-like non empty V24( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of L:]

f9 | (Image (c

[: the carrier of (Image (c

bool [: the carrier of (Image (c

dom c

bool the carrier of L is set

dom (f9 | (Image (c

bool the carrier of (Image (c

rng (f9 | (Image (c

x is set

y is set

(f9 | (Image (c

a is Element of the carrier of (Image (c

b is Element of the carrier of g

(c

c

f9 . a is set

dom (c

bool the carrier of g is set

x is set

y is set

(c

((c

c

f9 . x is set

(f9 | (Image (c

dom ((c

L is RelStr

f is non empty reflexive RelStr

MonMaps (L,f) is strict reflexive full SubRelStr of f |^ the carrier of L

the carrier of L is set

f |^ the carrier of L is non empty strict reflexive RelStr

the carrier of f is non empty set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

the Relation-like the carrier of L -defined the carrier of f -valued Function-like V24( the carrier of L) quasi_total monotone Element of bool [: the carrier of L, the carrier of f:] is Relation-like the carrier of L -defined the carrier of f -valued Function-like V24( the carrier of L) quasi_total monotone Element of bool [: the carrier of L, the carrier of f:]

Funcs ( the carrier of L, the carrier of f) is functional non empty FUNCTION_DOMAIN of the carrier of L, the carrier of f

L is RelStr

the carrier of L is set

f is non empty reflexive RelStr

MonMaps (L,f) is non empty strict reflexive full SubRelStr of f |^ the carrier of L

f |^ the carrier of L is non empty strict reflexive RelStr

the carrier of (MonMaps (L,f)) is non empty set

the carrier of f is non empty set

[: the carrier of L, the carrier of f:] is set

bool [: the carrier of L, the carrier of f:] is set

g is set

c

the carrier of (f |^ the carrier of L) is non empty set

Funcs ( the carrier of L, the carrier of f) is functional non empty FUNCTION_DOMAIN of the carrier of L, the carrier of f

f9 is Relation-like the carrier of L -defined the carrier of f -valued Function-like V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of f:]

c

L is non empty reflexive RelStr

MonMaps (L,L) is non empty strict reflexive full SubRelStr of L |^ the carrier of L

the carrier of L is non empty set

L |^ the carrier of L is non empty strict reflexive RelStr

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

the Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:] is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

Funcs ( the carrier of L, the carrier of L) is functional non empty FUNCTION_DOMAIN of the carrier of L, the carrier of L

the carrier of (MonMaps (L,L)) is non empty set

g is non empty strict reflexive full SubRelStr of MonMaps (L,L)

the carrier of g is non empty set

c

f is non empty strict reflexive full SubRelStr of MonMaps (L,L)

the carrier of f is non empty set

g is non empty strict reflexive full SubRelStr of MonMaps (L,L)

the carrier of g is non empty set

c

f9 is Element of the carrier of f

the carrier of (MonMaps (L,L)) is non empty set

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

c

f9 is Element of the carrier of g

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

L is non empty reflexive RelStr

(L) is non empty strict reflexive full SubRelStr of MonMaps (L,L)

MonMaps (L,L) is non empty strict reflexive full SubRelStr of L |^ the carrier of L

the carrier of L is non empty set

L |^ the carrier of L is non empty strict reflexive RelStr

the carrier of (L) is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

f is set

the carrier of (MonMaps (L,L)) is non empty set

L is set

f is non empty RelStr

the carrier of f is non empty set

[:L, the carrier of f:] is set

bool [:L, the carrier of f:] is set

f |^ L is non empty strict RelStr

the carrier of (f |^ L) is non empty set

g is Relation-like L -defined the carrier of f -valued Function-like V24(L) quasi_total Element of bool [:L, the carrier of f:]

c

f9 is Element of the carrier of (f |^ L)

h is Element of the carrier of (f |^ L)

L --> f is Relation-like L -defined {f} -valued Function-like constant V24(L) quasi_total V104() RelStr-yielding non-Empty Element of bool [:L,{f}:]

{f} is set

[:L,{f}:] is set

bool [:L,{f}:] is set

product (L --> f) is strict RelStr

the carrier of (product (L --> f)) is set

Carrier (L --> f) is Relation-like L -defined Function-like V24(L) set

product (Carrier (L --> f)) is set

y is Relation-like Function-like set

a is Relation-like Function-like set

y is set

g . y is set

c

(L --> f) . y is set

a is Relation-like Function-like set

b is Relation-like Function-like set

a is RelStr

the carrier of a is set

b is Element of the carrier of a

A is Element of the carrier of a

y is Relation-like Function-like set

a is Relation-like Function-like set

b is Relation-like Function-like set

A is Relation-like Function-like set

B is set

(L --> f) . B is set

g . B is set

c

b . B is set

A . B is set

i is Element of the carrier of f

j is Element of the carrier of f

y is Relation-like Function-like set

a is Relation-like Function-like set

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of MonMaps (L,L)

MonMaps (L,L) is non empty strict reflexive transitive antisymmetric full SubRelStr of L |^ the carrier of L

L |^ the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (L) is non empty set

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

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

c

f9 is Element of the carrier of (L)

the carrier of (MonMaps (L,L)) is non empty set

the carrier of (L |^ the carrier of L) is non empty set

h is Element of the carrier of (MonMaps (L,L))

x is Element of the carrier of (MonMaps (L,L))

y is Element of the carrier of (L |^ the carrier of L)

a is Element of the carrier of (L |^ the carrier of L)

L is reflexive RelStr

f is reflexive full SubRelStr of L

the carrier of f is set

g is reflexive full SubRelStr of L

the carrier of g is set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is set

bool [: the carrier of f, the carrier of f:] is set

the InternalRel of g is Relation-like the carrier of g -defined the carrier of g -valued Element of bool [: the carrier of g, the carrier of g:]

[: the carrier of g, the carrier of g:] is set

bool [: the carrier of g, the carrier of g:] is set

c

f9 is set

[c

{c

{c

{{c

the carrier of L is set

h is Element of the carrier of f

x is Element of the carrier of f

y is Element of the carrier of L

a is Element of the carrier of L

b is Element of the carrier of g

A is Element of the carrier of g

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

f is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

g is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

Image g is non empty strict reflexive transitive antisymmetric full SubRelStr of L

rng g is Element of bool the carrier of L

bool the carrier of L is set

subrelstr (rng g) is strict reflexive transitive antisymmetric full SubRelStr of L

Image f is non empty strict reflexive transitive antisymmetric full SubRelStr of L

rng f is Element of bool the carrier of L

subrelstr (rng f) is strict reflexive transitive antisymmetric full SubRelStr of L

the carrier of (Image g) is non empty set

the carrier of (Image f) is non empty set

c

f9 is Element of the carrier of L

g . f9 is Element of the carrier of L

g . (g . f9) is Element of the carrier of L

f . (g . f9) is Element of the carrier of L

the InternalRel of (Image g) is Relation-like the carrier of (Image g) -defined the carrier of (Image g) -valued Element of bool [: the carrier of (Image g), the carrier of (Image g):]

[: the carrier of (Image g), the carrier of (Image g):] is set

bool [: the carrier of (Image g), the carrier of (Image g):] is set

the InternalRel of (Image f) is Relation-like the carrier of (Image f) -defined the carrier of (Image f) -valued Element of bool [: the carrier of (Image f), the carrier of (Image f):]

[: the carrier of (Image f), the carrier of (Image f):] is set

bool [: the carrier of (Image f), the carrier of (Image f):] is set

c

g . c

f . (g . c

f9 is Element of the carrier of L

f . f9 is Element of the carrier of L

f . c

L is RelStr

the carrier of L is set

bool the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

{ RelStr(# b

{} L is Function-like functional empty directed filtered Element of bool the carrier of L

subrelstr ({} L) is strict full SubRelStr of L

the carrier of (subrelstr ({} L)) is set

the InternalRel of (subrelstr ({} L)) is Relation-like the carrier of (subrelstr ({} L)) -defined the carrier of (subrelstr ({} L)) -valued Element of bool [: the carrier of (subrelstr ({} L)), the carrier of (subrelstr ({} L)):]

[: the carrier of (subrelstr ({} L)), the carrier of (subrelstr ({} L)):] is set

bool [: the carrier of (subrelstr ({} L)), the carrier of (subrelstr ({} L)):] is set

g is non empty set

c

the carrier of c

f9 is set

h is Element of bool the carrier of L

[:h,h:] is set

bool [:h,h:] is set

x is Relation-like h -defined h -valued Element of bool [:h,h:]

RelStr(# h,x #) is strict RelStr

h is strict SubRelStr of L

the carrier of h is set

the InternalRel of h is Relation-like the carrier of h -defined the carrier of h -valued Element of bool [: the carrier of h, the carrier of h:]

[: the carrier of h, the carrier of h:] is set

bool [: the carrier of h, the carrier of h:] is set

f9 is Element of the carrier of c

h is Element of the carrier of c

y is Element of the carrier of c

a is RelStr

x is Element of the carrier of c

f is non empty strict RelStr

the carrier of f is non empty set

g is non empty strict RelStr

the carrier of g is non empty set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is set

bool [: the carrier of f, the carrier of f:] is set

RelStr(# the carrier of f, the InternalRel of f #) is strict RelStr

the InternalRel of g is Relation-like the carrier of g -defined the carrier of g -valued Element of bool [: the carrier of g, the carrier of g:]

[: the carrier of g, the carrier of g:] is set

bool [: the carrier of g, the carrier of g:] is set

RelStr(# the carrier of g, the InternalRel of g #) is strict RelStr

L is RelStr

(L) is non empty strict RelStr

the carrier of (L) is non empty set

f is RelStr

c

g is Element of the carrier of (L)

f9 is RelStr

f9 is RelStr

L is RelStr

(L) is non empty strict RelStr

the carrier of (L) is non empty set

g is Element of the carrier of (L)

c

the carrier of (L) is non empty set

g is Element of the carrier of (L)

c

h is strict SubRelStr of L

f9 is strict SubRelStr of L

the carrier of h is set

the carrier of f9 is set

the InternalRel of h is Relation-like the carrier of h -defined the carrier of h -valued Element of bool [: the carrier of h, the carrier of h:]

[: the carrier of h, the carrier of h:] is set

bool [: the carrier of h, the carrier of h:] is set

the InternalRel of f9 is Relation-like the carrier of f9 -defined the carrier of f9 -valued Element of bool [: the carrier of f9, the carrier of f9:]

[: the carrier of f9, the carrier of f9:] is set

bool [: the carrier of f9, the carrier of f9:] is set

the carrier of (L) is non empty set

g is Element of the carrier of (L)

c

f9 is Element of the carrier of (L)

x is strict SubRelStr of L

y is strict SubRelStr of L

the carrier of x is set

the carrier of y is set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is set

bool [: the carrier of x, the carrier of x:] is set

the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]

[: the carrier of y, the carrier of y:] is set

bool [: the carrier of y, the carrier of y:] is set

h is strict SubRelStr of L

the carrier of h is set

the InternalRel of h is Relation-like the carrier of h -defined the carrier of h -valued Element of bool [: the carrier of h, the carrier of h:]

[: the carrier of h, the carrier of h:] is set

bool [: the carrier of h, the carrier of h:] is set

L is RelStr

(L) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (L) is non empty set

bool the carrier of (L) is set

f is Element of bool the carrier of (L)

the carrier of L is set

g is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

c

[:g,g:] is set

f9 is set

h is RelStr

the InternalRel of h is Relation-like the carrier of h -defined the carrier of h -valued Element of bool [: the carrier of h, the carrier of h:]

the carrier of h is set

[: the carrier of h, the carrier of h:] is set

bool [: the carrier of h, the carrier of h:] is set

x is set

f9 is set

bool [:g,g:] is set

h is set

f9 is Relation-like g -defined g -valued Element of bool [:g,g:]

RelStr(# g,f9 #) is strict RelStr

h is SubRelStr of L

x is Element of the carrier of (L)

y is Element of the carrier of (L)

a is Element of the carrier of (L)

b is strict SubRelStr of L

the carrier of b is set

the InternalRel of b is Relation-like the carrier of b -defined the carrier of b -valued Element of bool [: the carrier of b, the carrier of b:]

[: the carrier of b, the carrier of b:] is set

bool [: the carrier of b, the carrier of b:] is set

A is set

B is set

[A,B] is set

{A,B} is set

{A} is set

{{A,B},{A}} is set

A is set

a is Element of the carrier of (L)

b is strict SubRelStr of L

the InternalRel of b is Relation-like the carrier of b -defined the carrier of b -valued Element of bool [: the carrier of b, the carrier of b:]

the carrier of b is set

[: the carrier of b, the carrier of b:] is set

bool [: the carrier of b, the carrier of b:] is set

A is set

B is set

[A,B] is set

{A,B} is set

{A} is set

{{A,B},{A}} is set

i is RelStr

the InternalRel of i is Relation-like the carrier of i -defined the carrier of i -valued Element of bool [: the carrier of i, the carrier of i:]

the carrier of i is set

[: the carrier of i, the carrier of i:] is set

bool [: the carrier of i, the carrier of i:] is set

j is Element of the carrier of (L)

A is set

B is RelStr

the carrier of B is set

i is Element of the carrier of (L)

g is Element of the carrier of (L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

f is SubRelStr of L

{} f is Function-like functional empty directed filtered Element of bool the carrier of f

the carrier of f is set

bool the carrier of f is set

f is SubRelStr of L

{} f is Function-like functional empty directed filtered Element of bool the carrier of f

the carrier of f is set

bool the carrier of f is set

L is non empty RelStr

L is non empty RelStr

[#] L is non empty non proper lower upper Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is set

subrelstr ([#] L) is non empty strict full SubRelStr of L

the carrier of (subrelstr ([#] L)) is non empty set

bool the carrier of (subrelstr ([#] L)) is set

g is Element of bool the carrier of (subrelstr ([#] L))

"/\" (g,L) is Element of the carrier of L

bool the carrier of (subrelstr ([#] L)) is set

g is Element of bool the carrier of (subrelstr ([#] L))

"\/" (g,L) is Element of the carrier of L

L is non empty RelStr

(L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

[#] L is non empty non proper lower upper Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is set

subrelstr ([#] L) is non empty strict full meet-inheriting join-inheriting infs-inheriting sups-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of L

the carrier of (L) is non empty set

g is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

the carrier of g is non empty set

c

f is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

the carrier of f is non empty set

g is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

the carrier of g is non empty set

c

the carrier of (L) is non empty set

c

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is set

bool [: the carrier of f, the carrier of f:] is set

RelStr(# the carrier of f, the InternalRel of f #) is strict RelStr

the InternalRel of g is Relation-like the carrier of g -defined the carrier of g -valued Element of bool [: the carrier of g, the carrier of g:]

[: the carrier of g, the carrier of g:] is set

bool [: the carrier of g, the carrier of g:] is set

RelStr(# the carrier of g, the InternalRel of g #) is strict RelStr

L is non empty RelStr

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

(L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

the carrier of (L) is non empty set

f is set

the carrier of (L) is non empty set

L is non empty RelStr

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

(L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

the carrier of (L) is non empty set

f is RelStr

c

g is Element of the carrier of (L)

the carrier of (L) is non empty set

f9 is Element of the carrier of (L)

h is Element of the carrier of (L)

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

f is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

Image f is non empty strict reflexive transitive antisymmetric full SubRelStr of L

rng f is Element of bool the carrier of L

bool the carrier of L is set

subrelstr (rng f) is strict reflexive transitive antisymmetric full SubRelStr of L

L is non empty reflexive transitive antisymmetric RelStr

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of MonMaps (L,L)

MonMaps (L,L) is non empty strict reflexive transitive antisymmetric full SubRelStr of L |^ the carrier of L

the carrier of L is non empty set

L |^ the carrier of L is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (L) is non empty set

(L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

((L),(L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L) ~

(L) ~ is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of ((L),(L)) is non empty set

[: the carrier of (L), the carrier of ((L),(L)):] is set

bool [: the carrier of (L), the carrier of ((L),(L)):] is set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

f is Element of the carrier of (L)

g is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

Image g is non empty strict reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

rng g is Element of bool the carrier of L

bool the carrier of L is set

subrelstr (rng g) is strict reflexive transitive antisymmetric full SubRelStr of L

(L) ~ is non empty strict reflexive transitive antisymmetric RelStr

the carrier of ((L) ~) is non empty set

c

c

f9 is Element of the carrier of ((L) ~)

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

g is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

f . g is set

Image g is non empty strict reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

rng g is Element of bool the carrier of L

subrelstr (rng g) is strict reflexive transitive antisymmetric full SubRelStr of L

c

Image c

rng c

subrelstr (rng c

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

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

c

f . c

f9 is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

Image f9 is non empty strict reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

rng f9 is Element of bool the carrier of L

bool the carrier of L is set

subrelstr (rng f9) is strict reflexive transitive antisymmetric full SubRelStr of L

g . c

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

f is SubRelStr of L

the carrier of f is set

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

c

f9 is Element of the carrier of L

g . f9 is Element of the carrier of L

uparrow f9 is Element of bool the carrier of L

bool the carrier of L is set

K103( the carrier of L,f9) is Element of bool the carrier of L

uparrow K103( the carrier of L,f9) is Element of bool the carrier of L

(uparrow f9) /\ the carrier of f is Element of bool the carrier of L

"/\" (((uparrow f9) /\ the carrier of f),L) is Element of the carrier of L

c

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

f is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

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

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

(L,f) * (L,f) is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of L:]

id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V24( the carrier of L) 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 L, the carrier of L:]

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

f9 is Element of the carrier of L

(id L) . f9 is Element of the carrier of L

uparrow f9 is non empty filtered upper Element of bool the carrier of L

bool the carrier of L is set

K103( the carrier of L,f9) is Element of bool the carrier of L

uparrow K103( the carrier of L,f9) is upper Element of bool the carrier of L

the carrier of f is non empty set

(uparrow f9) /\ the carrier of f is Element of bool the carrier of L

(L,f) . f9 is Element of the carrier of L

"/\" (((uparrow f9) /\ the carrier of f),L) is Element of the carrier of L

f9 is Element of the carrier of L

(L,f) . f9 is Element of the carrier of L

uparrow f9 is non empty filtered upper Element of bool the carrier of L

K103( the carrier of L,f9) is Element of bool the carrier of L

uparrow K103( the carrier of L,f9) is upper Element of bool the carrier of L

(uparrow f9) /\ the carrier of f is Element of bool the carrier of L

bool the carrier of f is set

(L,f) . ((L,f) . f9) is Element of the carrier of L

uparrow ((L,f) . f9) is non empty filtered upper Element of bool the carrier of L

K103( the carrier of L,((L,f) . f9)) is Element of bool the carrier of L

uparrow K103( the carrier of L,((L,f) . f9)) is upper Element of bool the carrier of L

(uparrow ((L,f) . f9)) /\ the carrier of f is Element of bool the carrier of L

"/\" (((uparrow ((L,f) . f9)) /\ the carrier of f),L) is Element of the carrier of L

y is Element of bool the carrier of f

"/\" (y,L) is Element of the carrier of L

"/\" (((uparrow f9) /\ the carrier of f),L) is Element of the carrier of L

(id L) . ((L,f) . f9) is Element of the carrier of L

c

c

f9 is Element of the carrier of L

uparrow f9 is non empty filtered upper Element of bool the carrier of L

K103( the carrier of L,f9) is Element of bool the carrier of L

uparrow K103( the carrier of L,f9) is upper Element of bool the carrier of L

(uparrow f9) /\ the carrier of f is Element of bool the carrier of L

h is Element of the carrier of L

uparrow h is non empty filtered upper Element of bool the carrier of L

K103( the carrier of L,h) is Element of bool the carrier of L

uparrow K103( the carrier of L,h) is upper Element of bool the carrier of L

(uparrow h) /\ the carrier of f is Element of bool the carrier of L

(L,f) . h is Element of the carrier of L

"/\" (((uparrow h) /\ the carrier of f),L) is Element of the carrier of L

(L,f) . f9 is Element of the carrier of L

"/\" (((uparrow f9) /\ the carrier of f),L) is Element of the carrier of L

f9 is set

(id L) . f9 is set

(L,f) . f9 is set

h is Element of the carrier of L

(id L) . h is Element of the carrier of L

(L,f) . h is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

f is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

(L,f) is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

Image (L,f) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

rng (L,f) is Element of bool the carrier of L

bool the carrier of L is set

subrelstr (rng (L,f)) is strict reflexive transitive antisymmetric full SubRelStr of L

the carrier of f is non empty set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is set

bool [: the carrier of f, the carrier of f:] is set

RelStr(# the carrier of f, the InternalRel of f #) is strict RelStr

the carrier of (Image (L,f)) is non empty set

g is set

c

f9 is Element of the carrier of L

(L,f) . f9 is Element of the carrier of L

uparrow f9 is non empty filtered upper Element of bool the carrier of L

K103( the carrier of L,f9) is Element of bool the carrier of L

uparrow K103( the carrier of L,f9) is upper Element of bool the carrier of L

(uparrow f9) /\ the carrier of f is Element of bool the carrier of L

bool the carrier of f is set

x is Element of bool the carrier of f

"/\" (x,L) is Element of the carrier of L

c

f9 is Element of the carrier of f

h is Element of the carrier of L

uparrow h is non empty filtered upper Element of bool the carrier of L

K103( the carrier of L,h) is Element of bool the carrier of L

uparrow K103( the carrier of L,h) is upper Element of bool the carrier of L

(uparrow h) /\ the carrier of f is Element of bool the carrier of L

id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V24( the carrier of L) 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 L, the carrier of L:]

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

(id L) . h is Element of the carrier of L

(L,f) . h is Element of the carrier of L

"/\" (((uparrow h) /\ the carrier of f),L) is Element of the carrier of L

dom (L,f) is Element of bool the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

f is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

Image f is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

rng f is Element of bool the carrier of L

bool the carrier of L is set

subrelstr (rng f) is strict reflexive transitive antisymmetric full SubRelStr of L

(L,(Image f)) is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty V24( the carrier of L) 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 L, the carrier of L:]

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

g is Element of the carrier of L

(id L) . g is Element of the carrier of L

f . g is Element of the carrier of L

uparrow g is non empty filtered upper Element of bool the carrier of L

K103( the carrier of L,g) is Element of bool the carrier of L

uparrow K103( the carrier of L,g) is upper Element of bool the carrier of L

dom f is Element of bool the carrier of L

(uparrow g) /\ (rng f) is Element of bool the carrier of L

"/\" (((uparrow g) /\ (rng f)),L) is Element of the carrier of L

c

f9 is set

f . f9 is set

h is Element of the carrier of L

f . h is Element of the carrier of L

f . (f . h) is Element of the carrier of L

the carrier of (Image f) is non empty set

(L,(Image f)) . g is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

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

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of MonMaps (L,L)

MonMaps (L,L) is non empty strict reflexive transitive antisymmetric full SubRelStr of L |^ the carrier of L

the carrier of L is non empty set

L |^ the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (L) is non empty set

(L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

((L),(L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L) ~

(L) ~ is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of ((L),(L)) is non empty set

[: the carrier of (L), the carrier of ((L),(L)):] is set

bool [: the carrier of (L), the carrier of ((L),(L)):] is set

f is Element of the carrier of (L)

(L) . f is Element of the carrier of ((L),(L))

g is Element of the carrier of (L)

(L) . g is Element of the carrier of ((L),(L))

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

c

Image c

rng c

bool the carrier of L is set

subrelstr (rng c

f9 is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

Image f9 is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

rng f9 is Element of bool the carrier of L

subrelstr (rng f9) is strict reflexive transitive antisymmetric full SubRelStr of L

(L,(Image f9)) is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

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

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of MonMaps (L,L)

MonMaps (L,L) is non empty strict reflexive transitive antisymmetric full SubRelStr of L |^ the carrier of L

the carrier of L is non empty set

L |^ the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (L) is non empty set

(L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

((L),(L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L) ~

(L) ~ is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of ((L),(L)) is non empty set

[: the carrier of (L), the carrier of ((L),(L)):] is set

bool [: the carrier of (L), the carrier of ((L),(L)):] is set

(L) " is Relation-like Function-like one-to-one set

[: the carrier of ((L),(L)), the carrier of (L):] is set

bool [: the carrier of ((L),(L)), the carrier of (L):] is set

rng ((L) ") is set

dom (L) is Element of bool the carrier of (L)

bool the carrier of (L) is set

rng (L) is Element of bool the carrier of ((L),(L))

bool the carrier of ((L),(L)) is set

g is set

c

f9 is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

(L,f9) is Relation-like the carrier of L -defined the carrier of L -valued Function-like non empty V24( the carrier of L) quasi_total idempotent monotone projection closure Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is set

bool [: the carrier of L, the carrier of L:] is set

(L) . (L,f9) is set

Image (L,f9) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

rng (L,f9) is Element of bool the carrier of L

bool the carrier of L is set

subrelstr (rng (L,f9)) is strict reflexive transitive antisymmetric full SubRelStr of L

dom ((L) ") is set

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

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

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of MonMaps (L,L)

MonMaps (L,L) is non empty strict reflexive transitive antisymmetric full SubRelStr of L |^ the carrier of L

the carrier of L is non empty set

L |^ the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (L) is non empty set

(L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V262() up-complete /\-complete RelStr

(L) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L)

((L),(L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of (L) ~

(L) ~ is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of (L) is non empty set

the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

[: the carrier of (L), the carrier of (L):] is set

bool [: the carrier of (L), the carrier of (L):] is set

the InternalRel of (L) ~ is Relation-like the carrier of (L) -defined the carrier of (L) -valued Element of bool [: the carrier of (L), the carrier of (L):]

RelStr(# the carrier of (L),( the InternalRel of (L) ~) #) is strict RelStr

the carrier of ((L),(L)) is non empty set

[: the carrier of (L), the carrier of ((L),(L)):] is set

bool [: the carrier of (L), the carrier of ((L),(L)):] is set

(L) " is Relation-like Function-like one-to-one set

f is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L

((L) ") . f is