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
c2 is non empty 1-sorted
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is M2( the carrier of L)
c3 . x is M2( the carrier of c2)
z1 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
x is set
z1 is set
c3 . x is set
c3 . z1 is set
L is non empty RelStr
the carrier of L is non empty set
c2 is non empty RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is M2( the carrier of L)
z1 is M2( the carrier of L)
c3 . x is M2( the carrier of c2)
c3 . z1 is M2( the carrier of c2)
x is M2( the carrier of L)
z1 is M2( the carrier of L)
z2 is M2( the carrier of c2)
c3 . x is M2( the carrier of c2)
z is M2( the carrier of c2)
c3 . z1 is M2( the carrier of c2)
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
c2 is M2( the carrier of L)
c3 is M2( the carrier of L)
x is M2( the carrier of L)
c2 "/\" x is M2( the carrier of L)
c3 "/\" x is M2( the carrier of L)
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
c2 is M2( the carrier of L)
c3 is M2( the carrier of L)
x is M2( the carrier of L)
c2 "\/" x is M2( the carrier of L)
c3 "\/" x is M2( the carrier of L)
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)
c2 is M2( the carrier of L)
(Bottom L) "/\" c2 is M2( the carrier of L)
(Bottom L) "\/" c2 is M2( the carrier of L)
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)
c2 is M2( the carrier of L)
(Top L) "/\" c2 is M2( the carrier of L)
(Top L) "\/" c2 is M2( the carrier of L)
c2 "/\" c2 is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
c2 is M2( the carrier of L)
c3 is M2( the carrier of L)
x is M2( the carrier of L)
c3 "/\" x is M2( the carrier of L)
c2 "\/" (c3 "/\" x) is M2( the carrier of L)
x "/\" c2 is M2( the carrier of L)
c2 "\/" (x "/\" c2) is M2( the carrier of L)
(c2 "\/" (x "/\" c2)) "\/" (c3 "/\" x) is M2( the carrier of L)
x "/\" c3 is M2( the carrier of L)
(x "/\" c2) "\/" (x "/\" c3) is M2( the carrier of L)
c2 "\/" ((x "/\" c2) "\/" (x "/\" c3)) is M2( the carrier of L)
c2 "\/" c3 is M2( the carrier of L)
(c2 "\/" c3) "/\" x is M2( the carrier of L)
c2 "\/" ((c2 "\/" c3) "/\" x) is M2( the carrier of L)
(c2 "\/" c3) "/\" c2 is M2( the carrier of L)
((c2 "\/" c3) "/\" c2) "\/" ((c2 "\/" c3) "/\" x) is M2( the carrier of L)
c2 "\/" x is M2( the carrier of L)
(c2 "\/" c3) "/\" (c2 "\/" x) is M2( the carrier of L)
c2 is M2( the carrier of L)
c3 is M2( the carrier of L)
x is M2( the carrier of L)
c3 "\/" x is M2( the carrier of L)
c2 "/\" (c3 "\/" x) is M2( the carrier of L)
c2 "/\" c3 is M2( the carrier of L)
c2 "/\" x is M2( the carrier of L)
(c2 "/\" c3) "\/" (c2 "/\" x) is M2( the carrier of L)
c3 "\/" x is M2( the carrier of L)
c2 "/\" (c3 "\/" x) is M2( the carrier of L)
c2 "\/" x is M2( the carrier of L)
c2 "/\" (c2 "\/" x) is M2( the carrier of L)
(c2 "/\" (c2 "\/" x)) "/\" (c3 "\/" x) is M2( the carrier of L)
x "\/" c2 is M2( the carrier of L)
(x "\/" c2) "/\" (c3 "\/" x) is M2( the carrier of L)
c2 "/\" ((x "\/" c2) "/\" (c3 "\/" x)) is M2( the carrier of L)
c2 "/\" c3 is M2( the carrier of L)
x "\/" (c2 "/\" c3) is M2( the carrier of L)
c2 "/\" (x "\/" (c2 "/\" c3)) is M2( the carrier of L)
c3 "/\" c2 is M2( the carrier of L)
(c3 "/\" c2) "\/" c2 is M2( the carrier of L)
(c2 "/\" c3) "\/" x is M2( the carrier of L)
((c3 "/\" c2) "\/" c2) "/\" ((c2 "/\" c3) "\/" x) is M2( the carrier of L)
c2 "/\" x is M2( the carrier of L)
(c2 "/\" c3) "\/" (c2 "/\" x) is M2( the carrier of L)
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
c2 is M2( the carrier of (BoolePoset L))
c3 is M2( the carrier of (BoolePoset L))
x is M2( the carrier of (BoolePoset L))
c3 "\/" x is M2( the carrier of (BoolePoset L))
c2 "/\" (c3 "\/" x) is M2( the carrier of (BoolePoset L))
c2 "/\" c3 is M2( the carrier of (BoolePoset L))
c2 "/\" x is M2( the carrier of (BoolePoset L))
(c2 "/\" c3) "\/" (c2 "/\" x) is M2( the carrier of (BoolePoset L))
c3 "\/" x is M2( the carrier of (BoolePoset L))
c2 "/\" (c3 "\/" x) is M2( the carrier of (BoolePoset L))
c2 /\ (c3 "\/" x) is set
c3 \/ x is set
c2 /\ (c3 \/ x) is set
c2 /\ c3 is set
c2 /\ x is set
(c2 /\ c3) \/ (c2 /\ x) is set
c2 "/\" c3 is M2( the carrier of (BoolePoset L))
(c2 "/\" c3) \/ (c2 /\ x) is set
c2 "/\" x is M2( the carrier of (BoolePoset L))
(c2 "/\" c3) \/ (c2 "/\" x) is set
(c2 "/\" c3) "\/" (c2 "/\" x) is M2( the carrier of (BoolePoset L))
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
c3 is RelStr
the carrier of c3 is set
[: the carrier of c3, the carrier of c3:] is V7() set
bool [: the carrier of c3, the carrier of c3:] is set
id c3 is V7() V10( the carrier of c3) V11( the carrier of c3) Function-like V27( the carrier of c3) quasi_total isomorphic M2( bool [: the carrier of c3, the carrier of c3:])
id the carrier of c3 is V7() V10( the carrier of c3) V11( the carrier of c3) Function-like one-to-one V27( the carrier of c3) quasi_total M2( bool [: the carrier of c3, the carrier of c3:])
L is non empty RelStr
c2 is non empty RelStr
the carrier of L is non empty set
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 " is V7() Function-like set
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
x " is V7() Function-like set
L is RelStr
c2 is RelStr
c3 is RelStr
the carrier of L is set
the carrier of c2 is set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
x is V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:])
the carrier of c3 is set
[: the carrier of c2, the carrier of c3:] is V7() set
bool [: the carrier of c2, the carrier of c3:] is set
z1 is V7() V10( the carrier of c2) V11( the carrier of c3) Function-like quasi_total M2( bool [: the carrier of c2, the carrier of c3:])
z1 * x is V7() V10( the carrier of L) V11( the carrier of c3) Function-like M2( bool [: the carrier of L, the carrier of c3:])
[: the carrier of L, the carrier of c3:] is V7() set
bool [: the carrier of L, the carrier of c3:] is set
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 c3) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c3:])
z2 is V7() V10( the carrier of L) V11( the carrier of c3) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c3:])
z2 is V7() V10( the carrier of L) V11( the carrier of c3) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c3:])
L is RelStr
the carrier of L is set
c2 is RelStr
the carrier of c2 is set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
the V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:]) is V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:])
the V7() V10( the carrier of c2) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c2, the carrier of L:]) is V7() V10( the carrier of c2) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c2, the carrier of L:])
[ the V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:]), the V7() V10( the carrier of c2) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c2, the carrier of L:])] is set
{ the V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:]), the V7() V10( the carrier of c2) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c2, the carrier of L:])} is functional set
{ the V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:])} is functional set
{{ the V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:]), the V7() V10( the carrier of c2) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c2, the carrier of L:])},{ the V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:])}} is set
L is RelStr
the carrier of L is set
c2 is RelStr
the carrier of c2 is set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is V7() V10( the carrier of L) V11( the carrier of c2) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is V7() V10( the carrier of c2) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c2, the carrier of L:])
[c3,x] is set
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
L is non empty RelStr
c2 is non empty RelStr
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
z1 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
z2 is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,z1,z2) is (L,c2)
{z1,z2} is functional set
{z1} is functional set
{{z1,z2},{z1}} is set
z is M2( the carrier of c2)
x is M2( the carrier of L)
c3 . x is M2( the carrier of c2)
x . z is M2( the carrier of L)
y is M2( the carrier of c2)
x . y is M2( the carrier of L)
Ix is M2( the carrier of L)
c3 . Ix is M2( the carrier of c2)
L is non empty RelStr
the carrier of L is non empty set
c2 is non empty RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c2 is non empty RelStr
the carrier of c2 is non empty set
L is non empty RelStr
the carrier of L is non empty set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
uparrow z1 is non empty filtered upper M2( bool the carrier of c2)
bool the carrier of c2 is set
{z1} is M2( bool the carrier of c2)
uparrow {z1} is upper M2( bool the carrier of c2)
c3 " (uparrow z1) is M2( bool the carrier of L)
bool the carrier of L is set
c3 . (x . z1) is M2( the carrier of c2)
z is M2( the carrier of L)
z is M2( the carrier of L)
c3 . z is M2( the carrier of c2)
"/\" ((c3 " (uparrow z1)),L) is M2( the carrier of L)
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c3 . z2 is M2( the carrier of c2)
uparrow z1 is non empty filtered upper M2( bool the carrier of c2)
{z1} is M2( bool the carrier of c2)
uparrow {z1} is upper M2( bool the carrier of c2)
c3 " (uparrow z1) is M2( bool the carrier of L)
"/\" ((c3 " (uparrow z1)),L) is M2( the carrier of L)
c3 . ("/\" ((c3 " (uparrow z1)),L)) is M2( the carrier of c2)
c3 . (x . z1) is M2( the carrier of c2)
z1 is M2( the carrier of c2)
z2 is M2( the carrier of c2)
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 c2)
{z2} is M2( bool the carrier of c2)
uparrow {z2} is upper M2( bool the carrier of c2)
uparrow z1 is non empty filtered upper M2( bool the carrier of c2)
{z1} is M2( bool the carrier of c2)
uparrow {z1} is upper M2( bool the carrier of c2)
c3 " (uparrow z2) is M2( bool the carrier of L)
c3 " (uparrow z1) is M2( bool the carrier of L)
"/\" ((c3 " (uparrow z1)),L) is M2( the carrier of L)
"/\" ((c3 " (uparrow z2)),L) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
z1 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
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 c2)
bool the carrier of c2 is set
x . (c3 . z1) is M2( the carrier of L)
z is M2( the carrier of c2)
z is M2( the carrier of c2)
x . z is M2( the carrier of L)
"\/" ((x " (downarrow z1)),c2) is M2( the carrier of c2)
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c3 . z2 is M2( the carrier of c2)
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 c2)
"\/" ((x " (downarrow z2)),c2) is M2( the carrier of c2)
x . ("\/" ((x " (downarrow z2)),c2)) is M2( the carrier of L)
x . (c3 . z2) is M2( the carrier of L)
z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
c3 . z2 is M2( the carrier of c2)
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 c2)
x " (downarrow z1) is M2( bool the carrier of c2)
"\/" ((x " (downarrow z1)),c2) is M2( the carrier of c2)
"\/" ((x " (downarrow z2)),c2) is M2( the carrier of c2)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
bool the carrier of L is set
z1 is M2( bool the carrier of L)
"/\" (z1,L) is M2( the carrier of L)
c3 .: z1 is M2( bool the carrier of c2)
bool the carrier of c2 is set
"/\" ((c3 .: z1),c2) is M2( the carrier of c2)
c3 . ("/\" (z1,L)) is M2( the carrier of c2)
z is M2( the carrier of c2)
x . z is M2( the carrier of L)
x is M2( the carrier of L)
c3 . x is M2( the carrier of c2)
z is M2( the carrier of c2)
x is M2( the carrier of L)
c3 . x is M2( the carrier of c2)
y is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
(L,c2,x,c3) is (L,c2)
{x,c3} is functional set
{x} is functional set
{{x,c3},{x}} is set
bool the carrier of c2 is set
z1 is M2( bool the carrier of c2)
"\/" (z1,c2) is M2( the carrier of c2)
c3 .: z1 is M2( bool the carrier of L)
bool the carrier of L is set
"\/" ((c3 .: z1),L) is M2( the carrier of L)
c3 . ("\/" (z1,c2)) is M2( the carrier of L)
z is M2( the carrier of L)
x . z is M2( the carrier of c2)
x is M2( the carrier of c2)
c3 . x is M2( the carrier of L)
z is M2( the carrier of L)
x is M2( the carrier of c2)
c3 . x is M2( the carrier of L)
y is M2( the carrier of c2)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is set
z1 is M2( the carrier of c2)
uparrow z1 is non empty filtered upper M2( bool the carrier of c2)
bool the carrier of c2 is set
{z1} is M2( bool the carrier of c2)
uparrow {z1} is upper M2( bool the carrier of c2)
c3 " (uparrow z1) is M2( bool the carrier of L)
bool the carrier of L is set
"/\" ((c3 " (uparrow z1)),L) is M2( the carrier of L)
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
uparrow z1 is non empty filtered upper M2( bool the carrier of c2)
bool the carrier of c2 is set
{z1} is M2( bool the carrier of c2)
uparrow {z1} is upper M2( bool the carrier of c2)
c3 " (uparrow z1) is M2( bool the carrier of L)
bool the carrier of L is set
"/\" ((c3 " (uparrow z1)),L) is M2( the carrier of L)
z2 is M2( the carrier of c2)
uparrow z2 is non empty filtered upper M2( bool the carrier of c2)
{z2} is M2( bool the carrier of c2)
uparrow {z2} is upper M2( bool the carrier of c2)
c3 " (uparrow z2) is M2( bool the carrier of L)
"/\" ((c3 " (uparrow z2)),L) is M2( the carrier of L)
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 c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
z2 is M2( the carrier of c2)
z1 . z2 is M2( the carrier of L)
z is M2( the carrier of L)
c3 . z is M2( the carrier of c2)
uparrow z2 is non empty filtered upper M2( bool the carrier of c2)
bool the carrier of c2 is set
{z2} is M2( bool the carrier of c2)
uparrow {z2} is upper M2( bool the carrier of c2)
c3 " (uparrow z2) is M2( bool the carrier of L)
"/\" ((c3 " (uparrow z2)),L) is M2( the carrier of L)
c3 .: (c3 " (uparrow z2)) is M2( bool the carrier of c2)
c3 . ("/\" ((c3 " (uparrow z2)),L)) is M2( the carrier of c2)
"/\" ((c3 .: (c3 " (uparrow z2))),c2) is M2( the carrier of c2)
"/\" ((uparrow z2),c2) is M2( the carrier of c2)
c3 . (z1 . z2) is M2( the carrier of c2)
(L,c2,c3,z1) is (L,c2)
{c3,z1} is functional set
{c3} is functional set
{{c3,z1},{c3}} is set
z2 is M2( the carrier of c2)
z is M2( the carrier of c2)
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 c2)
bool the carrier of c2 is set
{z} is M2( bool the carrier of c2)
uparrow {z} is upper M2( bool the carrier of c2)
uparrow z2 is non empty filtered upper M2( bool the carrier of c2)
{z2} is M2( bool the carrier of c2)
uparrow {z2} is upper M2( bool the carrier of c2)
c3 " (uparrow z2) is M2( bool the carrier of L)
c3 " (uparrow z) is M2( bool the carrier of L)
"/\" ((c3 " (uparrow z2)),L) is M2( the carrier of L)
"/\" ((c3 " (uparrow z)),L) is M2( the carrier of L)
z2 is M2( the carrier of c2)
z1 . z2 is M2( the carrier of L)
uparrow z2 is non empty filtered upper M2( bool the carrier of c2)
bool the carrier of c2 is set
{z2} is M2( bool the carrier of c2)
uparrow {z2} is upper M2( bool the carrier of c2)
c3 " (uparrow z2) is M2( bool the carrier of L)
"/\" ((c3 " (uparrow z2)),L) is M2( the carrier of L)
c3 .: (c3 " (uparrow z2)) is M2( bool the carrier of c2)
c3 . ("/\" ((c3 " (uparrow z2)),L)) is M2( the carrier of c2)
"/\" ((c3 .: (c3 " (uparrow z2))),c2) is M2( the carrier of c2)
"/\" ((uparrow z2),c2) is M2( the carrier of c2)
c3 . (z1 . z2) is M2( the carrier of c2)
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
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)
c3 " (downarrow z1) is M2( bool the carrier of c2)
bool the carrier of c2 is set
"\/" ((c3 " (downarrow z1)),c2) is M2( the carrier of c2)
x is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
z1 is M2( the carrier of L)
x . z1 is M2( the carrier of c2)
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)
c3 " (downarrow z1) is M2( bool the carrier of c2)
bool the carrier of c2 is set
"\/" ((c3 " (downarrow z1)),c2) is M2( the carrier of c2)
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)
c3 " (downarrow z2) is M2( bool the carrier of c2)
"\/" ((c3 " (downarrow z2)),c2) is M2( the carrier of c2)
bool the carrier of c2 is set
z2 is non empty directed lower M2( bool the carrier of c2)
z1 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
z2 is M2( the carrier of c2)
c3 . z2 is M2( the carrier of L)
z is M2( the carrier of L)
z1 . z is M2( the carrier of c2)
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)
c3 " (downarrow z) is M2( bool the carrier of c2)
"\/" ((c3 " (downarrow z)),c2) is M2( the carrier of c2)
c3 .: (c3 " (downarrow z)) is M2( bool the carrier of L)
c3 . ("\/" ((c3 " (downarrow z)),c2)) is M2( the carrier of L)
"\/" ((c3 .: (c3 " (downarrow z))),L) is M2( the carrier of L)
"\/" ((downarrow z),L) is M2( the carrier of L)
c3 . (z1 . z) is M2( the carrier of L)
(L,c2,z1,c3) is (L,c2)
{z1,c3} is functional set
{z1} is functional set
{{z1,c3},{z1}} is set
z2 is M2( the carrier of L)
z is M2( the carrier of L)
z1 . z2 is M2( the carrier of c2)
z1 . z is M2( the carrier of c2)
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)
c3 " (downarrow z2) is M2( bool the carrier of c2)
c3 " (downarrow z) is M2( bool the carrier of c2)
"\/" ((c3 " (downarrow z2)),c2) is M2( the carrier of c2)
"\/" ((c3 " (downarrow z)),c2) is M2( the carrier of c2)
z2 is M2( the carrier of L)
z1 . z2 is M2( the carrier of c2)
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)
c3 " (downarrow z2) is M2( bool the carrier of c2)
"\/" ((c3 " (downarrow z2)),c2) is M2( the carrier of c2)
c3 .: (c3 " (downarrow z2)) is M2( bool the carrier of L)
c3 . ("\/" ((c3 " (downarrow z2)),c2)) is M2( the carrier of L)
"\/" ((c3 .: (c3 " (downarrow z2))),L) is M2( the carrier of L)
"\/" ((downarrow z2),L) is M2( the carrier of L)
c3 . (z1 . z2) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
(L,c2,x,c3) is (L,c2)
{x,c3} is functional set
{x} is functional set
{{x,c3},{x}} is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
(L,c2,x,c3) is (L,c2)
{x,c3} is functional set
{x} is functional set
{{x,c3},{x}} is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, 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:])
[: 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 c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total monotone isomorphic M2( bool [: the carrier of c2, the carrier of c2:])
[: the carrier of c2, the carrier of c2:] is V7() set
bool [: the carrier of c2, the carrier of c2:] is set
id the carrier of c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
x * c3 is non empty 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:])
c3 * x is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
z1 is M2( the carrier of L)
(x * c3) . z1 is M2( the carrier of L)
(id L) . z1 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
x . (c3 . z1) is M2( the carrier of L)
z1 is M2( the carrier of c2)
(id c2) . z1 is M2( the carrier of c2)
(c3 * x) . z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
c3 . (x . z1) is M2( the carrier of c2)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, 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:])
[: 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 c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total monotone isomorphic M2( bool [: the carrier of c2, the carrier of c2:])
[: the carrier of c2, the carrier of c2:] is V7() set
bool [: the carrier of c2, the carrier of c2:] is set
id the carrier of c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
x * c3 is non empty 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:])
c3 * x is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c3 . z2 is M2( the carrier of c2)
(x * c3) . z2 is M2( the carrier of L)
(id L) . z2 is M2( the carrier of L)
x . (c3 . z2) is M2( the carrier of L)
(id c2) . z1 is M2( the carrier of c2)
(c3 * x) . z1 is M2( the carrier of c2)
c3 . (x . z1) is M2( the carrier of c2)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, 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:])
[: 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 c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total monotone isomorphic M2( bool [: the carrier of c2, the carrier of c2:])
[: the carrier of c2, the carrier of c2:] is V7() set
bool [: the carrier of c2, the carrier of c2:] is set
id the carrier of c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
x * c3 is non empty 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:])
c3 * x is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
(x * c3) * x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(c3 * x) * c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
((x * c3) * x) . z1 is M2( the carrier of L)
(id c2) . z1 is M2( the carrier of c2)
(c3 * x) . z1 is M2( the carrier of c2)
x . ((c3 * x) . z1) is M2( the carrier of L)
x * (c3 * x) is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(x * (c3 * x)) . z1 is M2( the carrier of L)
(x * c3) . (x . z1) is M2( the carrier of L)
(id L) . (x . z1) is M2( the carrier of L)
z1 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
((c3 * x) * c3) . z1 is M2( the carrier of c2)
(x * c3) . z1 is M2( the carrier of L)
(id L) . z1 is M2( the carrier of L)
c3 . ((x * c3) . z1) is M2( the carrier of c2)
c3 * (x * c3) is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
(c3 * (x * c3)) . z1 is M2( the carrier of c2)
(id c2) . (c3 . z1) is M2( the carrier of c2)
(c3 * x) . (c3 . z1) is M2( the carrier of c2)
L is non empty RelStr
the carrier of L is non empty set
c2 is non empty RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
c3 * x is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
[: the carrier of c2, the carrier of c2:] is V7() set
bool [: the carrier of c2, the carrier of c2:] is set
(c3 * x) * c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
(c3 * x) * (c3 * x) is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
{z1} is M2( bool the carrier of c2)
bool the carrier of c2 is set
c3 " {z1} is M2( bool the carrier of L)
bool the carrier of L is set
rng c3 is non empty M2( bool the carrier of c2)
uparrow z1 is non empty filtered upper M2( bool the carrier of c2)
uparrow {z1} is upper M2( bool the carrier of c2)
c3 " (uparrow z1) is M2( bool the carrier of L)
c3 .: (c3 " (uparrow z1)) is M2( bool the carrier of c2)
"/\" ((c3 " (uparrow z1)),L) is M2( the carrier of L)
c3 . (x . z1) is M2( the carrier of c2)
z2 is set
c3 . z2 is set
z is M2( the carrier of L)
x is M2( the carrier of L)
x is M2( the carrier of L)
"/\" ((c3 " {z1}),L) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
id c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total monotone isomorphic M2( bool [: the carrier of c2, the carrier of c2:])
[: the carrier of c2, the carrier of c2:] is V7() set
bool [: the carrier of c2, the carrier of c2:] is set
id the carrier of c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
c3 * x is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
z1 is M2( the carrier of c2)
(c3 * x) . z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
{z1} is M2( bool the carrier of c2)
bool the carrier of c2 is set
c3 " {z1} is M2( bool the carrier of L)
bool the carrier of L is set
"/\" ((c3 " {z1}),L) is M2( the carrier of L)
c3 . (x . z1) is M2( the carrier of c2)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
dom x is non empty M2( bool the carrier of c2)
bool the carrier of c2 is set
c3 * x is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
[: the carrier of c2, the carrier of c2:] is V7() set
bool [: the carrier of c2, the carrier of c2:] is set
dom (c3 * x) is non empty M2( bool the carrier of c2)
x * c3 is non empty 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, 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 c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total monotone isomorphic M2( bool [: the carrier of c2, the carrier of c2:])
id the carrier of c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
z1 is M2( the carrier of c2)
x . z1 is M2( the carrier of L)
{z1} is M2( bool the carrier of c2)
c3 " {z1} is M2( bool the carrier of L)
bool the carrier of L is set
rng (c3 * x) is non empty M2( bool the carrier of c2)
(x * c3) * x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
x * (c3 * x) is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
z1 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
{z1} is M2( bool the carrier of L)
bool the carrier of L is set
x " {z1} is M2( bool the carrier of c2)
bool the carrier of c2 is set
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 c2)
x .: (x " (downarrow z1)) is M2( bool the carrier of L)
"\/" ((x " (downarrow z1)),c2) is M2( the carrier of c2)
x . (c3 . z1) is M2( the carrier of L)
z2 is set
x . z2 is set
z is M2( the carrier of c2)
x is M2( the carrier of c2)
x is M2( the carrier of c2)
"\/" ((x " {z1}),c2) is M2( the carrier of c2)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, 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:])
[: 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:])
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
x * c3 is non empty 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:])
z1 is M2( the carrier of L)
(x * c3) . z1 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
{z1} is M2( bool the carrier of L)
bool the carrier of L is set
x " {z1} is M2( bool the carrier of c2)
bool the carrier of c2 is set
"\/" ((x " {z1}),c2) is M2( the carrier of c2)
x . (c3 . z1) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c2 is non empty reflexive transitive antisymmetric RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
[: the carrier of c2, the carrier of L:] is V7() set
bool [: the carrier of c2, the carrier of L:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is non empty V7() V10( the carrier of c2) V11( the carrier of L) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of L:])
(L,c2,c3,x) is (L,c2)
{c3,x} is functional set
{c3} is functional set
{{c3,x},{c3}} is set
x * c3 is non empty 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, 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 c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total monotone isomorphic M2( bool [: the carrier of c2, the carrier of c2:])
[: the carrier of c2, the carrier of c2:] is V7() set
bool [: the carrier of c2, the carrier of c2:] is set
id the carrier of c2 is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like one-to-one V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
c3 * x is non empty V7() V10( the carrier of c2) V11( the carrier of c2) Function-like V27( the carrier of c2) quasi_total M2( bool [: the carrier of c2, the carrier of c2:])
(c3 * x) * c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
c3 * (x * c3) is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
dom c3 is non empty M2( bool the carrier of L)
bool the carrier of L is set
dom (x * c3) is non empty M2( bool the carrier of L)
rng (x * c3) is non empty M2( bool the carrier of L)
z1 is M2( the carrier of L)
c3 . z1 is M2( the carrier of c2)
{z1} is M2( bool the carrier of L)
x " {z1} is M2( bool the carrier of c2)
bool the carrier of c2 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
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
c2 is non empty 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:])
L is non empty RelStr
the carrier of L is non empty set
c2 is non empty RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
x is M2( the carrier of L)
c3 . x is M2( the carrier of c2)
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
c2 is non empty 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:])
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
c2 is non empty 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:])
rng c2 is non empty M2( bool the carrier of L)
bool the carrier of L is set
c3 is set
c2 . c3 is set
dom c2 is non empty M2( bool the carrier of L)
x is set
c2 . x is set
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
c2 is non empty 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:])
rng c2 is non empty M2( bool the carrier of L)
c3 is M2( bool the carrier of L)
"/\" (c3,L) is M2( the carrier of L)
c2 . ("/\" (c3,L)) is M2( the carrier of L)
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)
c2 . x is M2( the carrier of L)
(id L) . ("/\" (c3,L)) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is V7() set
bool [: the carrier of L, the carrier of L:] is set
bool the carrier of L is set
c2 is non empty 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:])
rng c2 is non empty M2( bool the carrier of L)
c3 is M2( bool the carrier of L)
"\/" (c3,L) is M2( the carrier of L)
c2 . ("\/" (c3,L)) is M2( the carrier of L)
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)
c2 . x is M2( the carrier of L)
(id L) . ("\/" (c3,L)) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c2 is non empty RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set
bool [: the carrier of L, the carrier of c2:] is set
c3 is non empty V7() V10( the carrier of L) V11( the carrier of c2) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c2:])
Image c3 is non empty strict full SubRelStr of c2
rng c3 is non empty M2( bool the carrier of c2)
bool the carrier of c2 is set
subrelstr (rng c3) is non empty strict full SubRelStr of c2
the carrier of (Image c3) is non empty set
the carrier of (Image c3) |` c3 is V7() V10( the carrier of L) V11( the carrier of c2) V11( the carrier of (Image c3)) V11( the carrier of c2) Function-like M2( bool [: the carrier of L, the carrier of c2:])
[: the carrier of L, the carrier of (Image c3):] is V7() set
bool [: the carrier of L, the carrier of (Image c3):] is set
dom c3 is non empty M2( bool the carrier of L)
bool the carrier of L is set
L is non empty RelStr
the carrier of L is non empty set
c2 is non empty RelStr
the carrier of c2 is non empty set
[: the carrier of L, the carrier of c2:] is V7() set