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

K10(c

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

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

K10(c

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

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

{} 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

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

K10( the carrier of L) is non empty set

K10( the carrier of c

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

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

K10( the carrier of L) is non empty set

K10( the carrier of c

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

{c

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

the carrier of c

K10( the carrier of c

b is (c

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

the carrier of L is non empty set

c

the carrier of c

K10( the carrier of c

b is (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

the carrier of c

K10( the carrier of c

b is (c

"/\" (b,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

the carrier of c

K10( the carrier of c

b is (c

"\/" (b,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

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

c

K11(c

K10(K11(c

L is 1-sorted

the carrier of L is set

K11(c

K10(K11(c

b is Relation-like c

X is Relation-like c

(L,c

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

the of c

the carrier of c

the carrier of L is non empty set

K11( the carrier of c

K10(K11( the carrier of c

b is Element of the carrier of c

the of c

L is non empty RelStr

L is non empty 1-sorted

L is non empty 1-sorted

c

b is set

X is set

the carrier of c

X is Element of the carrier of c

c is Element of the carrier of c

(L,c

the carrier of L is non empty set

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

X is Element of the carrier of c

c is Element of the carrier of c

(L,c

the carrier of L is non empty set

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

L is non empty 1-sorted

the carrier of L is non empty set

c

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

X is Element of the carrier of c

c is Element of the carrier of c

(L,c

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

the carrier of c

X is Element of the carrier of c

c is Element of the carrier of c

(L,c

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

L is non empty 1-sorted

the carrier of L is non empty set

c

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

X is Element of the carrier of c

c is Element of the carrier of c

(L,c

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

the carrier of c

X is Element of the carrier of c

c is Element of the carrier of c

(L,c

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

F

F

the carrier of F

{ (F

c

b is Element of the carrier of F

X is Element of the carrier of F

(F

the carrier of F

the of F

K11( the carrier of F

K10(K11( the carrier of F

the of F

X is Element of the carrier of F

(F

the of F

c

b is Element of the carrier of F

(F

the of F

L is non empty RelStr

L is non empty RelStr

c

the carrier of c

the carrier of L is non empty set

b is Element of the carrier of c

(L,c

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

{ (L,c

b is Element of the carrier of c

(L,c

the of c

{ (L,c

b is Element of the carrier of c

(L,c

the of c

{ (L,c

X is Element of the carrier of c

L is non empty RelStr

c

the carrier of c

the carrier of L is non empty set

b is Element of the carrier of c

(L,c

the of c

K11( the carrier of c

K10(K11( the carrier of c

the of c

{ (L,c

b is Element of the carrier of c

(L,c

the of c

{ (L,c

b is Element of the carrier of c

(L,c

the of c

{ (L,c

X is Element of the carrier of c

L is non empty RelStr

c

the carrier of c

the carrier of L is non empty set

(L,c

K11( the carrier of c

K10(K11( the carrier of c

the of c

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

the of c

(L,c

the of c

c

the carrier of c

the carrier of L is non empty set

(L,c

K11( the carrier of c

K10(K11( the carrier of c

the of c

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

the of c

(L,c

the of c

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

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

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

K10( the carrier of L) is non empty set

K10( the carrier of c

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

(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

(L,c

{ b

( b

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

(L,c

{ b

( b

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

(L,c

the Element of c

X is Element of the carrier of L

(L,c

the 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

(L,c

(L,c

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

{c

K10( the carrier of L) is non empty set

(L,{c

(L,{c

L is non empty RelStr

the carrier of L is non empty set

b is Element of the carrier of L

c

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

{ b

( b

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

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

{ b

( b

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

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

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

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

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

b is Element of the carrier of L

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

(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

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

{c

(L,{c

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

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

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

(L,{c

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

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

(L,c

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

(L,c

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

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

K10( the carrier of L) is non empty set

K10( the carrier of c

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

(L,b) is Element of K10( the carrier of L)

(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

union c

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

b is Element of K10( the carrier of L)

c

c

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

union c

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

b is Element of K10( the carrier of L)

c

c

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

(L,c

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

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

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

(L,c

(L,{c

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

(L,c

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

(L,c

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

(L,c

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

(L,c

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

"\/" (c

(L,c

"\/" ((L,c

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

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

"\/" ((L,c

"\/" ({c

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

(L,c

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

(L,c

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

(L,c

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

(L,c

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

"/\" (c

(L,c

"/\" ((L,c

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

(L,c

K10( the carrier of L) is non empty set

{c

(L,{c

"/\" ((L,c

"/\" ({c

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

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

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

K10(c

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

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

K10(c

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

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

b is Element of K10( the carrier of L)

c

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

b is Element of K10( the carrier of L)

c

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

union 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

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

union 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

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

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

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

{ b

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

{{}} is non empty finite V38() set

(L) \/ {{}} is non empty set

(L) is set

{ b

(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

K10(c

{ ("\/" (b

X is set

X is finite Element of K10(c

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

{ ("/\" (b

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

(L,c

K10(c

{ ("\/" (b

{} c

"\/" (({} c

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

(L,c

K10(c

{ ("/\" (b

{} c

"/\" (({} c

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

(L,c

K10(c

{ ("\/" (b

the 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

{ ("/\" (b

the 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

(L,c

K10(c

{ ("\/" (b

(L,c

{ ("/\" (b

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

K10(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

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

(L,c

K10(c

{ ("\/" (b

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

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

K10(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

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

K10(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

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

K10(c

b is Element of K10( the carrier of L)

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

"\/" (c

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

"\/" (c

(L,c

K10(c

{ ("\/" (b

"\/" ((L,c

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

K10(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

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

(L,c

K10(c

{ ("/\" (b

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

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

K10(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

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

K10(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

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

K10(c

b is Element of K10( the carrier of L)

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

"/\" (c

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

"/\" (c

(L,c

K10(c

{ ("/\" (b

"/\" ((L,c

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

(L,c

K10(c

{ ("\/" (b

(L,(L,c

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

(L,c

K10(c

{ ("/\" (b

(L,(L,c

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

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

the carrier of c

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

b is Element of the carrier of (L ~)

~ c

(~ c

~ 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

subrelstr c

the carrier of (subrelstr c

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

subrelstr c

the carrier of (subrelstr c

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

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

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

the carrier of c

the InternalRel of c

K11( the carrier of c

K10(K11( the carrier of c

RelStr(# the carrier of c

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

K10(K11( the carrier of L, the carrier of c

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

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

"\/" ((X .: y),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

"/\" ((X .: y),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

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

b is Relation-like the carrier of L -defined 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

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

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

b is Relation-like the carrier of L -defined the carrier of c

rng b is Element of K10( the carrier of c

K10( the carrier of c

K11( the carrier of c

K10(K11( the carrier of c

b " is Relation-like Function-like set

X is Relation-like the carrier of c

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

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

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

b is Relation-like the carrier of L -defined the carrier of c

L is non empty RelStr

the carrier of L is non empty set

c

the carrier of c

K11( the carrier of L, the carrier of c

K10(K11( the carrier of L, the carrier of c

K11( the carrier of c

K10(K11( the carrier of c

b is Relation-like the carrier of L -defined the carrier of c

b " is Relation-like Function-like set

rng (b