:: YELLOW_7 semantic presentation

K225() is set

K229() is non empty V5() V24() V25() V26() non finite V36() V37() countable denumerable Element of K32(K225())

K32(K225()) is non empty set

K113() is non empty V5() V24() V25() V26() non finite V36() V37() countable denumerable set

K32(K113()) is non empty V5() non finite set

K32(K229()) is non empty V5() non finite set

K274() is set

{} is set

the empty Function-like functional V24() V25() V26() V28() V29() V30() finite V35() V36() V38( {} ) countable set is empty Function-like functional V24() V25() V26() V28() V29() V30() finite V35() V36() V38( {} ) countable set

{{}} is non empty V5() finite V38(1) countable set

1 is non empty V24() V25() V26() V30() finite V36() countable Element of K229()

K252({{}}) is M15({{}})

K33(K252({{}}),{{}}) is set

K32(K33(K252({{}}),{{}})) is non empty set

K95(K252({{}}),{{}}) is set

{{},1} is finite countable set

K33(1,1) is non empty finite countable set

K32(K33(1,1)) is non empty finite V35() countable set

K33(K33(1,1),1) is non empty finite countable set

K32(K33(K33(1,1),1)) is non empty finite V35() countable set

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

J is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

~ J is Element of the carrier of L

(~ J) ~ is Element of the carrier of (L ~)

(~ K) ~ is Element of the carrier of (L ~)

L is RelStr

the carrier of L is set

L ~ is strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

J is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

~ (J ~) is Element of the carrier of L

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is RelStr

J ~ is strict RelStr

the carrier of J is set

the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

K33( the carrier of J, the carrier of J) is set

K32(K33( the carrier of J, the carrier of J)) is non empty set

the InternalRel of J ~ is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

RelStr(# the carrier of J,( the InternalRel of J ~) #) is strict RelStr

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is set

the carrier of (L ~) is set

[J,J] is set

{J,J} is finite countable set

{J} is non empty V5() finite V38(1) countable set

{{J,J},{J}} is finite V35() countable set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

the carrier of (L ~) is set

K33( the carrier of (L ~), the carrier of (L ~)) is set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

J is set

[J,J] is set

{J,J} is finite countable set

{J} is non empty V5() finite V38(1) countable set

{{J,J},{J}} is finite V35() countable set

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

J is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

~ J is Element of the carrier of L

J is Element of the carrier of L

K is Element of the carrier of L

K ~ is Element of the carrier of (L ~)

the carrier of (L ~) is set

J ~ is Element of the carrier of (L ~)

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

J is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

F is Element of the carrier of (L ~)

~ K is Element of the carrier of L

~ J is Element of the carrier of L

~ F is Element of the carrier of L

J is Element of the carrier of L

K is Element of the carrier of L

F is Element of the carrier of L

K ~ is Element of the carrier of (L ~)

the carrier of (L ~) is set

J ~ is Element of the carrier of (L ~)

F ~ is Element of the carrier of (L ~)

L is non empty RelStr

L ~ is non empty strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

J is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

~ J is Element of the carrier of L

~ K is Element of the carrier of L

the carrier of (L ~) is non empty set

J is Element of the carrier of L

K is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

K ~ is Element of the carrier of (L ~)

L is reflexive RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is transitive RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is antisymmetric RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is non empty connected RelStr

L ~ is non empty strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is RelStr

the carrier of L is set

L ~ is strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

the carrier of (L ~) is set

K is set

F is RelStr

the carrier of F is set

a is set

G is Element of the carrier of F

F ~ is strict RelStr

the InternalRel of F is Relation-like the carrier of F -defined the carrier of F -valued Element of K32(K33( the carrier of F, the carrier of F))

K33( the carrier of F, the carrier of F) is set

K32(K33( the carrier of F, the carrier of F)) is non empty set

the InternalRel of F ~ is Relation-like the carrier of F -defined the carrier of F -valued Element of K32(K33( the carrier of F, the carrier of F))

RelStr(# the carrier of F,( the InternalRel of F ~) #) is strict RelStr

G ~ is Element of the carrier of (F ~)

the carrier of (F ~) is set

K9 is Element of the carrier of (F ~)

~ K9 is Element of the carrier of F

(~ K9) ~ is Element of the carrier of (F ~)

F is RelStr

the carrier of F is set

a is set

G is Element of the carrier of F

F ~ is strict RelStr

the InternalRel of F is Relation-like the carrier of F -defined the carrier of F -valued Element of K32(K33( the carrier of F, the carrier of F))

K33( the carrier of F, the carrier of F) is set

K32(K33( the carrier of F, the carrier of F)) is non empty set

the InternalRel of F ~ is Relation-like the carrier of F -defined the carrier of F -valued Element of K32(K33( the carrier of F, the carrier of F))

RelStr(# the carrier of F,( the InternalRel of F ~) #) is strict RelStr

G ~ is Element of the carrier of (F ~)

the carrier of (F ~) is set

K9 is Element of the carrier of (F ~)

~ K9 is Element of the carrier of F

(~ K9) ~ is Element of the carrier of (F ~)

(L ~) ~ is strict RelStr

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

the InternalRel of (L ~) ~ is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

RelStr(# the carrier of (L ~),( the InternalRel of (L ~) ~) #) is strict RelStr

(J ~) ~ is Element of the carrier of ((L ~) ~)

the carrier of ((L ~) ~) is set

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

J is Element of the carrier of (L ~)

~ J is Element of the carrier of L

K is set

(~ J) ~ is Element of the carrier of (L ~)

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is set

K is Element of the carrier of L

K ~ is Element of the carrier of (L ~)

the carrier of (L ~) is set

F is Element of the carrier of (L ~)

~ F is Element of the carrier of L

F is Element of the carrier of (L ~)

~ F is Element of the carrier of L

G is Element of the carrier of L

G ~ is Element of the carrier of (L ~)

the carrier of (L ~) is set

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

F is Element of the carrier of L

F ~ is Element of the carrier of (L ~)

F is Element of the carrier of L

F ~ is Element of the carrier of (L ~)

G is Element of the carrier of (L ~)

~ G is Element of the carrier of L

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is set

(L ~) ~ is strict RelStr

the carrier of (L ~) is set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

the InternalRel of (L ~) ~ is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

RelStr(# the carrier of (L ~),( the InternalRel of (L ~) ~) #) is strict RelStr

L is non empty RelStr

L ~ is non empty strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is set

"\/" (J,L) is Element of the carrier of L

"/\" (J,(L ~)) is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

("\/" (J,L)) ~ is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

L is non empty RelStr

L ~ is non empty strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is set

"/\" (J,L) is Element of the carrier of L

"\/" (J,(L ~)) is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

("/\" (J,L)) ~ is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

L is RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

J is RelStr

the carrier of J is set

the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

K33( the carrier of J, the carrier of J) is set

K32(K33( the carrier of J, the carrier of J)) is non empty set

RelStr(# the carrier of J, the InternalRel of J #) is strict RelStr

K is Element of the carrier of J

F is Element of the carrier of J

G is Element of the carrier of L

a is Element of the carrier of L

K9 is Element of the carrier of L

G is Element of the carrier of J

g is Element of the carrier of J

g9 is Element of the carrier of L

L is RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

J is RelStr

the carrier of J is set

the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

K33( the carrier of J, the carrier of J) is set

K32(K33( the carrier of J, the carrier of J)) is non empty set

RelStr(# the carrier of J, the InternalRel of J #) is strict RelStr

K is Element of the carrier of J

F is Element of the carrier of J

G is Element of the carrier of L

a is Element of the carrier of L

K9 is Element of the carrier of L

G is Element of the carrier of J

g is Element of the carrier of J

g9 is Element of the carrier of L

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

(L ~) ~ is strict RelStr

the carrier of (L ~) is set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

the InternalRel of (L ~) ~ is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

RelStr(# the carrier of (L ~),( the InternalRel of (L ~) ~) #) is strict RelStr

L is non empty RelStr

L ~ is non empty strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is non empty RelStr

J ~ is non empty strict RelStr

the carrier of J is non empty set

the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

K33( the carrier of J, the carrier of J) is non empty set

K32(K33( the carrier of J, the carrier of J)) is non empty set

the InternalRel of J ~ is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

RelStr(# the carrier of J,( the InternalRel of J ~) #) is strict RelStr

the carrier of (J ~) is non empty set

K is set

{ b

G is Element of the carrier of J

G ~ is Element of the carrier of (J ~)

a is Element of the carrier of (J ~)

K9 is Element of the carrier of (J ~)

~ K9 is Element of the carrier of J

G is Element of the carrier of J

g is Element of the carrier of J

K9 is Element of the carrier of (J ~)

~ K9 is Element of the carrier of J

~ a is Element of the carrier of J

(L ~) ~ is non empty strict RelStr

the carrier of (L ~) is non empty set

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is non empty set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

the InternalRel of (L ~) ~ is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

RelStr(# the carrier of (L ~),( the InternalRel of (L ~) ~) #) is strict RelStr

L is non empty with_infima RelStr

L ~ is non empty strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is non empty with_suprema RelStr

L ~ is non empty strict RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is non empty with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr

L ~ is non empty strict with_suprema with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is non empty RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

L ~ is non empty strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

K32( the carrier of (L ~)) is non empty set

J is Element of K32( the carrier of L)

fininfs J is Element of K32( the carrier of L)

K32(J) is non empty set

{ ("/\" (b

finsups J is Element of K32( the carrier of L)

{ ("\/" (b

K is Element of K32( the carrier of (L ~))

finsups K is Element of K32( the carrier of (L ~))

K32(K) is non empty set

{ ("\/" (b

fininfs K is Element of K32( the carrier of (L ~))

{ ("/\" (b

F is set

G is finite countable Element of K32(J)

"/\" (G,L) is Element of the carrier of L

"\/" (G,(L ~)) is Element of the carrier of (L ~)

F is set

G is finite countable Element of K32(K)

"\/" (G,(L ~)) is Element of the carrier of (L ~)

"/\" (G,L) is Element of the carrier of L

F is set

G is finite countable Element of K32(J)

"\/" (G,L) is Element of the carrier of L

"/\" (G,(L ~)) is Element of the carrier of (L ~)

F is set

G is finite countable Element of K32(K)

"/\" (G,(L ~)) is Element of the carrier of (L ~)

"\/" (G,L) is Element of the carrier of L

L is RelStr

the carrier of L is set

K32( the carrier of L) is non empty set

L ~ is strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

K32( the carrier of (L ~)) is non empty set

J is Element of K32( the carrier of L)

downarrow J is Element of K32( the carrier of L)

uparrow J is Element of K32( the carrier of L)

K is Element of K32( the carrier of (L ~))

uparrow K is Element of K32( the carrier of (L ~))

downarrow K is Element of K32( the carrier of (L ~))

F is set

G is Element of the carrier of L

a is Element of the carrier of L

a ~ is Element of the carrier of (L ~)

G ~ is Element of the carrier of (L ~)

F is set

G is Element of the carrier of (L ~)

a is Element of the carrier of (L ~)

~ G is Element of the carrier of L

~ a is Element of the carrier of L

F is set

G is Element of the carrier of L

a is Element of the carrier of L

G ~ is Element of the carrier of (L ~)

a ~ is Element of the carrier of (L ~)

F is set

G is Element of the carrier of (L ~)

a is Element of the carrier of (L ~)

~ a is Element of the carrier of L

~ G is Element of the carrier of L

L is non empty RelStr

the carrier of L is non empty set

L ~ is non empty strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

J is Element of the carrier of L

K is Element of the carrier of (L ~)

downarrow J is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

K80( the carrier of L,J) is non empty V5() finite V38(1) countable Element of K32( the carrier of L)

downarrow K80( the carrier of L,J) is Element of K32( the carrier of L)

uparrow K is Element of K32( the carrier of (L ~))

K32( the carrier of (L ~)) is non empty set

K80( the carrier of (L ~),K) is non empty V5() finite V38(1) countable Element of K32( the carrier of (L ~))

uparrow K80( the carrier of (L ~),K) is Element of K32( the carrier of (L ~))

uparrow J is Element of K32( the carrier of L)

uparrow K80( the carrier of L,J) is Element of K32( the carrier of L)

downarrow K is Element of K32( the carrier of (L ~))

downarrow K80( the carrier of (L ~),K) is Element of K32( the carrier of (L ~))

L is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

L ~ is non empty strict reflexive transitive antisymmetric with_suprema RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is Element of the carrier of L

K is Element of the carrier of L

J "/\" K is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

K ~ is Element of the carrier of (L ~)

(J ~) "\/" (K ~) is Element of the carrier of (L ~)

(J "/\" K) ~ is Element of the carrier of (L ~)

~ (J ~) is Element of the carrier of L

~ (K ~) is Element of the carrier of L

F is Element of the carrier of (L ~)

~ F is Element of the carrier of L

(~ F) ~ is Element of the carrier of (L ~)

L is non empty reflexive transitive antisymmetric with_infima RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

J is Element of the carrier of (L ~)

~ J is Element of the carrier of L

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

(~ J) "/\" (~ K) is Element of the carrier of L

J "\/" K is Element of the carrier of (L ~)

(~ J) ~ is Element of the carrier of (L ~)

(~ K) ~ is Element of the carrier of (L ~)

L is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

L ~ is non empty strict reflexive transitive antisymmetric with_infima RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is Element of the carrier of L

K is Element of the carrier of L

J "\/" K is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

K ~ is Element of the carrier of (L ~)

(J ~) "/\" (K ~) is Element of the carrier of (L ~)

(J "\/" K) ~ is Element of the carrier of (L ~)

~ (J ~) is Element of the carrier of L

~ (K ~) is Element of the carrier of L

F is Element of the carrier of (L ~)

~ F is Element of the carrier of L

(~ F) ~ is Element of the carrier of (L ~)

L is non empty reflexive transitive antisymmetric with_suprema RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

J is Element of the carrier of (L ~)

~ J is Element of the carrier of L

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

(~ J) "\/" (~ K) is Element of the carrier of L

J "/\" K is Element of the carrier of (L ~)

(~ J) ~ is Element of the carrier of (L ~)

(~ K) ~ is Element of the carrier of (L ~)

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

J is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

F is Element of the carrier of (L ~)

K "\/" F is Element of the carrier of (L ~)

J "/\" (K "\/" F) is Element of the carrier of (L ~)

J "/\" K is Element of the carrier of (L ~)

J "/\" F is Element of the carrier of (L ~)

(J "/\" K) "\/" (J "/\" F) is Element of the carrier of (L ~)

K "\/" F is Element of the carrier of (L ~)

J "/\" (K "\/" F) is Element of the carrier of (L ~)

~ J is Element of the carrier of L

~ (K "\/" F) is Element of the carrier of L

(~ J) "\/" (~ (K "\/" F)) is Element of the carrier of L

~ K is Element of the carrier of L

~ F is Element of the carrier of L

(~ K) "/\" (~ F) is Element of the carrier of L

(~ J) "\/" ((~ K) "/\" (~ F)) is Element of the carrier of L

(~ J) "\/" (~ K) is Element of the carrier of L

(~ J) "\/" (~ F) is Element of the carrier of L

((~ J) "\/" (~ K)) "/\" ((~ J) "\/" (~ F)) is Element of the carrier of L

J "/\" K is Element of the carrier of (L ~)

~ (J "/\" K) is Element of the carrier of L

(~ (J "/\" K)) "/\" ((~ J) "\/" (~ F)) is Element of the carrier of L

J "/\" F is Element of the carrier of (L ~)

~ (J "/\" F) is Element of the carrier of L

(~ (J "/\" K)) "/\" (~ (J "/\" F)) is Element of the carrier of L

(J "/\" K) "\/" (J "/\" F) is Element of the carrier of (L ~)

J is Element of the carrier of L

K is Element of the carrier of L

F is Element of the carrier of L

K "\/" F is Element of the carrier of L

J "/\" (K "\/" F) is Element of the carrier of L

J "/\" K is Element of the carrier of L

J "/\" F is Element of the carrier of L

(J "/\" K) "\/" (J "/\" F) is Element of the carrier of L

K "\/" F is Element of the carrier of L

J "/\" (K "\/" F) is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

(K "\/" F) ~ is Element of the carrier of (L ~)

(J ~) "\/" ((K "\/" F) ~) is Element of the carrier of (L ~)

K ~ is Element of the carrier of (L ~)

F ~ is Element of the carrier of (L ~)

(K ~) "/\" (F ~) is Element of the carrier of (L ~)

(J ~) "\/" ((K ~) "/\" (F ~)) is Element of the carrier of (L ~)

(J ~) "\/" (K ~) is Element of the carrier of (L ~)

(J ~) "\/" (F ~) is Element of the carrier of (L ~)

((J ~) "\/" (K ~)) "/\" ((J ~) "\/" (F ~)) is Element of the carrier of (L ~)

J "/\" K is Element of the carrier of L

(J "/\" K) ~ is Element of the carrier of (L ~)

((J "/\" K) ~) "/\" ((J ~) "\/" (F ~)) is Element of the carrier of (L ~)

J "/\" F is Element of the carrier of L

(J "/\" F) ~ is Element of the carrier of (L ~)

((J "/\" K) ~) "/\" ((J "/\" F) ~) is Element of the carrier of (L ~)

(J "/\" K) "\/" (J "/\" F) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima distributive RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is RelStr

the carrier of L is set

K32( the carrier of L) is non empty set

L ~ is strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

K32( the carrier of (L ~)) is non empty set

J is set

K is directed Element of K32( the carrier of L)

F is Element of K32( the carrier of (L ~))

G is Element of the carrier of (L ~)

a is Element of the carrier of (L ~)

~ G is Element of the carrier of L

~ a is Element of the carrier of L

K9 is Element of the carrier of L

K9 ~ is Element of the carrier of (L ~)

~ (K9 ~) is Element of the carrier of L

K is filtered Element of K32( the carrier of (L ~))

F is Element of K32( the carrier of L)

G is Element of the carrier of L

a is Element of the carrier of L

G ~ is Element of the carrier of (L ~)

a ~ is Element of the carrier of (L ~)

K9 is Element of the carrier of (L ~)

~ K9 is Element of the carrier of L

(~ K9) ~ is Element of the carrier of (L ~)

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

K32( the carrier of (L ~)) is non empty set

K32( the carrier of L) is non empty set

J is set

(L ~) ~ is strict RelStr

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

the InternalRel of (L ~) ~ is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

RelStr(# the carrier of (L ~),( the InternalRel of (L ~) ~) #) is strict RelStr

the carrier of ((L ~) ~) is set

K32( the carrier of ((L ~) ~)) is non empty set

L is RelStr

the carrier of L is set

K32( the carrier of L) is non empty set

L ~ is strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

K32( the carrier of (L ~)) is non empty set

J is set

K is lower Element of K32( the carrier of L)

F is Element of K32( the carrier of (L ~))

G is Element of the carrier of (L ~)

a is Element of the carrier of (L ~)

~ a is Element of the carrier of L

~ G is Element of the carrier of L

K is upper Element of K32( the carrier of (L ~))

F is Element of K32( the carrier of L)

G is Element of the carrier of L

a is Element of the carrier of L

G ~ is Element of the carrier of (L ~)

a ~ is Element of the carrier of (L ~)

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

K32( the carrier of (L ~)) is non empty set

K32( the carrier of L) is non empty set

J is set

(L ~) ~ is strict RelStr

the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

the InternalRel of (L ~) ~ is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

RelStr(# the carrier of (L ~),( the InternalRel of (L ~) ~) #) is strict RelStr

the carrier of ((L ~) ~) is set

K32( the carrier of ((L ~) ~)) is non empty set

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

the carrier of (L ~) is set

the carrier of (L ~) is set

J is Element of the carrier of (L ~)

~ J is Element of the carrier of L

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is set

J 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 ~)

the carrier of (L ~) is set

L is RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is non empty antisymmetric lower-bounded RelStr

Bottom L is Element of the carrier of L

the carrier of L is non empty set

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

(Bottom L) ~ is Element of the carrier of (L ~)

L ~ is non empty strict antisymmetric RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

Top (L ~) is Element of the carrier of (L ~)

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

J is non empty antisymmetric lower-bounded RelStr

J ~ is non empty strict antisymmetric RelStr

the carrier of J is non empty set

the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

K33( the carrier of J, the carrier of J) is non empty set

K32(K33( the carrier of J, the carrier of J)) is non empty set

the InternalRel of J ~ is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

RelStr(# the carrier of J,( the InternalRel of J ~) #) is strict RelStr

Top (J ~) is Element of the carrier of (J ~)

the carrier of (J ~) is non empty set

"/\" ({},(J ~)) is Element of the carrier of (J ~)

~ (Top (J ~)) is Element of the carrier of J

Bottom J is Element of the carrier of J

"\/" ({},J) is Element of the carrier of J

L is non empty antisymmetric upper-bounded RelStr

Top L is Element of the carrier of L

the carrier of L is non empty set

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

(Top L) ~ is Element of the carrier of (L ~)

L ~ is non empty strict antisymmetric RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

Bottom (L ~) is Element of the carrier of (L ~)

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

J is non empty antisymmetric upper-bounded RelStr

J ~ is non empty strict antisymmetric RelStr

the carrier of J is non empty set

the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

K33( the carrier of J, the carrier of J) is non empty set

K32(K33( the carrier of J, the carrier of J)) is non empty set

the InternalRel of J ~ is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

RelStr(# the carrier of J,( the InternalRel of J ~) #) is strict RelStr

Bottom (J ~) is Element of the carrier of (J ~)

the carrier of (J ~) is non empty set

"\/" ({},(J ~)) is Element of the carrier of (J ~)

~ (Bottom (J ~)) is Element of the carrier of J

Top J is Element of the carrier of J

"/\" ({},J) is Element of the carrier of J

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded RelStr

the carrier of L is non empty set

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is Element of the carrier of L

K is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

K ~ is Element of the carrier of (L ~)

J "/\" K is Element of the carrier of L

Bottom L is Element of the carrier of L

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

(J ~) "\/" (K ~) is Element of the carrier of (L ~)

(Bottom L) ~ is Element of the carrier of (L ~)

Top (L ~) is Element of the carrier of (L ~)

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

J "\/" K is Element of the carrier of L

Top L is Element of the carrier of L

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

(J ~) "/\" (K ~) is Element of the carrier of (L ~)

(Top L) ~ is Element of the carrier of (L ~)

Bottom (L ~) is Element of the carrier of (L ~)

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

J "/\" K is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

J is Element of the carrier of (L ~)

~ J is Element of the carrier of L

K is Element of the carrier of L

K ~ is Element of the carrier of (L ~)

(~ J) ~ is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

J is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

K is Element of the carrier of (L ~)

~ K is Element of the carrier of L

(~ K) ~ is Element of the carrier of (L ~)

L is lower-bounded RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is upper-bounded RelStr

L ~ is strict RelStr

the carrier of L is set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded complemented RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

the carrier of L is non empty set

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

J is Element of the carrier of L

J ~ is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

'not' (J ~) is Element of the carrier of (L ~)

Bottom (L ~) is Element of the carrier of (L ~)

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

(J ~) => (Bottom (L ~)) is Element of the carrier of (L ~)

(J ~) => is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Function-like V18( the carrier of (L ~), the carrier of (L ~)) Element of K32(K33( the carrier of (L ~), the carrier of (L ~)))

K33( the carrier of (L ~), the carrier of (L ~)) is non empty set

K32(K33( the carrier of (L ~), the carrier of (L ~))) is non empty set

((J ~) =>) . (Bottom (L ~)) is Element of the carrier of (L ~)

'not' J is Element of the carrier of L

Bottom L is Element of the carrier of L

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

J => (Bottom L) is Element of the carrier of L

J => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(J =>) . (Bottom L) is Element of the carrier of L

K is Element of the carrier of L

'not' K is Element of the carrier of L

K => (Bottom L) is Element of the carrier of L

K => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(K =>) . (Bottom L) is Element of the carrier of L

'not' ('not' K) is Element of the carrier of L

('not' K) => (Bottom L) is Element of the carrier of L

('not' K) => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(('not' K) =>) . (Bottom L) is Element of the carrier of L

('not' J) ~ is Element of the carrier of (L ~)

L is non empty RelStr

the carrier of L is non empty set

L ~ is non empty strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

K33( the carrier of L, the carrier of (L ~)) is non empty set

K32(K33( the carrier of L, the carrier of (L ~))) is non empty set

J is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

K is Relation-like the carrier of L -defined the carrier of (L ~) -valued Function-like V18( the carrier of L, the carrier of (L ~)) Element of K32(K33( the carrier of L, the carrier of (L ~)))

F is Element of the carrier of L

K . F is Element of the carrier of (L ~)

'not' F is Element of the carrier of L

Bottom L is Element of the carrier of L

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

F => (Bottom L) is Element of the carrier of L

F => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(F =>) . (Bottom L) is Element of the carrier of L

J is Relation-like the carrier of L -defined the carrier of (L ~) -valued Function-like V18( the carrier of L, the carrier of (L ~)) Element of K32(K33( the carrier of L, the carrier of (L ~)))

K is Relation-like the carrier of L -defined the carrier of (L ~) -valued Function-like V18( the carrier of L, the carrier of (L ~)) Element of K32(K33( the carrier of L, the carrier of (L ~)))

F is Element of the carrier of L

J . F is Element of the carrier of (L ~)

'not' F is Element of the carrier of L

Bottom L is Element of the carrier of L

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

F => (Bottom L) is Element of the carrier of L

F => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(F =>) . (Bottom L) is Element of the carrier of L

K . F is Element of the carrier of (L ~)

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

(L) is Relation-like the carrier of L -defined the carrier of (L ~) -valued Function-like V18( the carrier of L, the carrier of (L ~)) Element of K32(K33( the carrier of L, the carrier of (L ~)))

the carrier of L is non empty set

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

K33( the carrier of L, the carrier of (L ~)) is non empty set

K32(K33( the carrier of L, the carrier of (L ~))) is non empty set

J is Element of the carrier of L

(L) . J is Element of the carrier of (L ~)

K is Element of the carrier of L

(L) . K is Element of the carrier of (L ~)

'not' J is Element of the carrier of L

Bottom L is Element of the carrier of L

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

J => (Bottom L) is Element of the carrier of L

J => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(J =>) . (Bottom L) is Element of the carrier of L

'not' ('not' J) is Element of the carrier of L

('not' J) => (Bottom L) is Element of the carrier of L

('not' J) => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(('not' J) =>) . (Bottom L) is Element of the carrier of L

'not' K is Element of the carrier of L

K => (Bottom L) is Element of the carrier of L

K => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(K =>) . (Bottom L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

(L) is Relation-like the carrier of L -defined the carrier of (L ~) -valued Function-like one-to-one V18( the carrier of L, the carrier of (L ~)) Element of K32(K33( the carrier of L, the carrier of (L ~)))

the carrier of (L ~) is non empty set

K33( the carrier of L, the carrier of (L ~)) is non empty set

K32(K33( the carrier of L, the carrier of (L ~))) is non empty set

dom (L) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

rng (L) is Element of K32( the carrier of (L ~))

K32( the carrier of (L ~)) is non empty set

K is set

F is Element of the carrier of L

'not' F is Element of the carrier of L

Bottom L is Element of the carrier of L

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

F => (Bottom L) is Element of the carrier of L

F => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(F =>) . (Bottom L) is Element of the carrier of L

'not' ('not' F) is Element of the carrier of L

('not' F) => (Bottom L) is Element of the carrier of L

('not' F) => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(('not' F) =>) . (Bottom L) is Element of the carrier of L

(L) . ('not' F) is Element of the carrier of (L ~)

K is Element of the carrier of L

(L) . K is Element of the carrier of (L ~)

'not' K is Element of the carrier of L

Bottom L is Element of the carrier of L

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

K => (Bottom L) is Element of the carrier of L

K => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(K =>) . (Bottom L) is Element of the carrier of L

('not' K) ~ is Element of the carrier of (L ~)

F is Element of the carrier of L

(L) . F is Element of the carrier of (L ~)

'not' F is Element of the carrier of L

F => (Bottom L) is Element of the carrier of L

F => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(F =>) . (Bottom L) is Element of the carrier of L

('not' F) ~ is Element of the carrier of (L ~)

'not' ('not' K) is Element of the carrier of L

('not' K) => (Bottom L) is Element of the carrier of L

('not' K) => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(('not' K) =>) . (Bottom L) is Element of the carrier of L

'not' ('not' F) is Element of the carrier of L

('not' F) => (Bottom L) is Element of the carrier of L

('not' F) => is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

(('not' F) =>) . (Bottom L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

L ~ is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean RelStr

the carrier of L is non empty set

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

(L) is Relation-like the carrier of L -defined the carrier of (L ~) -valued Function-like one-to-one V18( the carrier of L, the carrier of (L ~)) monotone isomorphic Element of K32(K33( the carrier of L, the carrier of (L ~)))

the carrier of (L ~) is non empty set

K33( the carrier of L, the carrier of (L ~)) is non empty set

K32(K33( the carrier of L, the carrier of (L ~))) is non empty set

K is set

L is non empty RelStr

the carrier of L is non empty set

J is non empty RelStr

the carrier of J is non empty set

K33( the carrier of L, the carrier of J) is non empty set

K32(K33( the carrier of L, the carrier of J)) is non empty set

L ~ is non empty strict RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

K33( the carrier of L, the carrier of L) is non empty set

K32(K33( the carrier of L, the carrier of L)) is non empty set

the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of K32(K33( the carrier of L, the carrier of L))

RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr

the carrier of (L ~) is non empty set

K33( the carrier of (L ~), the carrier of J) is non empty set

K32(K33( the carrier of (L ~), the carrier of J)) is non empty set

a is set

F is non empty RelStr

F ~ is non empty strict RelStr

the carrier of F is non empty set

the InternalRel of F is Relation-like the carrier of F -defined the carrier of F -valued Element of K32(K33( the carrier of F, the carrier of F))

K33( the carrier of F, the carrier of F) is non empty set

K32(K33( the carrier of F, the carrier of F)) is non empty set

the InternalRel of F ~ is Relation-like the carrier of F -defined the carrier of F -valued Element of K32(K33( the carrier of F, the carrier of F))

RelStr(# the carrier of F,( the InternalRel of F ~) #) is strict RelStr

the carrier of (F ~) is non empty set

G is non empty RelStr

the carrier of G is non empty set

K33( the carrier of (F ~), the carrier of G) is non empty set

K32(K33( the carrier of (F ~), the carrier of G)) is non empty set

K33( the carrier of F, the carrier of G) is non empty set

K32(K33( the carrier of F, the carrier of G)) is non empty set

g is set

K9 is non empty RelStr

the carrier of K9 is non empty set

G is non empty RelStr

the carrier of G is non empty set

K33( the carrier of K9, the carrier of G) is non empty set

K32(K33( the carrier of K9, the carrier of G)) is non empty set

G ~ is non empty strict RelStr

the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of K32(K33( the carrier of G, the carrier of G))

K33( the carrier of G, the carrier of G) is non empty set

K32(K33( the carrier of G, the carrier of G)) is non empty set

the InternalRel of G ~ is Relation-like the carrier of G -defined the carrier of G -valued Element of K32(K33( the carrier of G, the carrier of G))

RelStr(# the carrier of G,( the InternalRel of G ~) #) is strict RelStr

the carrier of (G ~) is non empty set

K33( the carrier of K9, the carrier of (G ~)) is non empty set

K32(K33( the carrier of K9, the carrier of (G ~))) is non empty set

z is set

g9 is non empty RelStr

the carrier of g9 is non empty set

j is non empty RelStr

j ~ is non empty strict RelStr

the carrier of j is non empty set

the InternalRel of j is Relation-like the carrier of j -defined the carrier of j -valued Element of K32(K33( the carrier of j, the carrier of j))

K33( the carrier of j, the carrier of j) is non empty set

K32(K33( the carrier of j, the carrier of j)) is non empty set

the InternalRel of j ~ is Relation-like the carrier of j -defined the carrier of j -valued Element of K32(K33( the carrier of j, the carrier of j))

RelStr(# the carrier of j,( the InternalRel of j ~) #) is strict RelStr

the carrier of (j ~) is non empty set

K33( the carrier of g9, the carrier of (j ~)) is non empty set

K32(K33( the carrier of g9, the carrier of (j ~))) is non empty set

K33( the carrier of g9, the carrier of j) is non empty set

K32(K33( the carrier of g9, the carrier of j)) is non empty set

f is set

u is non empty RelStr

the carrier of u is non empty set

u is non empty RelStr

the carrier of u is non empty set

K33( the carrier of u, the carrier of u) is non empty set

K32(K33( the carrier of u, the carrier of u)) is non empty set

u ~ is non empty strict RelStr

the InternalRel of u is Relation-like the carrier of u -defined the carrier of u -valued Element of K32(K33( the carrier of u, the carrier of u))

K33( the carrier of u, the carrier of u) is non empty set

K32(K33( the carrier of u, the carrier of u)) is non empty set

the InternalRel of u ~ is Relation-like the carrier of u -defined the carrier of u -valued Element of K32(K33( the carrier of u, the carrier of u))

RelStr(# the carrier of u,( the InternalRel of u ~) #) is strict RelStr

the carrier of (u ~) is non empty set

u ~ is non empty strict RelStr

the InternalRel of u is Relation-like the carrier of u -defined the carrier of u -valued Element of K32(K33( the carrier of u, the carrier of u))

K33( the carrier of u, the carrier of u) is non empty set

K32(K33( the carrier of u, the carrier of u)) is non empty set

the InternalRel of u ~ is Relation-like the carrier of u -defined the carrier of u -valued Element of K32(K33( the carrier of u, the carrier of u))

RelStr(# the carrier of u,( the InternalRel of u ~) #) is strict RelStr

the carrier of (u ~) is non empty set

K33( the carrier of (u ~), the carrier of (u ~)) is non empty set

K32(K33( the carrier of (u ~), the carrier of (u ~))) is non empty set

c

c

c

the carrier of c

the InternalRel of c

K33( the carrier of c

K32(K33( the carrier of c

the InternalRel of c

RelStr(# the carrier of c

the carrier of (c

c

c

the carrier of c

the InternalRel of c

K33( the carrier of c

K32(K33( the carrier of c

the InternalRel of c

RelStr(# the carrier of c

the carrier of (c

K33( the carrier of (c

K32(K33( the carrier of (c

K33( the carrier of c

K32(K33( the carrier of c

L is non empty RelStr

the carrier of L is non empty set

J is non empty RelStr

the carrier of J is non empty set

K33( the carrier of L, the carrier of J) is non empty set

K32(K33( the carrier of L, the carrier of J)) is non empty set

J ~ is non empty strict RelStr

the InternalRel of J is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

K33( the carrier of J, the carrier of J) is non empty set

K32(K33( the carrier of J, the carrier of J)) is non empty set

the InternalRel of J ~ is Relation-like the carrier of J -defined the carrier of J -valued Element of K32(K33( the carrier of J, the carrier of J))

RelStr(# the carrier of J,( the InternalRel of J ~) #) is strict RelStr

the carrier of (J ~) is non empty set

K33( the carrier of