:: WAYBEL13 semantic presentation

K126() is Element of K32(K122())

K122() is set

K32(K122()) is non empty set

K121() is set

K32(K121()) is non empty set

{} is empty Function-like functional finite V37() set

1 is non empty set

{{},1} is non empty finite set

K32(K126()) is non empty set

L is non empty reflexive transitive RelStr

the carrier of L is non empty set

X is Element of the carrier of L

c is Element of the carrier of L

compactbelow X is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

compactbelow c is Element of K32( the carrier of L)

g is set

{ b

y is Element of the carrier of L

L is non empty reflexive RelStr

the carrier of L is non empty set

CompactSublatt L is strict reflexive full SubRelStr of L

the carrier of (CompactSublatt L) is set

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

X is Element of the carrier of L

compactbelow X is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

c is set

{ b

g is Element of the carrier of L

L is RelStr

the carrier of L is set

K32( the carrier of L) is non empty set

X is SubRelStr of L

the carrier of X is set

K32( the carrier of X) is non empty set

c is Element of K32( the carrier of X)

L is non empty reflexive transitive with_suprema RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

[#] L is non empty non proper directed lower upper Element of K32( the carrier of L)

L is non empty reflexive antisymmetric lower-bounded RelStr

the carrier of L is non empty set

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

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

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

RelStr(# the carrier of L, the InternalRel of L #) is non empty strict reflexive antisymmetric RelStr

CompactSublatt L is non empty strict reflexive antisymmetric full SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

X is non empty reflexive antisymmetric 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 K32(K33( the carrier of X, the carrier of X))

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

K32(K33( 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 reflexive antisymmetric RelStr

CompactSublatt X is strict reflexive antisymmetric full SubRelStr of X

the carrier of (CompactSublatt X) is set

g is set

c is non empty reflexive antisymmetric lower-bounded RelStr

CompactSublatt c is non empty strict reflexive antisymmetric full SubRelStr of c

the carrier of (CompactSublatt c) is non empty set

y is Element of the carrier of X

Y is Element of the carrier of L

c is set

g is Element of the carrier of L

y is Element of the carrier of X

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

X is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of L

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 K32(K33( the carrier of X, the carrier of X))

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

K32(K33( 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 reflexive transitive antisymmetric with_infima RelStr

closure_op X is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of L) V153() monotone directed-sups-preserving projection closure Element of K32(K33( the carrier of L, the carrier of L))

the carrier of L is non empty set

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

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

Image (closure_op X) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of L

rng (closure_op X) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

subrelstr (rng (closure_op X)) is strict reflexive transitive antisymmetric full SubRelStr of L

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

X is set

the carrier of (BoolePoset L) is non empty set

c is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset L

CompactSublatt c is strict reflexive transitive antisymmetric full SubRelStr of c

the carrier of (CompactSublatt c) is set

the carrier of c is non empty set

closure_op c is non empty Relation-like the carrier of (BoolePoset L) -defined the carrier of (BoolePoset L) -valued Function-like V20( the carrier of (BoolePoset L)) V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) V153() monotone directed-sups-preserving projection closure Element of K32(K33( the carrier of (BoolePoset L), the carrier of (BoolePoset L)))

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

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

CompactSublatt (BoolePoset L) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of BoolePoset L

[#] (CompactSublatt (BoolePoset L)) is non empty non proper directed lower upper Element of K32( the carrier of (CompactSublatt (BoolePoset L)))

the carrier of (CompactSublatt (BoolePoset L)) is non empty set

K32( the carrier of (CompactSublatt (BoolePoset L))) is non empty set

(closure_op c) .: ([#] (CompactSublatt (BoolePoset L))) is Element of K32( the carrier of (BoolePoset L))

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

Image (closure_op c) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset L

rng (closure_op c) is Element of K32( the carrier of (BoolePoset L))

subrelstr (rng (closure_op c)) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset L

CompactSublatt (Image (closure_op c)) is strict reflexive transitive antisymmetric full SubRelStr of Image (closure_op c)

[#] (CompactSublatt (Image (closure_op c))) is non proper Element of K32( the carrier of (CompactSublatt (Image (closure_op c))))

the carrier of (CompactSublatt (Image (closure_op c))) is set

K32( the carrier of (CompactSublatt (Image (closure_op c)))) is non empty set

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

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

K32(K33( 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 reflexive transitive antisymmetric with_infima RelStr

CompactSublatt RelStr(# the carrier of c, the InternalRel of c #) is strict reflexive transitive antisymmetric full SubRelStr of RelStr(# the carrier of c, the InternalRel of c #)

[#] (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #)) is non proper Element of K32( the carrier of (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #)))

the carrier of (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #)) is set

K32( the carrier of (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #))) is non empty set

dom (closure_op c) is Element of K32( the carrier of (BoolePoset L))

g is set

(closure_op c) . g is set

id (BoolePoset L) is non empty Relation-like the carrier of (BoolePoset L) -defined the carrier of (BoolePoset L) -valued Function-like one-to-one V20( the carrier of (BoolePoset L)) V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) V153() monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of (BoolePoset L), the carrier of (BoolePoset L)))

id the carrier of (BoolePoset L) is non empty Relation-like the carrier of (BoolePoset L) -defined the carrier of (BoolePoset L) -valued Function-like one-to-one V20( the carrier of (BoolePoset L)) V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of K32(K33( the carrier of (BoolePoset L), the carrier of (BoolePoset L)))

y is Element of the carrier of (BoolePoset L)

(id (BoolePoset L)) . y is Element of the carrier of (BoolePoset L)

(closure_op c) . y is Element of the carrier of (BoolePoset L)

the carrier of (Image (closure_op c)) is non empty set

the carrier of RelStr(# the carrier of c, the InternalRel of c #) is non empty set

{ b

meet { b

uparrow y is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

(uparrow y) /\ the carrier of c is Element of K32( the carrier of (BoolePoset L))

Y is set

X is Element of the carrier of (BoolePoset L)

Y is set

X is Element of the carrier of c

x is Element of the carrier of (BoolePoset L)

"/\" (((uparrow y) /\ the carrier of c),(BoolePoset L)) is Element of the carrier of (BoolePoset L)

Y is set

X is set

x is Element of the carrier of c

g is Element of the carrier of (BoolePoset L)

{ b

meet { b

CompactSublatt (BoolePoset L) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of BoolePoset L

[#] (CompactSublatt (BoolePoset L)) is non empty non proper directed lower upper Element of K32( the carrier of (CompactSublatt (BoolePoset L)))

the carrier of (CompactSublatt (BoolePoset L)) is non empty set

K32( the carrier of (CompactSublatt (BoolePoset L))) is non empty set

uparrow g is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

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

(uparrow g) /\ the carrier of c is Element of K32( the carrier of (BoolePoset L))

y is set

Y is Element of the carrier of (BoolePoset L)

y is set

Y is Element of the carrier of c

X is Element of the carrier of (BoolePoset L)

id (BoolePoset L) is non empty Relation-like the carrier of (BoolePoset L) -defined the carrier of (BoolePoset L) -valued Function-like one-to-one V20( the carrier of (BoolePoset L)) V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) V153() monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of (BoolePoset L), the carrier of (BoolePoset L)))

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

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

id the carrier of (BoolePoset L) is non empty Relation-like the carrier of (BoolePoset L) -defined the carrier of (BoolePoset L) -valued Function-like one-to-one V20( the carrier of (BoolePoset L)) V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of K32(K33( the carrier of (BoolePoset L), the carrier of (BoolePoset L)))

closure_op c is non empty Relation-like the carrier of (BoolePoset L) -defined the carrier of (BoolePoset L) -valued Function-like V20( the carrier of (BoolePoset L)) V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) V153() monotone directed-sups-preserving projection closure Element of K32(K33( the carrier of (BoolePoset L), the carrier of (BoolePoset L)))

(id (BoolePoset L)) . g is Element of the carrier of (BoolePoset L)

(closure_op c) . g is Element of the carrier of (BoolePoset L)

dom (closure_op c) is Element of K32( the carrier of (BoolePoset L))

rng (closure_op c) is Element of K32( the carrier of (BoolePoset L))

Image (closure_op c) is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset L

subrelstr (rng (closure_op c)) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset L

the carrier of (Image (closure_op c)) is non empty set

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

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

K32(K33( 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 reflexive transitive antisymmetric with_infima RelStr

the carrier of RelStr(# the carrier of c, the InternalRel of c #) is non empty set

"/\" (((uparrow g) /\ the carrier of c),(BoolePoset L)) is Element of the carrier of (BoolePoset L)

(closure_op c) .: ([#] (CompactSublatt (BoolePoset L))) is Element of K32( the carrier of (BoolePoset L))

CompactSublatt (Image (closure_op c)) is strict reflexive transitive antisymmetric full SubRelStr of Image (closure_op c)

[#] (CompactSublatt (Image (closure_op c))) is non proper Element of K32( the carrier of (CompactSublatt (Image (closure_op c))))

the carrier of (CompactSublatt (Image (closure_op c))) is set

K32( the carrier of (CompactSublatt (Image (closure_op c)))) is non empty set

CompactSublatt RelStr(# the carrier of c, the InternalRel of c #) is strict reflexive transitive antisymmetric full SubRelStr of RelStr(# the carrier of c, the InternalRel of c #)

[#] (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #)) is non proper Element of K32( the carrier of (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #)))

the carrier of (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #)) is set

K32( the carrier of (CompactSublatt RelStr(# the carrier of c, the InternalRel of c #))) is non empty set

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

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

the carrier of L is non empty set

BoolePoset the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

X is set

K32( the carrier of L) is non empty set

{ b

bool the carrier of L is non empty Element of K32(K32( the carrier of L))

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

c is non empty directed lower Element of K32( the carrier of L)

X is non empty reflexive transitive antisymmetric full SubRelStr of BoolePoset the carrier of L

the carrier of X is non empty set

K32( the carrier of X) is non empty set

c is directed Element of K32( the carrier of X)

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

the carrier of (BoolePoset the carrier of L) is non empty set

g is set

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

union c is set

Bottom L is Element of the carrier of L

y is Element of K32( the carrier of L)

X is set

X is Element of K32( the carrier of L)

x is Element of K32( the carrier of L)

fx is Element of the carrier of X

fc is Element of the carrier of X

gy1 is Element of the carrier of X

f1y1 is Element of K32( the carrier of L)

z is Element of K32( the carrier of L)

fx "\/" fc is Element of the carrier of X

X \/ x is Element of K32( the carrier of L)

X is Element of K32( the carrier of L)

x is Element of K32( the carrier of L)

Y is non empty Element of K32( the carrier of L)

c is Element of K32( the carrier of X)

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

the carrier of (BoolePoset the carrier of L) is non empty set

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

meet c is set

RelIncl (Ids L) is Relation-like Ids L -defined Ids L -valued V20( Ids L) V21( Ids L, Ids L) V128() V131() V135() Element of K32(K33((Ids L),(Ids L)))

K33((Ids L),(Ids L)) is non empty set

K32(K33((Ids L),(Ids L))) is non empty set

RelStr(# (Ids L),(RelIncl (Ids L)) #) is strict RelStr

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

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

L is non empty reflexive transitive RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

the Element of the carrier of L is Element of the carrier of L

downarrow the Element of the carrier of L is non empty directed lower Element of K32( the carrier of L)

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

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

the carrier of (InclPoset (Ids L)) is non empty set

K32( the carrier of (InclPoset (Ids L))) is non empty set

X is non empty directed Element of K32( the carrier of (InclPoset (Ids L)))

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

union X is set

c is set

g is set

the carrier of L is non empty set

K32( the carrier of L) is non empty set

{ b

bool the carrier of L is non empty Element of K32(K32( the carrier of L))

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

y is non empty directed lower Element of K32( the carrier of L)

g is Element of K32( the carrier of L)

y is non empty directed lower Element of K32( the carrier of L)

y is non empty directed lower Element of K32( the carrier of L)

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

Y is set

Y is Element of K32( the carrier of L)

X is Element of K32( the carrier of L)

x is Element of the carrier of (InclPoset (Ids L))

fx is Element of the carrier of (InclPoset (Ids L))

fc is Element of the carrier of (InclPoset (Ids L))

f1y1 is non empty directed lower Element of K32( the carrier of L)

gy1 is Element of K32( the carrier of L)

f1y1 is Element of K32( the carrier of L)

Y \/ X is Element of K32( the carrier of L)

Y is Element of K32( the carrier of L)

X is non empty directed lower Element of K32( the carrier of L)

y is non empty lower Element of K32( the carrier of L)

Y is non empty directed lower Element of K32( the carrier of L)

x is set

fx is Element of the carrier of (InclPoset (Ids L))

X is Element of the carrier of (InclPoset (Ids L))

x is Element of the carrier of (InclPoset (Ids L))

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

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

the carrier of L is non empty set

BoolePoset the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

bool the carrier of L is non empty Element of K32(K32( the carrier of L))

K32( the carrier of L) is non empty set

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

c is set

{ b

g is non empty directed lower Element of K32( the carrier of L)

c is non empty reflexive transitive antisymmetric full SubRelStr of BoolePoset the carrier of L

the carrier of c is non empty set

the carrier of (BoolePoset the carrier of L) is non empty set

K32( the carrier of c) is non empty set

g is Element of K32( the carrier of c)

y is set

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

meet g is set

"/\" (g,c) is Element of the carrier of c

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

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

[#] L is non empty non proper directed filtered lower upper Element of K32( the carrier of L)

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

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

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

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

g is directed Element of K32( the carrier of c)

y is set

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

union g is set

"\/" (g,c) is Element of the carrier of c

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

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

the carrier of (InclPoset (Ids L)) is non empty set

the carrier of L is non empty set

K32( the carrier of L) is non empty set

BoolePoset the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

c is Element of the carrier of (InclPoset (Ids L))

X is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset the carrier of L

CompactSublatt X is strict reflexive transitive antisymmetric full SubRelStr of X

the carrier of (CompactSublatt X) is set

the carrier of (BoolePoset the carrier of L) is non empty set

the carrier of X is non empty set

y is Element of the carrier of (BoolePoset the carrier of L)

{ b

meet { b

g is non empty directed lower Element of K32( the carrier of L)

Y is Element of K32( the carrier of L)

X is Element of K32( the carrier of L)

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

x is Element of the carrier of L

Bottom L is Element of the carrier of L

fx is set

fc is Element of the carrier of L

downarrow x is non empty directed lower Element of K32( the carrier of L)

fx is Element of the carrier of L

Y is Element of the carrier of L

g is non empty directed lower Element of K32( the carrier of L)

y is Element of the carrier of L

the carrier of (BoolePoset the carrier of L) is non empty set

X is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset the carrier of L

the carrier of X is non empty set

{y} is non empty finite Element of K32( the carrier of L)

Y is Element of the carrier of (BoolePoset the carrier of L)

{ b

meet { b

X is set

X is set

x is Element of the carrier of L

fx is set

fc is Element of the carrier of X

[#] L is non empty non proper directed filtered lower upper Element of K32( the carrier of L)

CompactSublatt X is strict reflexive transitive antisymmetric full SubRelStr of X

the carrier of (CompactSublatt X) is set

Y is Element of the carrier of (BoolePoset the carrier of L)

{ b

meet { b

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

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

the carrier of (InclPoset (Ids L)) is non empty set

the carrier of L is non empty set

X is Element of the carrier of (InclPoset (Ids L))

K32( the carrier of L) is non empty set

K32( the carrier of L) is non empty set

c is Element of the carrier of L

downarrow c is non empty directed lower Element of K32( the carrier of L)

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

the carrier of L is non empty set

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

CompactSublatt (InclPoset (Ids L)) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of InclPoset (Ids L)

the carrier of (CompactSublatt (InclPoset (Ids L))) is non empty set

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

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

X is non empty Relation-like the carrier of L -defined the carrier of (CompactSublatt (InclPoset (Ids L))) -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of (CompactSublatt (InclPoset (Ids L)))) Element of K32(K33( the carrier of L, the carrier of (CompactSublatt (InclPoset (Ids L)))))

c is Element of the carrier of L

g is Element of the carrier of L

X . c is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

X . g is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

the carrier of (InclPoset (Ids L)) is non empty set

downarrow c is non empty directed lower Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

downarrow g is non empty directed lower Element of K32( the carrier of L)

y is Element of the carrier of (InclPoset (Ids L))

Y is Element of the carrier of (InclPoset (Ids L))

downarrow c is non empty directed lower Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

y is Element of the carrier of (InclPoset (Ids L))

Y is Element of the carrier of (InclPoset (Ids L))

downarrow g is non empty directed lower Element of K32( the carrier of L)

c is set

the carrier of (InclPoset (Ids L)) is non empty set

g is Element of the carrier of (InclPoset (Ids L))

y is Element of the carrier of L

downarrow y is non empty directed lower Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

Y is set

X is set

X . X is set

rng X is Element of K32( the carrier of (CompactSublatt (InclPoset (Ids L))))

K32( the carrier of (CompactSublatt (InclPoset (Ids L)))) is non empty set

c is Element of the carrier of L

X . c is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

g is Element of the carrier of L

X . g is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

downarrow g is non empty directed lower Element of K32( the carrier of L)

downarrow c is non empty directed lower Element of K32( the carrier of L)

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

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

CompactSublatt (InclPoset (Ids L)) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of InclPoset (Ids L)

the carrier of (CompactSublatt (InclPoset (Ids L))) is non empty set

the carrier of (InclPoset (Ids L)) is non empty set

X is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

c is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

g is Element of the carrier of (InclPoset (Ids L))

the carrier of L is non empty set

Y is Element of the carrier of L

downarrow Y is non empty directed lower Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

y is Element of the carrier of (InclPoset (Ids L))

X is Element of the carrier of L

downarrow X is non empty directed lower Element of K32( the carrier of L)

Bottom L is Element of the carrier of L

(downarrow Y) /\ (downarrow X) is Element of K32( the carrier of L)

x is non empty Element of K32( the carrier of L)

fx is non empty lower Element of K32( the carrier of L)

fc is non empty directed lower Element of K32( the carrier of L)

{ b

g "/\" y is Element of the carrier of (InclPoset (Ids L))

gy1 is Element of the carrier of (InclPoset (Ids L))

Y "/\" X is Element of the carrier of L

downarrow (Y "/\" X) is non empty directed lower Element of K32( the carrier of L)

f1y1 is set

z is Element of the carrier of L

f1y1 is set

z is Element of the carrier of L

f1y1 is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

z is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

z9 is Element of the carrier of (CompactSublatt (InclPoset (Ids L)))

v1 is Element of the carrier of (InclPoset (Ids L))

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

CompactSublatt L is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

Bottom L is Element of the carrier of L

the carrier of L is non empty set

X is Element of the carrier of (CompactSublatt L)

c is Element of the carrier of (CompactSublatt L)

g is Element of the carrier of L

X is Element of the carrier of (CompactSublatt L)

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

CompactSublatt L is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of L

Ids (CompactSublatt L) is non empty set

InclPoset (Ids (CompactSublatt L)) is non empty strict reflexive transitive antisymmetric with_suprema RelStr

the carrier of (InclPoset (Ids (CompactSublatt L))) is non empty set

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

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

X is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids (CompactSublatt L))) -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of (InclPoset (Ids (CompactSublatt L)))) Element of K32(K33( the carrier of L, the carrier of (InclPoset (Ids (CompactSublatt L)))))

c is Element of the carrier of L

g is Element of the carrier of L

X . c is Element of the carrier of (InclPoset (Ids (CompactSublatt L)))

X . g is Element of the carrier of (InclPoset (Ids (CompactSublatt L)))

compactbelow c is non empty Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

compactbelow g is non empty Element of K32( the carrier of L)

compactbelow g is non empty Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

compactbelow c is non empty Element of K32( the carrier of L)

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

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

c is set

the carrier of (CompactSublatt L) is non empty set

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

K32( the carrier of L) is non empty set

g is non empty directed lower Element of K32( the carrier of (CompactSublatt L))

y is non empty Element of K32( the carrier of L)

Y is non empty directed Element of K32( the carrier of L)

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

x is set

fx is set

compactbelow ("\/" (Y,L)) is non empty Element of K32( the carrier of L)

fc is set

{ b

gy1 is Element of the carrier of L

z is Element of the carrier of L

f1y1 is Element of the carrier of (CompactSublatt L)

z9 is Element of the carrier of (CompactSublatt L)

fc is set

gy1 is Element of the carrier of (CompactSublatt L)

f1y1 is Element of the carrier of L

X . fx is set

rng X is Element of K32( the carrier of (InclPoset (Ids (CompactSublatt L))))

K32( the carrier of (InclPoset (Ids (CompactSublatt L)))) is non empty set

c is Element of the carrier of L

X . c is Element of the carrier of (InclPoset (Ids (CompactSublatt L)))

g is Element of the carrier of L

X . g is Element of the carrier of (InclPoset (Ids (CompactSublatt L)))

compactbelow g is non empty Element of K32( the carrier of L)

compactbelow c is non empty Element of K32( the carrier of L)

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

CompactSublatt L is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

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

X is Element of the carrier of L

compactbelow X is non empty Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

c is Element of the carrier of (CompactSublatt L)

g is Element of the carrier of L

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

c is non empty Element of K32( the carrier of (CompactSublatt L))

Y is Element of the carrier of (CompactSublatt L)

X is Element of the carrier of (CompactSublatt L)

y is non empty directed Element of K32( the carrier of (CompactSublatt L))

x is Element of the carrier of L

fx is Element of the carrier of L

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

Y is non empty directed lower Element of K32( the carrier of (CompactSublatt L))

g is Element of the carrier of (CompactSublatt L)

L is non empty RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

X is non empty RelStr

the carrier of X is non empty set

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

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

c is Element of K32( the carrier of L)

g is Element of the carrier of L

y is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

y .: c is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

y . g is Element of the carrier of X

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

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

y " is Relation-like Function-like set

Y is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

Y .: (y .: c) is Element of K32( the carrier of L)

Y . (y . g) is Element of the carrier of L

y " (y .: c) is Element of K32( the carrier of L)

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

L is non empty RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

X is non empty RelStr

the carrier of X is non empty set

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

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

c is Element of K32( the carrier of L)

g is Element of the carrier of L

y is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

y .: c is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

y . g is Element of the carrier of X

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

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

y " is Relation-like Function-like set

Y is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

Y .: (y .: c) is Element of K32( the carrier of L)

Y . (y . g) is Element of the carrier of L

y " (y .: c) is Element of K32( the carrier of L)

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

L is non empty antisymmetric RelStr

the carrier of L is non empty set

X is non empty antisymmetric RelStr

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

rng c is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

K32( the carrier of L) is non empty set

g is Element of K32( the carrier of L)

y is Element of the carrier of L

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

Y is Element of the carrier of X

X is set

c . X is set

c .: g is Element of K32( the carrier of X)

x is Element of the carrier of L

c . y is Element of the carrier of X

Y is Element of the carrier of X

X is set

c . X is set

x is Element of the carrier of L

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

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

"/\" ((c .: g),X) is Element of the carrier of X

g is Element of K32( the carrier of L)

y is Element of the carrier of L

Y is Element of the carrier of X

X is set

c . X is set

c .: g is Element of K32( the carrier of X)

x is Element of the carrier of L

c . y is Element of the carrier of X

Y is Element of the carrier of X

X is set

c . X is set

x is Element of the carrier of L

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

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

"\/" ((c .: g),X) is Element of the carrier of X

L is non empty antisymmetric RelStr

the carrier of L is non empty set

X is non empty antisymmetric RelStr

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

L is non empty transitive antisymmetric RelStr

the carrier of L is non empty set

X is non empty transitive antisymmetric RelStr

the carrier of X is non empty set

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

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

c is non empty transitive antisymmetric RelStr

the carrier of c is non empty set

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

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

g is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

y is non empty Relation-like the carrier of L -defined the carrier of c -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of c) Element of K32(K33( the carrier of L, the carrier of c))

K32( the carrier of L) is non empty set

Y is Element of K32( the carrier of L)

y .: Y is Element of K32( the carrier of c)

K32( the carrier of c) is non empty set

g .: Y is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

"/\" ((g .: Y),c) is Element of the carrier of c

"/\" ((y .: Y),c) is Element of the carrier of c

"/\" ((g .: Y),X) is Element of the carrier of X

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

y . ("/\" (Y,L)) is Element of the carrier of c

L is non empty transitive antisymmetric RelStr

the carrier of L is non empty set

X is non empty transitive antisymmetric RelStr

the carrier of X is non empty set

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

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

c is non empty transitive antisymmetric RelStr

the carrier of c is non empty set

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

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

g is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

y is non empty Relation-like the carrier of L -defined the carrier of c -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of c) Element of K32(K33( the carrier of L, the carrier of c))

K32( the carrier of L) is non empty set

Y is Element of K32( the carrier of L)

X is set

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

g . X is set

g .: Y is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

y .: Y is Element of K32( the carrier of c)

K32( the carrier of c) is non empty set

"\/" ((y .: Y),c) is Element of the carrier of c

"\/" ((g .: Y),X) is Element of the carrier of X

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

y . ("\/" (Y,L)) is Element of the carrier of c

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

CompactSublatt L is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of L

Ids (CompactSublatt L) is non empty set

InclPoset (Ids (CompactSublatt L)) is non empty strict reflexive transitive antisymmetric with_suprema RelStr

the carrier of (CompactSublatt L) is non empty set

BoolePoset the carrier of (CompactSublatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

CompactSublatt L is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

BoolePoset the carrier of (CompactSublatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of (BoolePoset the carrier of (CompactSublatt L)) is non empty set

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

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

K32( the carrier of L) is non empty set

Ids (CompactSublatt L) is non empty set

InclPoset (Ids (CompactSublatt L)) is non empty strict reflexive transitive antisymmetric with_suprema RelStr

the carrier of (InclPoset (Ids (CompactSublatt L))) is non empty set

X is Element of the carrier of L

compactbelow X is non empty Element of K32( the carrier of L)

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

c is non empty directed Element of K32( the carrier of L)

g is non empty Element of K32( the carrier of (CompactSublatt L))

Y is Element of the carrier of (CompactSublatt L)

X is Element of the carrier of (CompactSublatt L)

y is non empty directed Element of K32( the carrier of (CompactSublatt L))

x is Element of the carrier of L

fx is Element of the carrier of L

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

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

X is non empty Relation-like the carrier of L -defined the carrier of (InclPoset (Ids (CompactSublatt L))) -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of (InclPoset (Ids (CompactSublatt L)))) Element of K32(K33( the carrier of L, the carrier of (InclPoset (Ids (CompactSublatt L)))))

c is set

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

c is non empty Relation-like the carrier of L -defined the carrier of (BoolePoset the carrier of (CompactSublatt L)) -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))) Element of K32(K33( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))))

g is non empty Relation-like the carrier of L -defined the carrier of (BoolePoset the carrier of (CompactSublatt L)) -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))) Element of K32(K33( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))))

g is non empty Relation-like the carrier of L -defined the carrier of (BoolePoset the carrier of (CompactSublatt L)) -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))) Element of K32(K33( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))))

g is Element of the carrier of L

c . g is Element of the carrier of (BoolePoset the carrier of (CompactSublatt L))

compactbelow g is non empty Element of K32( the carrier of L)

L is non empty set

X is Relation-like L -defined Function-like V20(L) RelStr-yielding non-Empty reflexive-yielding set

product X is non empty strict reflexive RelStr

c is Element of L

X . c is non empty reflexive RelStr

g is Element of L

X . g is non empty reflexive RelStr

the carrier of (product X) is non empty set

g is Element of the carrier of (product X)

compactbelow g is Element of K32( the carrier of (product X))

K32( the carrier of (product X)) is non empty set

"\/" ((compactbelow g),(product X)) is Element of the carrier of (product X)

y is Element of L

X . y is non empty reflexive RelStr

g . y is Element of the carrier of (X . y)

the carrier of (X . y) is non empty set

compactbelow (g . y) is Element of K32( the carrier of (X . y))

K32( the carrier of (X . y)) is non empty set

"\/" ((compactbelow (g . y)),(X . y)) is Element of the carrier of (X . y)

("\/" ((compactbelow g),(product X))) . y is Element of the carrier of (X . y)

pi ((compactbelow g),y) is Element of K32( the carrier of (X . y))

Y is set

{ b

X is Element of the carrier of (X . y)

x is Relation-like Function-like set

dom x is set

x . y is set

fx is Element of L

x . fx is set

X . fx is non empty reflexive RelStr

the carrier of (X . fx) is non empty set

fx is Element of L

x . fx is set

X . fx is non empty reflexive RelStr

Bottom (X . fx) is Element of the carrier of (X . fx)

the carrier of (X . fx) is non empty set

fx is Element of L

x . fx is set

X . fx is non empty reflexive RelStr

the carrier of (X . fx) is non empty set

fx is Element of L

x . fx is set

X . fx is non empty reflexive RelStr

the carrier of (X . fx) is non empty set

fc is Element of L

X . fc is non empty reflexive RelStr

fx is Element of the carrier of (product X)

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

g . fc is Element of the carrier of (X . fc)

fx is Element of the carrier of (product X)

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

Bottom (X . fc) is Element of the carrier of (X . fc)

g . fc is Element of the carrier of (X . fc)

fx is Element of the carrier of (product X)

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

g . fc is Element of the carrier of (X . fc)

fx is Element of the carrier of (product X)

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

g . fc is Element of the carrier of (X . fc)

fc is Element of L

X . fc is non empty reflexive RelStr

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

Bottom (X . fc) is Element of the carrier of (X . fc)

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

fx . fc is Element of the carrier of (X . fc)

the carrier of (X . fc) is non empty set

K32(L) is non empty set

{y} is non empty finite Element of K32(L)

fc is non empty finite Element of K32(L)

gy1 is Element of L

fx . gy1 is Element of the carrier of (X . gy1)

X . gy1 is non empty reflexive RelStr

the carrier of (X . gy1) is non empty set

Bottom (X . gy1) is Element of the carrier of (X . gy1)

fc is finite Element of K32(L)

Y is set

X is Relation-like Function-like set

X . y is set

{ b

x is Element of the carrier of (product X)

x . y is Element of the carrier of (X . y)

"\/" ((pi ((compactbelow g),y)),(X . y)) is Element of the carrier of (X . y)

y is Element of L

X . y is non empty reflexive RelStr

g . y is Element of the carrier of (X . y)

the carrier of (X . y) is non empty set

compactbelow (g . y) is Element of K32( the carrier of (X . y))

K32( the carrier of (X . y)) is non empty set

"\/" ((compactbelow (g . y)),(X . y)) is Element of the carrier of (X . y)

("\/" ((compactbelow g),(product X))) . y is Element of the carrier of (X . y)

y is Element of L

X . y is non empty reflexive RelStr

g . y is Element of the carrier of (X . y)

the carrier of (X . y) is non empty set

compactbelow (g . y) is Element of K32( the carrier of (X . y))

K32( the carrier of (X . y)) is non empty set

"\/" ((compactbelow (g . y)),(X . y)) is Element of the carrier of (X . y)

("\/" ((compactbelow g),(product X))) . y is Element of the carrier of (X . y)

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

the carrier of c is non empty set

g is Element of the carrier of c

compactbelow g is non empty Element of K32( the carrier of c)

K32( the carrier of c) is non empty set

y is Element of the carrier of c

Y is Element of the carrier of c

y "\/" Y is Element of the carrier of c

X is Element of the carrier of c

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

CompactSublatt L is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

c is non empty set

BoolePoset c is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

BoolePoset the carrier of (CompactSublatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of (BoolePoset the carrier of (CompactSublatt L)) is non empty set

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

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

g is non empty Relation-like the carrier of L -defined the carrier of (BoolePoset the carrier of (CompactSublatt L)) -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))) Element of K32(K33( the carrier of L, the carrier of (BoolePoset the carrier of (CompactSublatt L))))

Image g is non empty strict reflexive transitive antisymmetric full SubRelStr of BoolePoset the carrier of (CompactSublatt L)

rng g is Element of K32( the carrier of (BoolePoset the carrier of (CompactSublatt L)))

K32( the carrier of (BoolePoset the carrier of (CompactSublatt L))) is non empty set

subrelstr (rng g) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset the carrier of (CompactSublatt L)

y is non empty reflexive transitive antisymmetric full SubRelStr of BoolePoset c

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of y is non empty set

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

K32( the carrier of L) is non empty set

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

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

X is Element of the carrier of L

x is Element of the carrier of L

Y is non empty Relation-like the carrier of L -defined the carrier of y -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of y) Element of K32(K33( the carrier of L, the carrier of y))

Y . X is Element of the carrier of y

Y . x is Element of the carrier of y

compactbelow X is non empty Element of K32( the carrier of L)

compactbelow x is non empty Element of K32( the carrier of L)

g . X is Element of the carrier of (BoolePoset the carrier of (CompactSublatt L))

g . x is Element of the carrier of (BoolePoset the carrier of (CompactSublatt L))

g . X is Element of the carrier of (BoolePoset the carrier of (CompactSublatt L))

g . x is Element of the carrier of (BoolePoset the carrier of (CompactSublatt L))

compactbelow x is non empty Element of K32( the carrier of L)

compactbelow X is non empty Element of K32( the carrier of L)

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

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

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

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

Y " is Relation-like Function-like set

X is non empty Relation-like the carrier of y -defined the carrier of L -valued Function-like V20( the carrier of y) V21( the carrier of y, the carrier of L) Element of K32(K33( the carrier of y, the carrier of L))

K32( the carrier of y) is non empty set

x is directed Element of K32( the carrier of y)

X .: x is Element of K32( the carrier of L)

K32((X .: x)) is non empty set

fx is finite Element of K32((X .: x))

Y .: fx is finite Element of K32( the carrier of y)

Y " (Y .: fx) is Element of K32( the carrier of L)

fc is set

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

Y .: (X .: x) is Element of K32( the carrier of y)

gy1 is set

Y . gy1 is set

Y " x is Element of K32( the carrier of L)

Y .: (Y " x) is Element of K32( the carrier of y)

K32(x) is non empty set

fc is finite Element of K32(x)

gy1 is Element of the carrier of y

X . gy1 is Element of the carrier of L

dom X is Element of K32( the carrier of y)

f1y1 is Element of the carrier of L

X .: fc is finite Element of K32( the carrier of L)

fx is non empty directed Element of K32( the carrier of L)

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

g . ("\/" (fx,L)) is Element of the carrier of (BoolePoset the carrier of (CompactSublatt L))

g .: fx is Element of K32( the carrier of (BoolePoset the carrier of (CompactSublatt L)))

"\/" ((g .: fx),(BoolePoset the carrier of (CompactSublatt L))) is Element of the carrier of (BoolePoset the carrier of (CompactSublatt L))

g .: (Y " x) is Element of K32( the carrier of (BoolePoset the carrier of (CompactSublatt L)))

"\/" (x,(BoolePoset c)) is Element of the carrier of (BoolePoset c)

the carrier of (BoolePoset c) 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 K32(K33( the carrier of L, the carrier of L))

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

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

RelStr(# the carrier of L, the InternalRel of L #) 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 K32(K33( the carrier of X, the carrier of X))

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

K32(K33( 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

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

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

id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one V20( the carrier of L) V21( the carrier of L, the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

g is set

y is set

c . y is set

rng c is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

g is Element of the carrier of L

y is Element of the carrier of L

c . g is Element of the carrier of X

c . y is Element of the carrier of X

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

X is non empty set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

c is reflexive transitive antisymmetric full SubRelStr of BoolePoset X

the carrier of (BoolePoset X) is non empty set

K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) is non empty set

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

g is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of BoolePoset X

closure_op g is non empty Relation-like the carrier of (BoolePoset X) -defined the carrier of (BoolePoset X) -valued Function-like V20( the carrier of (BoolePoset X)) V21( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) V153() monotone projection closure Element of K32(K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)))

y is non empty Relation-like the carrier of (BoolePoset X) -defined the carrier of (BoolePoset X) -valued Function-like V20( the carrier of (BoolePoset X)) V21( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) V153() monotone projection closure Element of K32(K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)))

Image y is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of BoolePoset X

rng y is Element of K32( the carrier of (BoolePoset X))

K32( the carrier of (BoolePoset X)) is non empty set

subrelstr (rng y) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset X

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 K32(K33( the carrier of c, the carrier of c))

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

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

RelStr(# the carrier of c, the InternalRel of c #) is strict transitive antisymmetric RelStr

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

c is reflexive transitive antisymmetric full SubRelStr of BoolePoset X

the carrier of (BoolePoset X) is non empty set

K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) is non empty set

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

g is non empty reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of BoolePoset X

closure_op g is non empty Relation-like the carrier of (BoolePoset X) -defined the carrier of (BoolePoset X) -valued Function-like V20( the carrier of (BoolePoset X)) V21( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) V153() monotone projection closure Element of K32(K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)))

y is non empty Relation-like the carrier of (BoolePoset X) -defined the carrier of (BoolePoset X) -valued Function-like V20( the carrier of (BoolePoset X)) V21( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) V153() monotone projection closure Element of K32(K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)))

Image y is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of BoolePoset X

rng y is Element of K32( the carrier of (BoolePoset X))

K32( the carrier of (BoolePoset X)) is non empty set

subrelstr (rng y) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset X

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 K32(K33( the carrier of c, the carrier of c))

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

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

RelStr(# the carrier of c, the InternalRel of c #) is strict transitive antisymmetric RelStr

L is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of L is non empty set

X is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

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

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

c " is Relation-like Function-like set

y is Element of the carrier of L

Y is Element of the carrier of L

c . y is Element of the carrier of X

c . Y is Element of the carrier of X

g is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

K32( the carrier of X) is non empty set

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

K32( the carrier of L) is non empty set

X is non empty directed Element of K32( the carrier of X)

rng c is Element of K32( the carrier of X)

g .: X is Element of K32( the carrier of L)

K32((g .: X)) is non empty set

x is finite Element of K32((g .: X))

c .: x is finite Element of K32( the carrier of X)

c " (c .: x) is Element of K32( the carrier of L)

fx is set

c .: (g .: X) is Element of K32( the carrier of X)

fc is set

c . fc is set

c " X is Element of K32( the carrier of L)

c .: (c " X) is Element of K32( the carrier of X)

K32(X) is non empty set

fx is finite Element of K32(X)

fc is Element of the carrier of X

g . fc is Element of the carrier of L

dom g is Element of K32( the carrier of X)

gy1 is Element of the carrier of L

g .: fx is finite Element of K32( the carrier of L)

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

g . (c . Y) is Element of the carrier of L

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

x is non empty directed Element of K32( the carrier of L)

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

fx is Element of the carrier of L

c . fx is Element of the carrier of X

c .: x is Element of K32( the carrier of X)

fc is Element of the carrier of X

L is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of L is non empty set

X is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

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

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

c " is Relation-like Function-like set

y is Element of the carrier of L

Y is Element of the carrier of L

c . y is Element of the carrier of X

c . Y is Element of the carrier of X

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

K32( the carrier of L) is non empty set

g is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

g . (c . y) is Element of the carrier of L

g . (c . Y) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of L is non empty set

X is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

g is Element of the carrier of L

c . g is Element of the carrier of X

L is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of L is non empty set

X is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

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

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

c " is Relation-like Function-like set

y is Element of the carrier of L

compactbelow y is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

c .: (compactbelow y) is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

c . y is Element of the carrier of X

compactbelow (c . y) is Element of K32( the carrier of X)

g is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

Y is set

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

{ b

X is Element of the carrier of X

g . X is Element of the carrier of L

g . (c . y) is Element of the carrier of L

rng c is Element of K32( the carrier of X)

c . (g . X) is Element of the carrier of X

Y is set

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

X is set

c . X is set

{ b

x is Element of the carrier of L

c . x is Element of the carrier of X

L is non empty reflexive transitive antisymmetric RelStr

X is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

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

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

c " is Relation-like Function-like set

g is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

K32( the carrier of X) is non empty set

y is non empty directed Element of K32( the carrier of X)

rng c is Element of K32( the carrier of X)

g .: y is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

K32((g .: y)) is non empty set

Y is finite Element of K32((g .: y))

c .: Y is finite Element of K32( the carrier of X)

c " (c .: Y) is Element of K32( the carrier of L)

X is set

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

c .: (g .: y) is Element of K32( the carrier of X)

x is set

c . x is set

c " y is Element of K32( the carrier of L)

c .: (c " y) is Element of K32( the carrier of X)

K32(y) is non empty set

X is finite Element of K32(y)

x is Element of the carrier of X

g . x is Element of the carrier of L

dom g is Element of K32( the carrier of X)

fx is Element of the carrier of L

g .: X is finite Element of K32( the carrier of L)

Y is non empty directed Element of K32( the carrier of L)

X is Element of the carrier of L

x is Element of the carrier of X

g . x is Element of the carrier of L

c . X is Element of the carrier of X

c . (g . x) is Element of the carrier of X

c .: Y is Element of K32( the carrier of X)

L is non empty reflexive transitive antisymmetric RelStr

X is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

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

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

c " is Relation-like Function-like set

g is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

y is Element of the carrier of X

g . y is Element of the carrier of L

compactbelow (g . y) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

dom g is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

rng c is Element of K32( the carrier of X)

c . (g . y) is Element of the carrier of X

"\/" ((compactbelow (g . y)),L) is Element of the carrier of L

c . ("\/" ((compactbelow (g . y)),L)) is Element of the carrier of X

c .: (compactbelow (g . y)) is Element of K32( the carrier of X)

"\/" ((c .: (compactbelow (g . y))),X) is Element of the carrier of X

compactbelow (c . (g . y)) is Element of K32( the carrier of X)

"\/" ((compactbelow (c . (g . y))),X) is Element of the carrier of X

compactbelow y is Element of K32( the carrier of X)

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

L is non empty reflexive transitive antisymmetric with_suprema RelStr

X is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

the carrier of X is non empty set

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

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

c is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V20( the carrier of L) V21( the carrier of L, the carrier of X) Element of K32(K33( the carrier of L, the carrier of X))

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

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

c " is Relation-like Function-like set

g is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of L) Element of K32(K33( the carrier of X, the carrier of L))

y is Element of the carrier of X

dom g is Element of K32( the carrier of X)

K32( the carrier of X) is non empty set

rng c is Element of K32( the carrier of X)

g . y is Element of the carrier of L

compactbelow (g . y) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

c . (g . y) is Element of the carrier of X

compactbelow (c . (g . y)) is Element of K32( the carrier of X)

K32((compactbelow (c . (g . y)))) is non empty set

Y is finite Element of K32((compactbelow (c . (g . y))))

X is set

g .: Y is finite Element of K32( the carrier of L)

x is set

g . x is set

fx is Element of the carrier of X

compactbelow y is Element of K32( the carrier of X)

g . fx is Element of the carrier of L

K32((compactbelow (g . y))) is non empty set

X is finite Element of K32((compactbelow (g . y)))

x is Element of the carrier of L

c . x is Element of the carrier of X

fx is Element of the carrier of X

c .: X is finite Element of K32( the carrier of X)

c " Y is Element of K32( the carrier of L)

c .: (c " Y) is Element of K32( the carrier of X)

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of (BoolePoset X) is non empty set

K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) is non empty set

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

c is non empty Relation-like the carrier of (BoolePoset X) -defined the carrier of (BoolePoset X) -valued Function-like V20( the carrier of (BoolePoset X)) V21( the carrier of (BoolePoset X), the carrier of (BoolePoset X)) V153() monotone projection closure Element of K32(K33( the carrier of (BoolePoset X), the carrier of (BoolePoset X)))

Image c is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of BoolePoset X

rng c is Element of K32( the carrier of (BoolePoset X))

K32( the carrier of (BoolePoset X)) is non empty set

subrelstr (rng c) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset X

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

Ids L is non empty set

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

SupMap L is non empty Relation-like the carrier of (InclPoset (Ids L)) -defined the carrier of L -valued Function-like V20( the carrier of (InclPoset (Ids L))) V21( the carrier of (InclPoset (Ids L)), the carrier of L) monotone Element of K32(K33( the carrier of (InclPoset (Ids L)), the carrier of L))

the carrier of (InclPoset (Ids L)) is non empty set

the carrier of L is non empty set

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

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

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr

Ids X is non empty set

InclPoset (Ids X) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete RelStr

SupMap X is non empty Relation-like the carrier of (InclPoset (Ids X)) -defined the carrier of X -valued Function-like V20( the carrier of (InclPoset (Ids X))) V21( the carrier of (InclPoset (Ids X)), the carrier of X) monotone Element of K32(K33( the carrier of (InclPoset (Ids X)), the carrier of X))

the carrier of (InclPoset (Ids X)) is non empty set

the carrier of X is non empty set

K33( the carrier of (InclPoset (Ids X)), the carrier of X) is non empty set

K32(K33( the carrier of (InclPoset (Ids X)), the carrier of X)) is non empty set

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

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

c is reflexive transitive antisymmetric full SubRelStr of BoolePoset X

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V223() up-complete /\-complete distributive V263() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K