:: WAYBEL_0 semantic presentation

K224() is Element of K10(K220())
K220() is set
K10(K220()) is non empty set
K122() is set
K10(K122()) is non empty set
{} is empty finite V38() set
the empty finite V38() set is empty finite V38() set
1 is non empty set
{{},1} is non empty finite set
K10(K224()) is non empty set
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
L is non empty transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
X is finite Element of K10(c₂)
b is non empty set
the Element of b is Element of b
c is Element of the carrier of L
y is set
y is set
x is Element of the carrier of L
x is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
{y} is non empty finite set
y \/ {y} is non empty set
c₁₂ is Element of the carrier of L
a9 is Element of the carrier of L
b is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
{b,X} is non empty finite Element of K10( the carrier of L)
X is Element of the carrier of L
L is non empty transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
X is finite Element of K10(c₂)
b is non empty set
the Element of b is Element of b
c is Element of the carrier of L
y is set
y is set
x is Element of the carrier of L
x is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
{y} is non empty finite set
y \/ {y} is non empty set
c₁₂ is Element of the carrier of L
a9 is Element of the carrier of L
b is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
{b,X} is non empty finite Element of K10( the carrier of L)
X is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
{} L is empty finite V38() strongly_connected Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
{} L is empty finite V38() strongly_connected (L) (L) Element of K10( 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 K10(K11( the carrier of L, the carrier of L))
K11( the carrier of L, the carrier of L) is set
K10(K11( the carrier of L, the carrier of L)) is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
c₂ is RelStr
the carrier of c₂ is set
the InternalRel of c₂ is Relation-like the carrier of c₂ -defined the carrier of c₂ -valued Element of K10(K11( the carrier of c₂, the carrier of c₂))
K11( the carrier of c₂, the carrier of c₂) is set
K10(K11( the carrier of c₂, the carrier of c₂)) is non empty set
RelStr(# the carrier of c₂, the InternalRel of c₂ #) is strict RelStr
K10( the carrier of L) is non empty set
K10( the carrier of c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of K10( the carrier of c₂)
X is Element of the carrier of c₂
c is Element of the carrier of c₂
y is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
Y is Element of the carrier of c₂
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 K10(K11( the carrier of L, the carrier of L))
K11( the carrier of L, the carrier of L) is set
K10(K11( the carrier of L, the carrier of L)) is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
c₂ is RelStr
the carrier of c₂ is set
the InternalRel of c₂ is Relation-like the carrier of c₂ -defined the carrier of c₂ -valued Element of K10(K11( the carrier of c₂, the carrier of c₂))
K11( the carrier of c₂, the carrier of c₂) is set
K10(K11( the carrier of c₂, the carrier of c₂)) is non empty set
RelStr(# the carrier of c₂, the InternalRel of c₂ #) is strict RelStr
K10( the carrier of L) is non empty set
K10( the carrier of c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of K10( the carrier of c₂)
X is Element of the carrier of c₂
c is Element of the carrier of c₂
y is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
Y is Element of the carrier of c₂
L is non empty V58() reflexive RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
{c₂} is non empty finite Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
L is non empty V58() reflexive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
the Element of the carrier of L is Element of the carrier of L
{ the Element of the carrier of L} is non empty finite Element of K10( the carrier of L)
L is non empty with_suprema RelStr
[#] L is non empty non proper Element of K10( the carrier of L)
the carrier of L is non empty set
K10( the carrier of L) is non empty set
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty upper-bounded RelStr
[#] L is non empty non proper Element of K10( the carrier of L)
the carrier of L is non empty set
K10( the carrier of L) is non empty set
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty with_infima RelStr
[#] L is non empty non proper Element of K10( the carrier of L)
the carrier of L is non empty set
K10( the carrier of L) is non empty set
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty lower-bounded RelStr
[#] L is non empty non proper Element of K10( the carrier of L)
the carrier of L is non empty set
K10( the carrier of L) is non empty set
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty RelStr
L is non empty RelStr
c₂ is SubRelStr of L
the carrier of c₂ is set
K10( the carrier of c₂) is non empty set
b is (c₂) Element of K10( the carrier of c₂)
"/\" (b,L) is Element of the carrier of L
the carrier of L is non empty set
c₂ is SubRelStr of L
the carrier of c₂ is set
K10( the carrier of c₂) is non empty set
b is (c₂) Element of K10( the carrier of c₂)
"\/" (b,L) is Element of the carrier of L
the carrier of L is non empty set
L is non empty RelStr
the non empty strict full meet-inheriting join-inheriting infs-inheriting sups-inheriting (L) (L) SubRelStr of L is non empty strict full meet-inheriting join-inheriting infs-inheriting sups-inheriting (L) (L) SubRelStr of L
L is non empty transitive RelStr
c₂ is non empty transitive full (L) SubRelStr of L
the carrier of c₂ is non empty set
K10( the carrier of c₂) is non empty set
b is (c₂) Element of K10( the carrier of c₂)
"/\" (b,c₂) is Element of the carrier of c₂
"/\" (b,L) is Element of the carrier of L
the carrier of L is non empty set
L is non empty transitive RelStr
c₂ is non empty transitive full (L) SubRelStr of L
the carrier of c₂ is non empty set
K10( the carrier of c₂) is non empty set
b is (c₂) Element of K10( the carrier of c₂)
"\/" (b,c₂) is Element of the carrier of c₂
"\/" (b,L) is Element of the carrier of L
the carrier of L is non empty set
L is RelStr
the carrier of L is set
c₂ is RelStr
the carrier of c₂ is set
K11( the carrier of L, the carrier of c₂) is set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
c₂ is non empty set
K11(c₂,c₂) is non empty set
K10(K11(c₂,c₂)) is non empty set
L is 1-sorted
the carrier of L is set
K11(c₂, the carrier of L) is set
K10(K11(c₂, the carrier of L)) is non empty set
b is Relation-like c₂ -defined c₂ -valued Element of K10(K11(c₂,c₂))
X is Relation-like c₂ -defined the carrier of L -valued Function-like V21(c₂, the carrier of L) Element of K10(K11(c₂, the carrier of L))
(L,c₂,b,X) is (L) (L)
L is 1-sorted
the non empty V58() reflexive transitive antisymmetric with_suprema RelStr is non empty V58() reflexive transitive antisymmetric with_suprema RelStr
the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr is non empty set
the carrier of L is set
K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L) is set
K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L)) is non empty set
the Relation-like the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr -defined the carrier of L -valued Function-like V21( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L) Element of K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L)) is Relation-like the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr -defined the carrier of L -valued Function-like V21( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L) Element of K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L))
the InternalRel of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr is Relation-like the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr -defined the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr -valued V20( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr ) reflexive antisymmetric transitive Element of K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr ))
K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr ) is non empty set
K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr )) is non empty set
(L, the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the Relation-like the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr -defined the carrier of L -valued Function-like V21( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L) Element of K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the carrier of L))) is non empty (L) (L)
X is non empty (L) (L)
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K10(K11( the carrier of X, the carrier of X))
the carrier of X is non empty set
K11( the carrier of X, the carrier of X) is non empty set
K10(K11( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict RelStr
RelStr(# the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr #) is non empty strict V58() reflexive transitive antisymmetric RelStr
[#] the non empty V58() reflexive transitive antisymmetric with_suprema RelStr is non empty non proper ( the non empty V58() reflexive transitive antisymmetric with_suprema RelStr ) Element of K10( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr )
K10( the carrier of the non empty V58() reflexive transitive antisymmetric with_suprema RelStr ) is non empty set
[#] X is non empty non proper Element of K10( the carrier of X)
K10( the carrier of X) is non empty set
L is non empty 1-sorted
c₂ is non empty (L)
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
the carrier of c₂ is non empty set
the carrier of L is non empty set
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
b is Element of the carrier of c₂
the of c₂ . b is Element of the carrier of L
L is non empty RelStr
L is non empty 1-sorted
L is non empty 1-sorted
c₂ is non empty (L)
b is set
X is set
the carrier of c₂ is non empty set
X is Element of the carrier of c₂
c is Element of the carrier of c₂
(L,c₂,c) is Element of the carrier of L
the carrier of L is non empty set
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . c is Element of the carrier of L
X is Element of the carrier of c₂
c is Element of the carrier of c₂
(L,c₂,c) is Element of the carrier of L
the carrier of L is non empty set
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . c is Element of the carrier of L
L is non empty 1-sorted
the carrier of L is non empty set
c₂ is non empty (L)
b is set
the carrier of L \ b is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
the carrier of c₂ is non empty set
X is Element of the carrier of c₂
c is Element of the carrier of c₂
(L,c₂,c) is Element of the carrier of L
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . c is Element of the carrier of L
the carrier of c₂ is non empty set
X is Element of the carrier of c₂
c is Element of the carrier of c₂
(L,c₂,c) is Element of the carrier of L
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . c is Element of the carrier of L
L is non empty 1-sorted
the carrier of L is non empty set
c₂ is non empty (L)
b is set
the carrier of L \ b is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
the carrier of c₂ is non empty set
X is Element of the carrier of c₂
c is Element of the carrier of c₂
(L,c₂,c) is Element of the carrier of L
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . c is Element of the carrier of L
the carrier of c₂ is non empty set
X is Element of the carrier of c₂
c is Element of the carrier of c₂
(L,c₂,c) is Element of the carrier of L
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . c is Element of the carrier of L
F₁() is non empty RelStr
F₂() is non empty (F₁())
the carrier of F₂() is non empty set
{ (F₁(),F₂(),b₁) where b₁ is Element of the carrier of F₂() : P₁[(F₁(),F₂(),b₁)] } is set
c₂ is Element of the carrier of F₂()
b is Element of the carrier of F₂()
X is Element of the carrier of F₂()
(F₁(),F₂(),X) is Element of the carrier of F₁()
the carrier of F₁() is non empty set
the of F₂() is Relation-like the carrier of F₂() -defined the carrier of F₁() -valued Function-like V21( the carrier of F₂(), the carrier of F₁()) Element of K10(K11( the carrier of F₂(), the carrier of F₁()))
K11( the carrier of F₂(), the carrier of F₁()) is non empty set
K10(K11( the carrier of F₂(), the carrier of F₁())) is non empty set
the of F₂() . X is Element of the carrier of F₁()
X is Element of the carrier of F₂()
(F₁(),F₂(),X) is Element of the carrier of F₁()
the of F₂() . X is Element of the carrier of F₁()
c₂ is Element of the carrier of F₂()
b is Element of the carrier of F₂()
(F₁(),F₂(),b) is Element of the carrier of F₁()
the of F₂() . b is Element of the carrier of F₁()
L is non empty RelStr
L is non empty RelStr
c₂ is non empty (L)
the carrier of c₂ is non empty set
the carrier of L is non empty set
b is Element of the carrier of c₂
(L,c₂,b) is Element of the carrier of L
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . b is Element of the carrier of L
{ (L,c₂,b₁) where b₁ is Element of the carrier of c₂ : S₁[(L,c₂,b₁)] } is set
b is Element of the carrier of c₂
(L,c₂,b) is Element of the carrier of L
the of c₂ . b is Element of the carrier of L
{ (L,c₂,b₁) where b₁ is Element of the carrier of c₂ : (L,c₂,b) <= (L,c₂,b₁) } is set
b is Element of the carrier of c₂
(L,c₂,b) is Element of the carrier of L
the of c₂ . b is Element of the carrier of L
{ (L,c₂,b₁) where b₁ is Element of the carrier of c₂ : (L,c₂,b) <= (L,c₂,b₁) } is set
X is Element of the carrier of c₂
L is non empty RelStr
c₂ is non empty (L)
the carrier of c₂ is non empty set
the carrier of L is non empty set
b is Element of the carrier of c₂
(L,c₂,b) is Element of the carrier of L
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ . b is Element of the carrier of L
{ (L,c₂,b₁) where b₁ is Element of the carrier of c₂ : S₁[(L,c₂,b₁)] } is set
b is Element of the carrier of c₂
(L,c₂,b) is Element of the carrier of L
the of c₂ . b is Element of the carrier of L
{ (L,c₂,b₁) where b₁ is Element of the carrier of c₂ : (L,c₂,b₁) <= (L,c₂,b) } is set
b is Element of the carrier of c₂
(L,c₂,b) is Element of the carrier of L
the of c₂ . b is Element of the carrier of L
{ (L,c₂,b₁) where b₁ is Element of the carrier of c₂ : (L,c₂,b₁) <= (L,c₂,b) } is set
X is Element of the carrier of c₂
L is non empty RelStr
c₂ is non empty () (L)
the carrier of c₂ is non empty set
the carrier of L is non empty set
(L,c₂) is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
b is Element of the carrier of c₂
X is Element of the carrier of c₂
X is Element of the carrier of c₂
(L,c₂,b) is Element of the carrier of L
the of c₂ . b is Element of the carrier of L
(L,c₂,X) is Element of the carrier of L
the of c₂ . X is Element of the carrier of L
c₂ is non empty () (L)
the carrier of c₂ is non empty set
the carrier of L is non empty set
(L,c₂) is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
the of c₂ is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
b is Element of the carrier of c₂
X is Element of the carrier of c₂
X is Element of the carrier of c₂
(L,c₂,X) is Element of the carrier of L
the of c₂ . X is Element of the carrier of L
(L,c₂,b) is Element of the carrier of L
the of c₂ . b is Element of the carrier of L
L is non empty V58() reflexive RelStr
the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr is non empty V58() reflexive transitive antisymmetric upper-bounded RelStr
the carrier of L is non empty set
the Element of the carrier of L is Element of the carrier of L
the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr is non empty set
the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr --> the Element of the carrier of L is Relation-like the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr -defined the carrier of L -valued Function-like V21( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of L) Element of K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of L))
K11( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of L) is non empty set
K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of L)) is non empty set
the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr is Relation-like the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr -defined the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr -valued V20( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ) reflexive antisymmetric transitive Element of K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ))
K11( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ) is non empty set
K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr )) is non empty set
X is Relation-like the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr -defined the carrier of L -valued Function-like V21( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of L) Element of K10(K11( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the carrier of L))
(L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X) is non empty (L) (L)
the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X) is non empty set
the InternalRel of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X) is Relation-like the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X) -defined the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X) -valued Element of K10(K11( the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X), the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X)))
K11( the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X), the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X)) is non empty set
K10(K11( the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X), the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X))) is non empty set
RelStr(# the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X), the InternalRel of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X) #) is non empty strict RelStr
RelStr(# the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr #) is non empty strict V58() reflexive transitive antisymmetric RelStr
[#] the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr is non empty non proper ( the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ) Element of K10( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr )
K10( the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ) is non empty set
[#] (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X) is non empty non proper Element of K10( the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X))
K10( the carrier of (L, the carrier of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr , the InternalRel of the non empty V58() reflexive transitive antisymmetric upper-bounded RelStr ,X)) is non empty set
y is non empty () (L)
the carrier of y is non empty set
y is Element of the carrier of y
x is Element of the carrier of y
(L,y) is Relation-like the carrier of y -defined the carrier of L -valued Function-like V21( the carrier of y, the carrier of L) Element of K10(K11( the carrier of y, the carrier of L))
K11( the carrier of y, the carrier of L) is non empty set
K10(K11( the carrier of y, the carrier of L)) is non empty set
the of y is Relation-like the carrier of y -defined the carrier of L -valued Function-like V21( the carrier of y, the carrier of L) Element of K10(K11( the carrier of y, the carrier of L))
(L,y) . y is set
(L,y) . x is set
Y is Element of the carrier of L
Y is Element of the carrier of L
(L,y) . y is Element of the carrier of L
(L,y) . x is Element of the carrier of L
the carrier of y is non empty set
y is Element of the carrier of y
x is Element of the carrier of y
(L,y) is Relation-like the carrier of y -defined the carrier of L -valued Function-like V21( the carrier of y, the carrier of L) Element of K10(K11( the carrier of y, the carrier of L))
K11( the carrier of y, the carrier of L) is non empty set
K10(K11( the carrier of y, the carrier of L)) is non empty set
the of y is Relation-like the carrier of y -defined the carrier of L -valued Function-like V21( the carrier of y, the carrier of L) Element of K10(K11( the carrier of y, the carrier of L))
(L,y) . y is set
(L,y) . x is set
Y is Element of the carrier of L
Y is Element of the carrier of L
(L,y) . y is Element of the carrier of L
(L,y) . x is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
b is set
X is set
X is Element of K10( the carrier of L)
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
c is Element of the carrier of L
b is Element of K10( the carrier of L)
X is Element of K10( the carrier of L)
X is set
c is Element of the carrier of L
y is Element of the carrier of L
X is set
c is Element of the carrier of L
y is Element of the carrier of L
b is set
X is set
X is Element of K10( the carrier of L)
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
c is Element of the carrier of L
b is Element of K10( the carrier of L)
X is Element of K10( the carrier of L)
X is set
c is Element of the carrier of L
y is Element of the carrier of L
X is set
c is Element of the carrier of L
y 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 K10(K11( the carrier of L, the carrier of L))
K11( the carrier of L, the carrier of L) is set
K10(K11( the carrier of L, the carrier of L)) is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
c₂ is RelStr
the carrier of c₂ is set
the InternalRel of c₂ is Relation-like the carrier of c₂ -defined the carrier of c₂ -valued Element of K10(K11( the carrier of c₂, the carrier of c₂))
K11( the carrier of c₂, the carrier of c₂) is set
K10(K11( the carrier of c₂, the carrier of c₂)) is non empty set
RelStr(# the carrier of c₂, the InternalRel of c₂ #) is strict RelStr
K10( the carrier of L) is non empty set
K10( the carrier of c₂) is non empty set
b is Element of K10( the carrier of L)
(L,b) is Element of K10( the carrier of L)
(L,b) is Element of K10( the carrier of L)
X is Element of K10( the carrier of c₂)
(c₂,X) is Element of K10( the carrier of c₂)
(c₂,X) is Element of K10( the carrier of c₂)
X is set
c is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of c₂
x is Element of the carrier of c₂
X is set
c is Element of the carrier of c₂
y is Element of the carrier of c₂
y is Element of the carrier of L
x is Element of the carrier of L
X is set
c is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of c₂
y is Element of the carrier of c₂
X is set
c is Element of the carrier of c₂
y is Element of the carrier of c₂
x is Element of the carrier of L
y is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in c₂ ) } is set
X is set
X is Element of the carrier of L
c is Element of the carrier of L
X is set
X is Element of the carrier of L
c is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in c₂ ) } is set
X is set
X is Element of the carrier of L
c is Element of the carrier of L
X is set
X is Element of the carrier of L
c is Element of the carrier of L
L is non empty V58() reflexive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
the Element of c₂ is Element of c₂
X is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
the Element of c₂ is Element of c₂
X is Element of the carrier of L
L is V58() reflexive RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V20( the carrier of L) reflexive Element of K10(K11( the carrier of L, the carrier of L))
K11( the carrier of L, the carrier of L) is set
K10(K11( the carrier of L, the carrier of L)) is non empty set
b is set
X is Element of the carrier of L
[X,X] is set
{X,X} is non empty finite set
{X} is non empty finite set
{{X,X},{X}} is non empty finite V38() set
b is set
X is Element of the carrier of L
[X,X] is set
{X,X} is non empty finite set
{X} is non empty finite set
{{X,X},{X}} is non empty finite V38() set
L is non empty RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
{c₂} is non empty finite Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
(L,{c₂}) is Element of K10( the carrier of L)
(L,{c₂}) is Element of K10( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
b is Element of the carrier of L
c₂ is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is Element of K10( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in {c₂} ) } is set
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
b is Element of the carrier of L
c₂ is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is Element of K10( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in {c₂} ) } is set
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive antisymmetric RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is non empty Element of K10( the carrier of L)
b is Element of the carrier of L
(L,b) is Element of K10( the carrier of L)
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is non empty Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive antisymmetric RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is non empty Element of K10( the carrier of L)
b is Element of the carrier of L
(L,b) is Element of K10( the carrier of L)
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is non empty Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty transitive RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
b is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is Element of K10( the carrier of L)
(L,b) is Element of K10( the carrier of L)
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is Element of K10( the carrier of L)
X is set
X is Element of the carrier of L
L is non empty transitive RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
b is Element of the carrier of L
(L,b) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is Element of K10( the carrier of L)
X is set
X is Element of the carrier of L
L is non empty V58() reflexive RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is non empty Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
(L,{c₂}) is non empty Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
b is set
X is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
b is set
X is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
X 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 K10(K11( the carrier of L, the carrier of L))
K11( the carrier of L, the carrier of L) is set
K10(K11( the carrier of L, the carrier of L)) is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
c₂ is RelStr
the carrier of c₂ is set
the InternalRel of c₂ is Relation-like the carrier of c₂ -defined the carrier of c₂ -valued Element of K10(K11( the carrier of c₂, the carrier of c₂))
K11( the carrier of c₂, the carrier of c₂) is set
K10(K11( the carrier of c₂, the carrier of c₂)) is non empty set
RelStr(# the carrier of c₂, the InternalRel of c₂ #) is strict RelStr
K10( the carrier of L) is non empty set
K10( the carrier of c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of K10( the carrier of c₂)
(L,b) is Element of K10( the carrier of L)
(c₂,X) is Element of K10( the carrier of c₂)
(L,b) is Element of K10( the carrier of L)
(c₂,X) is Element of K10( the carrier of c₂)
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
K10(K10( the carrier of L)) is non empty set
c₂ is Element of K10(K10( the carrier of L))
union c₂ is Element of K10( the carrier of L)
b is Element of K10(K10( the carrier of L))
union b is Element of K10( the carrier of L)
X is Element of K10( the carrier of L)
X is Element of the carrier of L
c is Element of the carrier of L
y is set
y is Element of K10( the carrier of L)
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
b is Element of K10( the carrier of L)
c₂ /\ b is Element of K10( the carrier of L)
c₂ \/ b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
K10(K10( the carrier of L)) is non empty set
c₂ is Element of K10(K10( the carrier of L))
union c₂ is Element of K10( the carrier of L)
b is Element of K10(K10( the carrier of L))
union b is Element of K10( the carrier of L)
X is Element of K10( the carrier of L)
X is Element of the carrier of L
c is Element of the carrier of L
y is set
y is Element of K10( the carrier of L)
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
b is Element of K10( the carrier of L)
c₂ /\ b is Element of K10( the carrier of L)
c₂ \/ b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty transitive RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is (L) Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
(L,{c₂}) is (L) Element of K10( the carrier of L)
L is non empty RelStr
[#] L is non empty non proper Element of K10( the carrier of L)
the carrier of L is non empty set
K10( the carrier of L) is non empty set
b is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
[#] L is non empty non proper (L) (L) Element of K10( the carrier of L)
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
the Element of the carrier of L is Element of the carrier of L
(L, the Element of the carrier of L) is non empty (L) (L) Element of K10( the carrier of L)
{ the Element of the carrier of L} is non empty finite Element of K10( the carrier of L)
(L,{ the Element of the carrier of L}) is non empty (L) Element of K10( the carrier of L)
the Element of the carrier of L is Element of the carrier of L
(L, the Element of the carrier of L) is non empty (L) (L) Element of K10( the carrier of L)
{ the Element of the carrier of L} is non empty finite Element of K10( the carrier of L)
(L,{ the Element of the carrier of L}) is non empty (L) Element of K10( the carrier of L)
L is non empty V58() reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
[#] L is non empty non proper (L) (L) (L) (L) Element of K10( the carrier of L)
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is (L) Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
"\/" (c₂,L) is Element of the carrier of L
(L,c₂) is (L) Element of K10( the carrier of L)
"\/" ((L,c₂),L) is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
(L,c₂) is non empty (L) (L) Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is non empty (L) Element of K10( the carrier of L)
"\/" ((L,c₂),L) is Element of the carrier of L
"\/" ({c₂},L) is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is (L) Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
"/\" (c₂,L) is Element of the carrier of L
(L,c₂) is (L) Element of K10( the carrier of L)
"/\" ((L,c₂),L) is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
(L,c₂) is non empty (L) (L) Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
{c₂} is non empty finite Element of K10( the carrier of L)
(L,{c₂}) is non empty (L) Element of K10( the carrier of L)
"/\" ((L,c₂),L) is Element of the carrier of L
"/\" ({c₂},L) is Element of the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
b "\/" X is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
b "\/" X is Element of the carrier of L
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
b "/\" X is Element of the carrier of L
X is Element of the carrier of L
b is Element of the carrier of L
X is Element of the carrier of L
b "/\" X is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) Element of K10( the carrier of L)
K10(c₂) is non empty set
b is finite Element of K10(c₂)
"\/" (b,L) is Element of the carrier of L
X is Element of the carrier of L
the Element of c₂ is Element of c₂
X is finite Element of K10(c₂)
X is Element of the carrier of L
X is finite Element of K10(c₂)
"\/" (X,L) is Element of the carrier of L
X is finite Element of K10(c₂)
L is non empty V58() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) Element of K10( the carrier of L)
K10(c₂) is non empty set
b is finite Element of K10(c₂)
"/\" (b,L) is Element of the carrier of L
X is Element of the carrier of L
the Element of c₂ is Element of c₂
X is finite Element of K10(c₂)
X is Element of the carrier of L
X is finite Element of K10(c₂)
"/\" (X,L) is Element of the carrier of L
X is finite Element of K10(c₂)
L is non empty antisymmetric RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
b is Element of K10( the carrier of L)
c₂ /\ b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
X "\/" X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
c "/\" y is Element of the carrier of L
y is Element of the carrier of L
L is non empty antisymmetric RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
b is Element of K10( the carrier of L)
c₂ /\ b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
X "/\" X is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
c "\/" y is Element of the carrier of L
y is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
K10(K10( the carrier of L)) is non empty set
c₂ is Element of K10(K10( the carrier of L))
union c₂ is Element of K10( the carrier of L)
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
c is set
y is set
y is Element of K10( the carrier of L)
x is Element of K10( the carrier of L)
y \/ x is Element of K10( the carrier of L)
Y is Element of K10( the carrier of L)
Y is Element of the carrier of L
L is RelStr
the carrier of L is set
K10( the carrier of L) is non empty set
K10(K10( the carrier of L)) is non empty set
c₂ is Element of K10(K10( the carrier of L))
union c₂ is Element of K10( the carrier of L)
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
c is set
y is set
y is Element of K10( the carrier of L)
x is Element of K10( the carrier of L)
y \/ x is Element of K10( the carrier of L)
Y is Element of K10( the carrier of L)
Y is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) (L) Element of K10( the carrier of L)
b is Element of the carrier of L
(L,b) is non empty (L) (L) Element of K10( the carrier of L)
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is non empty (L) Element of K10( the carrier of L)
X is set
X is Element of the carrier of L
X is set
X is Element of the carrier of L
b is Element of the carrier of L
(L,b) is non empty (L) (L) Element of K10( the carrier of L)
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is non empty (L) Element of K10( the carrier of L)
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) (L) Element of K10( the carrier of L)
b is Element of the carrier of L
(L,b) is non empty (L) (L) Element of K10( the carrier of L)
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is non empty (L) Element of K10( the carrier of L)
X is set
X is Element of the carrier of L
X is set
X is Element of the carrier of L
b is Element of the carrier of L
(L,b) is non empty (L) (L) Element of K10( the carrier of L)
{b} is non empty finite Element of K10( the carrier of L)
(L,{b}) is non empty (L) Element of K10( the carrier of L)
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
{ b₁ where b₁ is non empty (L) (L) Element of K10( the carrier of L) : verum } is set
{ b₁ where b₁ is non empty (L) (L) Element of K10( the carrier of L) : verum } is set
L is non empty V58() reflexive transitive RelStr
(L) is set
the carrier of L is non empty set
K10( the carrier of L) is non empty set
{ b₁ where b₁ is non empty (L) (L) Element of K10( the carrier of L) : verum } is set
{{}} is non empty finite V38() set
(L) \/ {{}} is non empty set
(L) is set
{ b₁ where b₁ is non empty (L) (L) Element of K10( the carrier of L) : verum } is set
(L) \/ {{}} is non empty set
L is non empty RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_sup_of b₁,L } is set
X is set
X is finite Element of K10(c₂)
"\/" (X,L) is Element of the carrier of L
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_inf_of b₁,L } is set
X is set
c is finite Element of K10(c₂)
"/\" (c,L) is Element of the carrier of L
L is non empty antisymmetric lower-bounded RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_sup_of b₁,L } is set
{} c₂ is empty finite V38() Element of K10(c₂)
"\/" (({} c₂),L) is Element of the carrier of L
L is non empty antisymmetric upper-bounded RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_inf_of b₁,L } is set
{} c₂ is empty finite V38() Element of K10(c₂)
"/\" (({} c₂),L) is Element of the carrier of L
L is non empty V58() reflexive antisymmetric RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_sup_of b₁,L } is set
the Element of c₂ is Element of c₂
X is Element of the carrier of L
{X} is non empty finite Element of K10( the carrier of L)
X is finite Element of K10(c₂)
"\/" (X,L) is Element of the carrier of L
(L,c₂) is Element of K10( the carrier of L)
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_inf_of b₁,L } is set
the Element of c₂ is Element of c₂
X is Element of the carrier of L
{X} is non empty finite Element of K10( the carrier of L)
X is finite Element of K10(c₂)
"/\" (X,L) is Element of the carrier of L
L is non empty V58() reflexive antisymmetric RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_sup_of b₁,L } is set
(L,c₂) is Element of K10( the carrier of L)
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_inf_of b₁,L } is set
b is set
{b} is non empty finite set
X is Element of the carrier of L
X is finite Element of K10(c₂)
"\/" (X,L) is Element of the carrier of L
{X} is non empty finite Element of K10( the carrier of L)
b is set
{b} is non empty finite set
X is Element of the carrier of L
X is finite Element of K10(c₂)
"/\" (X,L) is Element of the carrier of L
{X} is non empty finite Element of K10( the carrier of L)
L is non empty transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
c is finite Element of K10(c₂)
"\/" (c,L) is Element of the carrier of L
y is finite Element of K10(c₂)
"\/" (y,L) is Element of the carrier of L
c \/ y is finite Element of K10(c₂)
"\/" ((c \/ y),L) is Element of the carrier of L
y is Element of the carrier of L
{} \/ {} is finite V38() set
L is non empty V58() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_sup_of b₁,L } is set
b is Element of K10( the carrier of L)
K10(b) is non empty set
X is finite Element of K10(b)
X is Element of the carrier of L
(L,b) is Element of K10( the carrier of L)
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(b) : ex_sup_of b₁,L } is set
X is finite Element of K10(b)
"\/" (X,L) is Element of the carrier of L
X is finite Element of K10(b)
X is Element of K10( the carrier of L)
"\/" (X,L) is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
c is finite Element of K10(c₂)
"\/" (c,L) is Element of the carrier of L
X is Element of the carrier of L
{X} is non empty finite Element of K10( the carrier of L)
"\/" ({X},L) is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
"\/" (b,L) is Element of the carrier of L
"\/" (c₂,L) is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
"\/" (c₂,L) is Element of the carrier of L
(L,c₂) is (L) Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_sup_of b₁,L } is set
"\/" ((L,c₂),L) is Element of the carrier of L
b is finite Element of K10(c₂)
b is Element of the carrier of L
X is finite Element of K10(c₂)
"\/" (X,L) is Element of the carrier of L
b is finite Element of K10(c₂)
X is Element of K10( the carrier of L)
"\/" (b,L) is Element of the carrier of L
L is non empty transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
c is finite Element of K10(c₂)
"/\" (c,L) is Element of the carrier of L
y is finite Element of K10(c₂)
"/\" (y,L) is Element of the carrier of L
c \/ y is finite Element of K10(c₂)
"/\" ((c \/ y),L) is Element of the carrier of L
y is Element of the carrier of L
{} \/ {} is finite V38() set
L is non empty V58() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_inf_of b₁,L } is set
b is Element of K10( the carrier of L)
K10(b) is non empty set
X is finite Element of K10(b)
X is Element of the carrier of L
(L,b) is Element of K10( the carrier of L)
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(b) : ex_inf_of b₁,L } is set
X is finite Element of K10(b)
"/\" (X,L) is Element of the carrier of L
X is finite Element of K10(b)
X is Element of K10( the carrier of L)
"/\" (X,L) is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
c is finite Element of K10(c₂)
"/\" (c,L) is Element of the carrier of L
X is Element of the carrier of L
{X} is non empty finite Element of K10( the carrier of L)
"/\" ({X},L) is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
K10(c₂) is non empty set
b is Element of K10( the carrier of L)
"/\" (b,L) is Element of the carrier of L
"/\" (c₂,L) is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
"/\" (c₂,L) is Element of the carrier of L
(L,c₂) is (L) Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_inf_of b₁,L } is set
"/\" ((L,c₂),L) is Element of the carrier of L
b is finite Element of K10(c₂)
b is Element of the carrier of L
X is finite Element of K10(c₂)
"/\" (X,L) is Element of the carrier of L
b is finite Element of K10(c₂)
X is Element of K10( the carrier of L)
"/\" (b,L) is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_sup_of b₁,L } is set
(L,(L,c₂)) is (L) (L) Element of K10( the carrier of L)
b is non empty (L) (L) Element of K10( the carrier of L)
X is set
X is Element of the carrier of L
c is Element of the carrier of L
y is finite Element of K10(c₂)
"\/" (y,L) is Element of the carrier of L
the Element of b is Element of b
x is Element of the carrier of L
{x} is non empty finite Element of K10( the carrier of L)
"\/" ({x},L) is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of K10( the carrier of L)
(L,c₂) is (L) Element of K10( the carrier of L)
K10(c₂) is non empty set
{ ("/\" (b₁,L)) where b₁ is finite Element of K10(c₂) : ex_inf_of b₁,L } is set
(L,(L,c₂)) is (L) (L) Element of K10( the carrier of L)
b is non empty (L) (L) Element of K10( the carrier of L)
X is set
X is Element of the carrier of L
c is Element of the carrier of L
y is finite Element of K10(c₂)
"/\" (y,L) is Element of the carrier of L
the Element of b is Element of b
x is Element of the carrier of L
{x} is non empty finite Element of K10( the carrier of L)
"/\" ({x},L) is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
L is non empty V58() reflexive RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
b is Element of the carrier of L
0 is empty finite V38() Element of K224()
{0} is non empty finite V38() set
K11({0},{0}) is non empty finite set
K10(K11({0},{0})) is non empty finite V38() set
the Relation-like {0} -defined {0} -valued V20({0}) finite reflexive antisymmetric transitive Element of K10(K11({0},{0})) is Relation-like {0} -defined {0} -valued V20({0}) finite reflexive antisymmetric transitive Element of K10(K11({0},{0}))
RelStr(# {0}, the Relation-like {0} -defined {0} -valued V20({0}) finite reflexive antisymmetric transitive Element of K10(K11({0},{0})) #) is non empty trivial finite 1 -element strict V58() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() () RelStr
c₂ is non empty trivial finite 1 -element strict V58() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() () RelStr
the carrier of c₂ is non empty trivial finite set
b is Element of the carrier of c₂
X is Element of the carrier of c₂
L is non empty V58() reflexive transitive antisymmetric () RelStr
L ~ is non empty strict V58() 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 V20( the carrier of L) reflexive antisymmetric transitive Element of K10(K11( the carrier of L, the carrier of L))
K11( the carrier of L, the carrier of L) is non empty set
K10(K11( 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 K10(K11( the carrier of L, the carrier of L))
RelStr(# the carrier of L,( the InternalRel of L ~) #) is non empty strict RelStr
the carrier of (L ~) is non empty set
c₂ is Element of the carrier of (L ~)
b is Element of the carrier of (L ~)
~ c₂ is Element of the carrier of L
(~ c₂) ~ is Element of the carrier of (L ~)
~ b is Element of the carrier of L
(~ b) ~ is Element of the carrier of (L ~)
L is non empty V58() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) Element of K10( the carrier of L)
subrelstr c₂ is strict V58() reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₂) is set
X is Element of the carrier of L
X is Element of the carrier of L
{X,X} is non empty finite Element of K10( the carrier of L)
"/\" ({X,X},L) is Element of the carrier of L
c is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
{X,X} is non empty finite Element of K10( the carrier of L)
"/\" ({X,X},L) is Element of the carrier of L
c is Element of the carrier of L
X "/\" X is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) Element of K10( the carrier of L)
subrelstr c₂ is strict V58() reflexive transitive antisymmetric full SubRelStr of L
the carrier of (subrelstr c₂) is set
X is Element of the carrier of L
X is Element of the carrier of L
{X,X} is non empty finite Element of K10( the carrier of L)
"\/" ({X,X},L) is Element of the carrier of L
c is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
{X,X} is non empty finite Element of K10( the carrier of L)
"\/" ({X,X},L) is Element of the carrier of L
c is Element of the carrier of L
X "\/" X is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K10( the carrier of L) is non empty set
L is non empty 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 K10(K11( the carrier of L, the carrier of L))
K11( the carrier of L, the carrier of L) is non empty set
K10(K11( the carrier of L, the carrier of L)) is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is non empty strict RelStr
b is non empty RelStr
the carrier of b is non empty set
the InternalRel of b is Relation-like the carrier of b -defined the carrier of b -valued Element of K10(K11( the carrier of b, the carrier of b))
K11( the carrier of b, the carrier of b) is non empty set
K10(K11( the carrier of b, the carrier of b)) is non empty set
RelStr(# the carrier of b, the InternalRel of b #) is non empty strict RelStr
c₂ is non empty RelStr
the carrier of c₂ is non empty set
the InternalRel of c₂ is Relation-like the carrier of c₂ -defined the carrier of c₂ -valued Element of K10(K11( the carrier of c₂, the carrier of c₂))
K11( the carrier of c₂, the carrier of c₂) is non empty set
K10(K11( the carrier of c₂, the carrier of c₂)) is non empty set
RelStr(# the carrier of c₂, the InternalRel of c₂ #) is non empty strict RelStr
X is non empty RelStr
the carrier of X is non empty set
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K10(K11( the carrier of X, the carrier of X))
K11( the carrier of X, the carrier of X) is non empty set
K10(K11( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is non empty strict RelStr
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K11( the carrier of b, the carrier of X) is non empty set
K10(K11( the carrier of b, the carrier of X)) is non empty set
K10( the carrier of L) is non empty set
K10( the carrier of b) is non empty set
X is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
c is Relation-like the carrier of b -defined the carrier of X -valued Function-like V21( the carrier of b, the carrier of X) Element of K10(K11( the carrier of b, the carrier of X))
y is Element of K10( the carrier of L)
y is Element of K10( the carrier of b)
X .: y is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
"\/" ((X .: y),c₂) is Element of the carrier of c₂
"\/" (y,L) is Element of the carrier of L
X . ("\/" (y,L)) is Element of the carrier of c₂
c .: y is Element of K10( the carrier of X)
K10( the carrier of X) is non empty set
"\/" ((c .: y),X) is Element of the carrier of X
"\/" (y,b) is Element of the carrier of b
c . ("\/" (y,b)) is Element of the carrier of X
X .: y is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
"/\" ((X .: y),c₂) is Element of the carrier of c₂
"/\" (y,L) is Element of the carrier of L
X . ("/\" (y,L)) is Element of the carrier of c₂
c .: y is Element of K10( the carrier of X)
K10( the carrier of X) is non empty set
"/\" ((c .: y),X) is Element of the carrier of X
"/\" (y,b) is Element of the carrier of b
c . ("/\" (y,b)) is Element of the carrier of X
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
K10( the carrier of L) is non empty set
X is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
{X,X} is non empty finite Element of K10( the carrier of L)
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
K10( the carrier of L) is non empty set
X is Element of K10( the carrier of L)
X is Element of the carrier of L
X is Element of the carrier of L
{X,X} is non empty finite Element of K10( the carrier of L)
L is RelStr
the carrier of L is set
c₂ is RelStr
the carrier of c₂ is set
K11( the carrier of L, the carrier of c₂) is set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
rng b is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
b " is Relation-like Function-like set
X is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
dom X is Element of K10( the carrier of c₂)
X is Element of the carrier of L
c is Element of the carrier of L
b . X is Element of the carrier of c₂
b . c is Element of the carrier of c₂
X . (b . X) is Element of the carrier of L
X . (b . c) is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of c₂
b . X is Element of the carrier of c₂
y is Element of the carrier of c₂
b . X is Element of the carrier of c₂
X is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
X is Element of the carrier of c₂
c is Element of the carrier of c₂
X . X is set
X . c is set
dom b is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
y is set
b . y is set
y is set
b . y is set
X . X is Element of the carrier of L
x is Element of the carrier of L
X . c is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
c₁₂ is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
b " is Relation-like Function-like set
rng (b ") is set
rng b is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
dom b is Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
dom (b ") is set
L is non empty RelStr
the carrier of L is non empty set
c₂ is non empty RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K11( the carrier of c₂, the carrier of L) is non empty set
K10(K11( the carrier of c₂, the carrier of L)) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
b " is Relation-like Function-like set
X is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
X " is Relation-like Function-like set
X is Relation-like the carrier of c₂ -defined the carrier of L -valued Function-like V21( the carrier of c₂, the carrier of L) Element of K10(K11( the carrier of c₂, the carrier of L))
(b ") " is Relation-like Function-like set
L is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K10( the carrier of L) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
X is Element of the carrier of L
X is Element of the carrier of L
b . X is set
b . X is set
{X} is non empty finite Element of K10( the carrier of L)
{X} is non empty finite Element of K10( the carrier of L)
(L,X) is non empty (L) (L) Element of K10( the carrier of L)
(L,{X}) is non empty (L) Element of K10( the carrier of L)
(L,X) is non empty (L) (L) Element of K10( the carrier of L)
(L,{X}) is non empty (L) Element of K10( the carrier of L)
b .: (L,X) is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
b .: (L,X) is Element of K10( the carrier of c₂)
"/\" ((b .: (L,X)),c₂) is Element of the carrier of c₂
"/\" ((L,X),L) is Element of the carrier of L
b . ("/\" ((L,X),L)) is Element of the carrier of c₂
"/\" ((b .: (L,X)),c₂) is Element of the carrier of c₂
"/\" ((L,X),L) is Element of the carrier of L
b . ("/\" ((L,X),L)) is Element of the carrier of c₂
"/\" ({X},L) is Element of the carrier of L
b . ("/\" ({X},L)) is Element of the carrier of c₂
"/\" ({X},L) is Element of the carrier of L
b . ("/\" ({X},L)) is Element of the carrier of c₂
b . X is Element of the carrier of c₂
b . X is Element of the carrier of c₂
c is Element of the carrier of c₂
y is Element of the carrier of c₂
L is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K10( the carrier of L) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
X is Element of K10( the carrier of L)
b .: X is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
"/\" ((b .: X),c₂) is Element of the carrier of c₂
"/\" (X,L) is Element of the carrier of L
b . ("/\" (X,L)) is Element of the carrier of c₂
X is non empty (L) Element of K10( the carrier of L)
(L,X) is non empty (L) (L) Element of K10( the carrier of L)
(L,X) is (L) Element of K10( the carrier of L)
b .: (L,X) is Element of K10( the carrier of c₂)
"/\" ((b .: (L,X)),c₂) is Element of the carrier of c₂
"/\" ((L,X),L) is Element of the carrier of L
b . ("/\" ((L,X),L)) is Element of the carrier of c₂
c is Element of the carrier of c₂
c is Element of the carrier of c₂
y is Element of the carrier of c₂
dom b is Element of K10( the carrier of L)
y is set
b . y is set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in X ) } is set
x is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
b . Y is Element of the carrier of c₂
b . x is Element of the carrier of c₂
L is non empty V58() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
X is Element of K10( the carrier of L)
b .: X is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
"/\" ((b .: X),c₂) is Element of the carrier of c₂
"/\" (X,L) is Element of the carrier of L
b . ("/\" (X,L)) is Element of the carrier of c₂
K10(X) is non empty set
X is set
c is set
y is finite Element of K10(X)
y is finite Element of K10(X)
y is Element of K10( the carrier of L)
"/\" (y,L) is Element of the carrier of L
c is Element of K10( the carrier of L)
y is Element of the carrier of L
b .: c is Element of K10( the carrier of c₂)
"/\" ((b .: c),c₂) is Element of the carrier of c₂
"/\" (c,L) is Element of the carrier of L
b . ("/\" (c,L)) is Element of the carrier of c₂
y is set
{y} is non empty finite set
y is finite Element of K10(X)
x is Element of the carrier of L
"/\" (y,L) is Element of the carrier of L
y is Element of the carrier of c₂
y is Element of the carrier of c₂
y is Element of the carrier of c₂
dom b is Element of K10( the carrier of L)
x is set
b . x is set
Y is finite Element of K10(X)
"/\" (Y,L) is Element of the carrier of L
Y is Element of K10( the carrier of L)
b .: Y is Element of K10( the carrier of c₂)
"/\" ((b .: Y),c₂) is Element of the carrier of c₂
L is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K10( the carrier of L) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
X is Element of the carrier of L
X is Element of the carrier of L
b . X is set
b . X is set
{X} is non empty finite Element of K10( the carrier of L)
{X} is non empty finite Element of K10( the carrier of L)
(L,X) is non empty (L) (L) Element of K10( the carrier of L)
(L,{X}) is non empty (L) Element of K10( the carrier of L)
(L,X) is non empty (L) (L) Element of K10( the carrier of L)
(L,{X}) is non empty (L) Element of K10( the carrier of L)
b .: (L,X) is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
b .: (L,X) is Element of K10( the carrier of c₂)
"\/" ((b .: (L,X)),c₂) is Element of the carrier of c₂
"\/" ((L,X),L) is Element of the carrier of L
b . ("\/" ((L,X),L)) is Element of the carrier of c₂
"\/" ((b .: (L,X)),c₂) is Element of the carrier of c₂
"\/" ((L,X),L) is Element of the carrier of L
b . ("\/" ((L,X),L)) is Element of the carrier of c₂
"\/" ({X},L) is Element of the carrier of L
b . ("\/" ({X},L)) is Element of the carrier of c₂
"\/" ({X},L) is Element of the carrier of L
b . ("\/" ({X},L)) is Element of the carrier of c₂
b . X is Element of the carrier of c₂
b . X is Element of the carrier of c₂
c is Element of the carrier of c₂
y is Element of the carrier of c₂
L is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
c₂ is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
K10( the carrier of L) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
X is Element of K10( the carrier of L)
b .: X is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
"\/" ((b .: X),c₂) is Element of the carrier of c₂
"\/" (X,L) is Element of the carrier of L
b . ("\/" (X,L)) is Element of the carrier of c₂
X is non empty (L) Element of K10( the carrier of L)
(L,X) is non empty (L) (L) Element of K10( the carrier of L)
(L,X) is (L) Element of K10( the carrier of L)
b .: (L,X) is Element of K10( the carrier of c₂)
"\/" ((b .: (L,X)),c₂) is Element of the carrier of c₂
"\/" ((L,X),L) is Element of the carrier of L
b . ("\/" ((L,X),L)) is Element of the carrier of c₂
c is Element of the carrier of c₂
c is Element of the carrier of c₂
y is Element of the carrier of c₂
dom b is Element of K10( the carrier of L)
y is set
b . y is set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in X ) } is set
x is Element of the carrier of L
Y is Element of the carrier of L
Y is Element of the carrier of L
b . Y is Element of the carrier of c₂
b . x is Element of the carrier of c₂
L is non empty V58() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of c₂ is non empty set
K11( the carrier of L, the carrier of c₂) is non empty set
K10(K11( the carrier of L, the carrier of c₂)) is non empty set
b is Relation-like the carrier of L -defined the carrier of c₂ -valued Function-like V21( the carrier of L, the carrier of c₂) Element of K10(K11( the carrier of L, the carrier of c₂))
X is Element of K10( the carrier of L)
b .: X is Element of K10( the carrier of c₂)
K10( the carrier of c₂) is non empty set
"\/" ((b .: X),c₂) is Element of the carrier of c₂
"\/" (X,L) is Element of the carrier of L
b . ("\/" (X,L)) is Element of the carrier of c₂
K10(X) is non empty set
X is set
c is set
y is finite Element of K10(X)
y is finite Element of K10(X)
y is Element of K10( the carrier of L)
"\/" (y,L) is Element of the carrier of L
c is Element of K10( the carrier of L)
y is Element of the carrier of L
b .: c is Element of K10( the carrier of c₂)
"\/" ((b .: c),c₂) is Element of the carrier of c₂
"\/" (c,L) is Element of the carrier of L
b . ("\/" (c,L)) is Element of the carrier of c₂
y is set
{y} is non empty finite set
y is finite Element of K10(X)
x is Element of the carrier of L
"\/" (y,L) is Element of the carrier of L
y is Element of the carrier of c₂
y is Element of the carrier of c₂
y is Element of the carrier of c₂
dom b is Element of K10( the carrier of L)
x is set
b . x is set
Y is finite Element of K10(X)
"\/" (Y,L) is Element of the carrier of L
Y is Element of K10( the carrier of L)
b .: Y is Element of K10( the carrier of c₂)
"\/" ((b .: Y),c₂) is Element of the carrier of c₂
L is non empty V58() reflexive with_suprema RelStr
[#] L is non empty non proper (L) (L) (L) Element of K10( the carrier of L)
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is Element of the carrier of L
L is non empty V58() reflexive antisymmetric RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c₂ is non empty (L) Element of K10( the carrier of L)
b is Element of the carrier of L
L is non empty V58() reflexive antisymmetric RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty Element of K10( the carrier of L)
b is Element of the carrier of L
X is Element of the carrier of L
X is Element of the carrier of L
c₂ is non empty Element of K10( the carrier of L)
b is Element of the carrier of L
L is non empty V58() reflexive RelStr
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty (L) Element of K10( the carrier of L)
the carrier of L is non empty set
K10( the carrier of L) is non empty set
c₂ is non empty Element of K10( the carrier of L)
{ b₁ where b₁ is Element of the carrier of L : b₁ is_<=_than c₂ } is set
X is Element of the carrier of L
X is Element of the carrier of L
c is Element of the carrier of L
y is Element of the carrier of L
X is Element of the carrier of L
L is non empty V58() reflexive RelStr
the carrier of L is non empty set
[#] L is non empty non proper (L) (L) Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
c₂ is Element of the carrier of L
L is non empty V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
b is set
K10( the carrier of L) is non empty set
b /\ the carrier of L is set
c₂ is non empty V58() reflexive transitive antisymmetric with_suprema lower-bounded RelStr
the carrier of c₂ is non empty set
K10( the carrier of c₂) is non empty set
X is Element of K10( the carrier of L)
K10(X) is non empty set
c is finite Element of K10(X)
c is Element of the carrier of L
(L,X) is Element of K10( the carrier of L)
{ ("\/" (b₁,L)) where b₁ is finite Element of K10(X) : ex_sup_of b₁,L } is set
y is finite Element of K10(X)
"\/" (y,L) is Element of the carrier of L
c is finite Element of K10(X)
y is Element of K10( the carrier of L)
"\/" (c,L) is Element of the carrier of L
X is Element of K10( the carrier of c₂)
(c₂,X) is non empty (c₂) Element of K10( the carrier of c₂)
K10(X) is non empty set
{ ("\/" (b₁,c₂)) where b₁ is finite Element of K10(X) : ex_sup_of b₁,c₂ } is set
c is non empty (L) Element of K10( the carrier of L)
y is Element of the carrier of L
y is Element of the carrier of L
L is non empty V58() reflexive antisymmetric RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
b is Element of the carrier of L
{c₂,b} is non empty finite Element of K10( the carrier of L)
K10( the carrier of L) is non empty set
L is non empty V58() reflexive antisymmetric upper-bounded RelStr
the carrier of L is non empty set
c₂ is Element of the carrier of L
b is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ( c₂ <= b₁ & b <= b₁ ) } is set
X is set
c is Element of the carrier of L
K10( 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
X is Element of K10( the carrier of L)
c is Element of the carrier of L
{c₂,b} is non empty finite Element of K10( the carrier of L)
y is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
the non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() () () RelStr is non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V101() () () RelStr