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 L, the carrier of (J ~)) is non empty set
K32(K33( the carrier of L, the carrier of (J ~))) is non empty set
K is Relation-like the carrier of L -defined the carrier of J -valued Function-like V18( the carrier of L, the carrier of J) Element of K32(K33( the carrier of L, the carrier of J))
F is Relation-like the carrier of L -defined the carrier of (J ~) -valued Function-like V18( the carrier of L, the carrier of (J ~)) Element of K32(K33( the carrier of L, the carrier of (J ~)))
G is Element of the carrier of L
a is Element of the carrier of L
F . G is set
F . a is set
K . G is Element of the carrier of J
K . a is Element of the carrier of J
(K . G) ~ is Element of the carrier of (J ~)
(K . a) ~ 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 L
a is Element of the carrier of L
K . G is Element of the carrier of J
K . a is Element of the carrier of J
F . a is Element of the carrier of (J ~)
F . G is Element of the carrier of (J ~)
~ (F . G) is Element of the carrier of J
~ (F . a) is Element of the carrier of J
G is Element of the carrier of L
a is Element of the carrier of L
F . G is Element of the carrier of (J ~)
F . a is Element of the carrier of (J ~)
K . a is Element of the carrier of J
K . G is Element of the carrier of J
(K . G) ~ is Element of the carrier of (J ~)
(K . a) ~ is Element of the carrier of (J ~)
G is Element of the carrier of L
a is Element of the carrier of L
K . G is set
K . a is set
F . G is Element of the carrier of (J ~)
F . a is Element of the carrier of (J ~)
~ (F . G) is Element of the carrier of J
~ (F . a) is Element of the carrier of J
K9 is Element of the carrier of J
G is Element of the carrier of J
L is non empty RelStr
the carrier of L 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 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
K is Relation-like the carrier of L -defined the carrier of (J ~) -valued Function-like V18( the carrier of L, the carrier of (J ~)) Element of K32(K33( the carrier of L, the carrier of (J ~)))
F is Relation-like the carrier of (L ~) -defined the carrier of J -valued Function-like V18( the carrier of (L ~), the carrier of J) Element of K32(K33( the carrier of (L ~), the carrier of J))
G is Element of the carrier of (L ~)
a is Element of the carrier of (L ~)
F . G is Element of the carrier of J
F . a is Element of the carrier of J
~ a is Element of the carrier of L
~ G is Element of the carrier of L
K . (~ a) is Element of the carrier of (J ~)
K . (~ G) is Element of the carrier of (J ~)
~ (K . (~ G)) is Element of the carrier of J
~ (K . (~ a)) is Element of the carrier of J
G is Element of the carrier of L
a is Element of the carrier of L
K . G is Element of the carrier of (J ~)
K . a is Element of the carrier of (J ~)
a ~ is Element of the carrier of (L ~)
G ~ is Element of the carrier of (L ~)
F . (a ~) is Element of the carrier of J
F . (G ~) is Element of the carrier of J
(F . (G ~)) ~ is Element of the carrier of (J ~)
(F . (a ~)) ~ is Element of the carrier of (J ~)
G is Element of the carrier of (L ~)
a is Element of the carrier of (L ~)
F . G is set
F . a is set
~ a is Element of the carrier of L
~ G is Element of the carrier of L
K . (~ G) is Element of the carrier of (J ~)
K . (~ a) is Element of the carrier of (J ~)
~ (K . (~ G)) is Element of the carrier of J
~ (K . (~ a)) 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 L
a is Element of the carrier of L
K . G is set
K . a is set
a ~ is Element of the carrier of (L ~)
G ~ is Element of the carrier of (L ~)
F . (G ~) is Element of the carrier of J
F . (a ~) is Element of the carrier of J
(F . (G ~)) ~ is Element of the carrier of (J ~)
(F . (a ~)) ~ is Element of the carrier of (J ~)
K9 is Element of the carrier of (J ~)
G is Element of the carrier of (J ~)
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
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 (L ~), the carrier of (J ~)) is non empty set
K32(K33( the carrier of (L ~), the carrier of (J ~))) is non empty set
K is Relation-like the carrier of L -defined the carrier of J -valued Function-like V18( the carrier of L, the carrier of J) Element of K32(K33( the carrier of L, the carrier of J))
F is Relation-like the carrier of (L ~) -defined the carrier of (J ~) -valued Function-like V18( the carrier of (L ~), the carrier of (J ~)) Element of K32(K33( the carrier of (L ~), the carrier of (J ~)))
G is Element of the carrier of (L ~)
a is Element of the carrier of (L ~)
F . G is Element of the carrier of (J ~)
F . a is Element of the carrier of (J ~)
~ a is Element of the carrier of L
~ G is Element of the carrier of L
K . (~ a) is Element of the carrier of J
K . (~ G) is Element of the carrier of J
(K . (~ G)) ~ is Element of the carrier of (J ~)
(K . (~ a)) ~ is Element of the carrier of (J ~)
G is Element of the carrier of L
a is Element of the carrier of L
K . G is Element of the carrier of J
K . a is Element of the carrier of J
a ~ is Element of the carrier of (L ~)
G ~ is Element of the carrier of (L ~)
F . (a ~) is Element of the carrier of (J ~)
F . (G ~) is Element of the carrier of (J ~)
~ (F . (G ~)) is Element of the carrier of J
~ (F . (a ~)) is Element of the carrier of J
G is Element of the carrier of (L ~)
a is Element of the carrier of (L ~)
F . G is set
F . a is set
~ a is Element of the carrier of L
~ G is Element of the carrier of L
K . (~ G) is Element of the carrier of J
K . (~ a) is Element of the carrier of J
(K . (~ G)) ~ is Element of the carrier of (J ~)
(K . (~ a)) ~ 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 L
a is Element of the carrier of L
K . G is set
K . a is set
a ~ is Element of the carrier of (L ~)
G ~ is Element of the carrier of (L ~)
F . (G ~) is Element of the carrier of (J ~)
F . (a ~) is Element of the carrier of (J ~)
~ (F . (G ~)) is Element of the carrier of J
~ (F . (a ~)) is Element of the carrier of J
K9 is Element of the carrier of J
G is Element of the carrier of J
L is non empty RelStr
J 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 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
K is RelStr
the carrier of K is set
F is RelStr
the carrier of F is set
G is RelStr
the carrier of G is set
a is RelStr
the carrier of a is set
K33( the carrier of K, the carrier of G) is set
K32(K33( the carrier of K, the carrier of G)) is non empty set
K33( the carrier of G, the carrier of K) is set
K32(K33( the carrier of G, the carrier of K)) is non empty set
K9 is Connection of K,G
G is Relation-like the carrier of K -defined the carrier of G -valued Function-like V18( the carrier of K, the carrier of G) Element of K32(K33( the carrier of K, the carrier of G))
g is Relation-like the carrier of G -defined the carrier of K -valued Function-like V18( the carrier of G, the carrier of K) Element of K32(K33( the carrier of G, the carrier of K))
[G,g] is Connection of K,G
{G,g} is functional finite countable set
{G} is non empty V5() functional finite V38(1) with_common_domain countable set
{{G,g},{G}} is finite V35() countable set
K33( the carrier of a, the carrier of F) is set
K32(K33( the carrier of a, the carrier of F)) is non empty set
K33( the carrier of F, the carrier of a) is set
K32(K33( the carrier of F, the carrier of a)) is non empty set
j is Relation-like the carrier of F -defined the carrier of a -valued Function-like V18( the carrier of F, the carrier of a) Element of K32(K33( the carrier of F, the carrier of a))
g9 is Relation-like the carrier of a -defined the carrier of F -valued Function-like V18( the carrier of a, the carrier of F) Element of K32(K33( the carrier of a, the carrier of F))
[j,g9] is Connection of F,a
{j,g9} is functional finite countable set
{j} is non empty V5() functional finite V38(1) with_common_domain countable set
{{j,g9},{j}} is finite V35() countable set
K is set
F is set
G is set
a is set
K9 is set
G is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
J is non empty reflexive transitive antisymmetric 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
K33( the carrier of J, the carrier of L) is non empty set
K32(K33( the carrier of J, the carrier of L)) is non empty set
L ~ is non empty strict reflexive transitive 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
J ~ is non empty strict reflexive transitive antisymmetric 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 (L ~), the carrier of (J ~)) is non empty set
K32(K33( the carrier of (L ~), the carrier of (J ~))) is non empty set
K33( the carrier of (J ~), the carrier of (L ~)) is non empty set
K32(K33( the carrier of (J ~), the carrier of (L ~))) is non empty set
K is Relation-like the carrier of L -defined the carrier of J -valued Function-like V18( the carrier of L, the carrier of J) Element of K32(K33( the carrier of L, the carrier of J))
F is Relation-like the carrier of J -defined the carrier of L -valued Function-like V18( the carrier of J, the carrier of L) Element of K32(K33( the carrier of J, the carrier of L))
[K,F] is Connection of L,J
{K,F} is functional finite countable set
{K} is non empty V5() functional finite V38(1) with_common_domain countable set
{{K,F},{K}} is finite V35() countable set
G is Relation-like the carrier of (L ~) -defined the carrier of (J ~) -valued Function-like V18( the carrier of (L ~), the carrier of (J ~)) Element of K32(K33( the carrier of (L ~), the carrier of (J ~)))
a is Relation-like the carrier of (J ~) -defined the carrier of (L ~) -valued Function-like V18( the carrier of (J ~), the carrier of (L ~)) Element of K32(K33( the carrier of (J ~), the carrier of (L ~)))
[a,G] is Connection of J ~ ,L ~
{a,G} is functional finite countable set
{a} is non empty V5() functional finite V38(1) with_common_domain countable set
{{a,G},{a}} is finite V35() countable set
K9 is Element of the carrier of (L ~)
~ K9 is Element of the carrier of L
K . (~ K9) is Element of the carrier of J
(K . (~ K9)) ~ is Element of the carrier of (J ~)
G is Element of the carrier of (J ~)
~ G is Element of the carrier of J
F . (~ G) is Element of the carrier of L
(F . (~ G)) ~ is Element of the carrier of (L ~)
a . G is Element of the carrier of (L ~)
G . K9 is Element of the carrier of (J ~)
G is Element of the carrier of L
G ~ is Element of the carrier of (L ~)
G . (G ~) is Element of the carrier of (J ~)
~ (G . (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 . (K9 ~) is Element of the carrier of (L ~)
~ (a . (K9 ~)) is Element of the carrier of L
K . G is Element of the carrier of J
F . K9 is Element of the carrier of L
L is set
J is non empty set
L --> J is Relation-like non-empty L -defined {J} -valued Function-like constant V17(L) V18(L,{J}) Element of K32(K33(L,{J}))
{J} is non empty V5() finite V38(1) countable set
K33(L,{J}) is set
K32(K33(L,{J})) is non empty set
K is Relation-like L -defined Function-like V17(L) set
F is Relation-like L -defined Function-like V17(L) Function-yielding V105() ManySortedFunction of K,L --> J
doms F is Relation-like Function-like set
dom (doms F) is set
rng F is set
SubFuncs (rng F) is set
F " (SubFuncs (rng F)) is set
G is set
dom F is Element of K32(L)
K32(L) is non empty set
a is set
F . a is Relation-like Function-like set
dom F is Element of K32(L)
K32(L) is non empty set
G is set
F . G is Relation-like Function-like set
(L --> J) . G is set
K . G is set
K33((K . G),J) is set
K32(K33((K . G),J)) is non empty set
(doms F) . G is set
dom (F . G) is set
dom K is Element of K32(L)
F " (rng F) is set
L is non empty set
K is non empty Relation-like non-empty non empty-yielding L -defined Function-like V17(L) set
J is non empty set
L --> J is non empty Relation-like non-empty non empty-yielding L -defined {J} -valued Function-like constant V17(L) V18(L,{J}) Element of K32(K33(L,{J}))
{J} is non empty V5() finite V38(1) countable set
K33(L,{J}) is non empty set
K32(K33(L,{J})) is non empty set
G is Element of L
K . G is non empty set
F is non empty Relation-like non-empty non empty-yielding L -defined Function-like V17(L) Function-yielding V105() ManySortedFunction of K,L --> J
a is Element of K . G
F .. (G,a) is set
K491(F) is Relation-like Function-like set
K355(K491(F),G,a) is set
F . G is non empty Relation-like K . G -defined J -valued Function-like V18(K . G,J) Element of K32(K33((K . G),J))
K33((K . G),J) is non empty set
K32(K33((K . G),J)) is non empty set
dom (F . G) is Element of K32((K . G))
K32((K . G)) is non empty set
dom F is Element of K32(L)
K32(L) is non empty set
(F . G) . a is Element of J
J is set
a is set
F is set
K is Relation-like J -defined Function-like V17(J) set
L is non empty RelStr
the carrier of L is non empty set
J --> the carrier of L is Relation-like non-empty J -defined { the carrier of L} -valued Function-like constant V17(J) V18(J,{ the carrier of L}) Element of K32(K33(J,{ the carrier of L}))
{ the carrier of L} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of L}) is set
K32(K33(J,{ 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 --> the carrier of (L ~) is Relation-like non-empty J -defined { the carrier of (L ~)} -valued Function-like constant V17(J) V18(J,{ the carrier of (L ~)}) Element of K32(K33(J,{ the carrier of (L ~)}))
{ the carrier of (L ~)} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of (L ~)}) is set
K32(K33(J,{ the carrier of (L ~)})) is non empty set
G is set
K9 is Relation-like a -defined Function-like V17(a) set
G is non empty RelStr
G ~ is non empty strict RelStr
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))
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
a --> the carrier of (G ~) is Relation-like non-empty a -defined { the carrier of (G ~)} -valued Function-like constant V17(a) V18(a,{ the carrier of (G ~)}) Element of K32(K33(a,{ the carrier of (G ~)}))
{ the carrier of (G ~)} is non empty V5() finite V38(1) countable set
K33(a,{ the carrier of (G ~)}) is set
K32(K33(a,{ the carrier of (G ~)})) is non empty set
a --> the carrier of G is Relation-like non-empty a -defined { the carrier of G} -valued Function-like constant V17(a) V18(a,{ the carrier of G}) Element of K32(K33(a,{ the carrier of G}))
{ the carrier of G} is non empty V5() finite V38(1) countable set
K33(a,{ the carrier of G}) is set
K32(K33(a,{ the carrier of G})) is non empty set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete RelStr
the carrier of L is non empty set
J is non empty set
J --> the carrier of L is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of L} -valued Function-like constant V17(J) V18(J,{ the carrier of L}) Element of K32(K33(J,{ the carrier of L}))
{ the carrier of L} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of L}) is non empty set
K32(K33(J,{ the carrier of L})) is non empty set
K is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) set
F is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) Function-yielding V105() ManySortedFunction of K,J --> the carrier of L
/\\ (F,L) is Relation-like dom F -defined the carrier of L -valued Function-like V18( dom F, the carrier of L) Element of K32(K33((dom F), the carrier of L))
dom F is set
K33((dom F), the carrier of L) is set
K32(K33((dom F), the carrier of L)) is non empty set
\\/ ((/\\ (F,L)),L) is Element of the carrier of L
Frege F is non empty Relation-like non-empty non empty-yielding product (doms F) -defined Function-like V17( product (doms F)) Function-yielding V105() ManySortedFunction of (product (doms F)) --> J,(product (doms F)) --> the carrier of L
doms F is Relation-like non-empty Function-like set
product (doms F) is non empty functional with_common_domain product-like set
(product (doms F)) --> J is non empty Relation-like non-empty non empty-yielding product (doms F) -defined {J} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{J}) Element of K32(K33((product (doms F)),{J}))
{J} is non empty V5() finite V38(1) countable set
K33((product (doms F)),{J}) is non empty set
K32(K33((product (doms F)),{J})) is non empty set
(product (doms F)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms F) -defined { the carrier of L} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{ the carrier of L}) Element of K32(K33((product (doms F)),{ the carrier of L}))
K33((product (doms F)),{ the carrier of L}) is non empty set
K32(K33((product (doms F)),{ the carrier of L})) is non empty set
\// ((Frege F),L) is Relation-like dom (Frege F) -defined the carrier of L -valued Function-like V18( dom (Frege F), the carrier of L) Element of K32(K33((dom (Frege F)), the carrier of L))
dom (Frege F) is set
K33((dom (Frege F)), the carrier of L) is set
K32(K33((dom (Frege F)), the carrier of L)) is non empty set
//\ ((\// ((Frege F),L)),L) is Element of the carrier of L
rng (/\\ (F,L)) is non empty Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
G is Element of the carrier of L
a is Element of J
F . a is non empty Relation-like K . a -defined the carrier of L -valued Function-like V18(K . a, the carrier of L) Element of K32(K33((K . a), the carrier of L))
K . a is non empty set
K33((K . a), the carrier of L) is non empty set
K32(K33((K . a), the carrier of L)) is non empty set
//\ ((F . a),L) is Element of the carrier of L
rng (F . a) is non empty Element of K32( the carrier of L)
"/\" ((rng (F . a)),L) is Element of the carrier of L
rng (\// ((Frege F),L)) is non empty Element of K32( the carrier of L)
G is Element of the carrier of L
K9 is non empty set
K9 --> J is non empty Relation-like non-empty non empty-yielding K9 -defined {J} -valued Function-like constant V17(K9) V18(K9,{J}) Element of K32(K33(K9,{J}))
K33(K9,{J}) is non empty set
K32(K33(K9,{J})) is non empty set
g is non empty Relation-like K9 -defined Function-like V17(K9) set
K9 --> the carrier of L is non empty Relation-like non-empty non empty-yielding K9 -defined { the carrier of L} -valued Function-like constant V17(K9) V18(K9,{ the carrier of L}) Element of K32(K33(K9,{ the carrier of L}))
K33(K9,{ the carrier of L}) is non empty set
K32(K33(K9,{ the carrier of L})) is non empty set
g9 is non empty Relation-like K9 -defined Function-like V17(K9) Function-yielding V105() ManySortedFunction of g,K9 --> the carrier of L
j is Element of K9
g9 . j is Relation-like g . j -defined the carrier of L -valued Function-like V18(g . j, the carrier of L) Element of K32(K33((g . j), the carrier of L))
g . j is set
K33((g . j), the carrier of L) is set
K32(K33((g . j), the carrier of L)) is non empty set
\\/ ((g9 . j),L) is Element of the carrier of L
dom F is Element of K32(J)
K32(J) is non empty set
dom (Frege F) is functional with_common_domain Element of K32((product (doms F)))
K32((product (doms F))) is non empty set
z is Relation-like Function-like doms F -compatible Element of product (doms F)
z . a is set
dom (F . a) is Element of K32((K . a))
K32((K . a)) is non empty set
u is Element of K . a
(F . a) . u is Element of the carrier of L
(Frege F) . z is non empty Relation-like J -defined the carrier of L -valued Function-like V18(J, the carrier of L) Element of K32(K33(J, the carrier of L))
K33(J, the carrier of L) is non empty set
K32(K33(J, the carrier of L)) is non empty set
rng ((Frege F) . z) is non empty Element of K32( the carrier of L)
"\/" ((rng ((Frege F) . z)),L) is Element of the carrier of L
"/\" ((rng (\// ((Frege F),L))),L) is Element of the carrier of L
"\/" ((rng (/\\ (F,L))),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete RelStr
the carrier of L is non empty set
J is non empty set
J --> the carrier of L is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of L} -valued Function-like constant V17(J) V18(J,{ the carrier of L}) Element of K32(K33(J,{ the carrier of L}))
{ the carrier of L} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of L}) is non empty set
K32(K33(J,{ the carrier of L})) is non empty set
K is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) set
F is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) Function-yielding V105() ManySortedFunction of K,J --> the carrier of L
/\\ (F,L) is Relation-like dom F -defined the carrier of L -valued Function-like V18( dom F, the carrier of L) Element of K32(K33((dom F), the carrier of L))
dom F is set
K33((dom F), the carrier of L) is set
K32(K33((dom F), the carrier of L)) is non empty set
\\/ ((/\\ (F,L)),L) is Element of the carrier of L
Frege F is non empty Relation-like non-empty non empty-yielding product (doms F) -defined Function-like V17( product (doms F)) Function-yielding V105() ManySortedFunction of (product (doms F)) --> J,(product (doms F)) --> the carrier of L
doms F is Relation-like non-empty Function-like set
product (doms F) is non empty functional with_common_domain product-like set
(product (doms F)) --> J is non empty Relation-like non-empty non empty-yielding product (doms F) -defined {J} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{J}) Element of K32(K33((product (doms F)),{J}))
{J} is non empty V5() finite V38(1) countable set
K33((product (doms F)),{J}) is non empty set
K32(K33((product (doms F)),{J})) is non empty set
(product (doms F)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms F) -defined { the carrier of L} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{ the carrier of L}) Element of K32(K33((product (doms F)),{ the carrier of L}))
K33((product (doms F)),{ the carrier of L}) is non empty set
K32(K33((product (doms F)),{ the carrier of L})) is non empty set
\// ((Frege F),L) is Relation-like dom (Frege F) -defined the carrier of L -valued Function-like V18( dom (Frege F), the carrier of L) Element of K32(K33((dom (Frege F)), the carrier of L))
dom (Frege F) is set
K33((dom (Frege F)), the carrier of L) is set
K32(K33((dom (Frege F)), the carrier of L)) is non empty set
//\ ((\// ((Frege F),L)),L) is Element of the carrier of L
Frege (Frege F) is non empty Relation-like non-empty non empty-yielding product (doms (Frege F)) -defined Function-like V17( product (doms (Frege F))) Function-yielding V105() ManySortedFunction of (product (doms (Frege F))) --> (product (doms F)),(product (doms (Frege F))) --> the carrier of L
doms (Frege F) is Relation-like non-empty Function-like set
product (doms (Frege F)) is non empty functional with_common_domain product-like set
(product (doms (Frege F))) --> (product (doms F)) is non empty Relation-like non-empty non empty-yielding product (doms (Frege F)) -defined {(product (doms F))} -valued Function-like constant V17( product (doms (Frege F))) V18( product (doms (Frege F)),{(product (doms F))}) Element of K32(K33((product (doms (Frege F))),{(product (doms F))}))
{(product (doms F))} is non empty V5() finite V38(1) countable set
K33((product (doms (Frege F))),{(product (doms F))}) is non empty set
K32(K33((product (doms (Frege F))),{(product (doms F))})) is non empty set
(product (doms (Frege F))) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms (Frege F)) -defined { the carrier of L} -valued Function-like constant V17( product (doms (Frege F))) V18( product (doms (Frege F)),{ the carrier of L}) Element of K32(K33((product (doms (Frege F))),{ the carrier of L}))
K33((product (doms (Frege F))),{ the carrier of L}) is non empty set
K32(K33((product (doms (Frege F))),{ the carrier of L})) is non empty set
/\\ ((Frege (Frege F)),L) is Relation-like dom (Frege (Frege F)) -defined the carrier of L -valued Function-like V18( dom (Frege (Frege F)), the carrier of L) Element of K32(K33((dom (Frege (Frege F))), the carrier of L))
dom (Frege (Frege F)) is set
K33((dom (Frege (Frege F))), the carrier of L) is set
K32(K33((dom (Frege (Frege F))), the carrier of L)) is non empty set
\\/ ((/\\ ((Frege (Frege F)),L)),L) is Element of the carrier of L
dom K is Element of K32(J)
K32(J) is non empty set
dom F is Element of K32(J)
dom (Frege F) is functional with_common_domain Element of K32((product (doms F)))
K32((product (doms F))) is non empty set
rng (/\\ ((Frege (Frege F)),L)) is non empty Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
a is Element of the carrier of L
G is non empty set
G --> (product (doms F)) is non empty Relation-like non-empty non empty-yielding G -defined {(product (doms F))} -valued Function-like constant V17(G) V18(G,{(product (doms F))}) Element of K32(K33(G,{(product (doms F))}))
K33(G,{(product (doms F))}) is non empty set
K32(K33(G,{(product (doms F))})) is non empty set
K9 is non empty Relation-like G -defined Function-like V17(G) set
G --> the carrier of L is non empty Relation-like non-empty non empty-yielding G -defined { the carrier of L} -valued Function-like constant V17(G) V18(G,{ the carrier of L}) Element of K32(K33(G,{ the carrier of L}))
K33(G,{ the carrier of L}) is non empty set
K32(K33(G,{ the carrier of L})) is non empty set
G is non empty Relation-like G -defined Function-like V17(G) Function-yielding V105() ManySortedFunction of K9,G --> the carrier of L
g is Element of G
G . g is Relation-like K9 . g -defined the carrier of L -valued Function-like V18(K9 . g, the carrier of L) Element of K32(K33((K9 . g), the carrier of L))
K9 . g is set
K33((K9 . g), the carrier of L) is set
K32(K33((K9 . g), the carrier of L)) is non empty set
//\ ((G . g),L) is Element of the carrier of L
g9 is Relation-like Function-like set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = a1 } is set
dom ((product (doms F)) --> J) is functional with_common_domain Element of K32((product (doms F)))
j is set
z is Element of J
K . z is non empty set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is set
(K . z) \ H1(j) is Element of K32((K . z))
K32((K . z)) is non empty set
the Element of (K . z) \ H1(j) is Element of (K . z) \ H1(j)
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = z } is set
(K . z) \ H1(z) is Element of K32((K . z))
K . j is set
(K . j) \ H1(j) is Element of K32((K . j))
K32((K . j)) is non empty set
j is Relation-like Function-like set
dom j is set
z is set
j . z is set
K . z is set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = z } is set
(K . z) \ H1(z) is Element of K32((K . z))
K32((K . z)) is non empty set
(doms F) . z is set
z is Relation-like Function-like doms F -compatible Element of product (doms F)
g9 . z is set
(doms (Frege F)) . z is set
z . (g9 . z) is set
u is Element of J
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = u } is set
z . u is set
K . u is non empty set
(K . u) \ H1(u) is Element of K32((K . u))
K32((K . u)) is non empty set
j is Element of J
K . j is non empty set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is set
(K . j) \ { (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is Element of K32((K . j))
K32((K . j)) is non empty set
j is Element of J
K . j is non empty set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is set
(K . j) \ H1(j) is Element of K32((K . j))
K32((K . j)) is non empty set
F . j is non empty Relation-like K . j -defined the carrier of L -valued Function-like V18(K . j, the carrier of L) Element of K32(K33((K . j), the carrier of L))
K33((K . j), the carrier of L) is non empty set
K32(K33((K . j), the carrier of L)) is non empty set
rng (F . j) is non empty Element of K32( the carrier of L)
rng (G . g) is Element of K32( the carrier of L)
z is set
dom (F . j) is Element of K32((K . j))
u is set
(F . j) . u is set
u is Element of K . j
f is Relation-like Function-like doms F -compatible Element of product (doms F)
g9 . f is set
f . (g9 . f) is set
(Frege F) .. g9 is Relation-like Function-like set
(Frege F) . f is non empty Relation-like J -defined the carrier of L -valued Function-like V18(J, the carrier of L) Element of K32(K33(J, the carrier of L))
K33(J, the carrier of L) is non empty set
K32(K33(J, the carrier of L)) is non empty set
F .. f is Relation-like Function-like set
(G . g) . f is set
(F .. f) . j is set
dom (G . g) is Element of K32((K9 . g))
K32((K9 . g)) is non empty set
"/\" ((rng (G . g)),L) is Element of the carrier of L
"/\" ((rng (F . j)),L) is Element of the carrier of L
//\ ((F . j),L) is Element of the carrier of L
rng (/\\ (F,L)) is non empty Element of K32( the carrier of L)
"\/" ((rng (/\\ (F,L))),L) is Element of the carrier of L
"\/" ((rng (/\\ ((Frege (Frege F)),L))),L) is Element of the carrier of L
J is non empty set
J --> the carrier of L is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of L} -valued Function-like constant V17(J) V18(J,{ the carrier of L}) Element of K32(K33(J,{ the carrier of L}))
{ the carrier of L} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of L}) is non empty set
K32(K33(J,{ the carrier of L})) is non empty set
K is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) set
F is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) Function-yielding V105() ManySortedFunction of K,J --> the carrier of L
\// (F,L) is Relation-like dom F -defined the carrier of L -valued Function-like V18( dom F, the carrier of L) Element of K32(K33((dom F), the carrier of L))
dom F is set
K33((dom F), the carrier of L) is set
K32(K33((dom F), the carrier of L)) is non empty set
//\ ((\// (F,L)),L) is Element of the carrier of L
Frege F is non empty Relation-like non-empty non empty-yielding product (doms F) -defined Function-like V17( product (doms F)) Function-yielding V105() ManySortedFunction of (product (doms F)) --> J,(product (doms F)) --> the carrier of L
doms F is Relation-like non-empty Function-like set
product (doms F) is non empty functional with_common_domain product-like set
(product (doms F)) --> J is non empty Relation-like non-empty non empty-yielding product (doms F) -defined {J} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{J}) Element of K32(K33((product (doms F)),{J}))
{J} is non empty V5() finite V38(1) countable set
K33((product (doms F)),{J}) is non empty set
K32(K33((product (doms F)),{J})) is non empty set
(product (doms F)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms F) -defined { the carrier of L} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{ the carrier of L}) Element of K32(K33((product (doms F)),{ the carrier of L}))
K33((product (doms F)),{ the carrier of L}) is non empty set
K32(K33((product (doms F)),{ the carrier of L})) is non empty set
/\\ ((Frege F),L) is Relation-like dom (Frege F) -defined the carrier of L -valued Function-like V18( dom (Frege F), the carrier of L) Element of K32(K33((dom (Frege F)), the carrier of L))
dom (Frege F) is set
K33((dom (Frege F)), the carrier of L) is set
K32(K33((dom (Frege F)), the carrier of L)) is non empty set
\\/ ((/\\ ((Frege F),L)),L) is Element of the carrier of L
dom K is Element of K32(J)
K32(J) is non empty set
doms (Frege F) is Relation-like non-empty Function-like set
dom F is Element of K32(J)
dom (Frege F) is functional with_common_domain Element of K32((product (doms F)))
K32((product (doms F))) is non empty set
Frege (Frege F) is non empty Relation-like non-empty non empty-yielding product (doms (Frege F)) -defined Function-like V17( product (doms (Frege F))) Function-yielding V105() ManySortedFunction of (product (doms (Frege F))) --> (product (doms F)),(product (doms (Frege F))) --> the carrier of L
product (doms (Frege F)) is non empty functional with_common_domain product-like set
(product (doms (Frege F))) --> (product (doms F)) is non empty Relation-like non-empty non empty-yielding product (doms (Frege F)) -defined {(product (doms F))} -valued Function-like constant V17( product (doms (Frege F))) V18( product (doms (Frege F)),{(product (doms F))}) Element of K32(K33((product (doms (Frege F))),{(product (doms F))}))
{(product (doms F))} is non empty V5() finite V38(1) countable set
K33((product (doms (Frege F))),{(product (doms F))}) is non empty set
K32(K33((product (doms (Frege F))),{(product (doms F))})) is non empty set
(product (doms (Frege F))) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms (Frege F)) -defined { the carrier of L} -valued Function-like constant V17( product (doms (Frege F))) V18( product (doms (Frege F)),{ the carrier of L}) Element of K32(K33((product (doms (Frege F))),{ the carrier of L}))
K33((product (doms (Frege F))),{ the carrier of L}) is non empty set
K32(K33((product (doms (Frege F))),{ the carrier of L})) is non empty set
\// ((Frege (Frege F)),L) is Relation-like dom (Frege (Frege F)) -defined the carrier of L -valued Function-like V18( dom (Frege (Frege F)), the carrier of L) Element of K32(K33((dom (Frege (Frege F))), the carrier of L))
dom (Frege (Frege F)) is set
K33((dom (Frege (Frege F))), the carrier of L) is set
K32(K33((dom (Frege (Frege F))), the carrier of L)) is non empty set
rng (\// ((Frege (Frege F)),L)) is non empty Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
a is Element of the carrier of L
G is non empty set
G --> (product (doms F)) is non empty Relation-like non-empty non empty-yielding G -defined {(product (doms F))} -valued Function-like constant V17(G) V18(G,{(product (doms F))}) Element of K32(K33(G,{(product (doms F))}))
K33(G,{(product (doms F))}) is non empty set
K32(K33(G,{(product (doms F))})) is non empty set
K9 is non empty Relation-like G -defined Function-like V17(G) set
G --> the carrier of L is non empty Relation-like non-empty non empty-yielding G -defined { the carrier of L} -valued Function-like constant V17(G) V18(G,{ the carrier of L}) Element of K32(K33(G,{ the carrier of L}))
K33(G,{ the carrier of L}) is non empty set
K32(K33(G,{ the carrier of L})) is non empty set
G is non empty Relation-like G -defined Function-like V17(G) Function-yielding V105() ManySortedFunction of K9,G --> the carrier of L
g is Element of G
G . g is Relation-like K9 . g -defined the carrier of L -valued Function-like V18(K9 . g, the carrier of L) Element of K32(K33((K9 . g), the carrier of L))
K9 . g is set
K33((K9 . g), the carrier of L) is set
K32(K33((K9 . g), the carrier of L)) is non empty set
\\/ ((G . g),L) is Element of the carrier of L
g9 is Relation-like Function-like set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = a1 } is set
dom ((product (doms F)) --> J) is functional with_common_domain Element of K32((product (doms F)))
j is set
z is Element of J
K . z is non empty set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is set
(K . z) \ H1(j) is Element of K32((K . z))
K32((K . z)) is non empty set
the Element of (K . z) \ H1(j) is Element of (K . z) \ H1(j)
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = z } is set
(K . z) \ H1(z) is Element of K32((K . z))
K . j is set
(K . j) \ H1(j) is Element of K32((K . j))
K32((K . j)) is non empty set
j is Relation-like Function-like set
dom j is set
z is set
j . z is set
K . z is set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = z } is set
(K . z) \ H1(z) is Element of K32((K . z))
K32((K . z)) is non empty set
(doms F) . z is set
z is Relation-like Function-like doms F -compatible Element of product (doms F)
g9 . z is set
(doms (Frege F)) . z is set
z . (g9 . z) is set
u is Element of J
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = u } is set
z . u is set
K . u is non empty set
(K . u) \ H1(u) is Element of K32((K . u))
K32((K . u)) is non empty set
j is Element of J
K . j is non empty set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is set
(K . j) \ { (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is Element of K32((K . j))
K32((K . j)) is non empty set
j is Element of J
K . j is non empty set
{ (b1 . (g9 . b1)) where b1 is Relation-like Function-like doms F -compatible Element of product (doms F) : g9 . b1 = j } is set
(K . j) \ H1(j) is Element of K32((K . j))
K32((K . j)) is non empty set
F . j is non empty Relation-like K . j -defined the carrier of L -valued Function-like V18(K . j, the carrier of L) Element of K32(K33((K . j), the carrier of L))
K33((K . j), the carrier of L) is non empty set
K32(K33((K . j), the carrier of L)) is non empty set
rng (F . j) is non empty Element of K32( the carrier of L)
rng (G . g) is Element of K32( the carrier of L)
z is set
dom (F . j) is Element of K32((K . j))
u is set
(F . j) . u is set
u is Element of K . j
f is Relation-like Function-like doms F -compatible Element of product (doms F)
g9 . f is set
f . (g9 . f) is set
(Frege F) .. g9 is Relation-like Function-like set
(Frege F) . f is non empty Relation-like J -defined the carrier of L -valued Function-like V18(J, the carrier of L) Element of K32(K33(J, the carrier of L))
K33(J, the carrier of L) is non empty set
K32(K33(J, the carrier of L)) is non empty set
F .. f is Relation-like Function-like set
(G . g) . f is set
(F .. f) . j is set
dom (G . g) is Element of K32((K9 . g))
K32((K9 . g)) is non empty set
"\/" ((rng (F . j)),L) is Element of the carrier of L
"\/" ((rng (G . g)),L) is Element of the carrier of L
\\/ ((F . j),L) is Element of the carrier of L
rng (\// (F,L)) is non empty Element of K32( the carrier of L)
"/\" ((rng (\// (F,L))),L) is Element of the carrier of L
"/\" ((rng (\// ((Frege (Frege F)),L))),L) is Element of the carrier of L
//\ ((\// ((Frege (Frege F)),L)),L) is Element of the carrier of L
L is non empty antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr
L ~ is non empty strict antisymmetric with_suprema with_infima complete 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
J is Relation-like Function-like 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
\\/ (J,(L ~)) is Element of the carrier of (L ~)
rng J is set
"\/" ((rng J),L) is Element of the carrier of L
"/\" ((rng J),(L ~)) is Element of the carrier of (L ~)
"/\" ((rng J),L) is Element of the carrier of L
"\/" ((rng J),(L ~)) is Element of the carrier of (L ~)
L is non empty antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded RelStr
the carrier of L is non empty set
L ~ is non empty strict antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded 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 Relation-like Function-like Function-yielding V105() set
dom J is set
\// (J,L) is Relation-like dom J -defined the carrier of L -valued Function-like V18( dom J, the carrier of L) Element of K32(K33((dom J), the carrier of L))
K33((dom J), the carrier of L) is set
K32(K33((dom J), the carrier of L)) is non empty set
/\\ (J,(L ~)) is Relation-like dom J -defined the carrier of (L ~) -valued Function-like V18( dom J, the carrier of (L ~)) Element of K32(K33((dom J), the carrier of (L ~)))
K33((dom J), the carrier of (L ~)) is set
K32(K33((dom J), the carrier of (L ~))) is non empty set
/\\ (J,L) is Relation-like dom J -defined the carrier of L -valued Function-like V18( dom J, the carrier of L) Element of K32(K33((dom J), the carrier of L))
\// (J,(L ~)) is Relation-like dom J -defined the carrier of (L ~) -valued Function-like V18( dom J, the carrier of (L ~)) Element of K32(K33((dom J), the carrier of (L ~)))
K is set
(\// (J,L)) . K is set
J . K is Relation-like Function-like set
\\/ ((J . K),L) is Element of the carrier of L
(/\\ (J,(L ~))) . K is set
//\ ((J . K),(L ~)) is Element of the carrier of (L ~)
dom (\// (J,L)) is Element of K32((dom J))
K32((dom J)) is non empty set
dom (/\\ (J,(L ~))) is Element of K32((dom J))
K is set
(/\\ (J,L)) . K is set
J . K is Relation-like Function-like set
//\ ((J . K),L) is Element of the carrier of L
(\// (J,(L ~))) . K is set
\\/ ((J . K),(L ~)) is Element of the carrier of (L ~)
dom (/\\ (J,L)) is Element of K32((dom J))
dom (\// (J,(L ~))) is Element of K32((dom J))
L is non empty RelStr
the non empty V45() finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded connected up-complete /\-complete distributive V222() completely-distributive RelStr is non empty V45() finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded connected up-complete /\-complete distributive V222() completely-distributive RelStr
L is non empty reflexive transitive antisymmetric RelStr
L ~ is non empty strict reflexive transitive antisymmetric 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 non empty set
J --> the carrier of (L ~) is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of (L ~)} -valued Function-like constant V17(J) V18(J,{ the carrier of (L ~)}) Element of K32(K33(J,{ the carrier of (L ~)}))
{ the carrier of (L ~)} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of (L ~)}) is non empty set
K32(K33(J,{ the carrier of (L ~)})) is non empty set
K is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) set
F is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) Function-yielding V105() ManySortedFunction of K,J --> the carrier of (L ~)
\// (F,(L ~)) is Relation-like dom F -defined the carrier of (L ~) -valued Function-like V18( dom F, the carrier of (L ~)) Element of K32(K33((dom F), the carrier of (L ~)))
dom F is set
K33((dom F), the carrier of (L ~)) is set
K32(K33((dom F), the carrier of (L ~))) is non empty set
//\ ((\// (F,(L ~))),(L ~)) is Element of the carrier of (L ~)
Frege F is non empty Relation-like non-empty non empty-yielding product (doms F) -defined Function-like V17( product (doms F)) Function-yielding V105() ManySortedFunction of (product (doms F)) --> J,(product (doms F)) --> the carrier of (L ~)
doms F is Relation-like non-empty Function-like set
product (doms F) is non empty functional with_common_domain product-like set
(product (doms F)) --> J is non empty Relation-like non-empty non empty-yielding product (doms F) -defined {J} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{J}) Element of K32(K33((product (doms F)),{J}))
{J} is non empty V5() finite V38(1) countable set
K33((product (doms F)),{J}) is non empty set
K32(K33((product (doms F)),{J})) is non empty set
(product (doms F)) --> the carrier of (L ~) is non empty Relation-like non-empty non empty-yielding product (doms F) -defined { the carrier of (L ~)} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{ the carrier of (L ~)}) Element of K32(K33((product (doms F)),{ the carrier of (L ~)}))
K33((product (doms F)),{ the carrier of (L ~)}) is non empty set
K32(K33((product (doms F)),{ the carrier of (L ~)})) is non empty set
/\\ ((Frege F),(L ~)) is Relation-like dom (Frege F) -defined the carrier of (L ~) -valued Function-like V18( dom (Frege F), the carrier of (L ~)) Element of K32(K33((dom (Frege F)), the carrier of (L ~)))
dom (Frege F) is set
K33((dom (Frege F)), the carrier of (L ~)) is set
K32(K33((dom (Frege F)), the carrier of (L ~))) is non empty set
\\/ ((/\\ ((Frege F),(L ~))),(L ~)) is Element of the carrier of (L ~)
J --> the carrier of L is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of L} -valued Function-like constant V17(J) V18(J,{ the carrier of L}) Element of K32(K33(J,{ the carrier of L}))
{ the carrier of L} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of L}) is non empty set
K32(K33(J,{ the carrier of L})) is non empty set
\\/ ((\// (F,(L ~))),L) is Element of the carrier of L
G is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) Function-yielding V105() ManySortedFunction of K,J --> the carrier of L
/\\ (G,L) is Relation-like dom G -defined the carrier of L -valued Function-like V18( dom G, the carrier of L) Element of K32(K33((dom G), the carrier of L))
dom G is set
K33((dom G), the carrier of L) is set
K32(K33((dom G), the carrier of L)) is non empty set
\\/ ((/\\ (G,L)),L) is Element of the carrier of L
Frege G is non empty Relation-like non-empty non empty-yielding product (doms G) -defined Function-like V17( product (doms G)) Function-yielding V105() ManySortedFunction of (product (doms G)) --> J,(product (doms G)) --> the carrier of L
doms G is Relation-like non-empty Function-like set
product (doms G) is non empty functional with_common_domain product-like set
(product (doms G)) --> J is non empty Relation-like non-empty non empty-yielding product (doms G) -defined {J} -valued Function-like constant V17( product (doms G)) V18( product (doms G),{J}) Element of K32(K33((product (doms G)),{J}))
K33((product (doms G)),{J}) is non empty set
K32(K33((product (doms G)),{J})) is non empty set
(product (doms G)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms G) -defined { the carrier of L} -valued Function-like constant V17( product (doms G)) V18( product (doms G),{ the carrier of L}) Element of K32(K33((product (doms G)),{ the carrier of L}))
K33((product (doms G)),{ the carrier of L}) is non empty set
K32(K33((product (doms G)),{ the carrier of L})) is non empty set
\// ((Frege G),L) is Relation-like dom (Frege G) -defined the carrier of L -valued Function-like V18( dom (Frege G), the carrier of L) Element of K32(K33((dom (Frege G)), the carrier of L))
dom (Frege G) is set
K33((dom (Frege G)), the carrier of L) is set
K32(K33((dom (Frege G)), the carrier of L)) is non empty set
//\ ((\// ((Frege G),L)),L) is Element of the carrier of L
//\ ((/\\ ((Frege F),(L ~))),L) is Element of the carrier of L
J is non empty set
J --> the carrier of L is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of L} -valued Function-like constant V17(J) V18(J,{ the carrier of L}) Element of K32(K33(J,{ the carrier of L}))
{ the carrier of L} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of L}) is non empty set
K32(K33(J,{ the carrier of L})) is non empty set
K is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) set
F is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) Function-yielding V105() ManySortedFunction of K,J --> the carrier of L
\// (F,L) is Relation-like dom F -defined the carrier of L -valued Function-like V18( dom F, the carrier of L) Element of K32(K33((dom F), the carrier of L))
dom F is set
K33((dom F), the carrier of L) is set
K32(K33((dom F), the carrier of L)) is non empty set
//\ ((\// (F,L)),L) is Element of the carrier of L
Frege F is non empty Relation-like non-empty non empty-yielding product (doms F) -defined Function-like V17( product (doms F)) Function-yielding V105() ManySortedFunction of (product (doms F)) --> J,(product (doms F)) --> the carrier of L
doms F is Relation-like non-empty Function-like set
product (doms F) is non empty functional with_common_domain product-like set
(product (doms F)) --> J is non empty Relation-like non-empty non empty-yielding product (doms F) -defined {J} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{J}) Element of K32(K33((product (doms F)),{J}))
{J} is non empty V5() finite V38(1) countable set
K33((product (doms F)),{J}) is non empty set
K32(K33((product (doms F)),{J})) is non empty set
(product (doms F)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms F) -defined { the carrier of L} -valued Function-like constant V17( product (doms F)) V18( product (doms F),{ the carrier of L}) Element of K32(K33((product (doms F)),{ the carrier of L}))
K33((product (doms F)),{ the carrier of L}) is non empty set
K32(K33((product (doms F)),{ the carrier of L})) is non empty set
/\\ ((Frege F),L) is Relation-like dom (Frege F) -defined the carrier of L -valued Function-like V18( dom (Frege F), the carrier of L) Element of K32(K33((dom (Frege F)), the carrier of L))
dom (Frege F) is set
K33((dom (Frege F)), the carrier of L) is set
K32(K33((dom (Frege F)), the carrier of L)) is non empty set
\\/ ((/\\ ((Frege F),L)),L) is Element of the carrier of L
the carrier of (L ~) is non empty set
J --> the carrier of (L ~) is non empty Relation-like non-empty non empty-yielding J -defined { the carrier of (L ~)} -valued Function-like constant V17(J) V18(J,{ the carrier of (L ~)}) Element of K32(K33(J,{ the carrier of (L ~)}))
{ the carrier of (L ~)} is non empty V5() finite V38(1) countable set
K33(J,{ the carrier of (L ~)}) is non empty set
K32(K33(J,{ the carrier of (L ~)})) is non empty set
\\/ ((\// (F,L)),(L ~)) is Element of the carrier of (L ~)
G is non empty Relation-like non-empty non empty-yielding J -defined Function-like V17(J) Function-yielding V105() ManySortedFunction of K,J --> the carrier of (L ~)
/\\ (G,(L ~)) is Relation-like dom G -defined the carrier of (L ~) -valued Function-like V18( dom G, the carrier of (L ~)) Element of K32(K33((dom G), the carrier of (L ~)))
dom G is set
K33((dom G), the carrier of (L ~)) is set
K32(K33((dom G), the carrier of (L ~))) is non empty set
\\/ ((/\\ (G,(L ~))),(L ~)) is Element of the carrier of (L ~)
Frege G is non empty Relation-like non-empty non empty-yielding product (doms G) -defined Function-like V17( product (doms G)) Function-yielding V105() ManySortedFunction of (product (doms G)) --> J,(product (doms G)) --> the carrier of (L ~)
doms G is Relation-like non-empty Function-like set
product (doms G) is non empty functional with_common_domain product-like set
(product (doms G)) --> J is non empty Relation-like non-empty non empty-yielding product (doms G) -defined {J} -valued Function-like constant V17( product (doms G)) V18( product (doms G),{J}) Element of K32(K33((product (doms G)),{J}))
K33((product (doms G)),{J}) is non empty set
K32(K33((product (doms G)),{J})) is non empty set
(product (doms G)) --> the carrier of (L ~) is non empty Relation-like non-empty non empty-yielding product (doms G) -defined { the carrier of (L ~)} -valued Function-like constant V17( product (doms G)) V18( product (doms G),{ the carrier of (L ~)}) Element of K32(K33((product (doms G)),{ the carrier of (L ~)}))
K33((product (doms G)),{ the carrier of (L ~)}) is non empty set
K32(K33((product (doms G)),{ the carrier of (L ~)})) is non empty set
\// ((Frege G),(L ~)) is Relation-like dom (Frege G) -defined the carrier of (L ~) -valued Function-like V18( dom (Frege G), the carrier of (L ~)) Element of K32(K33((dom (Frege G)), the carrier of (L ~)))
dom (Frege G) is set
K33((dom (Frege G)), the carrier of (L ~)) is set
K32(K33((dom (Frege G)), the carrier of (L ~))) is non empty set
//\ ((\// ((Frege G),(L ~))),(L ~)) is Element of the carrier of (L ~)
//\ ((/\\ ((Frege F),L)),(L ~)) is Element of the carrier of (L ~)