K242() is Element of bool K238()
K238() is set
bool K238() is non empty set
K137() is set
bool K137() is non empty set
K180() is TopStruct
the carrier of K180() is set
bool K242() is non empty set
K318() is set
{} is Relation-like non-empty empty-yielding empty finite finite-yielding V30() set
the Relation-like non-empty empty-yielding empty finite finite-yielding V30() set is Relation-like non-empty empty-yielding empty finite finite-yielding V30() set
{{}} is non empty finite V30() set
K283({{}}) is M25({{}})
[:K283({{}}),{{}}:] is Relation-like set
bool [:K283({{}}),{{}}:] is non empty set
K107(K283({{}}),{{}}) is set
1 is non empty set
{{},1} is non empty finite set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
the Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:] is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
x is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[ the Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:],x] is Connection of S,T
{ the Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:],x} is non empty with_non-empty_elements non empty-membered finite set
{ the Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]} is non empty with_non-empty_elements non empty-membered finite set
{{ the Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:],x},{ the Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict RelStr
g is non empty RelStr
the carrier of g is non empty 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 Relation-like non empty set
bool [: the carrier of g, the carrier of g:] is non empty set
RelStr(# the carrier of g, the InternalRel of g #) is non empty strict RelStr
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict RelStr
x is non empty RelStr
the carrier of x is non empty 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 Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
RelStr(# the carrier of x, the InternalRel of x #) is non empty strict RelStr
x is Connection of S,T
x is Connection of g,x
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
x is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
y is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[x,y] is Connection of S,T
{x,y} is non empty with_non-empty_elements non empty-membered finite set
{x} is non empty with_non-empty_elements non empty-membered finite set
{{x,y},{x}} is non empty with_non-empty_elements non empty-membered finite V30() set
[: the carrier of g, the carrier of x:] is Relation-like non empty set
bool [: the carrier of g, the carrier of x:] is non empty set
[: the carrier of x, the carrier of g:] is Relation-like non empty set
bool [: the carrier of x, the carrier of g:] is non empty set
a is Relation-like the carrier of g -defined the carrier of x -valued Function-like non empty V22( the carrier of g) quasi_total Element of bool [: the carrier of g, the carrier of x:]
b is Relation-like the carrier of x -defined the carrier of g -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of g:]
[a,b] is Connection of g,x
{a,b} is non empty with_non-empty_elements non empty-membered finite set
{a} is non empty with_non-empty_elements non empty-membered finite set
{{a,b},{a}} is non empty with_non-empty_elements non empty-membered finite V30() set
a is Element of the carrier of x
b . a is Element of the carrier of g
b2 is Element of the carrier of g
a . b2 is Element of the carrier of x
f is Element of the carrier of T
g is Element of the carrier of S
x . g is Element of the carrier of T
y . f is Element of the carrier of S
S is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
x is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[g,x] is Connection of S,T
{g,x} is non empty with_non-empty_elements non empty-membered finite set
{g} is non empty with_non-empty_elements non empty-membered finite set
{{g,x},{g}} is non empty with_non-empty_elements non empty-membered finite V30() set
x is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[g,x] is Connection of S,T
{g,x} is non empty with_non-empty_elements non empty-membered finite set
{{g,x},{g}} is non empty with_non-empty_elements non empty-membered finite V30() set
x is Element of the carrier of T
x is Element of the carrier of T
x . x is Element of the carrier of S
uparrow x is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{x} is non empty finite Element of bool the carrier of T
uparrow {x} is non empty upper Element of bool the carrier of T
g " (uparrow x) is Element of bool the carrier of S
bool the carrier of S is non empty set
x . x is Element of the carrier of S
x . x is Element of the carrier of S
"/\" ((g " (uparrow x)),S) is Element of the carrier of S
x . x is Element of the carrier of S
T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
S is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
g is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
x is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[x,g] is Connection of S,T
{x,g} is non empty with_non-empty_elements non empty-membered finite set
{x} is non empty with_non-empty_elements non empty-membered finite set
{{x,g},{x}} is non empty with_non-empty_elements non empty-membered finite V30() set
x is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[x,g] is Connection of S,T
{x,g} is non empty with_non-empty_elements non empty-membered finite set
{x} is non empty with_non-empty_elements non empty-membered finite set
{{x,g},{x}} is non empty with_non-empty_elements non empty-membered finite V30() set
x is Element of the carrier of S
x is Element of the carrier of S
x . x is Element of the carrier of T
downarrow x is non empty directed lower Element of bool the carrier of S
bool the carrier of S is non empty set
{x} is non empty finite Element of bool the carrier of S
downarrow {x} is non empty lower Element of bool the carrier of S
g " (downarrow x) is Element of bool the carrier of T
bool the carrier of T is non empty set
x . x is Element of the carrier of T
x . x is Element of the carrier of T
"\/" ((g " (downarrow x)),T) is Element of the carrier of T
x . x is Element of the carrier of T
S is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
x is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
g is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of g is non empty set
x is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of x is non empty set
[: the carrier of g, the carrier of x:] is Relation-like non empty set
bool [: the carrier of g, the carrier of x:] is non empty set
x is Relation-like the carrier of g -defined the carrier of x -valued Function-like non empty V22( the carrier of g) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of g, the carrier of x:]
(g,x,x) is Relation-like the carrier of x -defined the carrier of g -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of g:]
[: the carrier of x, the carrier of g:] is Relation-like non empty set
bool [: the carrier of x, the carrier of g:] is non empty set
[x,(g,x,x)] is Connection of g,x
{x,(g,x,x)} is non empty with_non-empty_elements non empty-membered finite set
{x} is non empty with_non-empty_elements non empty-membered finite set
{{x,(g,x,x)},{x}} is non empty with_non-empty_elements non empty-membered finite V30() set
(S,T,x) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
S is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
x is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
g is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of g is non empty set
x is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of x is non empty set
[: the carrier of g, the carrier of x:] is Relation-like non empty set
bool [: the carrier of g, the carrier of x:] is non empty set
x is Relation-like the carrier of g -defined the carrier of x -valued Function-like non empty V22( the carrier of g) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of g, the carrier of x:]
(x,g,x) is Relation-like the carrier of x -defined the carrier of g -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of g:]
[: the carrier of x, the carrier of g:] is Relation-like non empty set
bool [: the carrier of x, the carrier of g:] is non empty set
[(x,g,x),x] is Connection of x,g
{(x,g,x),x} is non empty with_non-empty_elements non empty-membered finite set
{(x,g,x)} is non empty with_non-empty_elements non empty-membered finite set
{{(x,g,x),x},{(x,g,x)}} is non empty with_non-empty_elements non empty-membered finite V30() set
(T,S,x) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
g is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of T, the carrier of S:]
(S,T,g) is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
x is Element of the carrier of T
(S,T,g) . x is Element of the carrier of S
uparrow x is non empty filtered upper Element of bool the carrier of T
bool the carrier of T is non empty set
{x} is non empty finite Element of bool the carrier of T
uparrow {x} is non empty upper Element of bool the carrier of T
g " (uparrow x) is Element of bool the carrier of S
bool the carrier of S is non empty set
"/\" ((g " (uparrow x)),S) is Element of the carrier of S
[g,(S,T,g)] is Connection of S,T
{g,(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{g} is non empty with_non-empty_elements non empty-membered finite set
{{g,(S,T,g)},{g}} is non empty with_non-empty_elements non empty-membered finite V30() set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
g is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of T, the carrier of S:]
(S,T,g) is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
x is Element of the carrier of S
(S,T,g) . x is Element of the carrier of T
downarrow x is non empty directed lower Element of bool the carrier of S
bool the carrier of S is non empty set
{x} is non empty finite Element of bool the carrier of S
downarrow {x} is non empty lower Element of bool the carrier of S
g " (downarrow x) is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((g " (downarrow x)),T) is Element of the carrier of T
[(S,T,g),g] is Connection of S,T
{(S,T,g),g} is non empty with_non-empty_elements non empty-membered finite set
{(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{{(S,T,g),g},{(S,T,g)}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is RelStr
the carrier of S is set
T is RelStr
the carrier of T is set
[: the carrier of S, the carrier of T:] is Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of T:]
S ~ is strict RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
RelStr(# the carrier of S,( the InternalRel of S ~) #) is strict RelStr
the carrier of (S ~) is set
T ~ is strict RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
the carrier of (T ~) is set
[: the carrier of (S ~), the carrier of (T ~):] is Relation-like set
bool [: the carrier of (S ~), the carrier of (T ~):] is non empty set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
T ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued V22( the carrier of T) quasi_total V31() V34() V38() Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is non empty strict RelStr
S ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued V22( the carrier of S) quasi_total V31() V34() V38() Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
RelStr(# the carrier of S,( the InternalRel of S ~) #) is non empty strict RelStr
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,g) is Relation-like the carrier of (S ~) -defined the carrier of (T ~) -valued Function-like non empty V22( the carrier of (S ~)) quasi_total Element of bool [: the carrier of (S ~), the carrier of (T ~):]
the carrier of (S ~) is non empty set
the carrier of (T ~) is non empty set
[: the carrier of (S ~), the carrier of (T ~):] is Relation-like non empty set
bool [: the carrier of (S ~), the carrier of (T ~):] is non empty set
(S,T,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
[g,(S,T,g)] is Connection of S,T
{g,(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{g} is non empty with_non-empty_elements non empty-membered finite set
{{g,(S,T,g)},{g}} is non empty with_non-empty_elements non empty-membered finite V30() set
(T,S,(S,T,g)) is Relation-like the carrier of (T ~) -defined the carrier of (S ~) -valued Function-like non empty V22( the carrier of (T ~)) quasi_total Element of bool [: the carrier of (T ~), the carrier of (S ~):]
[: the carrier of (T ~), the carrier of (S ~):] is Relation-like non empty set
bool [: the carrier of (T ~), the carrier of (S ~):] is non empty set
[(T,S,(S,T,g)),(S,T,g)] is Connection of T ~ ,S ~
{(T,S,(S,T,g)),(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{(T,S,(S,T,g))} is non empty with_non-empty_elements non empty-membered finite set
{{(T,S,(S,T,g)),(S,T,g)},{(T,S,(S,T,g))}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
S ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued V22( the carrier of S) quasi_total V31() V34() V38() Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
RelStr(# the carrier of S,( the InternalRel of S ~) #) is non empty strict RelStr
T ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued V22( the carrier of T) quasi_total V31() V34() V38() Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is non empty strict RelStr
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,g) is Relation-like the carrier of (S ~) -defined the carrier of (T ~) -valued Function-like non empty V22( the carrier of (S ~)) quasi_total Element of bool [: the carrier of (S ~), the carrier of (T ~):]
the carrier of (S ~) is non empty set
the carrier of (T ~) is non empty set
[: the carrier of (S ~), the carrier of (T ~):] is Relation-like non empty set
bool [: the carrier of (S ~), the carrier of (T ~):] is non empty set
(T,S,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
[(T,S,g),g] is Connection of T,S
{(T,S,g),g} is non empty with_non-empty_elements non empty-membered finite set
{(T,S,g)} is non empty with_non-empty_elements non empty-membered finite set
{{(T,S,g),g},{(T,S,g)}} is non empty with_non-empty_elements non empty-membered finite V30() set
(T,S,(T,S,g)) is Relation-like the carrier of (T ~) -defined the carrier of (S ~) -valued Function-like non empty V22( the carrier of (T ~)) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of (T ~), the carrier of (S ~):]
[: the carrier of (T ~), the carrier of (S ~):] is Relation-like non empty set
bool [: the carrier of (T ~), the carrier of (S ~):] is non empty set
[(S,T,g),(T,S,(T,S,g))] is Connection of S ~ ,T ~
{(S,T,g),(T,S,(T,S,g))} is non empty with_non-empty_elements non empty-membered finite set
{(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{{(S,T,g),(T,S,(T,S,g))},{(S,T,g)}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
T ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued V22( the carrier of T) quasi_total V31() V34() V38() Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is non empty strict RelStr
the carrier of (T ~) is non empty set
S ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued V22( the carrier of S) quasi_total V31() V34() V38() Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
RelStr(# the carrier of S,( the InternalRel of S ~) #) is non empty strict RelStr
the carrier of (S ~) is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
(S,T,g) is Relation-like the carrier of (S ~) -defined the carrier of (T ~) -valued Function-like non empty V22( the carrier of (S ~)) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of (S ~), the carrier of (T ~):]
[: the carrier of (S ~), the carrier of (T ~):] is Relation-like non empty set
bool [: the carrier of (S ~), the carrier of (T ~):] is non empty set
((T ~),(S ~),(S,T,g)) is Relation-like the carrier of (T ~) -defined the carrier of (S ~) -valued Function-like non empty V22( the carrier of (T ~)) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of (T ~), the carrier of (S ~):]
[: the carrier of (T ~), the carrier of (S ~):] is Relation-like non empty set
bool [: the carrier of (T ~), the carrier of (S ~):] is non empty set
[g,(S,T,g)] is Connection of S,T
{g,(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{g} is non empty with_non-empty_elements non empty-membered finite set
{{g,(S,T,g)},{g}} is non empty with_non-empty_elements non empty-membered finite V30() set
(T,S,(S,T,g)) is Relation-like the carrier of (T ~) -defined the carrier of (S ~) -valued Function-like non empty V22( the carrier of (T ~)) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of (T ~), the carrier of (S ~):]
[(T,S,(S,T,g)),(S,T,g)] is Connection of T ~ ,S ~
{(T,S,(S,T,g)),(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{(T,S,(S,T,g))} is non empty with_non-empty_elements non empty-membered finite set
{{(T,S,(S,T,g)),(S,T,g)},{(T,S,(S,T,g))}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
T ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued V22( the carrier of T) quasi_total V31() V34() V38() Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is Relation-like non empty set
bool [: the carrier of T, the carrier of T:] is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
RelStr(# the carrier of T,( the InternalRel of T ~) #) is non empty strict RelStr
the carrier of (T ~) is non empty set
S ~ is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued V22( the carrier of S) quasi_total V31() V34() V38() Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
RelStr(# the carrier of S,( the InternalRel of S ~) #) is non empty strict RelStr
the carrier of (S ~) is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,g) is Relation-like the carrier of (S ~) -defined the carrier of (T ~) -valued Function-like non empty V22( the carrier of (S ~)) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of (S ~), the carrier of (T ~):]
[: the carrier of (S ~), the carrier of (T ~):] is Relation-like non empty set
bool [: the carrier of (S ~), the carrier of (T ~):] is non empty set
((S ~),(T ~),(S,T,g)) is Relation-like the carrier of (T ~) -defined the carrier of (S ~) -valued Function-like non empty V22( the carrier of (T ~)) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of (T ~), the carrier of (S ~):]
[: the carrier of (T ~), the carrier of (S ~):] is Relation-like non empty set
bool [: the carrier of (T ~), the carrier of (S ~):] is non empty set
(T,S,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
[(T,S,g),g] is Connection of T,S
{(T,S,g),g} is non empty with_non-empty_elements non empty-membered finite set
{(T,S,g)} is non empty with_non-empty_elements non empty-membered finite set
{{(T,S,g),g},{(T,S,g)}} is non empty with_non-empty_elements non empty-membered finite V30() set
(T,S,(T,S,g)) is Relation-like the carrier of (T ~) -defined the carrier of (S ~) -valued Function-like non empty V22( the carrier of (T ~)) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of (T ~), the carrier of (S ~):]
[(S,T,g),(T,S,(T,S,g))] is Connection of S ~ ,T ~
{(S,T,g),(T,S,(T,S,g))} is non empty with_non-empty_elements non empty-membered finite set
{(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{{(S,T,g),(T,S,(T,S,g))},{(S,T,g)}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty RelStr
id S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V22( the carrier of S) quasi_total isomorphic monotone projection Element of bool [: the carrier of S, the carrier of S:]
the carrier of S is non empty set
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
[(id S),(id S)] is Connection of S,S
{(id S),(id S)} is non empty with_non-empty_elements non empty-membered finite set
{(id S)} is non empty with_non-empty_elements non empty-membered finite set
{{(id S),(id S)},{(id S)}} is non empty with_non-empty_elements non empty-membered finite V30() set
T is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V22( the carrier of S) quasi_total isomorphic monotone projection Element of bool [: the carrier of S, the carrier of S:]
g is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V22( the carrier of S) quasi_total isomorphic monotone projection Element of bool [: the carrier of S, the carrier of S:]
[T,g] is Connection of S,S
{T,g} is non empty with_non-empty_elements non empty-membered finite set
{T} is non empty with_non-empty_elements non empty-membered finite set
{{T,g},{T}} is non empty with_non-empty_elements non empty-membered finite V30() set
x is Element of the carrier of S
x is Element of the carrier of S
T . x is Element of the carrier of S
g . x is Element of the carrier of S
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
id S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V22( the carrier of S) quasi_total infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic monotone projection closure kernel Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
(S,S,(id S)) is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of S, the carrier of S:]
(S,S,(id S)) is Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of S, the carrier of S:]
[(id S),(id S)] is Connection of S,S
{(id S),(id S)} is non empty with_non-empty_elements non empty-membered finite set
{(id S)} is non empty with_non-empty_elements non empty-membered finite set
{{(id S),(id S)},{(id S)}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
g is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of g is non empty set
[: the carrier of T, the carrier of g:] is Relation-like non empty set
bool [: the carrier of T, the carrier of g:] is non empty set
x is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,x) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
x is Relation-like the carrier of T -defined the carrier of g -valued Function-like non empty V22( the carrier of T) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of T, the carrier of g:]
x * x is Relation-like the carrier of S -defined the carrier of g -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of g:]
[: the carrier of S, the carrier of g:] is Relation-like non empty set
bool [: the carrier of S, the carrier of g:] is non empty set
(S,g,(x * x)) is Relation-like the carrier of g -defined the carrier of S -valued Function-like non empty V22( the carrier of g) quasi_total Element of bool [: the carrier of g, the carrier of S:]
[: the carrier of g, the carrier of S:] is Relation-like non empty set
bool [: the carrier of g, the carrier of S:] is non empty set
(T,g,x) is Relation-like the carrier of g -defined the carrier of T -valued Function-like non empty V22( the carrier of g) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of g, the carrier of T:]
[: the carrier of g, the carrier of T:] is Relation-like non empty set
bool [: the carrier of g, the carrier of T:] is non empty set
(S,T,x) * (T,g,x) is Relation-like the carrier of g -defined the carrier of S -valued Function-like non empty V22( the carrier of g) quasi_total Element of bool [: the carrier of g, the carrier of S:]
[x,(S,T,x)] is Connection of S,T
{x,(S,T,x)} is non empty with_non-empty_elements non empty-membered finite set
{x} is non empty with_non-empty_elements non empty-membered finite set
{{x,(S,T,x)},{x}} is non empty with_non-empty_elements non empty-membered finite V30() set
[x,(T,g,x)] is Connection of T,g
{x,(T,g,x)} is non empty with_non-empty_elements non empty-membered finite set
{x} is non empty with_non-empty_elements non empty-membered finite set
{{x,(T,g,x)},{x}} is non empty with_non-empty_elements non empty-membered finite V30() set
[(x * x),((S,T,x) * (T,g,x))] is Connection of S,g
{(x * x),((S,T,x) * (T,g,x))} is non empty with_non-empty_elements non empty-membered finite set
{(x * x)} is non empty with_non-empty_elements non empty-membered finite set
{{(x * x),((S,T,x) * (T,g,x))},{(x * x)}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
g is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of g is non empty set
[: the carrier of T, the carrier of g:] is Relation-like non empty set
bool [: the carrier of T, the carrier of g:] is non empty set
x is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(T,S,x) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
x is Relation-like the carrier of T -defined the carrier of g -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of T, the carrier of g:]
x * x is Relation-like the carrier of S -defined the carrier of g -valued Function-like non empty V22( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of g:]
[: the carrier of S, the carrier of g:] is Relation-like non empty set
bool [: the carrier of S, the carrier of g:] is non empty set
(g,S,(x * x)) is Relation-like the carrier of g -defined the carrier of S -valued Function-like non empty V22( the carrier of g) quasi_total Element of bool [: the carrier of g, the carrier of S:]
[: the carrier of g, the carrier of S:] is Relation-like non empty set
bool [: the carrier of g, the carrier of S:] is non empty set
(g,T,x) is Relation-like the carrier of g -defined the carrier of T -valued Function-like non empty V22( the carrier of g) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of g, the carrier of T:]
[: the carrier of g, the carrier of T:] is Relation-like non empty set
bool [: the carrier of g, the carrier of T:] is non empty set
(T,S,x) * (g,T,x) is Relation-like the carrier of g -defined the carrier of S -valued Function-like non empty V22( the carrier of g) quasi_total Element of bool [: the carrier of g, the carrier of S:]
[(T,S,x),x] is Connection of T,S
{(T,S,x),x} is non empty with_non-empty_elements non empty-membered finite set
{(T,S,x)} is non empty with_non-empty_elements non empty-membered finite set
{{(T,S,x),x},{(T,S,x)}} is non empty with_non-empty_elements non empty-membered finite V30() set
[(g,T,x),x] is Connection of g,T
{(g,T,x),x} is non empty with_non-empty_elements non empty-membered finite set
{(g,T,x)} is non empty with_non-empty_elements non empty-membered finite set
{{(g,T,x),x},{(g,T,x)}} is non empty with_non-empty_elements non empty-membered finite V30() set
[((T,S,x) * (g,T,x)),(x * x)] is Connection of g,S
{((T,S,x) * (g,T,x)),(x * x)} is non empty with_non-empty_elements non empty-membered finite set
{((T,S,x) * (g,T,x))} is non empty with_non-empty_elements non empty-membered finite set
{{((T,S,x) * (g,T,x)),(x * x)},{((T,S,x) * (g,T,x))}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(S,T,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
(S,T,(S,T,g)) is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of S, the carrier of T:]
[g,(S,T,g)] is Connection of S,T
{g,(S,T,g)} is non empty with_non-empty_elements non empty-membered finite set
{g} is non empty with_non-empty_elements non empty-membered finite set
{{g,(S,T,g)},{g}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of S is non empty set
T is non empty V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like non empty set
bool [: the carrier of S, the carrier of T:] is non empty set
g is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving join-preserving directed-sups-preserving monotone Element of bool [: the carrier of S, the carrier of T:]
(T,S,g) is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V22( the carrier of T) quasi_total infs-preserving meet-preserving filtered-infs-preserving monotone upper_adjoint Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is Relation-like non empty set
bool [: the carrier of T, the carrier of S:] is non empty set
(T,S,(T,S,g)) is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving join-preserving directed-sups-preserving monotone lower_adjoint Element of bool [: the carrier of S, the carrier of T:]
[(T,S,g),g] is Connection of T,S
{(T,S,g),g} is non empty with_non-empty_elements non empty-membered finite set
{(T,S,g)} is non empty with_non-empty_elements non empty-membered finite set
{{(T,S,g),g},{(T,S,g)}} is non empty with_non-empty_elements non empty-membered finite V30() set
S is non empty AltCatStr
the Arrows of S is Relation-like [: the carrier of S, the carrier of S:] -defined Function-like V22([: the carrier of S, the carrier of S:]) set
the carrier of S is non empty set
[: the carrier of S, the carrier of S:] is Relation-like non empty set
x is set
T is set
g is set
the Arrows of S . (T,g) is set
[T,g] is set
{T,g} is non empty finite set
{T} is non empty finite set
{{T,g},{T}} is non empty with_non-empty_elements non empty-membered finite V30() set
the Arrows of S . [T,g] is set
dom the Arrows of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
bool [: the carrier of S, the carrier of S:] is non empty set
x is Element of the carrier of S
x is Element of the carrier of S
<^x,x^> is set
S is non empty set
T is Element of S
g is non empty set
[:g,g:] is Relation-like non empty set
bool [:g,g:] is non empty set
the Relation-like g -defined g -valued well_founded well-ordering V22(g) quasi_total V31() V34() V36() V38() upper-bounded Element of bool [:g,g:] is Relation-like g -defined g -valued well_founded well-ordering V22(g) quasi_total V31() V34() V36() V38() upper-bounded Element of bool [:g,g:]
RelStr(# g, the Relation-like g -defined g -valued well_founded well-ordering V22(g) quasi_total V31() V34() V36() V38() upper-bounded Element of bool [:g,g:] #) is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() satisfying_axiom_K algebraic connected up-complete /\-complete satisfying_axiom_of_approximation continuous with_suprema with_infima complete RelStr
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of x is non empty set
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
y is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
a is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
a * y is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
id x is Relation-like the carrier of x -defined the carrier of x -valued Function-like one-to-one non empty V22( the carrier of x) quasi_total infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic monotone projection closure kernel Element of bool [: the carrier of x, the carrier of x:]
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
id the carrier of x is Relation-like the carrier of x -defined the carrier of x -valued non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
g is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the carrier of g is non empty set
x is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the carrier of x is non empty set
x is Element of the carrier of g
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
x is Element of the carrier of g
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
[: the carrier of (latt x), the carrier of (latt x):] is Relation-like non empty set
bool [: the carrier of (latt x), the carrier of (latt x):] is non empty set
x is Relation-like the carrier of (latt x) -defined the carrier of (latt x) -valued Function-like non empty V22( the carrier of (latt x)) quasi_total monotone Element of bool [: the carrier of (latt x), the carrier of (latt x):]
<^x,x^> is set
y is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of y is non empty set
a is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of a is non empty set
[: the carrier of y, the carrier of a:] is Relation-like non empty set
bool [: the carrier of y, the carrier of a:] is non empty set
b is Relation-like the carrier of y -defined the carrier of a -valued Function-like non empty V22( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of a:]
x is Element of the carrier of x
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
x is Element of the carrier of x
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
[: the carrier of (latt x), the carrier of (latt x):] is Relation-like non empty set
bool [: the carrier of (latt x), the carrier of (latt x):] is non empty set
x is Relation-like the carrier of (latt x) -defined the carrier of (latt x) -valued Function-like non empty V22( the carrier of (latt x)) quasi_total monotone Element of bool [: the carrier of (latt x), the carrier of (latt x):]
<^x,x^> is set
y is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of y is non empty set
a is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of a is non empty set
[: the carrier of y, the carrier of a:] is Relation-like non empty set
bool [: the carrier of y, the carrier of a:] is non empty set
b is Relation-like the carrier of y -defined the carrier of a -valued Function-like non empty V22( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of a:]
S is non empty non empty-membered set
(S) is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the Arrows of (S) is Relation-like [: the carrier of (S), the carrier of (S):] -defined Function-like V22([: the carrier of (S), the carrier of (S):]) set
the carrier of (S) is non empty set
[: the carrier of (S), the carrier of (S):] is Relation-like non empty set
T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
g is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of g is non empty set
[: the carrier of T, the carrier of g:] is Relation-like non empty set
bool [: the carrier of T, the carrier of g:] is non empty set
the Arrows of (S) . (T,g) is set
[T,g] is set
{T,g} is non empty finite set
{T} is non empty finite set
{{T,g},{T}} is non empty with_non-empty_elements non empty-membered finite V30() set
the Arrows of (S) . [T,g] is set
x is Relation-like the carrier of T -defined the carrier of g -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of g:]
x is Element of the carrier of (S)
x is Element of the carrier of (S)
<^x,x^> is set
a is non empty set
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
y is Relation-like Function-like Element of <^x,x^>
@ y is Relation-like the carrier of (latt x) -defined the carrier of (latt x) -valued Function-like non empty V22( the carrier of (latt x)) quasi_total monotone Element of bool [: the carrier of (latt x), the carrier of (latt x):]
[: the carrier of (latt x), the carrier of (latt x):] is Relation-like non empty set
bool [: the carrier of (latt x), the carrier of (latt x):] is non empty set
a is non empty set
x is Element of the carrier of (S)
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
x is Element of the carrier of (S)
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
<^x,x^> is set
y is non empty set
S is non empty set
T is Element of S
g is non empty set
[:g,g:] is Relation-like non empty set
bool [:g,g:] is non empty set
the Relation-like g -defined g -valued well_founded well-ordering V22(g) quasi_total V31() V34() V36() V38() upper-bounded Element of bool [:g,g:] is Relation-like g -defined g -valued well_founded well-ordering V22(g) quasi_total V31() V34() V36() V38() upper-bounded Element of bool [:g,g:]
RelStr(# g, the Relation-like g -defined g -valued well_founded well-ordering V22(g) quasi_total V31() V34() V36() V38() upper-bounded Element of bool [:g,g:] #) is non empty strict V87() reflexive transitive antisymmetric lower-bounded upper-bounded V94() satisfying_axiom_K algebraic connected up-complete /\-complete satisfying_axiom_of_approximation continuous with_suprema with_infima complete RelStr
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of x is non empty set
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
y is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
a is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
a * y is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
id x is Relation-like the carrier of x -defined the carrier of x -valued Function-like one-to-one non empty V22( the carrier of x) quasi_total infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic monotone projection closure kernel Element of bool [: the carrier of x, the carrier of x:]
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
id the carrier of x is Relation-like the carrier of x -defined the carrier of x -valued non empty V22( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
g is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the carrier of g is non empty set
x is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the carrier of x is non empty set
x is Element of the carrier of g
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
x is Element of the carrier of g
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
[: the carrier of (latt x), the carrier of (latt x):] is Relation-like non empty set
bool [: the carrier of (latt x), the carrier of (latt x):] is non empty set
x is Relation-like the carrier of (latt x) -defined the carrier of (latt x) -valued Function-like non empty V22( the carrier of (latt x)) quasi_total monotone Element of bool [: the carrier of (latt x), the carrier of (latt x):]
<^x,x^> is set
y is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of y is non empty set
a is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of a is non empty set
[: the carrier of y, the carrier of a:] is Relation-like non empty set
bool [: the carrier of y, the carrier of a:] is non empty set
b is Relation-like the carrier of y -defined the carrier of a -valued Function-like non empty V22( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of a:]
x is Element of the carrier of x
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
x is Element of the carrier of x
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
[: the carrier of (latt x), the carrier of (latt x):] is Relation-like non empty set
bool [: the carrier of (latt x), the carrier of (latt x):] is non empty set
x is Relation-like the carrier of (latt x) -defined the carrier of (latt x) -valued Function-like non empty V22( the carrier of (latt x)) quasi_total monotone Element of bool [: the carrier of (latt x), the carrier of (latt x):]
<^x,x^> is set
y is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of y is non empty set
a is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of a is non empty set
[: the carrier of y, the carrier of a:] is Relation-like non empty set
bool [: the carrier of y, the carrier of a:] is non empty set
b is Relation-like the carrier of y -defined the carrier of a -valued Function-like non empty V22( the carrier of y) quasi_total Element of bool [: the carrier of y, the carrier of a:]
S is non empty non empty-membered set
(S) is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the Arrows of (S) is Relation-like [: the carrier of (S), the carrier of (S):] -defined Function-like V22([: the carrier of (S), the carrier of (S):]) set
the carrier of (S) is non empty set
[: the carrier of (S), the carrier of (S):] is Relation-like non empty set
T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
g is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of g is non empty set
[: the carrier of T, the carrier of g:] is Relation-like non empty set
bool [: the carrier of T, the carrier of g:] is non empty set
the Arrows of (S) . (T,g) is set
[T,g] is set
{T,g} is non empty finite set
{T} is non empty finite set
{{T,g},{T}} is non empty with_non-empty_elements non empty-membered finite V30() set
the Arrows of (S) . [T,g] is set
x is Relation-like the carrier of T -defined the carrier of g -valued Function-like non empty V22( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of g:]
x is Element of the carrier of (S)
x is Element of the carrier of (S)
<^x,x^> is set
a is non empty set
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (latt x) is non empty set
y is Relation-like Function-like Element of <^x,x^>
@ y is Relation-like the carrier of (latt x) -defined the carrier of (latt x) -valued Function-like non empty V22( the carrier of (latt x)) quasi_total monotone Element of bool [: the carrier of (latt x), the carrier of (latt x):]
[: the carrier of (latt x), the carrier of (latt x):] is Relation-like non empty set
bool [: the carrier of (latt x), the carrier of (latt x):] is non empty set
a is non empty set
x is Element of the carrier of (S)
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
x is Element of the carrier of (S)
latt x is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
<^x,x^> is set
y is non empty set
S is non empty non empty-membered set
(S) is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
latt T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
g is non empty set
(S) is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise AltCatStr
the carrier of (S) is non empty set
T is Element of the carrier of (S)
latt T is non empty V87() reflexive transitive antisymmetric with_suprema with_infima RelStr
g is non empty set
S is non empty non empty-membered set
(S) is non empty transitive strict semi-functional V189() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_complete_lattices AltCatStr
the carrier of (S) is non