:: WAYBEL34 semantic presentation

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