:: YELLOW_2 semantic presentation

K133() is Element of bool K129()
K129() is set
bool K129() is non empty set
K128() is set
bool K128() is non empty set
{} is empty set
1 is non empty set
{{},1} is non empty set
bool K133() is non empty set
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is Element of the carrier of L
downarrow a is Element of bool the carrier of L
{a} is non empty Element of bool the carrier of L
downarrow {a} is Element of bool the carrier of L
J is Element of bool the carrier of L
F is Element of the carrier of L
F is set
c is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is Element of the carrier of L
uparrow a is Element of bool the carrier of L
{a} is non empty Element of bool the carrier of L
uparrow {a} is Element of bool the carrier of L
J is Element of bool the carrier of L
F is Element of the carrier of L
F is set
c is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
a is set
J is set
a \/ J is set
"\/" ((a \/ J),L) is Element of the carrier of L
the carrier of L is non empty set
"\/" (a,L) is Element of the carrier of L
"\/" (J,L) is Element of the carrier of L
("\/" (a,L)) "\/" ("\/" (J,L)) is Element of the carrier of L
c is Element of the carrier of L
c is Element of the carrier of L
L is non empty transitive antisymmetric with_infima RelStr
a is set
J is set
a \/ J is set
"/\" ((a \/ J),L) is Element of the carrier of L
the carrier of L is non empty set
"/\" (a,L) is Element of the carrier of L
"/\" (J,L) is Element of the carrier of L
("/\" (a,L)) "/\" ("/\" (J,L)) is Element of the carrier of L
c is Element of the carrier of L
c is Element of the carrier of L
L is Relation-like set
a is set
J is set
L |_2 a is Relation-like set
L |_2 J is Relation-like set
a |` L is Relation-like set
J |` L is Relation-like set
(a |` L) | a is Relation-like set
(J |` L) | a is Relation-like set
(J |` L) | J is Relation-like set
L is RelStr
a is full SubRelStr of L
the carrier of a is set
J is full SubRelStr of L
the carrier of J is set
the InternalRel of a is Relation-like the carrier of a -defined the carrier of a -valued Element of bool [: the carrier of a, the carrier of a:]
[: the carrier of a, the carrier of a:] is set
bool [: the carrier of a, the carrier of a:] is non empty set
the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of bool [: the carrier of J, the carrier of J:]
[: the carrier of J, the carrier of J:] is set
bool [: the carrier of J, the carrier of J:] is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is set
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is non empty set
the InternalRel of L |_2 the carrier of a is Relation-like set
the InternalRel of L |_2 the carrier of J is Relation-like set
L is set
a is non empty RelStr
the carrier of a is non empty set
bool the carrier of a is non empty set
J is non empty SubRelStr of a
the carrier of J is non empty set
bool the carrier of J is non empty set
F is Element of bool the carrier of a
c is Element of the carrier of a
j is Element of the carrier of a
j is Element of the carrier of J
a is Element of the carrier of J
b is Element of the carrier of J
DZ is Element of the carrier of a
F is Element of bool the carrier of a
c is Element of the carrier of a
j is Element of the carrier of a
j is Element of the carrier of J
a is Element of the carrier of J
b is Element of the carrier of J
DZ is Element of the carrier of a
L is non empty RelStr
a is non empty full SubRelStr of L
the carrier of a is non empty set
J is non empty full SubRelStr of L
the carrier of J is non empty set
bool the carrier of a is non empty set
bool the carrier of J is non empty set
F is Element of bool the carrier of a
c is Element of bool the carrier of J
j is Element of the carrier of J
j is Element of the carrier of J
a is Element of the carrier of a
b is Element of the carrier of a
DZ is Element of the carrier of a
the carrier of L is non empty set
p9 is Element of the carrier of J
a9 is Element of the carrier of L
DZ is Element of the carrier of L
a is Element of the carrier of L
j is Element of the carrier of J
j is Element of the carrier of J
a is Element of the carrier of a
b is Element of the carrier of a
DZ is Element of the carrier of a
the carrier of L is non empty set
p9 is Element of the carrier of J
DZ is Element of the carrier of L
a9 is Element of the carrier of L
a is Element of the carrier of L
L is set
a is RelStr
the carrier of a is set
[:L, the carrier of a:] is set
bool [:L, the carrier of a:] is non empty set
L is set
a is RelStr
the carrier of a is set
[:L, the carrier of a:] is set
bool [:L, the carrier of a:] is non empty set
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
F is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
c is Element of the carrier of L
J . c is Element of the carrier of a
F . c is Element of the carrier of a
j is Element of the carrier of a
j is Element of the carrier of a
c is set
J . c is set
F . c is set
j is Element of the carrier of L
J . j is Element of the carrier of a
F . j is Element of the carrier of a
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
rng J is Element of bool the carrier of a
bool the carrier of a is non empty set
subrelstr (rng J) is strict full SubRelStr of a
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
(L,a,J) is strict full SubRelStr of a
rng J is Element of bool the carrier of a
bool the carrier of a is non empty set
subrelstr (rng J) is strict full SubRelStr of a
the carrier of (L,a,J) is set
F is Element of the carrier of (L,a,J)
dom J is Element of bool the carrier of L
bool the carrier of L is non empty set
c is set
J . c is set
j is Element of the carrier of L
J . j is Element of the carrier of a
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty Element of bool the carrier of L
subrelstr a is strict full SubRelStr of L
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
(L,a,J) is strict full SubRelStr of a
rng J is Element of bool the carrier of a
bool the carrier of a is non empty set
subrelstr (rng J) is strict full SubRelStr of a
dom J is Element of bool the carrier of L
bool the carrier of L is non empty set
L is non empty RelStr
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of 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 non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
a is Element of the carrier of L
J is Element of the carrier of L
(id L) . a is set
(id L) . J is set
(id L) . J is Element of the carrier of L
F is Element of the carrier of L
c is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty RelStr
the carrier of J is non empty set
[: the carrier of a, the carrier of J:] is non empty set
bool [: the carrier of a, the carrier of J:] is non empty set
F is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
c is non empty Relation-like the carrier of a -defined the carrier of J -valued Function-like V30( the carrier of a) V32( the carrier of a, the carrier of J) Element of bool [: the carrier of a, the carrier of J:]
c * F is non empty Relation-like the carrier of L -defined the carrier of J -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of J) Element of bool [: the carrier of L, the carrier of J:]
[: the carrier of L, the carrier of J:] is non empty set
bool [: the carrier of L, the carrier of J:] is non empty set
j is Element of the carrier of L
j is Element of the carrier of L
(c * F) . j is set
(c * F) . j is set
F . j is Element of the carrier of a
F . j is Element of the carrier of a
c . (F . j) is Element of the carrier of J
c . (F . j) is Element of the carrier of J
(c * F) . j is Element of the carrier of J
a is Element of the carrier of J
b is Element of the carrier of J
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
bool the carrier of L is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
F is Element of bool the carrier of L
J .: F is Element of bool the carrier of a
bool the carrier of a is non empty set
c is Element of the carrier of L
J . c is Element of the carrier of a
j is Element of the carrier of a
j is Element of the carrier of L
J . j is Element of the carrier of a
a is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
bool the carrier of L is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
F is Element of bool the carrier of L
J .: F is Element of bool the carrier of a
bool the carrier of a is non empty set
c is Element of the carrier of L
J . c is Element of the carrier of a
j is Element of the carrier of a
j is Element of the carrier of L
J . j is Element of the carrier of a
a is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
bool the carrier of L is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
F is directed Element of bool the carrier of L
J .: F is Element of bool the carrier of a
bool the carrier of a is non empty set
j is Element of the carrier of a
j is Element of the carrier of a
dom J is Element of bool the carrier of L
a is set
J . a is set
b is set
J . b is set
DZ is Element of the carrier of L
DZ is Element of the carrier of L
a is Element of the carrier of L
J . a is Element of the carrier of a
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
J is Element of the carrier of L
F is Element of the carrier of L
a . J is set
a . F is set
F "\/" J is Element of the carrier of L
{J,F} is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
c is Element of the carrier of L
j is Element of the carrier of L
dom a is Element of bool the carrier of L
c is Element of the carrier of L
a .: {J,F} is Element of bool the carrier of L
"\/" ((a .: {J,F}),L) is Element of the carrier of L
"\/" ({J,F},L) is Element of the carrier of L
a . ("\/" ({J,F},L)) is Element of the carrier of L
a . F is Element of the carrier of L
a . J is Element of the carrier of L
{(a . J),(a . F)} is non empty Element of bool the carrier of L
"\/" ({(a . J),(a . F)},L) is Element of the carrier of L
(a . F) "\/" (a . J) is Element of the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
J is Element of the carrier of L
F is Element of the carrier of L
a . J is set
a . F is set
J "/\" F is Element of the carrier of L
{J,F} is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
c is Element of the carrier of L
j is Element of the carrier of L
dom a is Element of bool the carrier of L
c is Element of the carrier of L
a .: {J,F} is Element of bool the carrier of L
"/\" ((a .: {J,F}),L) is Element of the carrier of L
"/\" ({J,F},L) is Element of the carrier of L
a . ("/\" ({J,F},L)) is Element of the carrier of L
a . J is Element of the carrier of L
a . F is Element of the carrier of L
{(a . J),(a . F)} is non empty Element of bool the carrier of L
"/\" ({(a . J),(a . F)},L) is Element of the carrier of L
(a . J) "/\" (a . F) is Element of the carrier of L
c is Element of the carrier of L
j is Element of 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 non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
a * a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
J is Element of the carrier of L
a . J is Element of the carrier of L
a . (a . J) is Element of 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 non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
rng a is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : b₁ = a . b₁ } is set
a * a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
F is set
dom a is Element of bool the carrier of L
c is Element of the carrier of L
a . c is Element of the carrier of L
j is set
a . j is set
F is set
dom a is Element of bool the carrier of L
c is Element of the carrier of L
a . c is Element of the carrier of L
L is set
a is non empty 1-sorted
the carrier of a is non empty set
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of a -defined the carrier of a -valued Function-like V30( the carrier of a) V32( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]
rng J is Element of bool the carrier of a
bool the carrier of a is non empty set
J .: L is Element of bool the carrier of a
{ b₁ where b₁ is Element of the carrier of a : b₁ = J . b₁ } is set
c is set
dom J is Element of bool the carrier of a
j is set
J . j is set
j is Element of the carrier of a
J . j is Element of the carrier of a
c is set
j is Element of the carrier of a
J . j is Element of the carrier of a
L is non empty RelStr
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of 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 non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
(id L) * (id L) is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
the carrier of L /\ the carrier of L is set
id ( the carrier of L /\ the carrier of L) is Relation-like the carrier of L /\ the carrier of L -defined the carrier of L /\ the carrier of L -valued V30( the carrier of L /\ the carrier of L) V32( the carrier of L /\ the carrier of L, the carrier of L /\ the carrier of L) Element of bool [:( the carrier of L /\ the carrier of L),( the carrier of L /\ the carrier of L):]
[:( the carrier of L /\ the carrier of L),( the carrier of L /\ the carrier of L):] is set
bool [:( the carrier of L /\ the carrier of L),( the carrier of L /\ the carrier of L):] is non empty set
L is set
a is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of a is non empty set
"\/" (L,a) is Element of the carrier of a
"/\" (L,a) is Element of the carrier of a
J is Element of the carrier of a
L is non empty RelStr
the carrier of L is non empty set
a is set
{ b₁ where b₁ is Element of the carrier of L : b₁ is_<=_than a } is set
F is Element of the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
c is Element of the carrier of L
a is set
{ b₁ where b₁ is Element of the carrier of L : a is_<=_than b₁ } is set
F is Element of the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
c is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
a is set
"\/" (a,L) is Element of the carrier of L
J is Element of the carrier of L
F is Element of the carrier of L
L is non empty RelStr
a is set
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is set
"/\" (a,L) is Element of the carrier of L
a /\ the carrier of L is set
"/\" ((a /\ the carrier of L),L) is Element of the carrier of L
c is Element of bool the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is set
"\/" (a,L) is Element of the carrier of L
a /\ the carrier of L is set
"\/" ((a /\ the carrier of L),L) is Element of the carrier of L
c is Element of bool the carrier of L
j is Element of the carrier of L
j is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is set
L is non empty reflexive transitive antisymmetric RelStr
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
bool the carrier of L is non empty set
a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
{ b₁ where b₁ is Element of the carrier of L : b₁ = a . b₁ } is set
J is Element of bool the carrier of L
subrelstr J is strict reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr J) is set
bool the carrier of (subrelstr J) is non empty set
c is Element of bool the carrier of (subrelstr J)
{ b₁ where b₁ is Element of the carrier of L : ( c is_<=_than a . b₁ & a . b₁ <= b₁ ) } is set
j is Element of bool the carrier of L
"/\" (j,L) is Element of the carrier of L
a . ("/\" (j,L)) is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a . b is Element of the carrier of L
a . (a . ("/\" (j,L))) is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
DZ is Element of the carrier of L
a . DZ is Element of the carrier of L
a . a is Element of the carrier of L
b is Element of the carrier of L
a . b is Element of the carrier of L
c is Element of bool the carrier of (subrelstr J)
{ b₁ where b₁ is Element of the carrier of L : S₁[b₁] } is set
j is Element of bool the carrier of L
"/\" (j,L) is Element of the carrier of L
j is non empty reflexive transitive antisymmetric RelStr
the carrier of j is non empty set
bool the carrier of j is non empty set
a is Element of bool the carrier of j
{ b₁ where b₁ is Element of the carrier of L : S₂[b₁] } is set
b is Element of bool the carrier of L
"/\" (b,L) is Element of the carrier of L
DZ is Element of the carrier of j
a is Element of the carrier of j
a9 is Element of the carrier of L
a . a9 is Element of the carrier of L
p9 is Element of the carrier of L
u is Element of the carrier of L
a . u is Element of the carrier of L
a is Element of the carrier of j
a9 is Element of the carrier of L
a . a9 is Element of the carrier of L
a is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
a is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of L
the carrier of a is non empty set
bool the carrier of a is non empty set
J is Element of bool the carrier of a
"/\" (J,L) is Element of the carrier of L
the carrier of L is non empty set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
a is non empty reflexive transitive antisymmetric with_suprema full join-inheriting sups-inheriting directed-sups-inheriting SubRelStr of L
the carrier of a is non empty set
bool the carrier of a is non empty set
J is Element of bool the carrier of a
"\/" (J,L) is Element of the carrier of L
the carrier of L is non empty set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
(L,a,J) is non empty strict full SubRelStr of a
rng J is Element of bool the carrier of a
bool the carrier of a is non empty set
subrelstr (rng J) is strict full SubRelStr of a
the carrier of (subrelstr (rng J)) is set
bool the carrier of (subrelstr (rng J)) is non empty set
c is Element of bool the carrier of (subrelstr (rng J))
"\/" (c,a) is Element of the carrier of a
J " c is Element of bool the carrier of L
bool the carrier of L is non empty set
J .: (J " c) is Element of bool the carrier of a
"\/" ((J .: (J " c)),a) is Element of the carrier of a
"\/" ((J " c),L) is Element of the carrier of L
J . ("\/" ((J " c),L)) is Element of the carrier of a
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
a is non empty RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
(L,a,J) is non empty strict full SubRelStr of a
rng J is Element of bool the carrier of a
bool the carrier of a is non empty set
subrelstr (rng J) is strict full SubRelStr of a
the carrier of (subrelstr (rng J)) is set
bool the carrier of (subrelstr (rng J)) is non empty set
c is Element of bool the carrier of (subrelstr (rng J))
"/\" (c,a) is Element of the carrier of a
J " c is Element of bool the carrier of L
bool the carrier of L is non empty set
J .: (J " c) is Element of bool the carrier of a
"/\" ((J .: (J " c)),a) is Element of the carrier of a
"/\" ((J " c),L) is Element of the carrier of L
J . ("/\" ((J " c),L)) is Element of the carrier of a
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
a is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of a is non empty set
[: the carrier of L, the carrier of a:] is non empty set
bool [: the carrier of L, the carrier of a:] is non empty set
J is non empty Relation-like the carrier of L -defined the carrier of a -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of a) Element of bool [: the carrier of L, the carrier of a:]
(L,a,J) is non empty strict reflexive transitive antisymmetric full SubRelStr of a
rng J is Element of bool the carrier of a
bool the carrier of a is non empty set
subrelstr (rng J) is strict reflexive transitive antisymmetric full SubRelStr of a
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
a is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
(L,L,a) is non empty strict reflexive transitive antisymmetric full SubRelStr of L
rng a is Element of bool the carrier of L
bool the carrier of L is non empty set
subrelstr (rng a) is strict reflexive transitive antisymmetric full SubRelStr of L
the Element of the carrier of L is Element of the carrier of L
dom a is Element of bool the carrier of L
a . the Element of the carrier of L is Element of the carrier of L
the carrier of (subrelstr (rng a)) is set
bool the carrier of (subrelstr (rng a)) is non empty set
j is directed Element of bool the carrier of (subrelstr (rng a))
"\/" (j,L) is Element of the carrier of L
c is non empty reflexive transitive antisymmetric full SubRelStr of L
the carrier of c is non empty set
bool the carrier of c is non empty set
j is non empty directed Element of bool the carrier of L
a .: j is Element of bool the carrier of L
"\/" ((a .: j),L) is Element of the carrier of L
"\/" (j,L) is Element of the carrier of L
a . ("\/" (j,L)) is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ = a . b₁ } is set
L is RelStr
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
a is Element of bool (bool the carrier of L)
meet a is Element of bool the carrier of L
J is Element of bool (bool the carrier of L)
meet J is Element of bool the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
j is set
a is Element of bool the carrier of L
L is RelStr
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
a is Element of bool (bool the carrier of L)
meet a is Element of bool the carrier of L
J is Element of bool (bool the carrier of L)
meet J is Element of bool the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
j is set
a is Element of bool the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
a is Element of bool (bool the carrier of L)
meet a is Element of bool the carrier of L
J is Element of bool (bool the carrier of L)
meet J is Element of bool the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
c "\/" j is Element of the carrier of L
j is Element of the carrier of L
a is set
b is Element of bool the carrier of L
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
a is Element of bool (bool the carrier of L)
meet a is Element of bool the carrier of L
J is Element of bool (bool the carrier of L)
meet J is Element of bool the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
F is Element of bool the carrier of L
c is Element of the carrier of L
j is Element of the carrier of L
c "/\" j is Element of the carrier of L
j is Element of the carrier of L
a is set
b is Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty directed lower Element of bool the carrier of L
J is non empty directed lower Element of bool the carrier of L
a /\ J is Element of bool the carrier of L
the Element of a is Element of a
the Element of J is Element of J
the Element of a "/\" the Element of J is Element of the carrier of L
L is non empty reflexive transitive RelStr
Ids L is set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
the Element of the carrier of L is Element of the carrier of L
downarrow the Element of the carrier of L is non empty directed lower Element of bool the carrier of L
{ the Element of the carrier of L} is non empty Element of bool the carrier of L
downarrow { the Element of the carrier of L} is non empty lower Element of bool the carrier of L
L is set
a is non empty reflexive transitive RelStr
Ids a is non empty set
the carrier of a is non empty set
bool the carrier of a is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of a : verum } is set
InclPoset (Ids a) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids a)) is non empty set
J is non empty directed lower Element of bool the carrier of a
L is set
a is non empty reflexive transitive RelStr
Ids a is non empty set
the carrier of a is non empty set
bool the carrier of a is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of a : verum } is set
InclPoset (Ids a) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids a)) is non empty set
J is Element of the carrier of (InclPoset (Ids a))
F is non empty Element of bool the carrier of a
c is Element of F
L is non empty reflexive transitive antisymmetric with_infima RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids L)) is non empty set
a is Element of the carrier of (InclPoset (Ids L))
J is Element of the carrier of (InclPoset (Ids L))
a "/\" J is Element of the carrier of (InclPoset (Ids L))
a /\ J is set
F is non empty directed lower Element of bool the carrier of L
c is non empty directed lower Element of bool the carrier of L
F /\ c is Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
a is set
J is set
a /\ J is set
F is non empty directed lower Element of bool the carrier of L
c is non empty directed lower Element of bool the carrier of L
F /\ c is Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids L)) is non empty set
J is Element of the carrier of (InclPoset (Ids L))
F is Element of the carrier of (InclPoset (Ids L))
{ b₁ where b₁ is Element of the carrier of L : ( b₁ in J or b₁ in F or ex b₂, b₃ being Element of the carrier of L st
( b₂ in J & b₃ in F & b₁ = b₂ "\/" b₃ ) ) } is set
{J,F} is non empty Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
J "\/" F is Element of the carrier of (InclPoset (Ids L))
{ b₁ where b₁ is Element of the carrier of L : S₁[b₁] } is set
c is Element of bool the carrier of L
downarrow c is lower Element of bool the carrier of L
j is non empty directed lower Element of bool the carrier of L
the Element of j is Element of j
b is non empty Element of bool the carrier of L
downarrow b is non empty lower Element of bool the carrier of L
DZ is Element of the carrier of L
a is Element of the carrier of L
a9 is Element of the carrier of L
p9 is Element of the carrier of L
a9 "\/" p9 is Element of the carrier of L
a9 is Element of the carrier of L
p9 is Element of the carrier of L
a9 "\/" p9 is Element of the carrier of L
p9 "\/" DZ is Element of the carrier of L
u is Element of the carrier of L
a9 "\/" u is Element of the carrier of L
z is Element of the carrier of L
j is non empty directed lower Element of bool the carrier of L
DZ is Element of the carrier of L
a is Element of the carrier of L
a9 is Element of the carrier of L
p9 is Element of the carrier of L
a9 "\/" p9 is Element of the carrier of L
a9 is Element of the carrier of L
p9 is Element of the carrier of L
a9 "\/" p9 is Element of the carrier of L
a9 "\/" DZ is Element of the carrier of L
u is Element of the carrier of L
u "\/" p9 is Element of the carrier of L
z is Element of the carrier of L
DZ is Element of the carrier of L
a is Element of the carrier of L
a9 is Element of the carrier of L
p9 is Element of the carrier of L
u is Element of the carrier of L
a9 "\/" p9 is Element of the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
u "\/" z is Element of the carrier of L
u is Element of the carrier of L
p9 "\/" a9 is Element of the carrier of L
j is non empty directed lower Element of bool the carrier of L
u is Element of the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
u "\/" z is Element of the carrier of L
u is Element of the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
u "\/" z is Element of the carrier of L
u is Element of the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
u "\/" z is Element of the carrier of L
u is Element of the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
u "\/" z is Element of the carrier of L
d9 is Element of the carrier of L
d is Element of the carrier of L
d9 "\/" d is Element of the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
u "\/" z is Element of the carrier of L
d9 is Element of the carrier of L
d is Element of the carrier of L
d9 "\/" d is Element of the carrier of L
u "\/" d9 is Element of the carrier of L
z "\/" d is Element of the carrier of L
ac is Element of the carrier of L
bd is Element of the carrier of L
ac "\/" bd is Element of the carrier of L
z is Element of the carrier of L
j is non empty directed lower Element of bool the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
u "\/" z is Element of the carrier of L
d9 is Element of the carrier of L
d is Element of the carrier of L
d9 "\/" d is Element of the carrier of L
DZ is Element of the carrier of (InclPoset (Ids L))
a is Element of the carrier of (InclPoset (Ids L))
a9 is set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in b ) } is set
p9 is Element of the carrier of L
u is Element of the carrier of L
u is Element of the carrier of L
z is Element of the carrier of L
j is non empty directed lower Element of bool the carrier of L
d9 is non empty directed lower Element of bool the carrier of L
d is Element of the carrier of L
ac is Element of the carrier of L
d "\/" ac is Element of the carrier of L
d9 is Element of the carrier of L
d is Element of the carrier of L
d9 "\/" d is Element of the carrier of L
a is set
a9 is Element of the carrier of L
a is set
a9 is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids L)) is non empty set
J is Element of the carrier of (InclPoset (Ids L))
F is Element of the carrier of (InclPoset (Ids L))
J "\/" F is Element of the carrier of (InclPoset (Ids L))
{ b₁ where b₁ is Element of the carrier of L : ( b₁ in J or b₁ in F or ex b₂, b₃ being Element of the carrier of L st
( b₂ in J & b₃ in F & b₁ = b₂ "\/" b₃ ) ) } is set
{J,F} is non empty Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
c is Element of the carrier of (InclPoset (Ids L))
j is Element of bool the carrier of L
downarrow j is lower Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
bool (Ids L) is non empty set
a is non empty Element of bool (Ids L)
meet a is set
J is set
F is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
J is set
J is Element of bool (bool the carrier of L)
F is Element of bool the carrier of L
Bottom L is Element of the carrier of L
c is set
j is non empty directed lower Element of bool the carrier of L
the Element of j is Element of j
F is lower Element of bool the carrier of L
j is Element of bool the carrier of L
c is non empty lower Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema RelStr
the carrier of (InclPoset (Ids L)) is non empty set
bool the carrier of (InclPoset (Ids L)) is non empty set
a is non empty Element of bool the carrier of (InclPoset (Ids L))
"/\" (a,(InclPoset (Ids L))) is Element of the carrier of (InclPoset (Ids L))
meet a is set
bool (Ids L) is non empty set
F is non empty Element of bool (Ids L)
meet F is set
c is Element of the carrier of (InclPoset (Ids L))
j is Element of the carrier of (InclPoset (Ids L))
j is set
a is Element of the carrier of (InclPoset (Ids L))
j is set
a is set
j is Element of the carrier of (InclPoset (Ids L))
j is set
L is non empty reflexive transitive antisymmetric with_suprema RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema RelStr
"/\" ({},(InclPoset (Ids L))) is Element of the carrier of (InclPoset (Ids L))
the carrier of (InclPoset (Ids L)) is non empty set
[#] L is non empty non proper directed lower upper Element of bool the carrier of L
J is Element of the carrier of (InclPoset (Ids L))
F is Element of the carrier of (InclPoset (Ids L))
c is non empty directed lower Element of bool the carrier of L
F is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema RelStr
the carrier of (InclPoset (Ids L)) is non empty set
bool the carrier of (InclPoset (Ids L)) is non empty set
J is Element of bool the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema RelStr
L is non empty reflexive transitive antisymmetric RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids L)) is non empty set
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
J is set
"\/" (J,L) is Element of the carrier of L
J is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
J is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
F is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
c is non empty directed lower Element of bool the carrier of L
F . c is set
"\/" (c,L) is Element of the carrier of L
RelIncl (Ids L) is Relation-like Ids L -defined Ids L -valued V22() V25() V29() V30( Ids L) V32( Ids L, Ids L) Element of bool [:(Ids L),(Ids L):]
[:(Ids L),(Ids L):] is non empty set
bool [:(Ids L),(Ids L):] is non empty set
RelStr(# (Ids L),(RelIncl (Ids L)) #) is strict RelStr
the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) is set
c is non empty directed lower Element of bool the carrier of L
F . c is set
"\/" (c,L) is Element of the carrier of L
J is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
F is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
RelIncl (Ids L) is Relation-like Ids L -defined Ids L -valued V22() V25() V29() V30( Ids L) V32( Ids L, Ids L) Element of bool [:(Ids L),(Ids L):]
[:(Ids L),(Ids L):] is non empty set
bool [:(Ids L),(Ids L):] is non empty set
RelStr(# (Ids L),(RelIncl (Ids L)) #) is strict RelStr
the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) is set
c is set
j is non empty directed lower Element of bool the carrier of L
j is non empty directed lower Element of bool the carrier of L
J . j is set
"\/" (j,L) is Element of the carrier of L
J . c is set
F . c is set
dom J is Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
dom F is Element of bool the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids L)) is non empty set
(L) is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
dom (L) is Element of bool the carrier of (InclPoset (Ids L))
bool the carrier of (InclPoset (Ids L)) is non empty set
rng (L) is Element of bool the carrier of L
RelIncl (Ids L) is Relation-like Ids L -defined Ids L -valued V22() V25() V29() V30( Ids L) V32( Ids L, Ids L) Element of bool [:(Ids L),(Ids L):]
[:(Ids L),(Ids L):] is non empty set
bool [:(Ids L),(Ids L):] is non empty set
RelStr(# (Ids L),(RelIncl (Ids L)) #) is strict RelStr
the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) is set
L is set
a is non empty reflexive transitive antisymmetric RelStr
Ids a is non empty set
the carrier of a is non empty set
bool the carrier of a is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of a : verum } is set
InclPoset (Ids a) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids a)) is non empty set
(a) is non empty Relation-like the carrier of (InclPoset (Ids a)) -defined the carrier of a -valued Function-like V30( the carrier of (InclPoset (Ids a))) V32( the carrier of (InclPoset (Ids a)), the carrier of a) Element of bool [: the carrier of (InclPoset (Ids a)), the carrier of a:]
[: the carrier of (InclPoset (Ids a)), the carrier of a:] is non empty set
bool [: the carrier of (InclPoset (Ids a)), the carrier of a:] is non empty set
dom (a) is Element of bool the carrier of (InclPoset (Ids a))
bool the carrier of (InclPoset (Ids a)) is non empty set
J is non empty directed lower Element of bool the carrier of a
L is non empty reflexive transitive antisymmetric up-complete RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
(L) is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
the carrier of (InclPoset (Ids L)) is non empty set
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
F is Element of the carrier of (InclPoset (Ids L))
c is Element of the carrier of (InclPoset (Ids L))
(L) . F is Element of the carrier of L
(L) . c is Element of the carrier of L
j is non empty directed lower Element of bool the carrier of L
j is non empty directed lower Element of bool the carrier of L
"\/" (j,L) is Element of the carrier of L
"\/" (j,L) is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
L is non empty reflexive transitive antisymmetric up-complete RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
(L) is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V30( the carrier of (InclPoset (Ids L))) V32( the carrier of (InclPoset (Ids L)), the carrier of L) Element of bool [: the carrier of (InclPoset (Ids L)), the carrier of L:]
the carrier of (InclPoset (Ids L)) is non empty set
[: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
bool [: the carrier of (InclPoset (Ids L)), the carrier of L:] is non empty set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Ids L)) is non empty set
[: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
a is Element of the carrier of L
downarrow a is non empty directed lower Element of bool the carrier of L
{a} is non empty Element of bool the carrier of L
downarrow {a} is non empty lower Element of bool the carrier of L
a is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of (InclPoset (Ids L))) Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
J is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of (InclPoset (Ids L))) Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
F is Element of the carrier of L
a . F is Element of the carrier of (InclPoset (Ids L))
downarrow F is non empty directed lower Element of bool the carrier of L
{F} is non empty Element of bool the carrier of L
downarrow {F} is non empty lower Element of bool the carrier of L
J . F is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
(L) is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of (InclPoset (Ids L))) Element of 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 non empty set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
a is Element of the carrier of L
J is Element of the carrier of L
(L) . a is set
(L) . J is set
downarrow a is non empty directed lower Element of bool the carrier of L
{a} is non empty Element of bool the carrier of L
downarrow {a} is non empty lower Element of bool the carrier of L
downarrow J is non empty directed lower Element of bool the carrier of L
{J} is non empty Element of bool the carrier of L
downarrow {J} is non empty lower Element of bool the carrier of L
(L) . a is Element of the carrier of (InclPoset (Ids L))
(L) . J is Element of the carrier of (InclPoset (Ids L))
F is Element of the carrier of (InclPoset (Ids L))
c is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric RelStr
Ids L is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric RelStr
(L) is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids L)) -valued Function-like V30( the carrier of L) V32( the carrier of L, the carrier of (InclPoset (Ids L))) Element of 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 non empty set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
L is non empty RelStr
a is Relation-like set
rng a is set
"\/" ((rng a),L) is Element of the carrier of L
the carrier of L is non empty set
"/\" ((rng a),L) is Element of the carrier of L
L is set
a is non empty RelStr
the carrier of a is non empty set
[:L, the carrier of a:] is set
bool [:L, the carrier of a:] is non empty set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
a is non empty set
[:a, the carrier of L:] is non empty set
bool [:a, the carrier of L:] is non empty set
J is Element of a
F is non empty Relation-like a -defined the carrier of L -valued Function-like V30(a) V32(a, the carrier of L) Element of bool [:a, the carrier of L:]
F . J is Element of the carrier of L
(L,F) is Element of the carrier of L
rng F is set
"\/" ((rng F),L) is Element of the carrier of L
(L,F) is Element of the carrier of L
"/\" ((rng F),L) is Element of the carrier of L
rng F is Element of bool the carrier of L
bool the carrier of L is non empty set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
a is Element of the carrier of L
J is non empty set
[:J, the carrier of L:] is non empty set
bool [:J, the carrier of L:] is non empty set
F is non empty Relation-like J -defined the carrier of L -valued Function-like V30(J) V32(J, the carrier of L) Element of bool [:J, the carrier of L:]
(L,F) is Element of the carrier of L
rng F is set
"\/" ((rng F),L) is Element of the carrier of L
c is Element of the carrier of L
rng F is Element of bool the carrier of L
bool the carrier of L is non empty set
dom F is Element of bool J
bool J is non empty set
j is set
F . j is set
j is Element of J
F . j is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr
the carrier of L is non empty set
a is Element of the carrier of L
J is non empty set
[:J, the carrier of L:] is non empty set
bool [:J, the carrier of L:] is non empty set
F is non empty Relation-like J -defined the carrier of L -valued Function-like V30(J) V32(J, the carrier of L) Element of bool [:J, the carrier of L:]
(L,F) is Element of the carrier of L
rng F is set
"/\" ((rng F),L) is Element of the carrier of L
c is Element of the carrier of L
rng F is Element of bool the carrier of L
bool the carrier of L is non empty set
dom F is Element of bool J
bool J is non empty set
j is set
F . j is set
j is Element of J
F . j is Element of the carrier of L