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
F2() is set
F1() is non empty RelStr
the carrier of F1() is non empty set
L is set
f is set
bool the carrier of F1() is set
f is non empty Element of bool the carrier of F1()
subrelstr f is non empty strict full SubRelStr of F1()
the carrier of (subrelstr f) is non empty set
c4 is Element of the carrier of F1()
F1() is non empty RelStr
the carrier of F1() is non empty set
F2() is non empty RelStr
the carrier of F2() is non empty set
the InternalRel of F1() is Relation-like the carrier of F1() -defined the carrier of F1() -valued Element of bool [: the carrier of F1(), the carrier of F1():]
[: the carrier of F1(), the carrier of F1():] is set
bool [: the carrier of F1(), the carrier of F1():] is set
RelStr(# the carrier of F1(), the InternalRel of F1() #) is strict RelStr
the InternalRel of F2() is Relation-like the carrier of F2() -defined the carrier of F2() -valued Element of bool [: the carrier of F2(), the carrier of F2():]
[: the carrier of F2(), the carrier of F2():] is set
bool [: the carrier of F2(), the carrier of F2():] is set
RelStr(# the carrier of F2(), the InternalRel of F2() #) is strict RelStr
g is set
c4 is Element of the carrier of F1()
g is set
c4 is Element of the carrier of F2()
g is set
c4 is set
[g,c4] is set
{g,c4} is set
{g} is set
{{g,c4},{g}} is set
f9 is Element of the carrier of F1()
h is Element of the carrier of F1()
x is Element of the carrier of F2()
y is Element of the carrier of F2()
f9 is Element of the carrier of F2()
h is Element of the carrier of F2()
x is Element of the carrier of F1()
y is Element of the carrier of F1()
F1() is non empty RelStr
F2() is non empty full SubRelStr of F1()
the carrier of F2() is non empty set
F3() is non empty full SubRelStr of F1()
the carrier of F3() is non empty set
the InternalRel of F2() is Relation-like the carrier of F2() -defined the carrier of F2() -valued Element of bool [: the carrier of F2(), the carrier of F2():]
[: the carrier of F2(), the carrier of F2():] is set
bool [: the carrier of F2(), the carrier of F2():] is set
RelStr(# the carrier of F2(), the InternalRel of F2() #) is strict RelStr
the InternalRel of F3() is Relation-like the carrier of F3() -defined the carrier of F3() -valued Element of bool [: the carrier of F3(), the carrier of F3():]
[: the carrier of F3(), the carrier of F3():] is set
bool [: the carrier of F3(), the carrier of F3():] is set
RelStr(# the carrier of F3(), the InternalRel of F3() #) is strict RelStr
L is set
f is set
the InternalRel of F1() is Relation-like the carrier of F1() -defined the carrier of F1() -valued Element of bool [: the carrier of F1(), the carrier of F1():]
the carrier of F1() is non empty set
[: the carrier of F1(), the carrier of F1():] is set
bool [: the carrier of F1(), the carrier of F1():] is set
L is Element of the carrier of F2()
f is Element of the carrier of F2()
g is Element of the carrier of F1()
c4 is Element of the carrier of F1()
[g,c4] is set
{g,c4} is set
{g} is set
{{g,c4},{g}} is set
[L,f] is set
{L,f} is set
{L} is set
{{L,f},{L}} is set
L is Element of the carrier of F3()
f is Element of the carrier of F3()
g is Element of the carrier of F1()
c4 is Element of the carrier of F1()
[g,c4] is set
{g,c4} is set
{g} is set
{{g,c4},{g}} is set
[L,f] is set
{L,f} is set
{L} is set
{{L,f},{L}} is set
L is set
f is set
F1() is non empty RelStr
the carrier of F1() is non empty set
F2() is non empty full SubRelStr of F1()
the carrier of F2() is non empty set
F3() is non empty full SubRelStr of F1()
the carrier of F3() is non empty set
the InternalRel of F2() is Relation-like the carrier of F2() -defined the carrier of F2() -valued Element of bool [: the carrier of F2(), the carrier of F2():]
[: the carrier of F2(), the carrier of F2():] is set
bool [: the carrier of F2(), the carrier of F2():] is set
RelStr(# the carrier of F2(), the InternalRel of F2() #) is strict RelStr
the InternalRel of F3() is Relation-like the carrier of F3() -defined the carrier of F3() -valued Element of bool [: the carrier of F3(), the carrier of F3():]
[: the carrier of F3(), the carrier of F3():] is set
bool [: the carrier of F3(), the carrier of F3():] is set
RelStr(# the carrier of F3(), the InternalRel of F3() #) is strict RelStr
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:]
c4 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:]
f9 is Element of the carrier of L
h is Element of the carrier of L
c4 . f9 is set
c4 . h is set
[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:]
c4 is Element of the carrier of L
f9 is Element of the carrier of L
(corestr g) . c4 is Element of the carrier of (Image g)
(corestr g) . f9 is Element of the carrier of (Image g)
g . f9 is Element of the carrier of f
g . c4 is Element of the carrier of f
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:]
c4 is Element of the carrier of (subrelstr f)
f9 is Element of the carrier of (subrelstr f)
g . c4 is set
g . f9 is set
[c4,f9] is set
{c4,f9} is set
{c4} is set
{{c4,f9},{c4}} is set
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
c4 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:]
c4 | g is Relation-like the carrier of g -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of g, the carrier of f:]
[: the carrier of g, the carrier of f:] is set
bool [: the carrier of g, the carrier of f:] is set
c4 | the carrier of 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:]
f9 is set
(c4 | g) . f9 is set
c4 . f9 is set
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:]
c4 is SubRelStr of L
g | c4 is Relation-like the carrier of c4 -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of c4, the carrier of f:]
the carrier of c4 is set
[: the carrier of c4, the carrier of f:] is set
bool [: the carrier of c4, the carrier of f:] is set
g | the carrier of c4 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:]
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
c4 is SubRelStr of L
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 | c4 is Relation-like the carrier of c4 -defined the carrier of f -valued Function-like V24( the carrier of c4) quasi_total Element of bool [: the carrier of c4, the carrier of f:]
the carrier of c4 is set
[: the carrier of c4, the carrier of f:] is set
bool [: the carrier of c4, the carrier of f:] is set
f9 is Element of the carrier of c4
h is Element of the carrier of c4
(g | c4) . f9 is set
(g | c4) . h is set
[f9,h] is set
{f9,h} is set
{f9} is set
{{f9,h},{f9}} is set
the InternalRel of c4 is Relation-like the carrier of c4 -defined the carrier of c4 -valued Element of bool [: the carrier of c4, the carrier of c4:]
[: the carrier of c4, the carrier of c4:] is set
bool [: the carrier of c4, the carrier of c4:] is set
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
c4 is Relation-like the carrier of L -defined the carrier of f -valued Function-like non empty V24( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of f:]
c4 " is Relation-like Function-like set
c4 | g is Relation-like the carrier of g -defined the carrier of f -valued Function-like non empty V24( the carrier of g) quasi_total Element of bool [: the carrier of g, the carrier of f:]
[: the carrier of g, the carrier of f:] is set
bool [: the carrier of g, the carrier of f:] is set
Image (c4 | g) is non empty strict full SubRelStr of f
rng (c4 | g) is Element of bool the carrier of f
bool the carrier of f is set
subrelstr (rng (c4 | g)) is strict full SubRelStr of f
the carrier of (Image (c4 | g)) is non empty set
[: the carrier of (Image (c4 | g)), the carrier of g:] is set
bool [: the carrier of (Image (c4 | g)), the carrier of g:] is set
(c4 | g) " is Relation-like Function-like set
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 (c4 | g)) is Relation-like the carrier of (Image (c4 | g)) -defined the carrier of L -valued Function-like non empty V24( the carrier of (Image (c4 | g))) quasi_total Element of bool [: the carrier of (Image (c4 | g)), the carrier of L:]
[: the carrier of (Image (c4 | g)), the carrier of L:] is set
bool [: the carrier of (Image (c4 | g)), the carrier of L:] is set
dom c4 is Element of bool the carrier of L
bool the carrier of L is set
dom (f9 | (Image (c4 | g))) is Element of bool the carrier of (Image (c4 | g))
bool the carrier of (Image (c4 | g)) is set
rng (f9 | (Image (c4 | g))) is Element of bool the carrier of L
x is set
y is set
(f9 | (Image (c4 | g))) . y is set
a is Element of the carrier of (Image (c4 | g))
b is Element of the carrier of g
(c4 | g) . b is Element of the carrier of f
c4 . b is set
f9 . a is set
dom (c4 | g) is Element of bool the carrier of g
bool the carrier of g is set
x is set
y is set
(c4 | g) . y is set
((c4 | g) ") . x is set
c4 . y is set
f9 . x is set
(f9 | (Image (c4 | g))) . x is set
dom ((c4 | g) ") is set
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
c4 is Element of the carrier of (MonMaps (L,f))
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:]
c4 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:]
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
c4 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:]
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
c4 is set
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:]
c4 is set
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:]
c4 is Relation-like L -defined the carrier of f -valued Function-like V24(L) quasi_total Element of bool [:L, the carrier of f:]
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
c4 . y is set
(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
c4 . B is set
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:]
c4 is Element of the carrier of (L)
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
c4 is set
f9 is set
[c4,f9] is set
{c4,f9} is set
{c4} is set
{{c4,f9},{c4}} is set
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
c4 is set
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
c4 is Element of the carrier of L
g . c4 is Element of the carrier of L
f . (g . c4) is Element of the carrier of L
f9 is Element of the carrier of L
f . f9 is Element of the carrier of L
f . c4 is Element of the carrier of L
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(# b1,b2 #) where b1 is Element of bool the carrier of L, b2 is Relation-like b1 -defined b1 -valued Element of bool [:b1,b1:] : b2 c= the InternalRel of L } is set
{} 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
c4 is non empty strict RelStr
the carrier of c4 is non empty set
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 c4
h is Element of the carrier of c4
y is Element of the carrier of c4
a is RelStr
x is Element of the carrier of c4
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
c4 is Element of the carrier of (L)
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)
c4 is strict SubRelStr of L
the carrier of (L) is non empty set
g is Element of the carrier of (L)
c4 is Element of the carrier of (L)
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)
c4 is Element of the carrier of (L)
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
c4 is set
[: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
c4 is strict SubRelStr of L
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
c4 is set
the carrier of (L) is non empty set
c4 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
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
c4 is Element of the carrier of (L)
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
c4 is Element of the carrier of (L)
c4 ~ is Element of the carrier of ((L) ~)
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
c4 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 c4 is non empty strict reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng c4 is Element of bool the carrier of L
subrelstr (rng c4) is strict reflexive transitive antisymmetric full SubRelStr 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),(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)):]
c4 is Element of the carrier of (L)
f . c4 is Element of the carrier 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:]
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 . c4 is Element of the carrier of ((L),(L))
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:]
c4 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:]
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
c4 . f9 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 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
c4 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:]
c4 . f9 is Element of the carrier of L
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
c4 is Element of the carrier of (Image (L,f))
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
c4 is set
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
c4 is Element of the carrier of L
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
c4 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 c4 is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng c4 is Element of bool the carrier of L
bool the carrier of L is set
subrelstr (rng c4) is strict reflexive transitive antisymmetric full SubRelStr of 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:]
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
c4 is Element of the carrier of ((L),(L))
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 set
(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, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
(L) . (L,f) 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
L is non empty 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 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
(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
(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)):]
the carrier of (L) is non empty set
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),(L)), the carrier of (L):] is set
bool [: the carrier of ((L),(L)), the carrier of (L):] is set
(L) " is Relation-like Function-like one-to-one set
h is Element of the carrier of (L)
x is Element of the carrier of (L)
(L) . h is Element of the carrier of ((L),(L))
(L) . x 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
a 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 a is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng a is Element of bool the carrier of L
bool the carrier of L is set
subrelstr (rng a) is strict reflexive transitive antisymmetric full SubRelStr of L
y 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 y is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng y is Element of bool the carrier of L
subrelstr (rng y) is strict reflexive transitive antisymmetric full SubRelStr of L
~ ((L) . x) is Element of the carrier of (L)
~ ((L) . h) is Element of the carrier of (L)
f9 is Relation-like the carrier of ((L),(L)) -defined the carrier of (L) -valued Function-like non empty V24( the carrier of ((L),(L))) quasi_total Element of bool [: the carrier of ((L),(L)), the carrier of (L):]
h is Element of the carrier of ((L),(L))
x is Element of the carrier of ((L),(L))
f9 . h is Element of the carrier of (L)
f9 . x is Element of the carrier of (L)
~ h is Element of the carrier of (L)
~ x is Element of the carrier of (L)
a is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
(L,a) 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
Image (L,a) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng (L,a) is Element of bool the carrier of L
bool the carrier of L is set
subrelstr (rng (L,a)) is strict reflexive transitive antisymmetric full SubRelStr of L
y is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
f9 . y is set
(L,y) 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:]
f9 . a is set
Image (L,y) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng (L,y) is Element of bool the carrier of L
subrelstr (rng (L,y)) is strict reflexive transitive antisymmetric full SubRelStr 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 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
(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
(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 monotone isomorphic Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
the carrier of (L) is non empty set
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 RelStr
the carrier of L is set
bool the carrier of L is set
f is full SubRelStr of L
the carrier of f is set
bool the carrier of f is set
g is Element of bool the carrier of f
c4 is Element of the carrier of f
f9 is Element of the carrier of f
h is Element of the carrier 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 f
c4 is Element of the carrier of f
f9 is Element of the carrier of f
h is Element of the carrier 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 f
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
{ b1 where b1 is Element of the carrier of L : (L,f) . b1 <= b1 } is set
the Element of the carrier of L is Element of the carrier of L
h is set
x is Element of the carrier of L
(L,f) . x is Element of the carrier of L
(L,f) . the Element of the carrier of L is Element of the carrier of L
(L,f) . ((L,f) . the Element of the carrier of L) is Element of the carrier of L
bool the carrier of f is set
h is directed Element of bool the carrier of f
"\/" (h,L) is Element of the carrier of L
the carrier of (Image (L,f)) is non empty set
bool the carrier of (Image (L,f)) is set
x is Element of bool the carrier of (Image (L,f))
bool the carrier of f is set
c4 is Element of bool the carrier of L
(L,f) .: c4 is Element of bool the carrier of L
"\/" (((L,f) .: c4),L) is Element of the carrier of L
"\/" (c4,L) is Element of the carrier of L
(L,f) . ("\/" (c4,L)) is Element of the carrier of L
h is Element of the carrier of L
x is set
(L,f) . x is set
y is Element of the carrier of L
h is Element of the carrier of L
(L,f) . h is Element of the carrier of L
the Element of c4 is Element of c4
(L,f) . the Element of c4 is set
f9 is Element of bool the carrier of f
(L,f) . ("\/" (((L,f) .: c4),L)) is Element of the carrier of L
x is Element of the carrier of L
(L,f) . x 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
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:]
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 directed-sups-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
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 directed-sups-preserving 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:]
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, 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 directed-sups-preserving 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 directed-sups-preserving projection closure Element of bool [: the carrier of L, the carrier of L:]
the carrier of (L) is non empty set
g is non empty strict reflexive full SubRelStr of (L)
the carrier of g is non empty set
c4 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 is non empty strict reflexive full SubRelStr of (L)
the carrier of f is non empty set
g is non empty strict reflexive full SubRelStr of (L)
the carrier of g is non empty set
c4 is set
the carrier of (L) is non empty set
c4 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
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 reflexive RelStr
(L) is non empty strict reflexive full SubRelStr of (L)
(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 (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
[#] 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
c4 is strict full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
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
c4 is set
the carrier of (L) is non empty set
c4 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
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 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 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) 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
(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
(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 monotone isomorphic Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
the carrier of (L) is non empty set
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) | (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 monotone Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
the carrier of (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
Image ((L) | (L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of ((L),(L))
rng ((L) | (L)) is Element of bool the carrier of ((L),(L))
bool the carrier of ((L),(L)) is set
subrelstr (rng ((L) | (L))) is strict reflexive transitive antisymmetric full SubRelStr of ((L),(L))
(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
f is set
the carrier of (Image ((L) | (L))) is non empty set
g is Element of the carrier of (L)
((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
c4 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 directed-sups-preserving projection closure Element of bool [: the carrier of L, the carrier of L:]
(L) . c4 is set
Image c4 is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of L
rng c4 is Element of bool the carrier of L
bool the carrier of L is set
subrelstr (rng c4) is strict reflexive transitive antisymmetric full SubRelStr of L
g is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr 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 directed-sups-preserving projection closure Element of bool [: the carrier of L, the carrier of L:]
Image (L,g) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of L
rng (L,g) is Element of bool the carrier of L
subrelstr (rng (L,g)) is strict reflexive transitive antisymmetric full SubRelStr of L
(L) . (L,g) is set
c4 is Element of the carrier of (L)
((L) | (L)) . c4 is Element of the carrier of ((L),(L))
the carrier of ((L),(L)) is non empty set
f is set
g is set
the InternalRel of (Image ((L) | (L))) is Relation-like the carrier of (Image ((L) | (L))) -defined the carrier of (Image ((L) | (L))) -valued Element of bool [: the carrier of (Image ((L) | (L))), the carrier of (Image ((L) | (L))):]
[: the carrier of (Image ((L) | (L))), the carrier of (Image ((L) | (L))):] is set
bool [: the carrier of (Image ((L) | (L))), the carrier of (Image ((L) | (L))):] is set
RelStr(# the carrier of (Image ((L) | (L))), the InternalRel of (Image ((L) | (L))) #) is strict RelStr
the InternalRel of ((L),(L)) is Relation-like the carrier of ((L),(L)) -defined the carrier of ((L),(L)) -valued Element of bool [: the carrier of ((L),(L)), the carrier of ((L),(L)):]
[: the carrier of ((L),(L)), the carrier of ((L),(L)):] is set
bool [: the carrier of ((L),(L)), the carrier of ((L),(L)):] is set
RelStr(# the carrier of ((L),(L)), the InternalRel of ((L),(L)) #) is strict RelStr
L is non empty 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) 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
(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
(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 monotone isomorphic Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
the carrier of (L) is non empty set
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) | (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 monotone Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
the carrier of (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
Image ((L) | (L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of ((L),(L))
rng ((L) | (L)) is Element of bool the carrier of ((L),(L))
bool the carrier of ((L),(L)) is set
subrelstr (rng ((L) | (L))) is strict reflexive transitive antisymmetric full SubRelStr of ((L),(L))
corestr ((L) | (L)) is Relation-like the carrier of (L) -defined the carrier of (Image ((L) | (L))) -valued Function-like non empty V24( the carrier of (L)) quasi_total onto monotone Element of bool [: the carrier of (L), the carrier of (Image ((L) | (L))):]
the carrier of (Image ((L) | (L))) is non empty set
[: the carrier of (L), the carrier of (Image ((L) | (L))):] is set
bool [: the carrier of (L), the carrier of (Image ((L) | (L))):] is set
the carrier of (Image ((L) | (L))) |` ((L) | (L)) is Relation-like the carrier of (L) -defined the carrier of ((L),(L)) -valued Function-like Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
[: the carrier of (Image ((L) | (L))), the carrier of (L):] is set
bool [: the carrier of (Image ((L) | (L))), the carrier of (L):] is set
(corestr ((L) | (L))) " is Relation-like Function-like set
[: the carrier of ((L),(L)), the carrier of (L):] is set
bool [: the carrier of ((L),(L)), the carrier of (L):] is set
(L) " is Relation-like Function-like one-to-one set
f9 is Relation-like the carrier of ((L),(L)) -defined the carrier of (L) -valued Function-like non empty V24( the carrier of ((L),(L))) quasi_total Element of bool [: the carrier of ((L),(L)), the carrier of (L):]
f9 | (Image ((L) | (L))) is Relation-like the carrier of (Image ((L) | (L))) -defined the carrier of (L) -valued Function-like non empty V24( the carrier of (Image ((L) | (L)))) quasi_total Element of bool [: the carrier of (Image ((L) | (L))), the carrier of (L):]
[: the carrier of (Image ((L) | (L))), the carrier of (L):] is set
bool [: the carrier of (Image ((L) | (L))), the carrier of (L):] is set
h is Relation-like the carrier of (Image ((L) | (L))) -defined the carrier of (L) -valued Function-like non empty V24( the carrier of (Image ((L) | (L)))) quasi_total Element of bool [: the carrier of (Image ((L) | (L))), the carrier of (L):]
((L) | (L)) " is Relation-like Function-like set
x is Element of the carrier of (Image ((L) | (L)))
y is Element of the carrier of (Image ((L) | (L)))
h . x is Element of the carrier of (L)
h . y is Element of the carrier of (L)
a is Element of the carrier of ((L),(L))
~ a is Element of the carrier of (L)
b is Element of the carrier of ((L),(L))
~ b is Element of the carrier of (L)
A is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
(L,A) 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
B is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
(L,B) 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:]
f9 . y is set
j is Element of the carrier of (L)
Image (L,B) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng (L,B) is Element of bool the carrier of L
bool the carrier of L is set
subrelstr (rng (L,B)) is strict reflexive transitive antisymmetric full SubRelStr of L
Image (L,A) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
rng (L,A) is Element of bool the carrier of L
subrelstr (rng (L,A)) is strict reflexive transitive antisymmetric full SubRelStr of L
i is Element of the carrier of (L)
f9 . x 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 non empty strict reflexive transitive antisymmetric full SubRelStr of (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
(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
(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
((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
(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 monotone isomorphic Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
the carrier of (L) is non empty set
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) | (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 monotone Element of bool [: the carrier of (L), the carrier of ((L),(L)):]
the carrier of (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),(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
corestr ((L) | (L)) is Relation-like the carrier of (L) -defined the carrier of (L) -defined the carrier of (Image ((L) | (L))) -valued the carrier of (Image ((L) | (L))) -valued Function-like one-to-one non empty V24( the carrier of (L)) V24( the carrier of (L)) quasi_total quasi_total onto onto bijective monotone monotone isomorphic Element of bool [: the carrier of (L), the carrier of (Image ((L) | (L))):]
Image ((L) | (L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of ((L),(L))
rng ((L) | (L)) is Element of bool the carrier of ((L),(L))
bool the carrier of ((L),(L)) is set
subrelstr (rng ((L) | (L))) is strict reflexive transitive antisymmetric full SubRelStr of ((L),(L))
the carrier of (Image ((L) | (L))) is non empty set
[: the carrier of (L), the carrier of (Image ((L) | (L))):] is set
bool [: the carrier of (L), the carrier of (Image ((L) | (L))):] is set
the carrier of (Image ((L) | (L))) |` ((L) | (L)) is Relation-like the carrier of (L) -defined the carrier of ((L),(L)) -valued Function-like 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)):]