:: WAYBEL_1 semantic presentation

K133() is M2( bool K129())

K129() is set

bool K129() is set

K128() is set

bool K128() is set

{} is set

the empty V7() non-empty empty-yielding Function-like one-to-one constant functional set is empty V7() non-empty empty-yielding Function-like one-to-one constant functional set

1 is non empty set

{{},1} is set

bool K133() is set

L is non empty 1-sorted

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

x is M2( the carrier of L)

c

z1 is M2( the carrier of L)

c

x is set

z1 is set

c

c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

x is M2( the carrier of L)

z1 is M2( the carrier of L)

c

c

x is M2( the carrier of L)

z1 is M2( the carrier of L)

z2 is M2( the carrier of c

c

z is M2( the carrier of c

c

L is non empty transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

c

c

x is M2( the carrier of L)

c

c

L is non empty transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

c

c

x is M2( the carrier of L)

c

c

L is non empty antisymmetric lower-bounded RelStr

the carrier of L is non empty set

Bottom L is M2( the carrier of L)

"\/" ({},L) is M2( the carrier of L)

c

(Bottom L) "/\" c

(Bottom L) "\/" c

L is non empty antisymmetric upper-bounded RelStr

the carrier of L is non empty set

Top L is M2( the carrier of L)

"/\" ({},L) is M2( the carrier of L)

c

(Top L) "/\" c

(Top L) "\/" c

c

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

c

c

x is M2( the carrier of L)

c

c

x "/\" c

c

(c

x "/\" c

(x "/\" c

c

c

(c

c

(c

((c

c

(c

c

c

x is M2( the carrier of L)

c

c

c

c

(c

c

c

c

c

(c

x "\/" c

(x "\/" c

c

c

x "\/" (c

c

c

(c

(c

((c

c

(c

L is set

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

the carrier of (BoolePoset L) is non empty set

c

c

x is M2( the carrier of (BoolePoset L))

c

c

c

c

(c

c

c

c

c

c

c

c

(c

c

(c

c

(c

(c

L is non empty RelStr

the carrier of L is non empty set

L is RelStr

id L is V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

the carrier of L is set

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

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

id the carrier of L is V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

(id L) " is V7() Function-like set

c

the carrier of c

[: the carrier of c

bool [: the carrier of c

id c

id the carrier of c

L is non empty RelStr

c

the carrier of L is non empty set

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

x " is V7() Function-like set

L is RelStr

c

c

the carrier of L is set

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

x is V7() V10( the carrier of L) V11( the carrier of c

the carrier of c

[: the carrier of c

bool [: the carrier of c

z1 is V7() V10( the carrier of c

z1 * x is V7() V10( the carrier of L) V11( the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

z2 is non empty RelStr

the carrier of z2 is non empty set

z is non empty RelStr

the carrier of z is non empty set

[: the carrier of z2, the carrier of z:] is V7() set

bool [: the carrier of z2, the carrier of z:] is set

x is non empty RelStr

the carrier of x is non empty set

[: the carrier of z, the carrier of x:] is V7() set

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

[: the carrier of z, the carrier of z2:] is V7() set

bool [: the carrier of z, the carrier of z2:] is set

y is non empty V7() V10( the carrier of z2) V11( the carrier of z) Function-like V27( the carrier of z2) quasi_total M2( bool [: the carrier of z2, the carrier of z:])

y " is V7() Function-like set

Iy is non empty V7() V10( the carrier of z) V11( the carrier of z2) Function-like V27( the carrier of z) quasi_total M2( bool [: the carrier of z, the carrier of z2:])

[: the carrier of x, the carrier of z:] is V7() set

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

Ix is non empty V7() V10( the carrier of z) V11( the carrier of x) Function-like V27( the carrier of z) quasi_total M2( bool [: the carrier of z, the carrier of x:])

Ix " is V7() Function-like set

i1 is non empty V7() V10( the carrier of x) V11( the carrier of z) Function-like V27( the carrier of x) quasi_total M2( bool [: the carrier of x, the carrier of z:])

Ix * y is non empty V7() V10( the carrier of z2) V11( the carrier of x) Function-like V27( the carrier of z2) quasi_total M2( bool [: the carrier of z2, the carrier of x:])

[: the carrier of z2, the carrier of x:] is V7() set

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

Iy * i1 is non empty V7() V10( the carrier of x) V11( the carrier of z2) Function-like V27( the carrier of x) quasi_total M2( bool [: the carrier of x, the carrier of z2:])

[: the carrier of x, the carrier of z2:] is V7() set

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

(Ix * y) " is V7() Function-like set

z2 is V7() V10( the carrier of L) V11( the carrier of c

z2 is V7() V10( the carrier of L) V11( the carrier of c

z2 is V7() V10( the carrier of L) V11( the carrier of c

L is RelStr

the carrier of L is set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

the V7() V10( the carrier of L) V11( the carrier of c

the V7() V10( the carrier of c

[ the V7() V10( the carrier of L) V11( the carrier of c

{ the V7() V10( the carrier of L) V11( the carrier of c

{ the V7() V10( the carrier of L) V11( the carrier of c

{{ the V7() V10( the carrier of L) V11( the carrier of c

L is RelStr

the carrier of L is set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is V7() V10( the carrier of c

[c

{c

{c

{{c

L is non empty RelStr

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

z1 is non empty V7() V10( the carrier of L) V11( the carrier of c

z2 is non empty V7() V10( the carrier of c

(L,c

{z1,z2} is functional set

{z1} is functional set

{{z1,z2},{z1}} is set

z is M2( the carrier of c

x is M2( the carrier of L)

c

x . z is M2( the carrier of L)

y is M2( the carrier of c

x . y is M2( the carrier of L)

Ix is M2( the carrier of L)

c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

the carrier of c

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of c

bool [: the carrier of c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

uparrow z1 is non empty filtered upper M2( bool the carrier of c

bool the carrier of c

{z1} is M2( bool the carrier of c

uparrow {z1} is upper M2( bool the carrier of c

c

bool the carrier of L is set

c

z is M2( the carrier of L)

z is M2( the carrier of L)

c

"/\" ((c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

z2 is M2( the carrier of L)

c

uparrow z1 is non empty filtered upper M2( bool the carrier of c

{z1} is M2( bool the carrier of c

uparrow {z1} is upper M2( bool the carrier of c

c

"/\" ((c

c

c

z1 is M2( the carrier of c

z2 is M2( the carrier of c

x . z1 is M2( the carrier of L)

x . z2 is M2( the carrier of L)

uparrow z2 is non empty filtered upper M2( bool the carrier of c

{z2} is M2( bool the carrier of c

uparrow {z2} is upper M2( bool the carrier of c

uparrow z1 is non empty filtered upper M2( bool the carrier of c

{z1} is M2( bool the carrier of c

uparrow {z1} is upper M2( bool the carrier of c

c

c

"/\" ((c

"/\" ((c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

z1 is M2( the carrier of L)

c

downarrow z1 is non empty directed lower M2( bool the carrier of L)

bool the carrier of L is set

{z1} is M2( bool the carrier of L)

downarrow {z1} is lower M2( bool the carrier of L)

x " (downarrow z1) is M2( bool the carrier of c

bool the carrier of c

x . (c

z is M2( the carrier of c

z is M2( the carrier of c

x . z is M2( the carrier of L)

"\/" ((x " (downarrow z1)),c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

z2 is M2( the carrier of L)

c

downarrow z2 is non empty directed lower M2( bool the carrier of L)

{z2} is M2( bool the carrier of L)

downarrow {z2} is lower M2( bool the carrier of L)

x " (downarrow z2) is M2( bool the carrier of c

"\/" ((x " (downarrow z2)),c

x . ("\/" ((x " (downarrow z2)),c

x . (c

z1 is M2( the carrier of L)

z2 is M2( the carrier of L)

c

c

downarrow z1 is non empty directed lower M2( bool the carrier of L)

{z1} is M2( bool the carrier of L)

downarrow {z1} is lower M2( bool the carrier of L)

downarrow z2 is non empty directed lower M2( bool the carrier of L)

{z2} is M2( bool the carrier of L)

downarrow {z2} is lower M2( bool the carrier of L)

x " (downarrow z2) is M2( bool the carrier of c

x " (downarrow z1) is M2( bool the carrier of c

"\/" ((x " (downarrow z1)),c

"\/" ((x " (downarrow z2)),c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

[: the carrier of c

bool [: the carrier of c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

bool the carrier of L is set

z1 is M2( bool the carrier of L)

"/\" (z1,L) is M2( the carrier of L)

c

bool the carrier of c

"/\" ((c

c

z is M2( the carrier of c

x . z is M2( the carrier of L)

x is M2( the carrier of L)

c

z is M2( the carrier of c

x is M2( the carrier of L)

c

y is M2( the carrier of L)

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

c

the carrier of c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of c

bool [: the carrier of c

c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

x is non empty V7() V10( the carrier of L) V11( the carrier of c

(L,c

{x,c

{x} is functional set

{{x,c

bool the carrier of c

z1 is M2( bool the carrier of c

"\/" (z1,c

c

bool the carrier of L is set

"\/" ((c

c

z is M2( the carrier of L)

x . z is M2( the carrier of c

x is M2( the carrier of c

c

z is M2( the carrier of L)

x is M2( the carrier of c

c

y is M2( the carrier of c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is set

z1 is M2( the carrier of c

uparrow z1 is non empty filtered upper M2( bool the carrier of c

bool the carrier of c

{z1} is M2( bool the carrier of c

uparrow {z1} is upper M2( bool the carrier of c

c

bool the carrier of L is set

"/\" ((c

x is non empty V7() V10( the carrier of c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

uparrow z1 is non empty filtered upper M2( bool the carrier of c

bool the carrier of c

{z1} is M2( bool the carrier of c

uparrow {z1} is upper M2( bool the carrier of c

c

bool the carrier of L is set

"/\" ((c

z2 is M2( the carrier of c

uparrow z2 is non empty filtered upper M2( bool the carrier of c

{z2} is M2( bool the carrier of c

uparrow {z2} is upper M2( bool the carrier of c

c

"/\" ((c

bool the carrier of L is set

z2 is non empty filtered upper M2( bool the carrier of L)

z1 is non empty V7() V10( the carrier of c

z2 is M2( the carrier of c

z1 . z2 is M2( the carrier of L)

z is M2( the carrier of L)

c

uparrow z2 is non empty filtered upper M2( bool the carrier of c

bool the carrier of c

{z2} is M2( bool the carrier of c

uparrow {z2} is upper M2( bool the carrier of c

c

"/\" ((c

c

c

"/\" ((c

"/\" ((uparrow z2),c

c

(L,c

{c

{c

{{c

z2 is M2( the carrier of c

z is M2( the carrier of c

z1 . z2 is M2( the carrier of L)

z1 . z is M2( the carrier of L)

uparrow z is non empty filtered upper M2( bool the carrier of c

bool the carrier of c

{z} is M2( bool the carrier of c

uparrow {z} is upper M2( bool the carrier of c

uparrow z2 is non empty filtered upper M2( bool the carrier of c

{z2} is M2( bool the carrier of c

uparrow {z2} is upper M2( bool the carrier of c

c

c

"/\" ((c

"/\" ((c

z2 is M2( the carrier of c

z1 . z2 is M2( the carrier of L)

uparrow z2 is non empty filtered upper M2( bool the carrier of c

bool the carrier of c

{z2} is M2( bool the carrier of c

uparrow {z2} is upper M2( bool the carrier of c

c

"/\" ((c

c

c

"/\" ((c

"/\" ((uparrow z2),c

c

c

the carrier of c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of c

bool [: the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

x is set

z1 is M2( the carrier of L)

downarrow z1 is non empty directed lower M2( bool the carrier of L)

bool the carrier of L is set

{z1} is M2( bool the carrier of L)

downarrow {z1} is lower M2( bool the carrier of L)

c

bool the carrier of c

"\/" ((c

x is non empty V7() V10( the carrier of L) V11( the carrier of c

z1 is M2( the carrier of L)

x . z1 is M2( the carrier of c

downarrow z1 is non empty directed lower M2( bool the carrier of L)

bool the carrier of L is set

{z1} is M2( bool the carrier of L)

downarrow {z1} is lower M2( bool the carrier of L)

c

bool the carrier of c

"\/" ((c

z2 is M2( the carrier of L)

downarrow z2 is non empty directed lower M2( bool the carrier of L)

{z2} is M2( bool the carrier of L)

downarrow {z2} is lower M2( bool the carrier of L)

c

"\/" ((c

bool the carrier of c

z2 is non empty directed lower M2( bool the carrier of c

z1 is non empty V7() V10( the carrier of L) V11( the carrier of c

z2 is M2( the carrier of c

c

z is M2( the carrier of L)

z1 . z is M2( the carrier of c

downarrow z is non empty directed lower M2( bool the carrier of L)

bool the carrier of L is set

{z} is M2( bool the carrier of L)

downarrow {z} is lower M2( bool the carrier of L)

c

"\/" ((c

c

c

"\/" ((c

"\/" ((downarrow z),L) is M2( the carrier of L)

c

(L,c

{z1,c

{z1} is functional set

{{z1,c

z2 is M2( the carrier of L)

z is M2( the carrier of L)

z1 . z2 is M2( the carrier of c

z1 . z is M2( the carrier of c

downarrow z2 is non empty directed lower M2( bool the carrier of L)

bool the carrier of L is set

{z2} is M2( bool the carrier of L)

downarrow {z2} is lower M2( bool the carrier of L)

downarrow z is non empty directed lower M2( bool the carrier of L)

{z} is M2( bool the carrier of L)

downarrow {z} is lower M2( bool the carrier of L)

c

c

"\/" ((c

"\/" ((c

z2 is M2( the carrier of L)

z1 . z2 is M2( the carrier of c

downarrow z2 is non empty directed lower M2( bool the carrier of L)

bool the carrier of L is set

{z2} is M2( bool the carrier of L)

downarrow {z2} is lower M2( bool the carrier of L)

c

"\/" ((c

c

c

"\/" ((c

"\/" ((downarrow z2),L) is M2( the carrier of L)

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

[: the carrier of c

bool [: the carrier of c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

c

the carrier of c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of c

bool [: the carrier of c

c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

x is non empty V7() V10( the carrier of L) V11( the carrier of c

(L,c

{x,c

{x} is functional set

{{x,c

x is non empty V7() V10( the carrier of L) V11( the carrier of c

(L,c

{x,c

{x} is functional set

{{x,c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic M2( bool [: the carrier of L, the carrier of L:])

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

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

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

id c

[: the carrier of c

bool [: the carrier of c

id the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

x * c

c

z1 is M2( the carrier of L)

(x * c

(id L) . z1 is M2( the carrier of L)

c

x . (c

z1 is M2( the carrier of c

(id c

(c

x . z1 is M2( the carrier of L)

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic M2( bool [: the carrier of L, the carrier of L:])

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

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

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

id c

[: the carrier of c

bool [: the carrier of c

id the carrier of c

c

x is non empty V7() V10( the carrier of c

x * c

c

(L,c

{c

{c

{{c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

z2 is M2( the carrier of L)

c

(x * c

(id L) . z2 is M2( the carrier of L)

x . (c

(id c

(c

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic M2( bool [: the carrier of L, the carrier of L:])

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

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

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

id c

[: the carrier of c

bool [: the carrier of c

id the carrier of c

c

x is non empty V7() V10( the carrier of c

x * c

c

(x * c

(c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

((x * c

(id c

(c

x . ((c

x * (c

(x * (c

(x * c

(id L) . (x . z1) is M2( the carrier of L)

z1 is M2( the carrier of L)

c

((c

(x * c

(id L) . z1 is M2( the carrier of L)

c

c

(c

(id c

(c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

c

[: the carrier of c

bool [: the carrier of c

(c

(c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

{z1} is M2( bool the carrier of c

bool the carrier of c

c

bool the carrier of L is set

rng c

uparrow z1 is non empty filtered upper M2( bool the carrier of c

uparrow {z1} is upper M2( bool the carrier of c

c

c

"/\" ((c

c

z2 is set

c

z is M2( the carrier of L)

x is M2( the carrier of L)

x is M2( the carrier of L)

"/\" ((c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

id c

[: the carrier of c

bool [: the carrier of c

id the carrier of c

c

x is non empty V7() V10( the carrier of c

c

z1 is M2( the carrier of c

(c

x . z1 is M2( the carrier of L)

{z1} is M2( bool the carrier of c

bool the carrier of c

c

bool the carrier of L is set

"/\" ((c

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

dom x is non empty M2( bool the carrier of c

bool the carrier of c

c

[: the carrier of c

bool [: the carrier of c

dom (c

x * c

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

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

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic M2( bool [: the carrier of L, the carrier of L:])

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

id c

id the carrier of c

z1 is M2( the carrier of c

x . z1 is M2( the carrier of L)

{z1} is M2( bool the carrier of c

c

bool the carrier of L is set

rng (c

(x * c

x * (c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

z1 is M2( the carrier of L)

c

{z1} is M2( bool the carrier of L)

bool the carrier of L is set

x " {z1} is M2( bool the carrier of c

bool the carrier of c

rng x is non empty M2( bool the carrier of L)

downarrow z1 is non empty directed lower M2( bool the carrier of L)

downarrow {z1} is lower M2( bool the carrier of L)

x " (downarrow z1) is M2( bool the carrier of c

x .: (x " (downarrow z1)) is M2( bool the carrier of L)

"\/" ((x " (downarrow z1)),c

x . (c

z2 is set

x . z2 is set

z is M2( the carrier of c

x is M2( the carrier of c

x is M2( the carrier of c

"\/" ((x " {z1}),c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic M2( bool [: the carrier of L, the carrier of L:])

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

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

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

c

x is non empty V7() V10( the carrier of c

x * c

z1 is M2( the carrier of L)

(x * c

c

{z1} is M2( bool the carrier of L)

bool the carrier of L is set

x " {z1} is M2( bool the carrier of c

bool the carrier of c

"\/" ((x " {z1}),c

x . (c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

[: the carrier of c

bool [: the carrier of c

c

x is non empty V7() V10( the carrier of c

(L,c

{c

{c

{{c

x * c

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

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

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic M2( bool [: the carrier of L, the carrier of L:])

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

id c

[: the carrier of c

bool [: the carrier of c

id the carrier of c

c

(c

c

dom c

bool the carrier of L is set

dom (x * c

rng (x * c

z1 is M2( the carrier of L)

c

{z1} is M2( bool the carrier of L)

x " {z1} is M2( bool the carrier of c

bool the carrier of c

L is non empty RelStr

the carrier of L is non empty set

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

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

L is non empty RelStr

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic M2( bool [: the carrier of L, the carrier of L:])

the carrier of L is non empty set

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

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

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

L is non empty RelStr

the carrier of L is non empty set

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

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

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic (L) M2( bool [: the carrier of L, the carrier of L:])

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

L is non empty RelStr

the carrier of L is non empty set

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

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

L is non empty RelStr

the carrier of L is non empty set

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

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

c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

x is M2( the carrier of L)

c

L is non empty reflexive RelStr

the carrier of L is non empty set

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

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

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic (L) M2( bool [: the carrier of L, the carrier of L:])

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

L is non empty reflexive RelStr

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic (L) M2( bool [: the carrier of L, the carrier of L:])

the carrier of L is non empty set

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

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

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

L is non empty RelStr

the carrier of L is non empty set

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

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

L is non empty RelStr

the carrier of L is non empty set

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

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

c

L is non empty reflexive RelStr

the carrier of L is non empty set

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

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

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic (L) (L) M2( bool [: the carrier of L, the carrier of L:])

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

L is non empty reflexive RelStr

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic (L) (L) M2( bool [: the carrier of L, the carrier of L:])

the carrier of L is non empty set

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

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

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

L is non empty 1-sorted

the carrier of L is non empty set

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

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

c

rng c

bool the carrier of L is set

c

c

dom c

x is set

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

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

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

bool the carrier of L is set

c

rng c

c

"/\" (c

c

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic (L) (L) (L) M2( bool [: the carrier of L, the carrier of L:])

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

x is M2( the carrier of L)

c

(id L) . ("/\" (c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

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

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

bool the carrier of L is set

c

rng c

c

"\/" (c

c

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total monotone isomorphic (L) (L) (L) M2( bool [: the carrier of L, the carrier of L:])

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of L:])

x is M2( the carrier of L)

c

(id L) . ("\/" (c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c

bool [: the carrier of L, the carrier of c

c

Image c

rng c

bool the carrier of c

subrelstr (rng c

the carrier of (Image c

the carrier of (Image c

[: the carrier of L, the carrier of (Image c

bool [: the carrier of L, the carrier of (Image c

dom c

bool the carrier of L is set

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

[: the carrier of L, the carrier of c