:: 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

( b

{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

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

( b

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

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

( b

{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

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

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

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

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

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

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

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

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

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

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

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

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

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