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
{ b1 where b1 is Element of the carrier of J : b1 is_<=_than K } is set
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
{ ("/\" (b1,L)) where b1 is finite countable Element of K32(J) : ex_inf_of b1,L } is set
finsups J is Element of K32( the carrier of L)
{ ("\/" (b1,L)) where b1 is finite countable Element of K32(J) : ex_sup_of b1,L } is set
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
{ ("\/" (b1,(L ~))) where b1 is finite countable Element of K32(K) : ex_sup_of b1,L ~ } is set
fininfs K is Element of K32( the carrier of (L ~))
{ ("/\" (b1,(L ~))) where b1 is finite countable Element of K32(K) : ex_inf_of b1,L ~ } is set
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
c18 is set
c16 is non empty RelStr
c16 ~ is non empty strict RelStr
the carrier of c16 is non empty set
the InternalRel of c16 is Relation-like the carrier of c16 -defined the carrier of c16 -valued Element of K32(K33( the carrier of c16, the carrier of c16))
K33( the carrier of c16, the carrier of c16) is non empty set
K32(K33( the carrier of c16, the carrier of c16)) is non empty set
the InternalRel of c16 ~ is Relation-like the carrier of c16 -defined the carrier of c16 -valued Element of K32(K33( the carrier of c16, the carrier of c16))
RelStr(# the carrier of c16,( the InternalRel of c16 ~) #) is strict RelStr
the carrier of (c16 ~) is non empty set
c17 is non empty RelStr
c17 ~ is non empty strict RelStr
the carrier of c17 is non empty set
the InternalRel of c17 is Relation-like the carrier of c17 -defined the carrier of c17 -valued Element of K32(K33( the carrier of c17, the carrier of c17))
K33( the carrier of c17, the carrier of c17) is non empty set
K32(K33( the carrier of c17, the carrier of c17)) is non empty set
the InternalRel of c17 ~ is Relation-like the carrier of c17 -defined the carrier of c17 -valued Element of K32(K33( the carrier of c17, the carrier of c17))
RelStr(# the carrier of c17,( the InternalRel of c17 ~) #) is strict RelStr
the carrier of (c17 ~) is non empty set
K33( the carrier of (c16 ~), the carrier of (c17 ~)) is non empty set
K32(K33( the carrier of (c16 ~), the carrier of (c17 ~))) is non empty set
K33( the carrier of c16, the carrier of c17) is non empty set
K32(K33( the carrier of c16, the carrier of c17)) is non empty 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
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