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
{ b1 where b1 is Element of the carrier of L : ( b1 <= X & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of L : ( b1 <= X & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of c : y c= b1 } is set
meet { b1 where b1 is Element of the carrier of c : y c= b1 } is set
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)
{ b1 where b1 is Element of the carrier of c : g c= b1 } is set
meet { b1 where b1 is Element of the carrier of c : g c= b1 } is 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
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of L) : verum } is set
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of L) : verum } is set
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
{ b1 where b1 is non empty directed lower Element of K32( the carrier of L) : verum } is set
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)
{ b1 where b1 is Element of the carrier of X : y c= b1 } is set
meet { b1 where b1 is Element of the carrier of X : y c= b1 } is set
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)
{ b1 where b1 is Element of the carrier of X : Y c= b1 } is set
meet { b1 where b1 is Element of the carrier of X : Y c= b1 } is set
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)
{ b1 where b1 is Element of the carrier of X : Y c= b1 } is set
meet { b1 where b1 is Element of the carrier of X : Y c= b1 } is 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 (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)
{ b1 where b1 is non empty directed lower Element of K32( the carrier of L) : verum } is set
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
{ b1 where b1 is Element of the carrier of L : ( b1 <= "\/" (Y,L) & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of (X . y) : ( b1 <= g . y & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of (product X) : ( b1 <= g & b1 is compact ) } is set
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)
{ b1 where b1 is Element of the carrier of X : ( b1 <= c . y & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of L : ( b1 <= y & b1 is compact ) } is set
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 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 lower-bounded 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
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