:: 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₂ is non empty 1-sorted
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is M2( the carrier of L)
c₃ . x is M2( the carrier of c₂)
z1 is M2( the carrier of L)
c₃ . z1 is M2( the carrier of c₂)
x is set
z1 is set
c₃ . x is set
c₃ . z1 is set
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is M2( the carrier of L)
z1 is M2( the carrier of L)
c₃ . x is M2( the carrier of c₂)
c₃ . z1 is M2( the carrier of c₂)
x is M2( the carrier of L)
z1 is M2( the carrier of L)
z2 is M2( the carrier of c₂)
c₃ . x is M2( the carrier of c₂)
z is M2( the carrier of c₂)
c₃ . z1 is M2( the carrier of c₂)
L is non empty transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
c₂ "/\" x is M2( the carrier of L)
c₃ "/\" x is M2( the carrier of L)
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
c₂ "\/" x is M2( the carrier of L)
c₃ "\/" 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)
c₂ is M2( the carrier of L)
(Bottom L) "/\" c₂ is M2( the carrier of L)
(Bottom L) "\/" c₂ 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)
c₂ is M2( the carrier of L)
(Top L) "/\" c₂ is M2( the carrier of L)
(Top L) "\/" c₂ is M2( the carrier of L)
c₂ "/\" c₂ 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
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
c₃ "/\" x is M2( the carrier of L)
c₂ "\/" (c₃ "/\" x) is M2( the carrier of L)
x "/\" c₂ is M2( the carrier of L)
c₂ "\/" (x "/\" c₂) is M2( the carrier of L)
(c₂ "\/" (x "/\" c₂)) "\/" (c₃ "/\" x) is M2( the carrier of L)
x "/\" c₃ is M2( the carrier of L)
(x "/\" c₂) "\/" (x "/\" c₃) is M2( the carrier of L)
c₂ "\/" ((x "/\" c₂) "\/" (x "/\" c₃)) is M2( the carrier of L)
c₂ "\/" c₃ is M2( the carrier of L)
(c₂ "\/" c₃) "/\" x is M2( the carrier of L)
c₂ "\/" ((c₂ "\/" c₃) "/\" x) is M2( the carrier of L)
(c₂ "\/" c₃) "/\" c₂ is M2( the carrier of L)
((c₂ "\/" c₃) "/\" c₂) "\/" ((c₂ "\/" c₃) "/\" x) is M2( the carrier of L)
c₂ "\/" x is M2( the carrier of L)
(c₂ "\/" c₃) "/\" (c₂ "\/" x) is M2( the carrier of L)
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
c₃ "\/" x is M2( the carrier of L)
c₂ "/\" (c₃ "\/" x) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
c₂ "/\" x is M2( the carrier of L)
(c₂ "/\" c₃) "\/" (c₂ "/\" x) is M2( the carrier of L)
c₃ "\/" x is M2( the carrier of L)
c₂ "/\" (c₃ "\/" x) is M2( the carrier of L)
c₂ "\/" x is M2( the carrier of L)
c₂ "/\" (c₂ "\/" x) is M2( the carrier of L)
(c₂ "/\" (c₂ "\/" x)) "/\" (c₃ "\/" x) is M2( the carrier of L)
x "\/" c₂ is M2( the carrier of L)
(x "\/" c₂) "/\" (c₃ "\/" x) is M2( the carrier of L)
c₂ "/\" ((x "\/" c₂) "/\" (c₃ "\/" x)) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
x "\/" (c₂ "/\" c₃) is M2( the carrier of L)
c₂ "/\" (x "\/" (c₂ "/\" c₃)) is M2( the carrier of L)
c₃ "/\" c₂ is M2( the carrier of L)
(c₃ "/\" c₂) "\/" c₂ is M2( the carrier of L)
(c₂ "/\" c₃) "\/" x is M2( the carrier of L)
((c₃ "/\" c₂) "\/" c₂) "/\" ((c₂ "/\" c₃) "\/" x) is M2( the carrier of L)
c₂ "/\" x is M2( the carrier of L)
(c₂ "/\" c₃) "\/" (c₂ "/\" 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
c₂ is M2( the carrier of (BoolePoset L))
c₃ is M2( the carrier of (BoolePoset L))
x is M2( the carrier of (BoolePoset L))
c₃ "\/" x is M2( the carrier of (BoolePoset L))
c₂ "/\" (c₃ "\/" x) is M2( the carrier of (BoolePoset L))
c₂ "/\" c₃ is M2( the carrier of (BoolePoset L))
c₂ "/\" x is M2( the carrier of (BoolePoset L))
(c₂ "/\" c₃) "\/" (c₂ "/\" x) is M2( the carrier of (BoolePoset L))
c₃ "\/" x is M2( the carrier of (BoolePoset L))
c₂ "/\" (c₃ "\/" x) is M2( the carrier of (BoolePoset L))
c₂ /\ (c₃ "\/" x) is set
c₃ \/ x is set
c₂ /\ (c₃ \/ x) is set
c₂ /\ c₃ is set
c₂ /\ x is set
(c₂ /\ c₃) \/ (c₂ /\ x) is set
c₂ "/\" c₃ is M2( the carrier of (BoolePoset L))
(c₂ "/\" c₃) \/ (c₂ /\ x) is set
c₂ "/\" x is M2( the carrier of (BoolePoset L))
(c₂ "/\" c₃) \/ (c₂ "/\" x) is set
(c₂ "/\" c₃) "\/" (c₂ "/\" 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
c₃ is RelStr
the carrier of c₃ is set
[: the carrier of c₃, the carrier of c₃:] is V7() set
bool [: the carrier of c₃, the carrier of c₃:] is set
id c₃ is V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like V27( the carrier of c₃) quasi_total isomorphic M2( bool [: the carrier of c₃, the carrier of c₃:])
id the carrier of c₃ is V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of c₃:])
L is non empty RelStr
c₂ is non empty RelStr
the carrier of L is non empty set
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ " is V7() Function-like set
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
x " is V7() Function-like set
L is RelStr
c₂ is RelStr
c₃ is RelStr
the carrier of L is set
the carrier of c₂ is set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
x is V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
the carrier of c₃ is set
[: the carrier of c₂, the carrier of c₃:] is V7() set
bool [: the carrier of c₂, the carrier of c₃:] is set
z1 is V7() V10( the carrier of c₂) V11( the carrier of c₃) Function-like quasi_total M2( bool [: the carrier of c₂, the carrier of c₃:])
z1 * x is V7() V10( the carrier of L) V11( the carrier of c₃) Function-like M2( bool [: the carrier of L, the carrier of c₃:])
[: the carrier of L, the carrier of c₃:] is V7() set
bool [: the carrier of L, the carrier of c₃:] 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 c₃) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
z2 is V7() V10( the carrier of L) V11( the carrier of c₃) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
z2 is V7() V10( the carrier of L) V11( the carrier of c₃) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
L is RelStr
the carrier of L is set
c₂ is RelStr
the carrier of c₂ is set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
the V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:]) is V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
the V7() V10( the carrier of c₂) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c₂, the carrier of L:]) is V7() V10( the carrier of c₂) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
[ the V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:]), the V7() V10( the carrier of c₂) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c₂, the carrier of L:])] is set
{ the V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:]), the V7() V10( the carrier of c₂) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c₂, the carrier of L:])} is functional set
{ the V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:])} is functional set
{{ the V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:]), the V7() V10( the carrier of c₂) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c₂, the carrier of L:])},{ the V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:])}} is set
L is RelStr
the carrier of L is set
c₂ is RelStr
the carrier of c₂ is set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is V7() V10( the carrier of L) V11( the carrier of c₂) Function-like quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is V7() V10( the carrier of c₂) V11( the carrier of L) Function-like quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
[c₃,x] is set
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
L is non empty RelStr
c₂ is non empty RelStr
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
z1 is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
z2 is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,z1,z2) is (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 is M2( the carrier of 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₃ . Ix is M2( the carrier of c₂)
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
L is non empty RelStr
the carrier of L is non empty set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
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₂ is set
{z1} is M2( bool the carrier of c₂)
uparrow {z1} is upper M2( bool the carrier of c₂)
c₃ " (uparrow z1) is M2( bool the carrier of L)
bool the carrier of L is set
c₃ . (x . z1) is M2( the carrier of c₂)
z is M2( the carrier of L)
z is M2( the carrier of L)
c₃ . z is M2( the carrier of c₂)
"/\" ((c₃ " (uparrow z1)),L) is M2( the carrier of L)
z1 is M2( the carrier of c₂)
x . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c₃ . z2 is M2( 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₃ " (uparrow z1) is M2( bool the carrier of L)
"/\" ((c₃ " (uparrow z1)),L) is M2( the carrier of L)
c₃ . ("/\" ((c₃ " (uparrow z1)),L)) is M2( the carrier of c₂)
c₃ . (x . z1) is M2( the carrier of 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₃ " (uparrow z2) is M2( bool the carrier of L)
c₃ " (uparrow z1) is M2( bool the carrier of L)
"/\" ((c₃ " (uparrow z1)),L) is M2( the carrier of L)
"/\" ((c₃ " (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
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
z1 is M2( the carrier of L)
c₃ . 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)
x " (downarrow z1) is M2( bool the carrier of c₂)
bool the carrier of c₂ is set
x . (c₃ . z1) is M2( the carrier of L)
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₂) is M2( the carrier of c₂)
z1 is M2( the carrier of c₂)
x . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c₃ . z2 is M2( the carrier of 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₂) is M2( the carrier of c₂)
x . ("\/" ((x " (downarrow z2)),c₂)) is M2( the carrier of L)
x . (c₃ . z2) is M2( the carrier of L)
z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c₃ . z1 is M2( the carrier of c₂)
c₃ . z2 is M2( the carrier of 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₂) is M2( the carrier of c₂)
"\/" ((x " (downarrow z2)),c₂) is M2( the carrier of c₂)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} 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)
c₃ .: z1 is M2( bool the carrier of c₂)
bool the carrier of c₂ is set
"/\" ((c₃ .: z1),c₂) is M2( the carrier of c₂)
c₃ . ("/\" (z1,L)) is M2( the carrier of c₂)
z is M2( the carrier of c₂)
x . z is M2( the carrier of L)
x is M2( the carrier of L)
c₃ . x is M2( the carrier of c₂)
z is M2( the carrier of c₂)
x is M2( the carrier of L)
c₃ . x is M2( the carrier of 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₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
(L,c₂,x,c₃) is (L,c₂)
{x,c₃} is functional set
{x} is functional set
{{x,c₃},{x}} is set
bool the carrier of c₂ is set
z1 is M2( bool the carrier of c₂)
"\/" (z1,c₂) is M2( the carrier of c₂)
c₃ .: z1 is M2( bool the carrier of L)
bool the carrier of L is set
"\/" ((c₃ .: z1),L) is M2( the carrier of L)
c₃ . ("\/" (z1,c₂)) is M2( the carrier of L)
z is M2( the carrier of L)
x . z is M2( the carrier of c₂)
x is M2( the carrier of c₂)
c₃ . x is M2( the carrier of L)
z is M2( the carrier of L)
x is M2( the carrier of c₂)
c₃ . x is M2( the carrier of L)
y is M2( the carrier of c₂)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of 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₂ is set
{z1} is M2( bool the carrier of c₂)
uparrow {z1} is upper M2( bool the carrier of c₂)
c₃ " (uparrow z1) is M2( bool the carrier of L)
bool the carrier of L is set
"/\" ((c₃ " (uparrow z1)),L) is M2( the carrier of L)
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
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₂ is set
{z1} is M2( bool the carrier of c₂)
uparrow {z1} is upper M2( bool the carrier of c₂)
c₃ " (uparrow z1) is M2( bool the carrier of L)
bool the carrier of L is set
"/\" ((c₃ " (uparrow z1)),L) is M2( the carrier of L)
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₃ " (uparrow z2) is M2( bool the carrier of L)
"/\" ((c₃ " (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 c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
z2 is M2( the carrier of c₂)
z1 . z2 is M2( the carrier of L)
z is M2( the carrier of L)
c₃ . z is M2( the carrier of c₂)
uparrow z2 is non empty filtered upper M2( bool the carrier of c₂)
bool the carrier of c₂ is set
{z2} is M2( bool the carrier of c₂)
uparrow {z2} is upper M2( bool the carrier of c₂)
c₃ " (uparrow z2) is M2( bool the carrier of L)
"/\" ((c₃ " (uparrow z2)),L) is M2( the carrier of L)
c₃ .: (c₃ " (uparrow z2)) is M2( bool the carrier of c₂)
c₃ . ("/\" ((c₃ " (uparrow z2)),L)) is M2( the carrier of c₂)
"/\" ((c₃ .: (c₃ " (uparrow z2))),c₂) is M2( the carrier of c₂)
"/\" ((uparrow z2),c₂) is M2( the carrier of c₂)
c₃ . (z1 . z2) is M2( the carrier of c₂)
(L,c₂,c₃,z1) is (L,c₂)
{c₃,z1} is functional set
{c₃} is functional set
{{c₃,z1},{c₃}} is set
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₂ is set
{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₃ " (uparrow z2) is M2( bool the carrier of L)
c₃ " (uparrow z) is M2( bool the carrier of L)
"/\" ((c₃ " (uparrow z2)),L) is M2( the carrier of L)
"/\" ((c₃ " (uparrow z)),L) is M2( the carrier of L)
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₂ is set
{z2} is M2( bool the carrier of c₂)
uparrow {z2} is upper M2( bool the carrier of c₂)
c₃ " (uparrow z2) is M2( bool the carrier of L)
"/\" ((c₃ " (uparrow z2)),L) is M2( the carrier of L)
c₃ .: (c₃ " (uparrow z2)) is M2( bool the carrier of c₂)
c₃ . ("/\" ((c₃ " (uparrow z2)),L)) is M2( the carrier of c₂)
"/\" ((c₃ .: (c₃ " (uparrow z2))),c₂) is M2( the carrier of c₂)
"/\" ((uparrow z2),c₂) is M2( the carrier of c₂)
c₃ . (z1 . z2) is M2( the carrier of c₂)
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, 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)
c₃ " (downarrow z1) is M2( bool the carrier of c₂)
bool the carrier of c₂ is set
"\/" ((c₃ " (downarrow z1)),c₂) is M2( the carrier of c₂)
x is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, 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₃ " (downarrow z1) is M2( bool the carrier of c₂)
bool the carrier of c₂ is set
"\/" ((c₃ " (downarrow z1)),c₂) is M2( the carrier of 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₃ " (downarrow z2) is M2( bool the carrier of c₂)
"\/" ((c₃ " (downarrow z2)),c₂) is M2( the carrier of c₂)
bool the carrier of c₂ is set
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₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
z2 is M2( the carrier of c₂)
c₃ . z2 is M2( the carrier of L)
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₃ " (downarrow z) is M2( bool the carrier of c₂)
"\/" ((c₃ " (downarrow z)),c₂) is M2( the carrier of c₂)
c₃ .: (c₃ " (downarrow z)) is M2( bool the carrier of L)
c₃ . ("\/" ((c₃ " (downarrow z)),c₂)) is M2( the carrier of L)
"\/" ((c₃ .: (c₃ " (downarrow z))),L) is M2( the carrier of L)
"\/" ((downarrow z),L) is M2( the carrier of L)
c₃ . (z1 . z) is M2( the carrier of L)
(L,c₂,z1,c₃) is (L,c₂)
{z1,c₃} is functional set
{z1} is functional set
{{z1,c₃},{z1}} is set
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₃ " (downarrow z2) is M2( bool the carrier of c₂)
c₃ " (downarrow z) is M2( bool the carrier of c₂)
"\/" ((c₃ " (downarrow z2)),c₂) is M2( the carrier of c₂)
"\/" ((c₃ " (downarrow z)),c₂) is M2( the carrier of 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₃ " (downarrow z2) is M2( bool the carrier of c₂)
"\/" ((c₃ " (downarrow z2)),c₂) is M2( the carrier of c₂)
c₃ .: (c₃ " (downarrow z2)) is M2( bool the carrier of L)
c₃ . ("\/" ((c₃ " (downarrow z2)),c₂)) is M2( the carrier of L)
"\/" ((c₃ .: (c₃ " (downarrow z2))),L) is M2( the carrier of L)
"\/" ((downarrow z2),L) is M2( the carrier of L)
c₃ . (z1 . z2) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
(L,c₂,x,c₃) is (L,c₂)
{x,c₃} is functional set
{x} is functional set
{{x,c₃},{x}} is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
(L,c₂,x,c₃) is (L,c₂)
{x,c₃} is functional set
{x} is functional set
{{x,c₃},{x}} is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, 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 c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total monotone isomorphic M2( bool [: the carrier of c₂, the carrier of c₂:])
[: the carrier of c₂, the carrier of c₂:] is V7() set
bool [: the carrier of c₂, the carrier of c₂:] is set
id the carrier of c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
x * c₃ 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:])
c₃ * x is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
z1 is M2( the carrier of L)
(x * c₃) . z1 is M2( the carrier of L)
(id L) . z1 is M2( the carrier of L)
c₃ . z1 is M2( the carrier of c₂)
x . (c₃ . z1) is M2( the carrier of L)
z1 is M2( the carrier of c₂)
(id c₂) . z1 is M2( the carrier of c₂)
(c₃ * x) . z1 is M2( the carrier of c₂)
x . z1 is M2( the carrier of L)
c₃ . (x . z1) is M2( the carrier of c₂)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, 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 c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total monotone isomorphic M2( bool [: the carrier of c₂, the carrier of c₂:])
[: the carrier of c₂, the carrier of c₂:] is V7() set
bool [: the carrier of c₂, the carrier of c₂:] is set
id the carrier of c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
x * c₃ 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:])
c₃ * x is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
z1 is M2( the carrier of c₂)
x . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c₃ . z2 is M2( the carrier of c₂)
(x * c₃) . z2 is M2( the carrier of L)
(id L) . z2 is M2( the carrier of L)
x . (c₃ . z2) is M2( the carrier of L)
(id c₂) . z1 is M2( the carrier of c₂)
(c₃ * x) . z1 is M2( the carrier of c₂)
c₃ . (x . z1) is M2( the carrier of c₂)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, 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 c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total monotone isomorphic M2( bool [: the carrier of c₂, the carrier of c₂:])
[: the carrier of c₂, the carrier of c₂:] is V7() set
bool [: the carrier of c₂, the carrier of c₂:] is set
id the carrier of c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
x * c₃ 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:])
c₃ * x is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
(x * c₃) * x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(c₃ * x) * c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
z1 is M2( the carrier of c₂)
x . z1 is M2( the carrier of L)
((x * c₃) * x) . z1 is M2( the carrier of L)
(id c₂) . z1 is M2( the carrier of c₂)
(c₃ * x) . z1 is M2( the carrier of c₂)
x . ((c₃ * x) . z1) is M2( the carrier of L)
x * (c₃ * x) is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(x * (c₃ * x)) . z1 is M2( the carrier of L)
(x * c₃) . (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)
c₃ . z1 is M2( the carrier of c₂)
((c₃ * x) * c₃) . z1 is M2( the carrier of c₂)
(x * c₃) . z1 is M2( the carrier of L)
(id L) . z1 is M2( the carrier of L)
c₃ . ((x * c₃) . z1) is M2( the carrier of c₂)
c₃ * (x * c₃) is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
(c₃ * (x * c₃)) . z1 is M2( the carrier of c₂)
(id c₂) . (c₃ . z1) is M2( the carrier of c₂)
(c₃ * x) . (c₃ . z1) is M2( the carrier of c₂)
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
c₃ * x is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
[: the carrier of c₂, the carrier of c₂:] is V7() set
bool [: the carrier of c₂, the carrier of c₂:] is set
(c₃ * x) * c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
(c₃ * x) * (c₃ * x) is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
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₂ is set
c₃ " {z1} is M2( bool the carrier of L)
bool the carrier of L is set
rng c₃ is non empty M2( bool the carrier of 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₃ " (uparrow z1) is M2( bool the carrier of L)
c₃ .: (c₃ " (uparrow z1)) is M2( bool the carrier of c₂)
"/\" ((c₃ " (uparrow z1)),L) is M2( the carrier of L)
c₃ . (x . z1) is M2( the carrier of c₂)
z2 is set
c₃ . z2 is set
z is M2( the carrier of L)
x is M2( the carrier of L)
x is M2( the carrier of L)
"/\" ((c₃ " {z1}),L) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
id c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total monotone isomorphic M2( bool [: the carrier of c₂, the carrier of c₂:])
[: the carrier of c₂, the carrier of c₂:] is V7() set
bool [: the carrier of c₂, the carrier of c₂:] is set
id the carrier of c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
c₃ * x is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
z1 is M2( the carrier of c₂)
(c₃ * x) . 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₂ is set
c₃ " {z1} is M2( bool the carrier of L)
bool the carrier of L is set
"/\" ((c₃ " {z1}),L) is M2( the carrier of L)
c₃ . (x . z1) is M2( the carrier of c₂)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
dom x is non empty M2( bool the carrier of c₂)
bool the carrier of c₂ is set
c₃ * x is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
[: the carrier of c₂, the carrier of c₂:] is V7() set
bool [: the carrier of c₂, the carrier of c₂:] is set
dom (c₃ * x) is non empty M2( bool the carrier of c₂)
x * c₃ 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 c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total monotone isomorphic M2( bool [: the carrier of c₂, the carrier of c₂:])
id the carrier of c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, 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₃ " {z1} is M2( bool the carrier of L)
bool the carrier of L is set
rng (c₃ * x) is non empty M2( bool the carrier of c₂)
(x * c₃) * x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
x * (c₃ * x) is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
z1 is M2( the carrier of L)
c₃ . z1 is M2( the carrier of 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₂ 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 c₂)
x .: (x " (downarrow z1)) is M2( bool the carrier of L)
"\/" ((x " (downarrow z1)),c₂) is M2( the carrier of c₂)
x . (c₃ . z1) is M2( the carrier of L)
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₂) is M2( the carrier of c₂)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, 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:])
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
x * c₃ 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 * c₃) . z1 is M2( the carrier of L)
c₃ . z1 is M2( the carrier of 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₂ is set
"\/" ((x " {z1}),c₂) is M2( the carrier of c₂)
x . (c₃ . z1) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
[: the carrier of c₂, the carrier of L:] is V7() set
bool [: the carrier of c₂, the carrier of L:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is non empty V7() V10( the carrier of c₂) V11( the carrier of L) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of L:])
(L,c₂,c₃,x) is (L,c₂)
{c₃,x} is functional set
{c₃} is functional set
{{c₃,x},{c₃}} is set
x * c₃ 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 c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total monotone isomorphic M2( bool [: the carrier of c₂, the carrier of c₂:])
[: the carrier of c₂, the carrier of c₂:] is V7() set
bool [: the carrier of c₂, the carrier of c₂:] is set
id the carrier of c₂ is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like one-to-one V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
c₃ * x is non empty V7() V10( the carrier of c₂) V11( the carrier of c₂) Function-like V27( the carrier of c₂) quasi_total M2( bool [: the carrier of c₂, the carrier of c₂:])
(c₃ * x) * c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
c₃ * (x * c₃) is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
dom c₃ is non empty M2( bool the carrier of L)
bool the carrier of L is set
dom (x * c₃) is non empty M2( bool the carrier of L)
rng (x * c₃) is non empty M2( bool the carrier of L)
z1 is M2( the carrier of L)
c₃ . z1 is M2( the carrier of c₂)
{z1} is M2( bool the carrier of L)
x " {z1} is M2( bool the carrier of c₂)
bool the carrier of c₂ 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
c₂ 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
c₂ is non empty RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
x is M2( the carrier of L)
c₃ . x is M2( the carrier of 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₂ 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
c₂ 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 c₂ is non empty M2( bool the carrier of L)
bool the carrier of L is set
c₃ is set
c₂ . c₃ is set
dom c₂ is non empty M2( bool the carrier of L)
x is set
c₂ . 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
c₂ 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 c₂ is non empty M2( bool the carrier of L)
c₃ is M2( bool the carrier of L)
"/\" (c₃,L) is M2( the carrier of L)
c₂ . ("/\" (c₃,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)
c₂ . x is M2( the carrier of L)
(id L) . ("/\" (c₃,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
c₂ 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 c₂ is non empty M2( bool the carrier of L)
c₃ is M2( bool the carrier of L)
"\/" (c₃,L) is M2( the carrier of L)
c₂ . ("\/" (c₃,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)
c₂ . x is M2( the carrier of L)
(id L) . ("\/" (c₃,L)) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
Image c₃ is non empty strict full SubRelStr of c₂
rng c₃ is non empty M2( bool the carrier of c₂)
bool the carrier of c₂ is set
subrelstr (rng c₃) is non empty strict full SubRelStr of c₂
the carrier of (Image c₃) is non empty set
the carrier of (Image c₃) |` c<sub>3</sub> is V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) V11( the carrier of (Image c<sub>3</sub>)) V11( the carrier of c<sub>2</sub>) Function-like M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
[: the carrier of L, the carrier of (Image c<sub>3</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>3</sub>):] is set
dom c<sub>3</sub> 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
c<sub>2</sub> is non empty RelStr
the carrier of c<sub>2</sub> is non empty set
[: the carrier of L, the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>2</sub>:] is set
c<sub>3</sub> is non empty V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
Image c<sub>3</sub> is non empty strict full SubRelStr of c<sub>2</sub>
rng c<sub>3</sub> is non empty M2( bool the carrier of c<sub>2</sub>)
bool the carrier of c<sub>2</sub> is set
subrelstr (rng c<sub>3</sub>) is non empty strict full SubRelStr of c<sub>2</sub>
the carrier of (Image c<sub>3</sub>) is non empty set
(L,c<sub>2</sub>,c<sub>3</sub>) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c<sub>3</sub>)) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of (Image c<sub>3</sub>):])
[: the carrier of L, the carrier of (Image c<sub>3</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>3</sub>):] is set
the carrier of (Image c<sub>3</sub>) |` c₃ is V7() V10( the carrier of L) V11( the carrier of c₂) V11( the carrier of (Image c₃)) V11( the carrier of c₂) Function-like M2( bool [: the carrier of L, the carrier of c₂:])
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
Image c₃ is non empty strict full SubRelStr of c₂
rng c₃ is non empty M2( bool the carrier of c₂)
bool the carrier of c₂ is set
subrelstr (rng c₃) is non empty strict full SubRelStr of c₂
the carrier of (Image c₃) is non empty set
(L,c₂,c₃) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c₃)) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of (Image c₃):])
[: the carrier of L, the carrier of (Image c₃):] is V7() set
bool [: the carrier of L, the carrier of (Image c₃):] is set
the carrier of (Image c₃) |` c<sub>3</sub> is V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) V11( the carrier of (Image c<sub>3</sub>)) V11( the carrier of c<sub>2</sub>) Function-like M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
rng (L,c<sub>2</sub>,c<sub>3</sub>) is non empty M2( bool the carrier of (Image c<sub>3</sub>))
bool the carrier of (Image c<sub>3</sub>) is set
L is non empty RelStr
the carrier of L is non empty set
c<sub>2</sub> is non empty RelStr
the carrier of c<sub>2</sub> is non empty set
[: the carrier of L, the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>2</sub>:] is set
c<sub>3</sub> is non empty V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
Image c<sub>3</sub> is non empty strict full SubRelStr of c<sub>2</sub>
rng c<sub>3</sub> is non empty M2( bool the carrier of c<sub>2</sub>)
bool the carrier of c<sub>2</sub> is set
subrelstr (rng c<sub>3</sub>) is non empty strict full SubRelStr of c<sub>2</sub>
the carrier of (Image c<sub>3</sub>) is non empty set
(L,c<sub>2</sub>,c<sub>3</sub>) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c<sub>3</sub>)) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of (Image c<sub>3</sub>):])
[: the carrier of L, the carrier of (Image c<sub>3</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>3</sub>):] is set
the carrier of (Image c<sub>3</sub>) |` c₃ is V7() V10( the carrier of L) V11( the carrier of c₂) V11( the carrier of (Image c₃)) V11( the carrier of c₂) Function-like M2( bool [: the carrier of L, the carrier of c₂:])
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
[: the carrier of L, the carrier of c₂:] is V7() set
bool [: the carrier of L, the carrier of c₂:] is set
c₃ is non empty V7() V10( the carrier of L) V11( the carrier of c₂) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₂:])
Image c₃ is non empty strict full SubRelStr of c₂
rng c₃ is non empty M2( bool the carrier of c₂)
bool the carrier of c₂ is set
subrelstr (rng c₃) is non empty strict full SubRelStr of c₂
(L,c₂,c₃) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c₃)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c₃):])
the carrier of (Image c₃) is non empty set
[: the carrier of L, the carrier of (Image c₃):] is V7() set
bool [: the carrier of L, the carrier of (Image c₃):] is set
the carrier of (Image c₃) |` c<sub>3</sub> is V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) V11( the carrier of (Image c<sub>3</sub>)) V11( the carrier of c<sub>2</sub>) Function-like M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
x is M2( the carrier of L)
z1 is M2( the carrier of L)
(L,c<sub>2</sub>,c<sub>3</sub>) . x is M2( the carrier of (Image c<sub>3</sub>))
(L,c<sub>2</sub>,c<sub>3</sub>) . z1 is M2( the carrier of (Image c<sub>3</sub>))
c<sub>3</sub> . x is M2( the carrier of c<sub>2</sub>)
c<sub>3</sub> . z1 is M2( the carrier of c<sub>2</sub>)
z2 is M2( the carrier of c<sub>2</sub>)
z is M2( the carrier of c<sub>2</sub>)
L is non empty RelStr
the carrier of L is non empty set
c<sub>2</sub> is non empty RelStr
the carrier of c<sub>2</sub> is non empty set
[: the carrier of L, the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>2</sub>:] is set
c<sub>3</sub> is non empty V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
Image c<sub>3</sub> is non empty strict full SubRelStr of c<sub>2</sub>
rng c<sub>3</sub> is non empty M2( bool the carrier of c<sub>2</sub>)
bool the carrier of c<sub>2</sub> is set
subrelstr (rng c<sub>3</sub>) is non empty strict full SubRelStr of c<sub>2</sub>
id (Image c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of (Image c<sub>3</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>3</sub>)) quasi_total monotone isomorphic ( Image c<sub>3</sub>) M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):])
the carrier of (Image c<sub>3</sub>) is non empty set
[: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):] is V7() set
bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):] is set
id the carrier of (Image c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of (Image c<sub>3</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>3</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):])
[: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:] is set
rng (id (Image c<sub>3</sub>)) is non empty M2( bool the carrier of (Image c<sub>3</sub>))
bool the carrier of (Image c<sub>3</sub>) is set
dom (id (Image c<sub>3</sub>)) is non empty M2( bool the carrier of (Image c<sub>3</sub>))
L is non empty RelStr
the carrier of L is non empty set
c<sub>2</sub> is non empty RelStr
the carrier of c<sub>2</sub> is non empty set
[: the carrier of L, the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>2</sub>:] is set
c<sub>3</sub> is non empty V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
Image c<sub>3</sub> is non empty strict full SubRelStr of c<sub>2</sub>
rng c<sub>3</sub> is non empty M2( bool the carrier of c<sub>2</sub>)
bool the carrier of c<sub>2</sub> is set
subrelstr (rng c<sub>3</sub>) is non empty strict full SubRelStr of c<sub>2</sub>
(L,c<sub>2</sub>,c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of c<sub>2</sub>) Function-like V27( the carrier of (Image c<sub>3</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:])
the carrier of (Image c<sub>3</sub>) is non empty set
[: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:] is set
id (Image c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of (Image c<sub>3</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>3</sub>)) quasi_total monotone isomorphic ( Image c<sub>3</sub>) M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):])
[: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):] is V7() set
bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):] is set
id the carrier of (Image c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of (Image c<sub>3</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>3</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):])
x is M2( the carrier of (Image c<sub>3</sub>))
z1 is M2( the carrier of (Image c<sub>3</sub>))
(L,c<sub>2</sub>,c<sub>3</sub>) . x is M2( the carrier of c<sub>2</sub>)
(L,c<sub>2</sub>,c<sub>3</sub>) . z1 is M2( the carrier of c<sub>2</sub>)
(id (Image c<sub>3</sub>)) . x is M2( the carrier of (Image c<sub>3</sub>))
(id (Image c<sub>3</sub>)) . z1 is M2( the carrier of (Image c<sub>3</sub>))
L is non empty RelStr
the carrier of L is non empty set
c<sub>2</sub> is non empty RelStr
the carrier of c<sub>2</sub> is non empty set
[: the carrier of L, the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>2</sub>:] is set
c<sub>3</sub> is non empty V7() V10( the carrier of L) V11( the carrier of c<sub>2</sub>) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c<sub>2</sub>:])
(L,c<sub>2</sub>,c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of c<sub>2</sub>) Function-like V27( the carrier of (Image c<sub>3</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:])
Image c<sub>3</sub> is non empty strict full SubRelStr of c<sub>2</sub>
rng c<sub>3</sub> is non empty M2( bool the carrier of c<sub>2</sub>)
bool the carrier of c<sub>2</sub> is set
subrelstr (rng c<sub>3</sub>) is non empty strict full SubRelStr of c<sub>2</sub>
the carrier of (Image c<sub>3</sub>) is non empty set
[: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:] is V7() set
bool [: the carrier of (Image c<sub>3</sub>), the carrier of c<sub>2</sub>:] is set
id (Image c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of (Image c<sub>3</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>3</sub>)) quasi_total monotone isomorphic ( Image c<sub>3</sub>) M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):])
[: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):] is V7() set
bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):] is set
id the carrier of (Image c<sub>3</sub>) is non empty V7() V10( the carrier of (Image c<sub>3</sub>)) V11( the carrier of (Image c<sub>3</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>3</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>3</sub>), the carrier of (Image c<sub>3</sub>):])
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<sub>2</sub> 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:])
Image c<sub>2</sub> is non empty strict full SubRelStr of L
rng c<sub>2</sub> is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c<sub>2</sub>) is non empty strict full SubRelStr of L
the carrier of (Image c<sub>2</sub>) is non empty set
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):])
[: the carrier of L, the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):] is set
the carrier of (Image c<sub>2</sub>) |` c₂ is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c₂)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
(L,L,c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone M2( bool [: the carrier of (Image c₂), the carrier of L:])
[: the carrier of (Image c₂), the carrier of L:] is V7() set
bool [: the carrier of (Image c₂), the carrier of L:] is set
id (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone isomorphic ( Image c₂) M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
[: the carrier of (Image c₂), the carrier of (Image c₂):] is V7() set
bool [: the carrier of (Image c₂), the carrier of (Image c₂):] is set
id the carrier of (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
(L,L,c₂) * (L,L,c₂) 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:])
(id the carrier of (Image c₂)) * c₂ is V7() V10( the carrier of L) V11( the carrier of (Image c₂)) Function-like M2( bool [: the carrier of L, the carrier of (Image c₂):])
id (rng c₂) is non empty V7() V10( rng c₂) V11( rng c₂) Function-like one-to-one V27( rng c₂) quasi_total M2( bool [:(rng c₂),(rng c₂):])
[:(rng c₂),(rng c₂):] is V7() set
bool [:(rng c₂),(rng c₂):] is set
(id (rng c₂)) * c₂ is V7() V10( the carrier of L) V11( rng c₂) Function-like M2( bool [: the carrier of L,(rng c₂):])
[: the carrier of L,(rng c₂):] is V7() set
bool [: the carrier of L,(rng c₂):] 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
c₂ 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:])
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (Image c₂) is non empty set
(L,L,c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone M2( bool [: the carrier of (Image c₂), the carrier of L:])
[: the carrier of (Image c₂), the carrier of L:] is V7() set
bool [: the carrier of (Image c₂), the carrier of L:] is set
id (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone isomorphic ( Image c₂) ( Image c₂) ( Image c₂) M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
[: the carrier of (Image c₂), the carrier of (Image c₂):] is V7() set
bool [: the carrier of (Image c₂), the carrier of (Image c₂):] is set
id the carrier of (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
(L,L,c₂) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c₂)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c₂):])
[: the carrier of L, the carrier of (Image c₂):] is V7() set
bool [: the carrier of L, the carrier of (Image c₂):] is set
the carrier of (Image c₂) |` c<sub>2</sub> is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
(L,L,c<sub>2</sub>) * (L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of (Image c<sub>2</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
c<sub>3</sub> is M2( the carrier of (Image c<sub>2</sub>))
((L,L,c<sub>2</sub>) * (L,L,c<sub>2</sub>)) . c<sub>3</sub> is M2( the carrier of (Image c<sub>2</sub>))
rng (L,L,c<sub>2</sub>) is non empty M2( bool the carrier of (Image c<sub>2</sub>))
bool the carrier of (Image c<sub>2</sub>) is set
x is set
(L,L,c<sub>2</sub>) . x is set
z1 is M2( the carrier of L)
(L,L,c<sub>2</sub>) . z1 is M2( the carrier of (Image c<sub>2</sub>))
c<sub>2</sub> . z1 is M2( the carrier of L)
(L,L,c<sub>2</sub>) . c<sub>3</sub> is M2( the carrier of L)
(L,L,c<sub>2</sub>) . ((L,L,c<sub>2</sub>) . c<sub>3</sub>) is M2( the carrier of (Image c<sub>2</sub>))
(L,L,c<sub>2</sub>) . c<sub>3</sub> is set
c<sub>2</sub> . (c<sub>2</sub> . z1) 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
c<sub>2</sub> 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:])
Image c<sub>2</sub> is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c<sub>2</sub> is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c<sub>2</sub>) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
c<sub>3</sub> is non empty reflexive transitive antisymmetric RelStr
the carrier of c<sub>3</sub> is non empty set
[: the carrier of L, the carrier of c<sub>3</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>3</sub>:] is set
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):])
the carrier of (Image c<sub>2</sub>) is non empty set
[: the carrier of L, the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):] is set
the carrier of (Image c<sub>2</sub>) |` c₂ is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c₂)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
[: the carrier of c₃, the carrier of L:] is V7() set
bool [: the carrier of c₃, the carrier of L:] is set
(L,L,c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone M2( bool [: the carrier of (Image c₂), the carrier of L:])
[: the carrier of (Image c₂), the carrier of L:] is V7() set
bool [: the carrier of (Image c₂), the carrier of L:] is set
id (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone isomorphic ( Image c₂) ( Image c₂) ( Image c₂) M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
[: the carrier of (Image c₂), the carrier of (Image c₂):] is V7() set
bool [: the carrier of (Image c₂), the carrier of (Image c₂):] is set
id the carrier of (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
id c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total monotone isomorphic (c₃) (c₃) (c₃) M2( bool [: the carrier of c₃, the carrier of c₃:])
[: the carrier of c₃, the carrier of c₃:] is V7() set
bool [: the carrier of c₃, the carrier of c₃:] is set
id the carrier of c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of c₃:])
x is non empty V7() V10( the carrier of L) V11( the carrier of c₃) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of L:])
z1 * x 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:])
x * z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of 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
c₂ 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:])
c₃ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₃ is non empty set
[: the carrier of L, the carrier of c₃:] is V7() set
bool [: the carrier of L, the carrier of c₃:] is set
[: the carrier of c₃, the carrier of L:] is V7() set
bool [: the carrier of c₃, the carrier of L:] is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c₃) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of L:])
z1 * x 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:])
id c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total monotone isomorphic (c₃) (c₃) (c₃) M2( bool [: the carrier of c₃, the carrier of c₃:])
[: the carrier of c₃, the carrier of c₃:] is V7() set
bool [: the carrier of c₃, the carrier of c₃:] is set
id the carrier of c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of c₃:])
x * z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of c₃:])
(z1 * x) * z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of L:])
z1 * (id the carrier of c₃) is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, 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
c₂ 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:])
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
(L,L,c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone M2( bool [: the carrier of (Image c₂), the carrier of L:])
the carrier of (Image c₂) is non empty set
[: the carrier of (Image c₂), the carrier of L:] is V7() set
bool [: the carrier of (Image c₂), the carrier of L:] is set
id (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone isomorphic ( Image c₂) ( Image c₂) ( Image c₂) M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
[: the carrier of (Image c₂), the carrier of (Image c₂):] is V7() set
bool [: the carrier of (Image c₂), the carrier of (Image c₂):] is set
id the carrier of (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
(L,L,c₂) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c₂)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c₂):])
[: the carrier of L, the carrier of (Image c₂):] is V7() set
bool [: the carrier of L, the carrier of (Image c₂):] is set
the carrier of (Image c₂) |` c<sub>2</sub> is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
((Image c<sub>2</sub>),L,(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)) is ( Image c<sub>2</sub>,L)
{(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)} is functional set
{(L,L,c<sub>2</sub>)} is functional set
{{(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)},{(L,L,c<sub>2</sub>)}} 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) (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,L,c<sub>2</sub>) * (L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of (Image c<sub>2</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
(L,L,c<sub>2</sub>) * (L,L,c<sub>2</sub>) 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 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
c<sub>2</sub> 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:])
Image c<sub>2</sub> is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c<sub>2</sub> is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c<sub>2</sub>) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
c<sub>3</sub> is non empty reflexive transitive antisymmetric RelStr
the carrier of c<sub>3</sub> is non empty set
[: the carrier of c<sub>3</sub>, the carrier of L:] is V7() set
bool [: the carrier of c<sub>3</sub>, the carrier of L:] is set
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total monotone M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of L:])
the carrier of (Image c<sub>2</sub>) is non empty set
[: the carrier of (Image c<sub>2</sub>), the carrier of L:] is V7() set
bool [: the carrier of (Image c<sub>2</sub>), the carrier of L:] is set
id (Image c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total monotone isomorphic ( Image c<sub>2</sub>) ( Image c<sub>2</sub>) ( Image c<sub>2</sub>) M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
[: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):] is set
id the carrier of (Image c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
[: the carrier of L, the carrier of c<sub>3</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>3</sub>:] is set
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):])
[: the carrier of L, the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):] is set
the carrier of (Image c<sub>2</sub>) |` c₂ is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c₂)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
x is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of L:])
z1 is non empty V7() V10( the carrier of L) V11( the carrier of c₃) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
(c₃,L,x,z1) is (c₃,L)
{x,z1} is functional set
{x} is functional set
{{x,z1},{x}} is set
x * z1 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 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
c₂ 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:])
c₃ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₃ is non empty set
[: the carrier of c₃, the carrier of L:] is V7() set
bool [: the carrier of c₃, the carrier of L:] is set
[: the carrier of L, the carrier of c₃:] is V7() set
bool [: the carrier of L, the carrier of c₃:] is set
x is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of L:])
z1 is non empty V7() V10( the carrier of L) V11( the carrier of c₃) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
(c₃,L,x,z1) is (c₃,L)
{x,z1} is functional set
{x} is functional set
{{x,z1},{x}} is set
x * z1 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 * x is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of c₃:])
[: the carrier of c₃, the carrier of c₃:] is V7() set
bool [: the carrier of c₃, the carrier of c₃:] is set
id c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total monotone isomorphic (c₃) (c₃) (c₃) M2( bool [: the carrier of c₃, the carrier of c₃:])
id the carrier of c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, 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 (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 * z1) * x is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, 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
c₂ 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:])
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
(L,L,c₂) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c₂)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c₂):])
the carrier of (Image c₂) is non empty set
[: the carrier of L, the carrier of (Image c₂):] is V7() set
bool [: the carrier of L, the carrier of (Image c₂):] is set
the carrier of (Image c₂) |` c<sub>2</sub> is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total monotone M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of L:])
[: the carrier of (Image c<sub>2</sub>), the carrier of L:] is V7() set
bool [: the carrier of (Image c<sub>2</sub>), the carrier of L:] is set
id (Image c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total monotone isomorphic ( Image c<sub>2</sub>) ( Image c<sub>2</sub>) ( Image c<sub>2</sub>) M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
[: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):] is set
id the carrier of (Image c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
(L,(Image c<sub>2</sub>),(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)) is (L, Image c<sub>2</sub>)
{(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)} is functional set
{(L,L,c<sub>2</sub>)} is functional set
{{(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)},{(L,L,c<sub>2</sub>)}} 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) (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,L,c<sub>2</sub>) * (L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of (Image c<sub>2</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
(L,L,c<sub>2</sub>) * (L,L,c<sub>2</sub>) 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 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
c<sub>2</sub> 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:])
Image c<sub>2</sub> is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c<sub>2</sub> is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c<sub>2</sub>) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
c<sub>3</sub> is non empty reflexive transitive antisymmetric RelStr
the carrier of c<sub>3</sub> is non empty set
[: the carrier of L, the carrier of c<sub>3</sub>:] is V7() set
bool [: the carrier of L, the carrier of c<sub>3</sub>:] is set
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):])
the carrier of (Image c<sub>2</sub>) is non empty set
[: the carrier of L, the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):] is set
the carrier of (Image c<sub>2</sub>) |` c₂ is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c₂)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
[: the carrier of c₃, the carrier of L:] is V7() set
bool [: the carrier of c₃, the carrier of L:] is set
(L,L,c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone M2( bool [: the carrier of (Image c₂), the carrier of L:])
[: the carrier of (Image c₂), the carrier of L:] is V7() set
bool [: the carrier of (Image c₂), the carrier of L:] is set
id (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone isomorphic ( Image c₂) ( Image c₂) ( Image c₂) M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
[: the carrier of (Image c₂), the carrier of (Image c₂):] is V7() set
bool [: the carrier of (Image c₂), the carrier of (Image c₂):] is set
id the carrier of (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
x is non empty V7() V10( the carrier of L) V11( the carrier of c₃) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of L:])
(L,c₃,x,z1) is (L,c₃)
{x,z1} is functional set
{x} is functional set
{{x,z1},{x}} is set
z1 * x 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 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
c₂ 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:])
c₃ is non empty reflexive transitive antisymmetric RelStr
the carrier of c₃ is non empty set
[: the carrier of L, the carrier of c₃:] is V7() set
bool [: the carrier of L, the carrier of c₃:] is set
[: the carrier of c₃, the carrier of L:] is V7() set
bool [: the carrier of c₃, the carrier of L:] is set
x is non empty V7() V10( the carrier of L) V11( the carrier of c₃) Function-like V27( the carrier of L) quasi_total M2( bool [: the carrier of L, the carrier of c₃:])
z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of L:])
(L,c₃,x,z1) is (L,c₃)
{x,z1} is functional set
{x} is functional set
{{x,z1},{x}} is set
z1 * x 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:])
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:])
id c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total monotone isomorphic (c₃) (c₃) (c₃) M2( bool [: the carrier of c₃, the carrier of c₃:])
[: the carrier of c₃, the carrier of c₃:] is V7() set
bool [: the carrier of c₃, the carrier of c₃:] is set
id the carrier of c₃ is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like one-to-one V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of c₃:])
x * z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of c₃) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, the carrier of c₃:])
(z1 * x) * z1 is non empty V7() V10( the carrier of c₃) V11( the carrier of L) Function-like V27( the carrier of c₃) quasi_total M2( bool [: the carrier of c₃, 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
c₂ 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 c₂ is non empty M2( bool the carrier of L)
bool the carrier of L is set
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } /\ { b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
z1 is set
dom c₂ is non empty M2( bool the carrier of L)
z2 is M2( the carrier of L)
c₂ . z2 is M2( the carrier of L)
z is set
c₂ . z is set
z is set
c₂ . z is set
z1 is set
dom c₂ is non empty M2( bool the carrier of L)
c₂ . z1 is set
z2 is M2( the carrier of L)
c₂ . z2 is M2( the carrier of L)
z is M2( the carrier of L)
c₂ . z is M2( the carrier of L)
z2 is M2( the carrier of L)
c₂ . z2 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
{ b₁ where b₁ is M2( the carrier of L) : S₂[b₁] } is set
{ b₁ where b₁ is M2( the carrier of L) : S₁[b₁] } is set
rng c₂ is non empty M2( bool the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : S₂[b₁] } /\ { b₁ where b₁ is M2( the carrier of L) : S₁[b₁] } 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
c₂ | { b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is V7() V10( the carrier of L) V10( { b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } ) V10( the carrier of L) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
rng (c₂ | { b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } ) is M2( bool the carrier of L)
bool the carrier of L is set
rng c₂ is non empty M2( bool the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
c₂ | { b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is V7() V10( the carrier of L) V10( { b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } ) V10( the carrier of L) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
rng (c₂ | { b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } ) is M2( bool the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } /\ { b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
dom c₂ is non empty M2( bool the carrier of L)
z1 is set
c₂ . z1 is set
z2 is M2( the carrier of L)
c₂ . z2 is M2( the carrier of L)
z is M2( the carrier of L)
c₂ . z is M2( the carrier of L)
z2 is M2( the carrier of L)
c₂ . z2 is M2( the carrier of L)
z1 is set
c₂ . z1 is set
z2 is M2( the carrier of L)
c₂ . z2 is M2( the carrier of L)
z is M2( the carrier of L)
c₂ . z is M2( the carrier of L)
z2 is M2( the carrier of L)
c₂ . z2 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
c₃ is non empty M2( bool the carrier of L)
c₂ | c₃ is V7() V10( the carrier of L) V10(c₃) V10( the carrier of L) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
subrelstr c₃ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₃) is non empty set
[: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is V7() set
bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is set
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
rng c₂ is non empty M2( bool the carrier of L)
c₃ /\ { b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
rng (c₂ | c₃) is M2( bool the carrier of L)
[:c₃, the carrier of L:] is V7() set
bool [:c₃, the carrier of L:] 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
x is non empty M2( bool the carrier of L)
c₂ | x is V7() V10( the carrier of L) V10(x) V10( the carrier of L) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
subrelstr x is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr x) is non empty set
[: the carrier of (subrelstr x), the carrier of (subrelstr x):] is V7() set
bool [: the carrier of (subrelstr x), the carrier of (subrelstr x):] is set
rng c₂ is non empty M2( bool the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } /\ x is set
rng (c₂ | x) is M2( bool the carrier of L)
[:x, the carrier of L:] is V7() set
bool [:x, the carrier of L:] 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
c₃ is non empty M2( bool the carrier of L)
subrelstr c₃ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₃) is non empty set
[: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is V7() set
bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is set
c₂ | c₃ is V7() V10( the carrier of L) V10(c₃) V10( the carrier of L) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
x is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like V27( the carrier of (subrelstr c₃)) quasi_total M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
dom x is non empty M2( bool the carrier of (subrelstr c₃))
bool the carrier of (subrelstr c₃) is set
z1 is M2( the carrier of (subrelstr c₃))
x . z1 is M2( the carrier of (subrelstr c₃))
c₂ . z1 is set
c₂ . (c₂ . z1) is set
x . (x . z1) is M2( the carrier of (subrelstr c₃))
x * x is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like V27( the carrier of (subrelstr c₃)) quasi_total M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
(x * x) . z1 is M2( the carrier of (subrelstr c₃))
z1 is M2( the carrier of (subrelstr c₃))
z2 is M2( the carrier of (subrelstr c₃))
x . z1 is M2( the carrier of (subrelstr c₃))
x . z2 is M2( the carrier of (subrelstr c₃))
z is M2( the carrier of L)
x is M2( the carrier of L)
c₂ . z is M2( the carrier of L)
c₂ . x is M2( the carrier of L)
id (subrelstr c₃) is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like one-to-one V27( the carrier of (subrelstr c₃)) quasi_total monotone isomorphic ( subrelstr c₃) ( subrelstr c₃) ( subrelstr c₃) M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
id the carrier of (subrelstr c₃) is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like one-to-one V27( the carrier of (subrelstr c₃)) quasi_total M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
z1 is M2( the carrier of (subrelstr c₃))
x . z1 is M2( the carrier of (subrelstr c₃))
z2 is M2( the carrier of L)
c₂ . z2 is M2( the carrier of L)
z is M2( the carrier of L)
c₂ . z is M2( the carrier of L)
(id (subrelstr c₃)) . z1 is M2( the carrier of (subrelstr 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₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
c₃ is non empty M2( bool the carrier of L)
subrelstr c₃ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₃) is non empty set
[: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is V7() set
bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is set
c₂ | c₃ is V7() V10( the carrier of L) V10(c₃) V10( the carrier of L) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
x is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like V27( the carrier of (subrelstr c₃)) quasi_total M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
dom x is non empty M2( bool the carrier of (subrelstr c₃))
bool the carrier of (subrelstr c₃) is set
z1 is M2( the carrier of (subrelstr c₃))
x . z1 is M2( the carrier of (subrelstr c₃))
c₂ . z1 is set
c₂ . (c₂ . z1) is set
x . (x . z1) is M2( the carrier of (subrelstr c₃))
x * x is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like V27( the carrier of (subrelstr c₃)) quasi_total M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
(x * x) . z1 is M2( the carrier of (subrelstr c₃))
z1 is M2( the carrier of (subrelstr c₃))
z2 is M2( the carrier of (subrelstr c₃))
x . z1 is M2( the carrier of (subrelstr c₃))
x . z2 is M2( the carrier of (subrelstr c₃))
z is M2( the carrier of L)
x is M2( the carrier of L)
c₂ . z is M2( the carrier of L)
c₂ . x is M2( the carrier of L)
id (subrelstr c₃) is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like one-to-one V27( the carrier of (subrelstr c₃)) quasi_total monotone isomorphic ( subrelstr c₃) ( subrelstr c₃) ( subrelstr c₃) M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
id the carrier of (subrelstr c₃) is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like one-to-one V27( the carrier of (subrelstr c₃)) quasi_total M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
z1 is M2( the carrier of (subrelstr c₃))
x . z1 is M2( the carrier of (subrelstr c₃))
z2 is M2( the carrier of L)
c₂ . z2 is M2( the carrier of L)
z is M2( the carrier of L)
c₂ . z is M2( the carrier of L)
(id (subrelstr c₃)) . z1 is M2( the carrier of (subrelstr 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₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
c₃ is M2( bool the carrier of L)
subrelstr c₃ is strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₃) is set
bool the carrier of (subrelstr c₃) is set
x is M2( bool the carrier of (subrelstr c₃))
"\/" (x,L) is M2( the carrier of L)
c₂ . ("\/" (x,L)) is M2( the carrier of L)
z1 is M2( the carrier of L)
c₂ . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c₂ . z2 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
c₃ is M2( bool the carrier of L)
subrelstr c₃ is strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₃) is set
bool the carrier of (subrelstr c₃) is set
x is M2( bool the carrier of (subrelstr c₃))
"/\" (x,L) is M2( the carrier of L)
c₂ . ("/\" (x,L)) is M2( the carrier of L)
z1 is M2( the carrier of L)
c₂ . z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c₂ . z2 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
x is non empty M2( bool the carrier of L)
subrelstr x is non empty strict reflexive transitive antisymmetric full SubRelStr of L
c₃ is non empty M2( bool the carrier of L)
subrelstr c₃ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr x) is non empty set
the carrier of (Image c₂) is non empty set
x /\ c₃ is set
the carrier of (subrelstr c₃) is non empty set
bool the carrier of (subrelstr x) is set
z1 is M2( bool the carrier of (subrelstr x))
"/\" (z1,L) is M2( the carrier of L)
z2 is M2( bool the carrier of L)
c₂ .: z2 is M2( bool the carrier of L)
"/\" (z2,L) is M2( the carrier of L)
z is M2( the carrier of L)
x is M2( the carrier of L)
c₂ . x is M2( the carrier of L)
y is M2( the carrier of L)
Ix is M2( the carrier of L)
c₂ . Ix is M2( the carrier of L)
c₂ .: z1 is M2( bool the carrier of L)
"/\" ((c₂ .: z2),L) is M2( the carrier of L)
c₂ . ("/\" (z2,L)) is M2( the carrier of L)
bool the carrier of (Image c₂) is set
z1 is M2( bool the carrier of (Image c₂))
"/\" (z1,L) is M2( the carrier of L)
bool the carrier of (subrelstr x) is set
z1 is filtered M2( bool the carrier of (subrelstr x))
"/\" (z1,L) is M2( the carrier of L)
z2 is non empty filtered M2( bool the carrier of L)
c₂ .: z2 is M2( bool the carrier of L)
"/\" (z2,L) is M2( the carrier of L)
z is M2( the carrier of L)
x is M2( the carrier of L)
c₂ . x is M2( the carrier of L)
y is M2( the carrier of L)
Ix is M2( the carrier of L)
c₂ . Ix is M2( the carrier of L)
c₂ .: z1 is M2( bool the carrier of L)
"/\" ((c₂ .: z2),L) is M2( the carrier of L)
c₂ . ("/\" (z2,L)) is M2( the carrier of L)
bool the carrier of (Image c₂) is set
z1 is filtered M2( bool the carrier of (Image c₂))
"/\" (z1,L) is M2( the carrier of L)
bool the carrier of (subrelstr 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
c₂ 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:])
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
x is non empty M2( bool the carrier of L)
subrelstr x is non empty strict reflexive transitive antisymmetric full SubRelStr of L
c₃ is non empty M2( bool the carrier of L)
subrelstr c₃ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₃) is non empty set
the carrier of (Image c₂) is non empty set
c₃ /\ x is set
the carrier of (subrelstr x) is non empty set
bool the carrier of (subrelstr x) is set
z1 is M2( bool the carrier of (subrelstr x))
"\/" (z1,L) is M2( the carrier of L)
z2 is M2( bool the carrier of L)
c₂ .: z2 is M2( bool the carrier of L)
"\/" (z2,L) is M2( the carrier of L)
z is M2( the carrier of L)
x is M2( the carrier of L)
c₂ . x is M2( the carrier of L)
y is M2( the carrier of L)
Ix is M2( the carrier of L)
c₂ . Ix is M2( the carrier of L)
c₂ .: z1 is M2( bool the carrier of L)
"\/" ((c₂ .: z2),L) is M2( the carrier of L)
c₂ . ("\/" (z2,L)) is M2( the carrier of L)
bool the carrier of (Image c₂) is set
z1 is M2( bool the carrier of (Image c₂))
"\/" (z1,L) is M2( the carrier of L)
bool the carrier of (subrelstr x) is set
z1 is directed M2( bool the carrier of (subrelstr x))
"\/" (z1,L) is M2( the carrier of L)
z2 is non empty directed M2( bool the carrier of L)
c₂ .: z2 is M2( bool the carrier of L)
"\/" (z2,L) is M2( the carrier of L)
z is M2( the carrier of L)
x is M2( the carrier of L)
c₂ . x is M2( the carrier of L)
y is M2( the carrier of L)
Ix is M2( the carrier of L)
c₂ . Ix is M2( the carrier of L)
c₂ .: z1 is M2( bool the carrier of L)
"\/" ((c₂ .: z2),L) is M2( the carrier of L)
c₂ . ("\/" (z2,L)) is M2( the carrier of L)
bool the carrier of (Image c₂) is set
z1 is directed M2( bool the carrier of (Image c₂))
"\/" (z1,L) is M2( the carrier of L)
bool the carrier of (subrelstr 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
c₂ 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:])
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (Image c₂) is non empty set
bool the carrier of (Image c₂) is set
c₃ is M2( bool the carrier of (Image c₂))
"/\" (c₃,L) is M2( the carrier of L)
x is M2( bool the carrier of L)
"/\" (x,L) is M2( the carrier of L)
c₂ . ("/\" (x,L)) is M2( the carrier of L)
the carrier of (Image c₂) is non empty set
bool the carrier of (Image c₂) is set
c₃ is M2( bool the carrier of (Image c₂))
"\/" (c₃,L) is M2( the carrier of L)
x is M2( bool the carrier of L)
"\/" (x,L) is M2( the carrier of L)
c₂ . ("\/" (x,L)) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete 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₂ 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:])
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
bool the carrier of L is set
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (Image c₂) is non empty set
{ b₁ where b₁ is M2( the carrier of L) : b₁ <= c₂ . b₁ } is set
{ b₁ where b₁ is M2( the carrier of L) : c₂ . b₁ <= b₁ } is set
c₃ is non empty M2( bool the carrier of L)
subrelstr c₃ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₃) is non empty set
x is non empty M2( bool the carrier of L)
c₃ /\ x is set
[: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is V7() set
bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):] is set
c₂ | c₃ is V7() V10( the carrier of L) V10(c₃) V10( the carrier of L) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
z1 is non empty V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) Function-like V27( the carrier of (subrelstr c₃)) quasi_total M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
Image z1 is non empty strict reflexive transitive antisymmetric full SubRelStr of subrelstr c₃
rng z1 is non empty M2( bool the carrier of (subrelstr c₃))
bool the carrier of (subrelstr c₃) is set
subrelstr (rng z1) is non empty strict reflexive transitive antisymmetric full SubRelStr of subrelstr c₃
the carrier of (Image z1) is non empty set
the InternalRel of (Image z1) is V7() V10( the carrier of (Image z1)) V11( the carrier of (Image z1)) M2( bool [: the carrier of (Image z1), the carrier of (Image z1):])
[: the carrier of (Image z1), the carrier of (Image z1):] is V7() set
bool [: the carrier of (Image z1), the carrier of (Image z1):] is set
the InternalRel of (subrelstr c₃) is V7() V10( the carrier of (subrelstr c₃)) V11( the carrier of (subrelstr c₃)) M2( bool [: the carrier of (subrelstr c₃), the carrier of (subrelstr c₃):])
the InternalRel of (subrelstr c₃) |_2 the carrier of (Image c₂) is V7() set
the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) M2( bool [: the carrier of L, the carrier of L:])
the InternalRel of L |_2 the carrier of (subrelstr c₃) is V7() set
( the InternalRel of L |_2 the carrier of (subrelstr c₃)) |_2 the carrier of (Image c₂) is V7() set
the InternalRel of L |_2 the carrier of (Image c₂) is V7() set
the InternalRel of (Image c₂) is V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
[: the carrier of (Image c₂), the carrier of (Image c₂):] is V7() set
bool [: the carrier of (Image c₂), the carrier of (Image c₂):] 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
c₂ 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:])
Image c₂ is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c₂ is non empty M2( bool the carrier of L)
subrelstr (rng c₂) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
(L,L,c₂) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c₂)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c₂):])
the carrier of (Image c₂) is non empty set
[: the carrier of L, the carrier of (Image c₂):] is V7() set
bool [: the carrier of L, the carrier of (Image c₂):] is set
the carrier of (Image c₂) |` c<sub>2</sub> is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total monotone M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of L:])
[: the carrier of (Image c<sub>2</sub>), the carrier of L:] is V7() set
bool [: the carrier of (Image c<sub>2</sub>), the carrier of L:] is set
id (Image c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total monotone isomorphic ( Image c<sub>2</sub>) ( Image c<sub>2</sub>) ( Image c<sub>2</sub>) M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
[: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):] is set
id the carrier of (Image c<sub>2</sub>) is non empty V7() V10( the carrier of (Image c<sub>2</sub>)) V11( the carrier of (Image c<sub>2</sub>)) Function-like one-to-one V27( the carrier of (Image c<sub>2</sub>)) quasi_total M2( bool [: the carrier of (Image c<sub>2</sub>), the carrier of (Image c<sub>2</sub>):])
((Image c<sub>2</sub>),L,(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)) is ( Image c<sub>2</sub>,L)
{(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)} is functional set
{(L,L,c<sub>2</sub>)} is functional set
{{(L,L,c<sub>2</sub>),(L,L,c<sub>2</sub>)},{(L,L,c<sub>2</sub>)}} is set
c<sub>3</sub> is M2( bool the carrier of L)
"\/" (c<sub>3</sub>,(Image c<sub>2</sub>)) is M2( the carrier of (Image c<sub>2</sub>))
"\/" (c<sub>3</sub>,L) is M2( the carrier of L)
c<sub>2</sub> . ("\/" (c<sub>3</sub>,L)) is M2( the carrier of L)
c<sub>2</sub> .: c<sub>3</sub> is M2( bool 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
c<sub>2</sub> 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:])
Image c<sub>2</sub> is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng c<sub>2</sub> is non empty M2( bool the carrier of L)
subrelstr (rng c<sub>2</sub>) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
(L,L,c<sub>2</sub>) is non empty V7() V10( the carrier of L) V11( the carrier of (Image c<sub>2</sub>)) Function-like V27( the carrier of L) quasi_total onto M2( bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):])
the carrier of (Image c<sub>2</sub>) is non empty set
[: the carrier of L, the carrier of (Image c<sub>2</sub>):] is V7() set
bool [: the carrier of L, the carrier of (Image c<sub>2</sub>):] is set
the carrier of (Image c<sub>2</sub>) |` c₂ is V7() V10( the carrier of L) V11( the carrier of L) V11( the carrier of (Image c₂)) V11( the carrier of L) Function-like M2( bool [: the carrier of L, the carrier of L:])
(L,L,c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of L) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone M2( bool [: the carrier of (Image c₂), the carrier of L:])
[: the carrier of (Image c₂), the carrier of L:] is V7() set
bool [: the carrier of (Image c₂), the carrier of L:] is set
id (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total monotone isomorphic ( Image c₂) ( Image c₂) ( Image c₂) M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
[: the carrier of (Image c₂), the carrier of (Image c₂):] is V7() set
bool [: the carrier of (Image c₂), the carrier of (Image c₂):] is set
id the carrier of (Image c₂) is non empty V7() V10( the carrier of (Image c₂)) V11( the carrier of (Image c₂)) Function-like one-to-one V27( the carrier of (Image c₂)) quasi_total M2( bool [: the carrier of (Image c₂), the carrier of (Image c₂):])
(L,(Image c₂),(L,L,c₂),(L,L,c₂)) is (L, Image c₂)
{(L,L,c₂),(L,L,c₂)} is functional set
{(L,L,c₂)} is functional set
{{(L,L,c₂),(L,L,c₂)},{(L,L,c₂)}} is set
c₃ is M2( bool the carrier of L)
"/\" (c₃,(Image c₂)) is M2( the carrier of (Image c₂))
"/\" (c₃,L) is M2( the carrier of L)
c₂ . ("/\" (c₃,L)) is M2( the carrier of L)
c₂ .: c₃ is M2( bool the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is set
{ b₁ where b₁ is non empty directed lower M2( bool the carrier of L) : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete RelStr
IdsMap L is non empty V7() V10( the carrier of L) V11( the carrier of (InclPoset (Ids L))) Function-like V27( the carrier of L) quasi_total monotone M2( bool [: the carrier of L, the carrier of (InclPoset (Ids L)):])
the carrier of (InclPoset (Ids L)) is non empty set
[: the carrier of L, the carrier of (InclPoset (Ids L)):] is V7() set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is set
SupMap L is non empty V7() V10( the carrier of (InclPoset (Ids L))) V11( the carrier of L) Function-like V27( the carrier of (InclPoset (Ids L))) quasi_total monotone M2( bool [: the carrier of (InclPoset (Ids L)), the carrier of L:])
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is V7() set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is set
(L,(InclPoset (Ids L)),(IdsMap L),(SupMap L)) is (L, InclPoset (Ids L))
{(IdsMap L),(SupMap L)} is functional set
{(IdsMap L)} is functional set
{{(IdsMap L),(SupMap L)},{(IdsMap L)}} is set
x is M2( the carrier of (InclPoset (Ids L)))
z1 is M2( the carrier of L)
(IdsMap L) . z1 is M2( the carrier of (InclPoset (Ids L)))
z2 is non empty directed lower M2( bool the carrier of L)
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)
"\/" (z2,L) is M2( the carrier of L)
(SupMap L) . x is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is set
{ b₁ where b₁ is non empty directed lower M2( bool the carrier of L) : verum } is set
InclPoset (Ids 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 (InclPoset (Ids L)) is non empty set
SupMap L is non empty V7() V10( the carrier of (InclPoset (Ids L))) V11( the carrier of L) Function-like V27( the carrier of (InclPoset (Ids L))) quasi_total monotone M2( bool [: the carrier of (InclPoset (Ids L)), the carrier of L:])
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is V7() set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is set
IdsMap L is non empty V7() V10( the carrier of L) V11( the carrier of (InclPoset (Ids L))) Function-like V27( the carrier of L) quasi_total monotone M2( bool [: the carrier of L, the carrier of (InclPoset (Ids L)):])
[: the carrier of L, the carrier of (InclPoset (Ids L)):] is V7() set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is set
(IdsMap L) * (SupMap L) is non empty V7() V10( the carrier of (InclPoset (Ids L))) V11( the carrier of (InclPoset (Ids L))) Function-like V27( the carrier of (InclPoset (Ids L))) quasi_total M2( bool [: the carrier of (InclPoset (Ids L)), the carrier of (InclPoset (Ids L)):])
[: the carrier of (InclPoset (Ids L)), the carrier of (InclPoset (Ids L)):] is V7() set
bool [: the carrier of (InclPoset (Ids L)), the carrier of (InclPoset (Ids L)):] is set
Image ((IdsMap L) * (SupMap L)) is non empty strict reflexive transitive antisymmetric full SubRelStr of InclPoset (Ids L)
rng ((IdsMap L) * (SupMap L)) is non empty M2( bool the carrier of (InclPoset (Ids L)))
bool the carrier of (InclPoset (Ids L)) is set
subrelstr (rng ((IdsMap L) * (SupMap L))) is non empty strict reflexive transitive antisymmetric full SubRelStr of InclPoset (Ids L)
c₃ is non empty directed lower M2( bool the carrier of L)
((IdsMap L) * (SupMap L)) . c₃ is set
(SupMap L) . c₃ is set
(IdsMap L) . ((SupMap L) . c₃) is set
"\/" (c₃,L) is M2( the carrier of L)
(IdsMap L) . ("\/" (c₃,L)) is M2( the carrier of (InclPoset (Ids L)))
downarrow ("\/" (c₃,L)) is non empty directed lower M2( bool the carrier of L)
{("\/" (c₃,L))} is M2( bool the carrier of L)
downarrow {("\/" (c₃,L))} is lower M2( bool the carrier of L)
(L,(InclPoset (Ids L)),(IdsMap L),(SupMap L)) is (L, InclPoset (Ids L))
{(IdsMap L),(SupMap L)} is functional set
{(IdsMap L)} is functional set
{{(IdsMap L),(SupMap L)},{(IdsMap L)}} is set
the carrier of (Image ((IdsMap L) * (SupMap L))) is non empty set
[: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of L:] is V7() set
bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of L:] is set
((InclPoset (Ids L)),(InclPoset (Ids L)),((IdsMap L) * (SupMap L))) is non empty V7() V10( the carrier of (Image ((IdsMap L) * (SupMap L)))) V11( the carrier of (InclPoset (Ids L))) Function-like one-to-one V27( the carrier of (Image ((IdsMap L) * (SupMap L)))) quasi_total monotone M2( bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of (InclPoset (Ids L)):])
[: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of (InclPoset (Ids L)):] is V7() set
bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of (InclPoset (Ids L)):] is set
id (Image ((IdsMap L) * (SupMap L))) is non empty V7() V10( the carrier of (Image ((IdsMap L) * (SupMap L)))) V11( the carrier of (Image ((IdsMap L) * (SupMap L)))) Function-like one-to-one V27( the carrier of (Image ((IdsMap L) * (SupMap L)))) quasi_total monotone isomorphic ( Image ((IdsMap L) * (SupMap L))) ( Image ((IdsMap L) * (SupMap L))) ( Image ((IdsMap L) * (SupMap L))) M2( bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of (Image ((IdsMap L) * (SupMap L))):])
[: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of (Image ((IdsMap L) * (SupMap L))):] is V7() set
bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of (Image ((IdsMap L) * (SupMap L))):] is set
id the carrier of (Image ((IdsMap L) * (SupMap L))) is non empty V7() V10( the carrier of (Image ((IdsMap L) * (SupMap L)))) V11( the carrier of (Image ((IdsMap L) * (SupMap L)))) Function-like one-to-one V27( the carrier of (Image ((IdsMap L) * (SupMap L)))) quasi_total M2( bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of (Image ((IdsMap L) * (SupMap L))):])
(SupMap L) * ((InclPoset (Ids L)),(InclPoset (Ids L)),((IdsMap L) * (SupMap L))) is non empty V7() V10( the carrier of (Image ((IdsMap L) * (SupMap L)))) V11( the carrier of L) Function-like V27( the carrier of (Image ((IdsMap L) * (SupMap L)))) quasi_total M2( bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of L:])
c₃ is non empty V7() V10( the carrier of (Image ((IdsMap L) * (SupMap L)))) V11( the carrier of L) Function-like V27( the carrier of (Image ((IdsMap L) * (SupMap L)))) quasi_total M2( bool [: the carrier of (Image ((IdsMap L) * (SupMap L))), the carrier of L:])
x is M2( the carrier of (Image ((IdsMap L) * (SupMap L))))
z1 is non empty directed lower M2( bool the carrier of L)
c₃ . z1 is set
((InclPoset (Ids L)),(InclPoset (Ids L)),((IdsMap L) * (SupMap L))) . z1 is set
(SupMap L) . (((InclPoset (Ids L)),(InclPoset (Ids L)),((IdsMap L) * (SupMap L))) . z1) is set
(SupMap L) . z1 is set
"\/" (z1,L) is M2( the carrier of L)
x is M2( the carrier of (Image ((IdsMap L) * (SupMap L))))
z2 is M2( the carrier of (InclPoset (Ids L)))
((IdsMap L) * (SupMap L)) . z2 is M2( the carrier of (InclPoset (Ids L)))
z1 is M2( the carrier of (Image ((IdsMap L) * (SupMap L))))
c₃ . x is M2( the carrier of L)
c₃ . z1 is M2( the carrier of L)
y is M2( the carrier of (InclPoset (Ids L)))
((IdsMap L) * (SupMap L)) . y is M2( the carrier of (InclPoset (Ids L)))
Ix is non empty directed lower M2( bool the carrier of L)
"\/" (Ix,L) is M2( the carrier of L)
downarrow ("\/" (Ix,L)) is non empty directed lower M2( bool the carrier of L)
{("\/" (Ix,L))} is M2( bool the carrier of L)
downarrow {("\/" (Ix,L))} is lower M2( bool the carrier of L)
Iy is non empty directed lower M2( bool the carrier of L)
"\/" (Iy,L) is M2( the carrier of L)
downarrow ("\/" (Iy,L)) is non empty directed lower M2( bool the carrier of L)
{("\/" (Iy,L))} is M2( bool the carrier of L)
downarrow {("\/" (Iy,L))} is lower M2( bool the carrier of L)
((IdsMap L) * (SupMap L)) . Ix is set
((IdsMap L) * (SupMap L)) . Iy is set
z is non empty directed lower M2( bool the carrier of L)
c₃ . z is set
"\/" (z,L) is M2( the carrier of L)
x is non empty directed lower M2( bool the carrier of L)
c₃ . x is set
"\/" (x,L) is M2( the carrier of L)
"\/" ((downarrow ("\/" (Ix,L))),L) is M2( the carrier of L)
"\/" ((downarrow ("\/" (Iy,L))),L) is M2( the carrier of L)
i1 is M2( the carrier of (InclPoset (Ids L)))
i2 is M2( the carrier of (InclPoset (Ids L)))
rng c₃ is non empty M2( bool 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)
{z1} is M2( bool the carrier of L)
downarrow {z1} is lower M2( bool the carrier of L)
(SupMap L) . (downarrow z1) is set
"\/" ((downarrow z1),L) is M2( the carrier of L)
((IdsMap L) * (SupMap L)) . (downarrow z1) is set
(IdsMap L) . ((SupMap L) . (downarrow z1)) is set
c₃ . (downarrow z1) is set
((InclPoset (Ids L)),(InclPoset (Ids L)),((IdsMap L) * (SupMap L))) . (downarrow z1) is set
(SupMap L) . (((InclPoset (Ids L)),(InclPoset (Ids L)),((IdsMap L) * (SupMap L))) . (downarrow z1)) is set
x is M2( the carrier of (Image ((IdsMap L) * (SupMap L))))
c₃ . x is M2( the carrier of L)
z1 is M2( the carrier of (Image ((IdsMap L) * (SupMap L))))
c₃ . z1 is M2( the carrier of L)
z2 is M2( the carrier of (InclPoset (Ids L)))
((IdsMap L) * (SupMap L)) . z2 is M2( the carrier of (InclPoset (Ids L)))
z is M2( the carrier of (InclPoset (Ids L)))
((IdsMap L) * (SupMap L)) . z is M2( the carrier of (InclPoset (Ids L)))
Ix is non empty directed lower M2( bool the carrier of L)
"\/" (Ix,L) is M2( the carrier of L)
downarrow ("\/" (Ix,L)) is non empty directed lower M2( bool the carrier of L)
{("\/" (Ix,L))} is M2( bool the carrier of L)
downarrow {("\/" (Ix,L))} is lower M2( bool the carrier of L)
"\/" ((downarrow ("\/" (Ix,L))),L) is M2( the carrier of L)
((IdsMap L) * (SupMap L)) . Ix is set
Iy is non empty directed lower M2( bool the carrier of L)
((IdsMap L) * (SupMap L)) . Iy is set
"\/" (Iy,L) is M2( the carrier of L)
downarrow ("\/" (Iy,L)) is non empty directed lower M2( bool the carrier of L)
{("\/" (Iy,L))} is M2( bool the carrier of L)
downarrow {("\/" (Iy,L))} is lower M2( bool the carrier of L)
x is non empty directed lower M2( bool the carrier of L)
c₃ . x is set
"\/" (x,L) is M2( the carrier of L)
y is non empty directed lower M2( bool the carrier of L)
c₃ . y is set
"\/" (y,L) is M2( 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
c₂ is M2( the carrier of L)
c₃ 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:])
x 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)
c₃ . z1 is M2( the carrier of L)
c₂ "/\" z1 is M2( the carrier of L)
x . z1 is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ <= c₃ } is set
(L,c₂) 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
downarrow c₃ is M2( bool the carrier of L)
bool the carrier of L is set
{c₃} is M2( bool the carrier of L)
downarrow {c₃} is M2( bool the carrier of L)
(L,c₂) " (downarrow c₃) is M2( bool the carrier of L)
x is set
z1 is M2( the carrier of L)
c₂ "/\" z1 is M2( the carrier of L)
(L,c₂) . z1 is M2( the carrier of L)
x is set
z1 is M2( the carrier of L)
(L,c₂) . z1 is M2( the carrier of L)
c₂ "/\" z1 is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
(L,c₂) 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
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
(L,c₂) . c₃ is M2( the carrier of L)
(L,c₂) . x is M2( the carrier of L)
{c₂,c₃} is M2( bool the carrier of L)
bool the carrier of L is set
c₂ "/\" c₃ is M2( the carrier of L)
{c₂,x} is M2( bool the carrier of L)
c₂ "/\" x is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
(L,c₂) 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
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is set
c₂ is M2( the carrier of L)
(L,c₂) 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
c₃ is M2( bool the carrier of L)
(L,c₂) .: c₃ is M2( bool the carrier of L)
{ (c₂ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₃ } is set
z1 is set
z2 is set
(L,c₂) . z2 is set
z is M2( the carrier of L)
c₂ "/\" z is M2( the carrier of L)
z1 is set
z2 is M2( the carrier of L)
c₂ "/\" z2 is M2( the carrier of L)
(L,c₂) . z2 is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
(L,c₂) is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone 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
x 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,L,x,(L,c₂)) is (L,L)
{x,(L,c₂)} is functional set
{x} is functional set
{{x,(L,c₂)},{x}} is set
c₃ is M2( the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ <= c₃ } is set
downarrow c₃ is non empty directed lower M2( bool the carrier of L)
bool the carrier of L is set
{c₃} is M2( bool the carrier of L)
downarrow {c₃} is lower M2( bool the carrier of L)
(L,c₂) " (downarrow c₃) is M2( bool the carrier of L)
x . c₃ is M2( the carrier of L)
"\/" ( { b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ <= c₃ } ,L) is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂) is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone M2( bool [: the carrier of L, the carrier of L:])
c₃ 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:])
x is M2( the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ <= x } is set
"\/" ( { b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ <= x } ,L) is M2( the carrier of L)
downarrow x is non empty directed lower M2( bool the carrier of L)
{x} is M2( bool the carrier of L)
downarrow {x} is lower M2( bool the carrier of L)
(L,c₂) " (downarrow x) is M2( bool the carrier of L)
c₃ . x is M2( the carrier of L)
"\/" (((L,c₂) " (downarrow x)),L) is M2( the carrier of L)
(L,L,c₃,(L,c₂)) is (L,L)
{c₃,(L,c₂)} is functional set
{c₃} is functional set
{{c₃,(L,c₂)},{c₃}} is set
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is set
c₂ is M2( bool the carrier of L)
"\/" (c₂,L) is M2( the carrier of L)
c₃ is M2( the carrier of L)
c₃ "/\" ("\/" (c₂,L)) is M2( the carrier of L)
{ (c₃ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₂ } is set
"\/" ( { (c₃ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₂ } ,L) is M2( the carrier of L)
(L,c₃) is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone 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
(L,c₃) .: c₂ is M2( bool the carrier of L)
"\/" (((L,c₃) .: c₂),L) is M2( the carrier of L)
(L,c₃) . ("\/" (c₂,L)) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete RelStr
the carrier of L is non empty set
bool the carrier of L is set
c₃ is M2( the carrier of L)
c₂ is M2( bool the carrier of L)
"\/" (c₂,L) is M2( the carrier of L)
c₃ "/\" ("\/" (c₂,L)) is M2( the carrier of L)
{ (c₃ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₂ } is set
"\/" ( { (c₃ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₂ } ,L) is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂) is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone 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
c₃ is M2( bool the carrier of L)
(L,c₂) .: c₃ is M2( bool the carrier of L)
"\/" (((L,c₂) .: c₃),L) is M2( the carrier of L)
"\/" (c₃,L) is M2( the carrier of L)
(L,c₂) . ("\/" (c₃,L)) is M2( the carrier of L)
c₂ "/\" ("\/" (c₃,L)) is M2( the carrier of L)
{ (c₂ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₃ } is set
"\/" ( { (c₂ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₃ } ,L) 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
bool the carrier of L is set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
c₃ "\/" x is M2( the carrier of L)
c₂ "/\" (c₃ "\/" x) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
c₂ "/\" x is M2( the carrier of L)
(c₂ "/\" c₃) "\/" (c₂ "/\" x) is M2( the carrier of L)
{c₃,x} is M2( bool the carrier of L)
{ (c₂ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in {c₃,x} } is set
z2 is set
c₂ "/\" c₃ is M2( the carrier of L)
c₂ "/\" x is M2( the carrier of L)
z is M2( the carrier of L)
c₂ "/\" z is M2( the carrier of L)
{ (c₂ "/\" b₂) where b₁ is M2( the carrier of L) : b₂ in {c₃,x} } is set
{ (c₂ "/\" b₂) where b₁ is M2( the carrier of L) : b₂ in {c₃,x} } is set
{ (c₂ "/\" b₂) where b₁ is M2( the carrier of L) : b₂ in {c₃,x} } is set
{(c₂ "/\" c₃),(c₂ "/\" x)} is M2( bool the carrier of L)
c₃ "\/" x is M2( the carrier of L)
c₂ "/\" (c₃ "\/" x) is M2( the carrier of L)
"\/" ({c₃,x},L) is M2( the carrier of L)
c₂ "/\" ("\/" ({c₃,x},L)) is M2( the carrier of L)
"\/" ({(c₂ "/\" c₃),(c₂ "/\" x)},L) is M2( the carrier of L)
(c₂ "/\" c₃) "\/" (c₂ "/\" x) is M2( the carrier of L)
L is non empty RelStr
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₂ is M2( the carrier of L)
(L,c₂) 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:])
c₃ 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,L,c₃,(L,c₂)) is (L,L)
{c₃,(L,c₂)} is functional set
{c₃} is functional set
{{c₃,(L,c₂)},{c₃}} is set
x 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,L,x,(L,c₂)) is (L,L)
{x,(L,c₂)} is functional set
{x} is functional set
{{x,(L,c₂)},{x}} is set
z1 is M2( the carrier of L)
c₃ . z1 is M2( the carrier of L)
downarrow z1 is M2( bool the carrier of L)
bool the carrier of L is set
{z1} is M2( bool the carrier of L)
downarrow {z1} is M2( bool the carrier of L)
(L,c₂) " (downarrow z1) is M2( bool the carrier of L)
"\/" (((L,c₂) " (downarrow z1)),L) is M2( the carrier of L)
x . z1 is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is set
c₂ is M2( bool the carrier of L)
c₃ is M2( the carrier of L)
"\/" (c₂,L) is M2( the carrier of L)
c₃ "/\" ("\/" (c₂,L)) is M2( the carrier of L)
{ (c₃ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₂ } is set
"\/" ( { (c₃ "/\" b₁) where b₁ is M2( the carrier of L) : b₁ in c₂ } ,L) is M2( the carrier of L)
L is non empty RelStr
L is non empty RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
(L,c₂) 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
c₃ is M2( the carrier of L)
(L,c₂) . c₃ is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
c₃ "/\" x is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₃,c₂) is M2( the carrier of L)
(L,c₃) 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
(L,c₃) . c₂ is M2( the carrier of L)
(L,c₃) 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,L,(L,c₃),(L,c₃)) is (L,L)
{(L,c₃),(L,c₃)} is functional set
{(L,c₃)} is functional set
{{(L,c₃),(L,c₃)},{(L,c₃)}} is set
(L,c₃) . x is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
the M2( the carrier of L) is M2( the carrier of L)
(L, the M2( the carrier of L), the M2( the carrier of L)) is M2( the carrier of L)
(L, the M2( the carrier of L)) 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
(L, the M2( the carrier of L)) . the M2( the carrier of L) is M2( the carrier of L)
c₃ is M2( the carrier of L)
the M2( the carrier of L) "/\" c₃ is M2( the carrier of L)
L is non empty RelStr
L is non empty 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₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
(L,c₂,c₃) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . c₃ is M2( the carrier of L)
c₂ "/\" (Top L) is M2( the carrier of L)
(Top L) "/\" c₂ is M2( the carrier of L)
L is non empty 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₂ is M2( the carrier of L)
(L,c₂,c₂) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . c₂ is M2( the carrier of L)
c₂ "/\" (Top L) is M2( the carrier of L)
L is non empty 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₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
(L,c₂,c₃) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . c₃ is M2( the carrier of L)
(L,c₃,c₂) is M2( the carrier of L)
(L,c₃) 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,c₃) . c₂ is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₃ is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂,c₃) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . c₃ is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
L is non empty 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₂ is M2( the carrier of L)
(L,c₂,(Top L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Top L) is M2( the carrier of L)
L is non empty 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₂ is M2( the carrier of L)
(L,(Top L),c₂) is M2( the carrier of L)
(L,(Top L)) 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
(L,(Top L)) . c₂ is M2( the carrier of L)
(Top L) "/\" (L,(Top L),c₂) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
(L,c₂,c₃) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . c₃ is M2( the carrier of L)
c₂ "/\" (L,c₂,c₃) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
(L,c₃,x) is M2( the carrier of L)
(L,c₃) 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
(L,c₃) . x is M2( the carrier of L)
(L,c₂,x) is M2( the carrier of L)
(L,c₂) 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,c₂) . x is M2( the carrier of L)
c₂ "/\" (L,c₃,x) is M2( the carrier of L)
c₃ "/\" (L,c₃,x) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂,c₃) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . c₃ is M2( the carrier of L)
(L,c₂,x) is M2( the carrier of L)
(L,c₂) . x is M2( the carrier of L)
c₂ "/\" (L,c₂,c₃) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
(L,c₂,c₃) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . c₃ is M2( the carrier of L)
c₂ "/\" (L,c₂,c₃) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
(c₂ "/\" (L,c₂,c₃)) "/\" c₂ is M2( the carrier of L)
c₃ "/\" c₂ is M2( the carrier of L)
c₂ "/\" (c₂ "/\" (L,c₂,c₃)) is M2( the carrier of L)
c₂ "/\" c₂ is M2( the carrier of L)
(c₂ "/\" c₂) "/\" (L,c₂,c₃) is M2( the carrier of L)
(L,c₂,c₃) "/\" c₂ is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
c₂ "\/" c₃ is M2( the carrier of L)
x is M2( the carrier of L)
(L,(c₂ "\/" c₃),x) is M2( the carrier of L)
(L,(c₂ "\/" c₃)) 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
(L,(c₂ "\/" c₃)) . x is M2( the carrier of L)
(L,c₂,x) is M2( the carrier of L)
(L,c₂) 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,c₂) . x is M2( the carrier of L)
(L,c₃,x) is M2( the carrier of L)
(L,c₃) 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,c₃) . x is M2( the carrier of L)
(L,c₂,x) "/\" (L,c₃,x) is M2( the carrier of L)
c₂ "/\" x is M2( the carrier of L)
(c₂ "/\" x) "/\" (L,c₃,x) is M2( the carrier of L)
c₃ "/\" x is M2( the carrier of L)
(c₃ "/\" x) "/\" (L,c₂,x) is M2( the carrier of L)
(c₂ "\/" c₃) "/\" ((L,c₂,x) "/\" (L,c₃,x)) is M2( the carrier of L)
((L,c₂,x) "/\" (L,c₃,x)) "/\" (c₂ "\/" c₃) is M2( the carrier of L)
((L,c₂,x) "/\" (L,c₃,x)) "/\" c₂ is M2( the carrier of L)
((L,c₂,x) "/\" (L,c₃,x)) "/\" c₃ is M2( the carrier of L)
(((L,c₂,x) "/\" (L,c₃,x)) "/\" c₂) "\/" (((L,c₂,x) "/\" (L,c₃,x)) "/\" c₃) is M2( the carrier of L)
c₂ "/\" ((L,c₂,x) "/\" (L,c₃,x)) is M2( the carrier of L)
(c₂ "/\" ((L,c₂,x) "/\" (L,c₃,x))) "\/" (((L,c₂,x) "/\" (L,c₃,x)) "/\" c₃) is M2( the carrier of L)
c₃ "/\" ((L,c₂,x) "/\" (L,c₃,x)) is M2( the carrier of L)
(c₂ "/\" ((L,c₂,x) "/\" (L,c₃,x))) "\/" (c₃ "/\" ((L,c₂,x) "/\" (L,c₃,x))) is M2( the carrier of L)
c₂ "/\" (L,c₂,x) is M2( the carrier of L)
(c₂ "/\" (L,c₂,x)) "/\" (L,c₃,x) is M2( the carrier of L)
((c₂ "/\" (L,c₂,x)) "/\" (L,c₃,x)) "\/" (c₃ "/\" ((L,c₂,x) "/\" (L,c₃,x))) is M2( the carrier of L)
(L,c₃,x) "/\" (L,c₂,x) is M2( the carrier of L)
c₃ "/\" ((L,c₃,x) "/\" (L,c₂,x)) is M2( the carrier of L)
((c₂ "/\" (L,c₂,x)) "/\" (L,c₃,x)) "\/" (c₃ "/\" ((L,c₃,x) "/\" (L,c₂,x))) is M2( the carrier of L)
c₃ "/\" (L,c₃,x) is M2( the carrier of L)
(c₃ "/\" (L,c₃,x)) "/\" (L,c₂,x) is M2( the carrier of L)
((c₂ "/\" (L,c₂,x)) "/\" (L,c₃,x)) "\/" ((c₃ "/\" (L,c₃,x)) "/\" (L,c₂,x)) is M2( the carrier of L)
((c₂ "/\" x) "/\" (L,c₃,x)) "\/" ((c₃ "/\" (L,c₃,x)) "/\" (L,c₂,x)) is M2( the carrier of L)
((c₂ "/\" x) "/\" (L,c₃,x)) "\/" ((c₃ "/\" x) "/\" (L,c₂,x)) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
L is non empty 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₂ is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
{ b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ = Bottom L } is set
{ b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ <= Bottom L } is set
z1 is set
z2 is M2( the carrier of L)
c₂ "/\" z2 is M2( the carrier of L)
z1 is set
z2 is M2( the carrier of L)
c₂ "/\" z2 is M2( the carrier of L)
c₂ "/\" (L,c₂) is M2( the carrier of L)
z1 is M2( the carrier of L)
z1 is M2( the carrier of L)
(L,z1) 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:])
"\/" ( { b₁ where b₁ is M2( the carrier of L) : c₂ "/\" b₁ = Bottom L } ,L) is M2( the carrier of L)
z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
c₂ "/\" z2 is M2( the carrier of L)
L is non empty RelStr
Bottom L is M2( the carrier of L)
the carrier of L is non empty set
"\/" ({},L) is M2( the carrier of L)
(L,(Bottom L)) is M2( the carrier of L)
(L,(Bottom L),(Bottom L)) is M2( the carrier of L)
(L,(Bottom L)) 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
(L,(Bottom L)) . (Bottom L) is M2( the carrier of L)
Top L is M2( the carrier of L)
"/\" ({},L) is M2( the carrier of L)
(L,(Top L)) is M2( the carrier of L)
(L,(Top L),(Bottom L)) is M2( the carrier of L)
(L,(Top L)) 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,(Top L)) . (Bottom L) is M2( the carrier of L)
(Top L) "/\" (L,(Top L)) is M2( the carrier of L)
(Bottom L) "/\" (Top L) is M2( the carrier of L)
(L,(Top L)) "/\" (Top L) is M2( the carrier of L)
L is non empty lower-bounded RelStr
the carrier of L is non empty set
c₃ is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
(L,c₃) is M2( the carrier of L)
(L,c₃,(Bottom L)) is M2( the carrier of L)
(L,c₃) 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,c₃) . (Bottom L) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
c₃ "/\" c₂ is M2( the carrier of L)
L is non empty 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₃ is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
L is non empty lower-bounded RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
(L,c₃) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,c₃,(Bottom L)) is M2( the carrier of L)
(L,c₃) 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
(L,c₃) . (Bottom L) is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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,c₂) . (Bottom L) is M2( the carrier of L)
c₂ "/\" (L,c₃) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
(c₂ "/\" c₃) "/\" (L,c₃) is M2( the carrier of L)
c₃ "/\" (L,c₃) is M2( the carrier of L)
c₂ "/\" (c₃ "/\" (L,c₃)) is M2( the carrier of L)
c₂ "/\" (Bottom L) is M2( the carrier of L)
(Bottom L) "/\" c₂ is M2( the carrier of L)
L is non empty lower-bounded RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
c₂ "\/" c₃ is M2( the carrier of L)
(L,(c₂ "\/" c₃)) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,(c₂ "\/" c₃),(Bottom L)) is M2( the carrier of L)
(L,(c₂ "\/" c₃)) 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
(L,(c₂ "\/" c₃)) . (Bottom L) is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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,c₂) . (Bottom L) is M2( the carrier of L)
(L,c₃) is M2( the carrier of L)
(L,c₃,(Bottom L)) is M2( the carrier of L)
(L,c₃) 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,c₃) . (Bottom L) is M2( the carrier of L)
(L,c₂) "/\" (L,c₃) is M2( the carrier of L)
L is non empty 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₂ is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
c₃ is M2( the carrier of L)
(L,c₃) is M2( the carrier of L)
(L,c₃,(Bottom L)) is M2( the carrier of L)
(L,c₃) 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,c₃) . (Bottom L) is M2( the carrier of L)
(L,c₂) "\/" (L,c₃) is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
(L,(c₂ "/\" c₃)) is M2( the carrier of L)
(L,(c₂ "/\" c₃),(Bottom L)) is M2( the carrier of L)
(L,(c₂ "/\" c₃)) 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,(c₂ "/\" c₃)) . (Bottom L) is M2( the carrier of L)
(c₂ "/\" c₃) "/\" ((L,c₂) "\/" (L,c₃)) is M2( the carrier of L)
(c₂ "/\" c₃) "/\" (L,c₂) is M2( the carrier of L)
(c₂ "/\" c₃) "/\" (L,c₃) is M2( the carrier of L)
((c₂ "/\" c₃) "/\" (L,c₂)) "\/" ((c₂ "/\" c₃) "/\" (L,c₃)) is M2( the carrier of L)
c₃ "/\" c₂ is M2( the carrier of L)
(c₃ "/\" c₂) "/\" (L,c₂) is M2( the carrier of L)
((c₃ "/\" c₂) "/\" (L,c₂)) "\/" ((c₂ "/\" c₃) "/\" (L,c₃)) is M2( the carrier of L)
c₂ "/\" (L,c₂) is M2( the carrier of L)
c₃ "/\" (c₂ "/\" (L,c₂)) is M2( the carrier of L)
(c₃ "/\" (c₂ "/\" (L,c₂))) "\/" ((c₂ "/\" c₃) "/\" (L,c₃)) is M2( the carrier of L)
c₃ "/\" (L,c₃) is M2( the carrier of L)
c₂ "/\" (c₃ "/\" (L,c₃)) is M2( the carrier of L)
(c₃ "/\" (c₂ "/\" (L,c₂))) "\/" (c₂ "/\" (c₃ "/\" (L,c₃))) is M2( the carrier of L)
c₃ "/\" (Bottom L) is M2( the carrier of L)
(c₃ "/\" (Bottom L)) "\/" (c₂ "/\" (c₃ "/\" (L,c₃))) is M2( the carrier of L)
c₂ "/\" (Bottom L) is M2( the carrier of L)
(c₃ "/\" (Bottom L)) "\/" (c₂ "/\" (Bottom L)) is M2( the carrier of L)
(Bottom L) "/\" c₃ is M2( the carrier of L)
((Bottom L) "/\" c₃) "\/" (c₂ "/\" (Bottom L)) is M2( the carrier of L)
(Bottom L) "/\" c₂ is M2( the carrier of L)
((Bottom L) "/\" c₃) "\/" ((Bottom L) "/\" c₂) is M2( the carrier of L)
(Bottom L) "\/" ((Bottom L) "/\" c₂) is M2( the carrier of L)
(Bottom L) "\/" (Bottom L) is M2( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
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₂ is M2( the carrier of (BoolePoset L))
BooleLatt L is non empty V120() V127() V134() complete L15()
LattPOSet (BooleLatt 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 (BooleLatt L) is non empty set
K220((BooleLatt L)) is V7() V10( the carrier of (BooleLatt L)) V11( the carrier of (BooleLatt L)) V19() V22() V26() V27( the carrier of (BooleLatt L)) quasi_total M2( bool [: the carrier of (BooleLatt L), the carrier of (BooleLatt L):])
[: the carrier of (BooleLatt L), the carrier of (BooleLatt L):] is V7() set
bool [: the carrier of (BooleLatt L), the carrier of (BooleLatt L):] is set
RelStr(# the carrier of (BooleLatt L),K220((BooleLatt L)) #) is strict RelStr
the carrier of (LattPOSet (BooleLatt L)) is non empty set
bool L is set
L \ c₂ is set
c₃ is M2( the carrier of (BoolePoset L))
c₂ "\/" c₃ is M2( the carrier of (BoolePoset L))
c₂ \/ c₃ is set
L \/ c₂ is set
Top (BoolePoset L) is M2( the carrier of (BoolePoset L))
"/\" ({},(BoolePoset L)) is M2( the carrier of (BoolePoset L))
c₂ "/\" c₃ is M2( the carrier of (BoolePoset L))
Bottom (BoolePoset L) is M2( the carrier of (BoolePoset L))
"\/" ({},(BoolePoset L)) is M2( the carrier of (BoolePoset L))
c₂ "/\" c₃ is M2( the carrier of (BoolePoset L))
c₂ /\ c₃ is set
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₃ is M2( the carrier of L)
x is M2( the carrier of L)
x "\/" c₃ is M2( the carrier of L)
(x "\/" c₃) "/\" c₂ is M2( the carrier of L)
x "/\" c₂ is M2( the carrier of L)
(x "/\" c₂) "\/" c₃ is M2( the carrier of L)
c₂ "/\" x is M2( the carrier of L)
c₂ "/\" c₃ is M2( the carrier of L)
(c₂ "/\" x) "\/" (c₂ "/\" c₃) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(Bottom L) "\/" (c₂ "/\" x) is M2( the carrier of L)
c₃ "\/" x is M2( the carrier of L)
c₃ "\/" c₂ is M2( the carrier of L)
(c₃ "\/" x) "/\" (c₃ "\/" c₂) is M2( the carrier of L)
Top L is M2( the carrier of L)
"/\" ({},L) is M2( the carrier of L)
(c₃ "\/" x) "/\" (Top L) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded 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₂ 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:])
x 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:])
c₃ is M2( the carrier of L)
c₂ . c₃ is M2( the carrier of L)
z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
x . z2 is M2( the carrier of L)
(c₂ . c₃) "\/" z2 is M2( the carrier of L)
z1 "/\" c₃ is M2( the carrier of L)
((c₂ . c₃) "\/" z2) "/\" c₃ is M2( the carrier of L)
(L,c₃) is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone M2( bool [: the carrier of L, the carrier of L:])
(L,c₃) . z1 is M2( the carrier of L)
c₃ "/\" z1 is M2( the carrier of L)
(z1 "/\" c₃) "\/" (c₂ . c₃) is M2( the carrier of L)
z2 "\/" (c₂ . c₃) is M2( the carrier of L)
z1 is M2( the carrier of L)
z2 is M2( the carrier of L)
x . z1 is M2( the carrier of L)
x . z2 is M2( the carrier of L)
(c₂ . c₃) "\/" z1 is M2( the carrier of L)
z2 "\/" (c₂ . c₃) is M2( the carrier of L)
(c₂ . c₃) "\/" z2 is M2( the carrier of L)
(L,L,x,(L,c₃)) is (L,L)
{x,(L,c₃)} is functional set
{x} is functional set
{{x,(L,c₃)},{x}} is set
c₃ is M2( the carrier of L)
(L,c₃) is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone M2( bool [: the carrier of L, the carrier of L:])
c₂ . c₃ is M2( the carrier of L)
x 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,L,x,(L,c₃)) is (L,L)
{x,(L,c₃)} is functional set
{x} is functional set
{{x,(L,c₃)},{x}} is set
c₃ is M2( the carrier of L)
c₂ . c₃ is M2( the carrier of L)
x 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,c₃) is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone M2( bool [: the carrier of L, the carrier of L:])
(L,L,x,(L,c₃)) is (L,L)
{x,(L,c₃)} is functional set
{x} is functional set
{{x,(L,c₃)},{x}} is set
(L,c₃) 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,c₃) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,c₃,(Bottom L)) is M2( the carrier of L)
(L,c₃) . (Bottom L) is M2( the carrier of L)
(Bottom L) "\/" (c₂ . c₃) is M2( the carrier of L)
c₃ is M2( the carrier of L)
c₂ . c₃ is M2( the carrier of L)
(Bottom L) "\/" (c₂ . c₃) is M2( the carrier of L)
((Bottom L) "\/" (c₂ . c₃)) "/\" c₃ is M2( the carrier of L)
c₃ "/\" (Bottom L) is M2( the carrier of L)
c₃ "/\" (c₂ . c₃) is M2( the carrier of L)
(c₃ "/\" (Bottom L)) "\/" (c₃ "/\" (c₂ . c₃)) is M2( the carrier of L)
(Bottom L) "\/" (c₃ "/\" (c₂ . c₃)) is M2( the carrier of L)
(L,c₃) is M2( the carrier of L)
(L,c₃,(Bottom L)) is M2( the carrier of L)
(L,c₃) 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,c₃) . (Bottom L) is M2( the carrier of L)
c₃ "/\" (L,c₃) is M2( the carrier of L)
c₃ is M2( the carrier of L)
(L,c₃) is M2( the carrier of L)
(L,c₃,(Bottom L)) is M2( the carrier of L)
(L,c₃) 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,c₃) . (Bottom L) is M2( the carrier of L)
(L,(L,c₃)) is M2( the carrier of L)
(L,(L,c₃),(Bottom L)) is M2( the carrier of L)
(L,(L,c₃)) 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,(L,c₃)) . (Bottom L) is M2( the carrier of L)
Top L is M2( the carrier of L)
"/\" ({},L) is M2( the carrier of L)
x is M2( the carrier of L)
(Top L) "/\" x is M2( the carrier of L)
c₂ . x is M2( the carrier of L)
((Top L) "/\" x) "\/" (c₂ . x) is M2( the carrier of L)
x "\/" (c₂ . x) is M2( the carrier of L)
(L,x) is M2( the carrier of L)
(L,x,(Bottom L)) is M2( the carrier of L)
(L,x) 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,x) . (Bottom L) is M2( the carrier of L)
x "\/" (L,x) is M2( the carrier of L)
(L,c₃) "\/" (L,(L,c₃)) is M2( the carrier of L)
((L,c₃) "\/" (L,(L,c₃))) "/\" c₃ is M2( the carrier of L)
(Top L) "/\" c₃ is M2( the carrier of L)
c₃ "/\" ((L,c₃) "\/" (L,(L,c₃))) is M2( the carrier of L)
c₃ "/\" (L,c₃) is M2( the carrier of L)
c₃ "/\" (L,(L,c₃)) is M2( the carrier of L)
(c₃ "/\" (L,c₃)) "\/" (c₃ "/\" (L,(L,c₃))) is M2( the carrier of L)
(Bottom L) "\/" (c₃ "/\" (L,(L,c₃))) is M2( the carrier of L)
(Bottom L) "\/" c₃ is M2( the carrier of L)
(L,c₃) "/\" (L,(L,c₃)) is M2( the carrier of L)
((L,c₃) "/\" (L,(L,c₃))) "\/" c₃ is M2( the carrier of L)
c₃ "\/" ((L,c₃) "/\" (L,(L,c₃))) is M2( the carrier of L)
c₃ "\/" (L,c₃) is M2( the carrier of L)
c₃ "\/" (L,(L,c₃)) is M2( the carrier of L)
(c₃ "\/" (L,c₃)) "/\" (c₃ "\/" (L,(L,c₃))) is M2( the carrier of L)
(Top L) "/\" (c₃ "\/" (L,(L,c₃))) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
c₂ "\/" (L,c₂) is M2( the carrier of L)
(L,(c₂ "\/" (L,c₂))) is M2( the carrier of L)
(L,(c₂ "\/" (L,c₂)),(Bottom L)) is M2( the carrier of L)
(L,(c₂ "\/" (L,c₂))) 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,(c₂ "\/" (L,c₂))) . (Bottom L) is M2( the carrier of L)
(L,(L,c₂)) is M2( the carrier of L)
(L,(L,c₂),(Bottom L)) is M2( the carrier of L)
(L,(L,c₂)) 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,(L,c₂)) . (Bottom L) is M2( the carrier of L)
(L,c₂) "/\" (L,(L,c₂)) is M2( the carrier of L)
c₂ "/\" (L,c₂) is M2( the carrier of L)
(L,(Bottom L)) is M2( the carrier of L)
(L,(Bottom L),(Bottom L)) is M2( the carrier of L)
(L,(Bottom L)) 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,(Bottom L)) . (Bottom L) is M2( the carrier of L)
Top L is M2( the carrier of L)
"/\" ({},L) is M2( the carrier of L)
c₂ "/\" (L,c₂) is M2( the carrier of L)
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded RelStr
the carrier of L is non empty set
c₂ is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
(L,(L,c₂)) is M2( the carrier of L)
(L,(L,c₂),(Bottom L)) is M2( the carrier of L)
(L,(L,c₂)) 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,(L,c₂)) . (Bottom L) is M2( the carrier of L)
c₂ is M2( the carrier of L)
(L,c₂) is M2( the carrier of L)
Bottom L is M2( the carrier of L)
"\/" ({},L) is M2( the carrier of L)
(L,c₂,(Bottom L)) is M2( the carrier of L)
(L,c₂) 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
(L,c₂) . (Bottom L) is M2( the carrier of L)
L is non empty RelStr
L is non empty RelStr
L is non empty RelStr
BoolePoset {} is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete () () () () RelStr
the non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded () () () () RelStr is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded () () () () RelStr