K165() is Element of K32(K161())
K161() is set
K32(K161()) is non empty set
K113() is set
K32(K113()) is non empty set
{} is empty finite V35() set
the empty finite V35() set is empty finite V35() set
1 is non empty set
{{},1} is non empty finite set
K32(K165()) is non empty set
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
p is Element of the carrier of L
uparrow p is non empty filtered upper Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
(uparrow p) /\ (uparrow A) is Element of K32( the carrier of L)
"/\" (((uparrow p) /\ (uparrow A)),L) is Element of the carrier of L
p "\/" A is Element of the carrier of L
uparrow (p "\/" A) is non empty filtered upper Element of K32( the carrier of L)
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
p is Element of the carrier of L
downarrow p is non empty directed lower Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
A is Element of the carrier of L
downarrow A is non empty directed lower Element of K32( the carrier of L)
(downarrow p) /\ (downarrow A) is Element of K32( the carrier of L)
"\/" (((downarrow p) /\ (downarrow A)),L) is Element of the carrier of L
p "/\" A is Element of the carrier of L
downarrow (p "/\" A) is non empty directed lower Element of K32( the carrier of L)
L is non empty RelStr
the carrier of L is non empty set
A is Element of the carrier of L
uparrow A is Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
the carrier of L \ (uparrow A) is Element of K32( the carrier of L)
p is Element of the carrier of L
uparrow p is Element of K32( the carrier of L)
{p} is non empty finite Element of K32( the carrier of L)
(uparrow p) \ {p} is Element of K32( the carrier of L)
(uparrow p) /\ (uparrow A) is Element of K32( the carrier of L)
x is set
k is Element of the carrier of L
x is set
k is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
A is Element of the carrier of L
downarrow A is Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
the carrier of L \ (downarrow A) is Element of K32( the carrier of L)
p is Element of the carrier of L
downarrow p is Element of K32( the carrier of L)
{p} is non empty finite Element of K32( the carrier of L)
(downarrow p) \ {p} is Element of K32( the carrier of L)
(downarrow p) /\ (downarrow A) is Element of K32( the carrier of L)
x is set
k is Element of the carrier of L
x is set
k is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
L ~ is non empty strict reflexive transitive antisymmetric with_infima RelStr
the carrier of (L ~) is non empty set
K32( the carrier of (L ~)) is non empty set
p is Element of K32( the carrier of L)
A is Element of K32( the carrier of L)
p "\/" A is Element of K32( the carrier of L)
x is Element of K32( the carrier of (L ~))
k is Element of K32( the carrier of (L ~))
x "/\" k is Element of K32( the carrier of (L ~))
c6 is set
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of L : ( b1 in p & b2 in A ) } is set
y is Element of the carrier of L
x is Element of the carrier of L
y "\/" x is Element of the carrier of L
y ~ is Element of the carrier of (L ~)
x ~ is Element of the carrier of (L ~)
(y ~) "/\" (x ~) is Element of the carrier of (L ~)
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of (L ~) : ( b1 in x & b2 in k ) } is set
c6 is set
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of (L ~) : ( b1 in x & b2 in k ) } is set
y is Element of the carrier of (L ~)
x is Element of the carrier of (L ~)
y "/\" x is Element of the carrier of (L ~)
~ y is Element of the carrier of L
~ x is Element of the carrier of L
(~ y) "\/" (~ x) is Element of the carrier of L
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of L : ( b1 in p & b2 in A ) } is set
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
L ~ is non empty strict reflexive transitive antisymmetric with_suprema RelStr
the carrier of (L ~) is non empty set
K32( the carrier of (L ~)) is non empty set
p is Element of K32( the carrier of L)
A is Element of K32( the carrier of L)
p "/\" A is Element of K32( the carrier of L)
x is Element of K32( the carrier of (L ~))
k is Element of K32( the carrier of (L ~))
x "\/" k is Element of K32( the carrier of (L ~))
c6 is set
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of L : ( b1 in p & b2 in A ) } is set
y is Element of the carrier of L
x is Element of the carrier of L
y "/\" x is Element of the carrier of L
y ~ is Element of the carrier of (L ~)
x ~ is Element of the carrier of (L ~)
(y ~) "\/" (x ~) is Element of the carrier of (L ~)
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of (L ~) : ( b1 in x & b2 in k ) } is set
c6 is set
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of (L ~) : ( b1 in x & b2 in k ) } is set
y is Element of the carrier of (L ~)
x is Element of the carrier of (L ~)
y "\/" x is Element of the carrier of (L ~)
~ y is Element of the carrier of L
~ x is Element of the carrier of L
(~ y) "/\" (~ x) is Element of the carrier of L
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of L : ( b1 in p & b2 in A ) } is set
L is non empty reflexive transitive RelStr
Filt L is set
L ~ is non empty strict reflexive transitive RelStr
Ids (L ~) is non empty set
p 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
A is non empty directed lower Element of K32( the carrier of (L ~))
the carrier of L is non empty set
K32( the carrier of L) is non empty set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of L) : verum } is set
p 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 filtered upper Element of K32( the carrier of L) : verum } is set
A is non empty filtered upper Element of K32( the carrier of L)
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
L is non empty reflexive transitive RelStr
Ids L is non empty set
L ~ is non empty strict reflexive transitive RelStr
Filt (L ~) is set
p 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 filtered upper Element of K32( the carrier of (L ~)) : verum } is set
A is non empty filtered upper Element of K32( the carrier of (L ~))
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
p 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
A is non empty directed lower Element of K32( the carrier of L)
the carrier of (L ~) is non empty set
K32( the carrier of (L ~)) is non empty set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of (L ~)) : verum } is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
p is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of p is non empty set
K33( the carrier of L, the carrier of p) is non empty set
K32(K33( the carrier of L, the carrier of p)) is non empty set
Top p is Element of the carrier of p
the carrier of L --> (Top p) is V7() V10( the carrier of L) V11( the carrier of p) V12() V18( the carrier of L, the carrier of p) Element of K32(K33( the carrier of L, the carrier of p))
A is V7() V10( the carrier of L) V11( the carrier of p) V12() V18( the carrier of L, the carrier of p) Element of K32(K33( the carrier of L, the carrier of p))
x is V7() V10( the carrier of L) V11( the carrier of p) V12() V18( the carrier of L, the carrier of p) Element of K32(K33( the carrier of L, the carrier of p))
K32( the carrier of L) is non empty set
k is Element of K32( the carrier of L)
rng x is Element of K32( the carrier of p)
K32( the carrier of p) is non empty set
{(Top p)} is non empty finite Element of K32( the carrier of p)
x .: k is Element of K32( the carrier of p)
c6 is Element of the carrier of L
y is Element of the carrier of L
x . c6 is Element of the carrier of p
x . y is Element of the carrier of p
"\/" ((x .: k),p) is Element of the carrier of p
"\/" (k,L) is Element of the carrier of L
x . ("\/" (k,L)) is Element of the carrier of p
k is Element of K32( the carrier of L)
x .: k is Element of K32( the carrier of p)
K32({(Top p)}) is non empty finite V35() set
"/\" ((x .: k),p) is Element of the carrier of p
"/\" (k,L) is Element of the carrier of L
x . ("/\" (k,L)) is Element of the carrier of p
"/\" ((x .: k),p) is Element of the carrier of p
"/\" (k,L) is Element of the carrier of L
x . ("/\" (k,L)) is Element of the carrier of p
"/\" ((x .: k),p) is Element of the carrier of p
"/\" (k,L) is Element of the carrier of L
x . ("/\" (k,L)) is Element of the carrier of p
"/\" ((x .: k),p) is Element of the carrier of p
"/\" (k,L) is Element of the carrier of L
x . ("/\" (k,L)) is Element of the carrier of p
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
L is non empty reflexive transitive antisymmetric upper-bounded RelStr
Filt L is set
the carrier of L is non empty set
p is Element of the carrier of L
Top L is Element of the carrier of L
{(Top L)} is non empty finite Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
A is Element of the carrier of L
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of L) : verum } is set
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
Filt (BoolePoset L) is non empty set
InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set
K32( the carrier of (InclPoset (Filt (BoolePoset L)))) is non empty set
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
A is non empty Element of K32( the carrier of (InclPoset (Filt (BoolePoset L))))
meet A is set
x is set
RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))
K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set
K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set
RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr
the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of (BoolePoset L)) : verum } is set
Top (BoolePoset L) is Element of the carrier of (BoolePoset L)
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
x is Element of K32( the carrier of (BoolePoset L))
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
x is Element of K32( the carrier of (BoolePoset L))
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
bool the carrier of (BoolePoset L) is non empty Element of K32(K32( the carrier of (BoolePoset L)))
K32(K32( the carrier of (BoolePoset L))) is non empty set
x is set
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
Filt (BoolePoset L) is non empty set
InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set
K32( the carrier of (InclPoset (Filt (BoolePoset L)))) is non empty set
A is non empty Element of K32( the carrier of (InclPoset (Filt (BoolePoset L))))
"/\" (A,(InclPoset (Filt (BoolePoset L)))) is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
meet A is set
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of (BoolePoset L)) : verum } is set
RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))
K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set
K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set
RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr
the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set
x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
k is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
c6 is set
y is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
k is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
L is set
bool L is non empty Element of K32(K32(L))
K32(L) is non empty set
K32(K32(L)) is non empty set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
A is set
p is non empty Element of K32( the carrier of (BoolePoset L))
x is set
A /\ x is set
L /\ L is set
A is set
x is set
L is set
{L} is non empty finite set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
p is set
p is non empty Element of K32( the carrier of (BoolePoset L))
A is set
x is set
A is set
x is set
A /\ x is set
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
Filt (BoolePoset L) is non empty set
InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr
bool L is non empty Element of K32(K32(L))
K32(L) is non empty set
K32(K32(L)) is non empty set
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of (BoolePoset L)) : verum } is set
RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))
K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set
K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set
RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr
the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set
the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set
x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
Filt (BoolePoset L) is non empty set
InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr
{L} is non empty finite set
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of (BoolePoset L)) : verum } is set
RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))
K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set
K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set
RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr
the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set
the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set
x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
c6 is set
y is set
A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
Filt (BoolePoset L) is non empty set
InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr
Top (InclPoset (Filt (BoolePoset L))) is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set
bool L is non empty Element of K32(K32(L))
K32(L) is non empty set
K32(K32(L)) is non empty set
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of (BoolePoset L)) : verum } is set
RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))
K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set
K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set
RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr
the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set
A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
"/\" ({},(InclPoset (Filt (BoolePoset L)))) is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
Filt (BoolePoset L) is non empty set
InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr
Bottom (InclPoset (Filt (BoolePoset L))) is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set
{L} is non empty finite set
the carrier of (BoolePoset L) is non empty set
K32( the carrier of (BoolePoset L)) is non empty set
{ b1 where b1 is non empty filtered upper Element of K32( the carrier of (BoolePoset L)) : verum } is set
RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))
K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set
K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set
RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr
the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set
A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))
c6 is set
y is set
"\/" ({},(InclPoset (Filt (BoolePoset L)))) is Element of the carrier of (InclPoset (Filt (BoolePoset L)))
L is non empty set
InclPoset L is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset L) is non empty set
K32( the carrier of (InclPoset L)) is non empty set
p is non empty Element of K32( the carrier of (InclPoset L))
union p is set
"\/" (p,(InclPoset L)) is Element of the carrier of (InclPoset L)
A is set
x is Element of the carrier of (InclPoset L)
L is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
Filt L is non empty set
InclPoset (Filt L) is non empty strict reflexive transitive antisymmetric RelStr
L ~ is non empty strict reflexive transitive antisymmetric lower-bounded with_suprema RelStr
Ids (L ~) is non empty set
InclPoset (Ids (L ~)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete RelStr
L is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
Filt L is non empty set
InclPoset (Filt L) is non empty strict reflexive transitive antisymmetric RelStr
L is non empty RelStr
the carrier of L is non empty set
L is non empty RelStr
the carrier of L is non empty set
p is Element of the carrier of L
uparrow p is Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
{p} is non empty finite Element of K32( the carrier of L)
(uparrow p) \ {p} is Element of K32( the carrier of L)
"/\" (((uparrow p) \ {p}),L) is Element of 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
p is Element of K32( the carrier of L)
A is Element of the carrier of L
x is Element of the carrier of L
p is Element of K32( the carrier of L)
A is Element of K32( the carrier of L)
x is set
k is Element of the carrier of L
k is Element of the carrier of L
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
p is Element of the carrier of L
uparrow p is non empty filtered upper Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
{p} is non empty finite Element of K32( the carrier of L)
(uparrow p) \ {p} is Element of K32( the carrier of L)
"/\" (((uparrow p) \ {p}),L) is Element of the carrier of L
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
{p} \/ (uparrow A) is non empty Element of K32( the carrier of L)
x is Element of the carrier of L
x is set
k is Element of the carrier of L
x is Element of the carrier of L
x is set
k is Element of the carrier of L
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
{p} \/ (uparrow A) is non empty Element of K32( the carrier of L)
(uparrow p) \ {p} is Element of K32( the carrier of L)
x is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
"/\" (((uparrow p) \ {p}),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric upper-bounded RelStr
Top L is Element of the carrier of L
the carrier of L is non empty set
(L) is Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
uparrow (Top L) is non empty filtered upper Element of K32( the carrier of L)
{(Top L)} is non empty finite Element of K32( the carrier of L)
(uparrow (Top L)) \ {(Top L)} is Element of K32( the carrier of L)
"/\" (((uparrow (Top L)) \ {(Top L)}),L) is Element of the carrier of L
{(Top L)} \ {(Top L)} is finite Element of K32( the carrier of L)
"/\" (({(Top L)} \ {(Top L)}),L) is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
(L) is Element of K32( the carrier of L)
the carrier of L is non empty set
K32( the carrier of L) is non empty set
IRR L is Element of K32( the carrier of L)
p is set
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
{A} is non empty finite Element of K32( the carrier of L)
x is Element of the carrier of L
uparrow x is non empty filtered upper Element of K32( the carrier of L)
{A} \/ (uparrow x) is non empty Element of K32( the carrier of L)
k is Element of the carrier of L
c6 is Element of the carrier of L
k "/\" c6 is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
p is Element of the carrier of L
(L) is Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
IRR L is Element of K32( the carrier of L)
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
p is Element of the carrier of L
uparrow p is non empty filtered upper Element of K32( the carrier of L)
{p} is non empty finite Element of K32( the carrier of L)
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
{p} \/ (uparrow A) is non empty 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
k is set
c6 is Element of the carrier of L
"/\" ((uparrow A),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
(L) is Element of K32( the carrier of L)
p is Element of K32( the carrier of L)
A is set
x is Element of the carrier of L
uparrow x is non empty filtered upper Element of K32( the carrier of L)
(uparrow x) /\ p is Element of K32( the carrier of L)
"/\" (((uparrow x) /\ p),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
p is Element of the carrier of L
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
the carrier of L \ (uparrow A) is Element of K32( the carrier of L)
p "\/" A is Element of the carrier of L
uparrow p is non empty filtered upper Element of K32( the carrier of L)
{p} is non empty finite Element of K32( the carrier of L)
(uparrow p) \ {p} is Element of K32( the carrier of L)
(uparrow p) /\ (uparrow A) is Element of K32( the carrier of L)
"/\" (((uparrow p) \ {p}),L) is Element of the carrier of L
L is non empty transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
p is Element of the carrier of L
A is Element of the carrier of L
x is Element of the carrier of L
p "\/" x is Element of the carrier of L
A "\/" x is Element of the carrier of L
k is Element of the carrier of L
L is non empty reflexive transitive antisymmetric distributive with_suprema with_infima RelStr
the carrier of L is non empty set
p is Element of the carrier of L
A is Element of the carrier of L
x is Element of the carrier of L
x "/\" A is Element of the carrier of L
p "\/" (x "/\" A) is Element of the carrier of L
p "\/" x is Element of the carrier of L
A "\/" p is Element of the carrier of L
(p "\/" x) "/\" (A "\/" p) is Element of the carrier of L
(p "\/" x) "/\" A is Element of the carrier of L
A "\/" x is Element of the carrier of L
A "/\" (A "\/" x) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete RelStr
L ~ is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
p is Element of the carrier of L
downarrow p is non empty directed lower Element of K32( the carrier of L)
the carrier of L \ (downarrow p) is Element of K32( the carrier of L)
uparrow p is non empty filtered upper Element of K32( the carrier of L)
{p} is non empty finite Element of K32( the carrier of L)
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
{p} \/ (uparrow A) is non empty Element of K32( the carrier of L)
{ b1 where b1 is Element of the carrier of L : S1[b1] } is set
x is Element of K32( the carrier of L)
k is Element of the carrier of L
c6 is Element of the carrier of L
k "/\" c6 is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
k "/\" A is Element of the carrier of L
c6 "\/" p is Element of the carrier of L
k "/\" (c6 "\/" p) is Element of the carrier of L
k "/\" p is Element of the carrier of L
y "\/" (k "/\" p) is Element of the carrier of L
k "\/" y is Element of the carrier of L
y "\/" p is Element of the carrier of L
(k "\/" y) "/\" (y "\/" p) is Element of the carrier of L
p "\/" y is Element of the carrier of L
k "/\" (p "\/" y) is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
Top L is Element of the carrier of L
(L) is Element of K32( the carrier of L)
(downarrow p) ` is Element of K32( the carrier of L)
the carrier of (L ~) is non empty set
K32( the carrier of (L ~)) is non empty set
c6 is non empty filtered Element of K32( the carrier of L)
x is Element of the carrier of L
k is non empty filtered upper Element of K32( the carrier of L)
"/\" (c6,L) is Element of the carrier of L
y is Element of the carrier of L
D is Element of the carrier of L
{p} "\/" c6 is Element of K32( the carrier of L)
{ (p "\/" b1) where b1 is Element of the carrier of L : b1 in c6 } is set
d is Element of the carrier of L
p "\/" d is Element of the carrier of L
d is Element of the carrier of L
p ~ is Element of the carrier of (L ~)
{(p ~)} is non empty finite Element of K32( the carrier of (L ~))
y is non empty directed Element of K32( the carrier of (L ~))
{(p ~)} "/\" y is Element of K32( the carrier of (L ~))
"\/" (y,(L ~)) is Element of the carrier of (L ~)
p "\/" y is Element of the carrier of L
("/\" (c6,L)) ~ is Element of the carrier of (L ~)
(p ~) "/\" (("/\" (c6,L)) ~) is Element of the carrier of (L ~)
(p ~) "/\" ("\/" (y,(L ~))) is Element of the carrier of (L ~)
"\/" (({(p ~)} "/\" y),(L ~)) is Element of the carrier of (L ~)
"/\" (({(p ~)} "/\" y),L) is Element of the carrier of L
"/\" (({p} "\/" c6),L) is Element of the carrier of L
D is non empty directed Element of K32( the carrier of L)
"\/" (D,L) is Element of the carrier of L
D \ (downarrow p) is Element of K32( the carrier of L)
"\/" ((downarrow p),L) is Element of the carrier of L
d is set
d is Element of the carrier of L
d is Element of the carrier of L
d "/\" A is Element of the carrier of L
x "/\" A is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete RelStr
L ~ is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete RelStr
the carrier of L is non empty set
CompactSublatt L is non empty strict reflexive transitive antisymmetric V128(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
p is Element of the carrier of L
K32( the carrier of L) is non empty set
downarrow p is non empty directed lower Element of K32( the carrier of L)
the carrier of L \ (downarrow p) is Element of K32( the carrier of L)
x is Element of the carrier of L
uparrow p is non empty filtered upper Element of K32( the carrier of L)
{p} is non empty finite Element of K32( the carrier of L)
(uparrow p) \ {p} is Element of K32( the carrier of L)
"/\" (((uparrow p) \ {p}),L) is Element of the carrier of L
A is non empty filtered upper Open Element of K32( the carrier of L)
"/\" (A,L) is Element of the carrier of L
("/\" (A,L)) ~ is Element of the carrier of (L ~)
the carrier of (L ~) is non empty set
x is Element of the carrier of L
uparrow x is non empty filtered upper Element of K32( the carrier of L)
the carrier of L \ (uparrow x) is Element of K32( the carrier of L)
K32( the carrier of (L ~)) is non empty set
p ~ is Element of the carrier of (L ~)
{(p ~)} is non empty finite Element of K32( the carrier of (L ~))
k is non empty directed Element of K32( the carrier of (L ~))
{(p ~)} "/\" k is Element of K32( the carrier of (L ~))
{p} "\/" A is Element of K32( the carrier of L)
c6 is set
{ (p "\/" b1) where b1 is Element of the carrier of L : b1 in A } is set
y is Element of the carrier of L
p "\/" y is Element of the carrier of L
p "\/" x is Element of the carrier of L
(p ~) "/\" (("/\" (A,L)) ~) is Element of the carrier of (L ~)
"\/" (A,(L ~)) is Element of the carrier of (L ~)
(p ~) "/\" ("\/" (A,(L ~))) is Element of the carrier of (L ~)
"\/" (({(p ~)} "/\" k),(L ~)) is Element of the carrier of (L ~)
"/\" (({(p ~)} "/\" k),L) is Element of the carrier of L
"/\" (({p} "\/" A),L) is Element of the carrier of L
c6 is set
y is Element of the carrier of L
c6 is set
y is Element of the carrier of L
c6 is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
the carrier of L is non empty set
A is Element of the carrier of L
p is Element of the carrier of L
x is Element of the carrier of L
waybelow x is non empty directed lower Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
k is Element of the carrier of L
waybelow k is non empty directed lower Element of K32( the carrier of L)
x is Element of the carrier of L
CompactSublatt L is non empty strict reflexive transitive antisymmetric V128(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
k is Element of the carrier of L
uparrow k is non empty filtered upper Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
the carrier of L \ (uparrow k) is Element of K32( the carrier of L)
(uparrow k) ` is Element of K32( the carrier of L)
c6 is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
(L) is Element of K32( the carrier of L)
the carrier of L is non empty set
K32( the carrier of L) is non empty set
A is Element of the carrier of L
p is Element of the carrier of L
x is Element of the carrier of L
k is Element of the carrier of L
p is Element of K32( the carrier of L)
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr
the carrier of L is non empty set
(L) is Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
p is Element of the carrier of L
uparrow p is non empty filtered upper Element of K32( the carrier of L)
(uparrow p) /\ (L) is Element of K32( the carrier of L)
"/\" (((uparrow p) /\ (L)),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
K32( the carrier of L) is non empty set
p is Element of K32( the carrier of L)
"/\" (p,L) is Element of the carrier of L
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
{A} is non empty finite Element of K32( the carrier of L)
x is Element of the carrier of L
uparrow x is non empty filtered upper Element of K32( the carrier of L)
{A} \/ (uparrow x) is non empty Element of K32( the carrier of L)
k is Element of the carrier of L
k is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima 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 V128(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
p is Element of the carrier of L
uparrow p is non empty filtered upper Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
{ b1 where b1 is Element of the carrier of L : ( b1 in uparrow p & ex b2 being Element of the carrier of L st
( b2 in the carrier of (CompactSublatt L) & b1 is_maximal_in the carrier of L \ (uparrow b2) ) ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( b1 in uparrow p & ex b2 being Element of the carrier of L st
( b2 in the carrier of (CompactSublatt L) & b1 is_maximal_in the carrier of L \ (uparrow b2) ) ) } ,L) is Element of the carrier of L
x is Element of the carrier of L
k is Element of the carrier of L
c6 is Element of the carrier of L
uparrow c6 is non empty filtered upper Element of K32( the carrier of L)
the carrier of L \ (uparrow c6) is Element of K32( the carrier of L)
{p} is non empty finite Element of K32( the carrier of L)
x is Element of the carrier of L
uparrow x is non empty filtered upper Element of K32( the carrier of L)
{p} \/ (uparrow x) is non empty Element of K32( the carrier of L)
compactbelow p 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
k is set
{ b1 where b1 is Element of the carrier of L : ( b1 <= x & b1 is compact ) } is set
c6 is Element of the carrier of L
uparrow c6 is non empty filtered upper Element of K32( the carrier of L)
the carrier of L \ (uparrow c6) is Element of K32( the carrier of L)
y is Element of the carrier of L
y is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima 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 V128(L) join-inheriting with_suprema SubRelStr of L
the carrier of (CompactSublatt L) is non empty set
p is Element of the carrier of L
A is Element of the carrier of L
uparrow A is non empty filtered upper Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
the carrier of L \ (uparrow A) is Element of K32( the carrier of L)
uparrow p is non empty filtered upper Element of K32( the carrier of L)
K32( the carrier of L) is non empty set
{ b1 where b1 is Element of the carrier of L : S1[b1] } is set
A is Element of K32( the carrier of L)
"/\" (A,L) is Element of the carrier of L
x is Element of the carrier of L
k is Element of the carrier of L
uparrow k is non empty filtered upper Element of K32( the carrier of L)
the carrier of L \ (uparrow k) is Element of K32( the carrier of L)
k is Element of the carrier of L
uparrow k is non empty filtered upper Element of K32( the carrier of L)
the carrier of L \ (uparrow k) is Element of K32( the carrier of L)