:: WAYBEL31 semantic presentation

K96() is set
K100() is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K32(K96())
K32(K96()) is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
K32(omega) is non empty non trivial non finite set
K32(K100()) is non empty non trivial non finite set
{} is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element FinSequence-membered set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of K100()
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of K100()
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of K100()
F₁() is RelStr
the carrier of F₁() is set
K32( the carrier of F₁()) is non empty set
K32(K32( the carrier of F₁())) is non empty set
{ b₁ where b₁ is Element of K32( the carrier of F₁()) : P₁[b₁] } is set
{ (uparrow b₁) where b₁ is Element of K32( the carrier of F₁()) : P₁[b₁] } is set
union { (uparrow b₁) where b₁ is Element of K32( the carrier of F₁()) : P₁[b₁] } is set
L1 is Element of K32(K32( the carrier of F₁()))
union L1 is Element of K32( the carrier of F₁())
uparrow (union L1) is Element of K32( the carrier of F₁())
S is set
f is set
B0 is Element of K32( the carrier of F₁())
uparrow B0 is Element of K32( the carrier of F₁())
B2 is Element of the carrier of F₁()
f is Element of the carrier of F₁()
S is set
f is Element of the carrier of F₁()
B0 is Element of the carrier of F₁()
B2 is set
f is Element of K32( the carrier of F₁())
uparrow f is Element of K32( the carrier of F₁())
F₁() is RelStr
the carrier of F₁() is set
K32( the carrier of F₁()) is non empty set
K32(K32( the carrier of F₁())) is non empty set
{ b₁ where b₁ is Element of K32( the carrier of F₁()) : P₁[b₁] } is set
{ (downarrow b₁) where b₁ is Element of K32( the carrier of F₁()) : P₁[b₁] } is set
union { (downarrow b₁) where b₁ is Element of K32( the carrier of F₁()) : P₁[b₁] } is set
L1 is Element of K32(K32( the carrier of F₁()))
union L1 is Element of K32( the carrier of F₁())
downarrow (union L1) is Element of K32( the carrier of F₁())
S is set
f is set
B0 is Element of K32( the carrier of F₁())
downarrow B0 is Element of K32( the carrier of F₁())
B2 is Element of the carrier of F₁()
f is Element of the carrier of F₁()
S is set
f is Element of the carrier of F₁()
B0 is Element of the carrier of F₁()
B2 is set
f is Element of K32( the carrier of F₁())
downarrow f is Element of K32( the carrier of F₁())
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
S is non empty directed join-closed with_bottom CLbasis of L1
subrelstr S is non empty strict reflexive transitive antisymmetric lower-bounded full directed with_suprema V204() SubRelStr of L1
Ids (subrelstr S) is non empty set
InclPoset (Ids (subrelstr S)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete V204() RelStr
L1 is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema satisfying_axiom_of_approximation continuous V204() RelStr
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
[#] L1 is non empty non proper directed lower upper meet-closed join-closed infs-closed sups-closed with_bottom with_top Element of K32( the carrier of L1)
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
len ([#] L1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
f is epsilon-transitive epsilon-connected ordinal set
B2 is non empty directed join-closed with_bottom CLbasis of L1
len B2 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
B2 is set
B0 is epsilon-transitive epsilon-connected ordinal cardinal set
f is set
B2 is non empty directed join-closed with_bottom CLbasis of L1
len B2 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
B2 is epsilon-transitive epsilon-connected ordinal cardinal set
[#] L1 is non empty non proper directed lower upper meet-closed join-closed infs-closed sups-closed with_bottom with_top Element of K32( the carrier of L1)
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
len ([#] L1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema satisfying_axiom_of_approximation continuous V204() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
S is non empty directed join-closed with_bottom CLbasis of L1
len S is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema satisfying_axiom_of_approximation continuous V204() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
[#] L1 is non empty non proper directed lower upper meet-closed join-closed infs-closed sups-closed with_bottom with_top Element of K32( the carrier of L1)
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
len ([#] L1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
f is epsilon-transitive epsilon-connected ordinal set
B0 is non empty directed join-closed with_bottom CLbasis of L1
len B0 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
B2 is set
f is set
B2 is non empty directed join-closed with_bottom CLbasis of L1
len B2 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
B2 is epsilon-transitive epsilon-connected ordinal cardinal set
[#] L1 is non empty non proper directed lower upper meet-closed join-closed infs-closed sups-closed with_bottom with_top Element of K32( the carrier of L1)
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
len ([#] L1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete satisfying_axiom_K algebraic with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
CompactSublatt L1 is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema V204() SubRelStr of L1
the carrier of (CompactSublatt L1) is non empty set
len the carrier of (CompactSublatt L1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
f is set
B0 is non empty directed join-closed with_bottom CLbasis of L1
len B0 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty TopSpace-like TopStruct
the topology of L1 is non empty Element of K32(K32( the carrier of L1))
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset the topology of L1 is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete distributive with_suprema with_infima complete V204() RelStr
S is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema satisfying_axiom_of_approximation continuous V204() RelStr
f is non empty directed join-closed with_bottom CLbasis of S
the carrier of S is non empty set
B0 is Element of K32(K32( the carrier of L1))
B2 is Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
f is Element of the carrier of S
waybelow f is non empty directed lower join-closed Element of K32( the carrier of S)
K32( the carrier of S) is non empty set
(waybelow f) /\ f is Element of K32( the carrier of S)
"\/" (((waybelow f) /\ f),S) is Element of the carrier of S
union ((waybelow f) /\ f) is set
B2 is set
x is Element of K32( the carrier of L1)
y is Element of the carrier of S
B2 is set
f is Element of the carrier of S
L1 is non empty TopSpace-like TopStruct
the topology of L1 is non empty Element of K32(K32( the carrier of L1))
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset the topology of L1 is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete distributive with_suprema with_infima complete V204() RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty set
f is open quasi_basis Element of K32(K32( the carrier of L1))
B0 is Element of K32( the carrier of S)
finsups B0 is non empty directed Element of K32( the carrier of S)
f is Element of the carrier of S
B2 is Element of the carrier of S
B2 is set
B2 is Element of K32( the carrier of L1)
x is Element of the carrier of L1
y is Element of K32( the carrier of L1)
x1 is Element of the carrier of S
{x1} is non empty trivial finite 1 -element Element of K32( the carrier of S)
y1 is set
K32(B0) is non empty set
"\/" ({x1},S) is Element of the carrier of S
{ ("\/" (b₁,S)) where b₁ is finite Element of K32(B0) : ex_sup_of b₁,S } is set
B2 is Element of the carrier of S
f is Element of the carrier of S
K32(B0) is non empty set
{ ("\/" (b₁,S)) where b₁ is finite Element of K32(B0) : ex_sup_of b₁,S } is set
B2 is finite Element of K32(B0)
"\/" (B2,S) is Element of the carrier of S
B2 is finite Element of K32(B0)
"\/" (B2,S) is Element of the carrier of S
B2 \/ B2 is finite Element of K32(B0)
"\/" ((B2 \/ B2),S) is Element of the carrier of S
("\/" (B2,S)) "\/" ("\/" (B2,S)) is Element of the carrier of S
B2 "\/" f is Element of the carrier of S
{B2,f} is non empty finite Element of K32( the carrier of S)
"\/" ({B2,f},S) is Element of the carrier of S
"\/" ({},S) is Element of the carrier of S
Bottom S is Element of the carrier of S
L1 is non empty TopSpace-like T_0 TopStruct
the topology of L1 is non empty Element of K32(K32( the carrier of L1))
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset the topology of L1 is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete distributive with_suprema with_infima complete V204() RelStr
weight L1 is epsilon-transitive epsilon-connected ordinal cardinal set
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(S) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of S : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of S : verum } is set
{ (len b₁) where b₁ is open quasi_basis Element of K32(K32( the carrier of L1)) : verum } is set
f is set
B0 is open quasi_basis Element of K32(K32( the carrier of L1))
len B0 is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of S is non empty set
K32( the carrier of S) is non empty set
B2 is Element of K32( the carrier of S)
finsups B2 is non empty directed Element of K32( the carrier of S)
len (finsups B2) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
f is set
B0 is non empty directed join-closed with_bottom CLbasis of S
len B0 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty TopSpace-like T_0 TopStruct
the topology of L1 is non empty Element of K32(K32( the carrier of L1))
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset the topology of L1 is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete distributive with_suprema with_infima complete V204() RelStr
len the carrier of L1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
S is non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema satisfying_axiom_of_approximation continuous V204() RelStr
the carrier of S is non empty set
len the carrier of S is non empty epsilon-transitive epsilon-connected ordinal cardinal set
len the topology of L1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty TopSpace-like T_0 TopStruct
weight L1 is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of L1 is non empty set
len the carrier of L1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
K32( the carrier of L1) is non empty set
the topology of L1 is non empty Element of K32(K32( the carrier of L1))
K32(K32( the carrier of L1)) is non empty set
{ b₁ where b₁ is Element of the topology of L1 : a₁ in b₁ } is set
meet { b₁ where b₁ is Element of the topology of L1 : a₁ in b₁ } is set
BoolePoset the carrier of L1 is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete satisfying_axiom_K algebraic with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
the carrier of (BoolePoset the carrier of L1) is non empty set
S is set
{ b₁ where b₁ is Element of the topology of L1 : S in b₁ } is set
meet { b₁ where b₁ is Element of the topology of L1 : S in b₁ } is set
bool the carrier of L1 is non empty Element of K32(K32( the carrier of L1))
K33( the carrier of L1, the carrier of (BoolePoset the carrier of L1)) is non empty set
K32(K33( the carrier of L1, the carrier of (BoolePoset the carrier of L1))) is non empty set
S is Relation-like the carrier of L1 -defined the carrier of (BoolePoset the carrier of L1) -valued Function-like V29( the carrier of L1, the carrier of (BoolePoset the carrier of L1)) Element of K32(K33( the carrier of L1, the carrier of (BoolePoset the carrier of L1)))
rng S is Element of K32( the carrier of (BoolePoset the carrier of L1))
K32( the carrier of (BoolePoset the carrier of L1)) is non empty set
f is Element of K32(K32( the carrier of L1))
B0 is Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
{ b₁ where b₁ is Element of the topology of L1 : B2 in b₁ } is set
meet { b₁ where b₁ is Element of the topology of L1 : B2 in b₁ } is set
f is set
f is Element of K32( the carrier of L1)
dom S is Element of K32( the carrier of L1)
S . B2 is Element of the carrier of (BoolePoset the carrier of L1)
B2 is set
B2 is Element of the topology of L1
B2 is set
B2 is set
dom S is Element of K32( the carrier of L1)
f is set
S . f is set
{ b₁ where b₁ is Element of the topology of L1 : f in b₁ } is set
bool the carrier of L1 is non empty Element of K32(K32( the carrier of L1))
B2 is set
B2 is Element of the topology of L1
B2 is Element of K32(K32( the carrier of L1))
x is Element of K32( the carrier of L1)
B2 is Element of K32(K32( the carrier of L1))
y is Element of the topology of L1
B0 is non empty finite set
{ H₂(b₁) where b₁ is Element of B0 : S₁[b₁] } is set
meet B2 is Element of K32( the carrier of L1)
meet { b₁ where b₁ is Element of the topology of L1 : f in b₁ } is set
len (rng S) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is open quasi_basis Element of K32(K32( the carrier of L1)) : verum } is set
meet { (len b₁) where b₁ is open quasi_basis Element of K32(K32( the carrier of L1)) : verum } is set
B0 is set
dom S is Element of K32( the carrier of L1)
B2 is set
S . B0 is set
S . B2 is set
f is Element of the carrier of L1
B2 is Element of the carrier of L1
B2 is Element of K32( the carrier of L1)
S . f is Element of the carrier of (BoolePoset the carrier of L1)
{ b₁ where b₁ is Element of the topology of L1 : f in b₁ } is set
meet { b₁ where b₁ is Element of the topology of L1 : f in b₁ } is set
S . B2 is Element of the carrier of (BoolePoset the carrier of L1)
{ b₁ where b₁ is Element of the topology of L1 : B2 in b₁ } is set
meet { b₁ where b₁ is Element of the topology of L1 : B2 in b₁ } is set
x is set
x is set
y is Element of the topology of L1
x is set
x is set
y is Element of the topology of L1
B0 is set
B2 is open quasi_basis Element of K32(K32( the carrier of L1))
len B2 is epsilon-transitive epsilon-connected ordinal cardinal set
f is set
B2 is set
S . B2 is set
B2 is Element of the carrier of L1
{ b₁ where b₁ is Element of the topology of L1 : B2 in b₁ } is set
meet { b₁ where b₁ is Element of the topology of L1 : B2 in b₁ } is set
L1 is TopStruct
the topology of L1 is Element of K32(K32( the carrier of L1))
the carrier of L1 is set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset the topology of L1 is strict reflexive transitive antisymmetric RelStr
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(S) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of S : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of S : verum } is set
the carrier of S is non empty set
len the carrier of S is non empty epsilon-transitive epsilon-connected ordinal cardinal set
[#] S is non empty non proper directed filtered lower upper meet-closed join-closed infs-closed sups-closed with_bottom with_top Element of K32( the carrier of S)
K32( the carrier of S) is non empty set
f is set
f is set
B0 is non empty directed join-closed with_bottom CLbasis of S
len B0 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
Bottom S is Element of the carrier of S
"\/" ({},S) is Element of the carrier of S
CompactSublatt S is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema V204() SubRelStr of S
the carrier of (CompactSublatt S) is non empty set
len the carrier of (CompactSublatt S) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
the carrier of S is non empty set
K32( the carrier of S) is non empty set
K32(K32( the carrier of S)) is non empty set
f is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
the carrier of f is non empty set
K32( the carrier of f) is non empty set
K32(K32( the carrier of f)) is non empty set
B0 is open quasi_basis Element of K32(K32( the carrier of f))
{ (uparrow b₁) where b₁ is Element of K32( the carrier of f) : b₁ in B0 } is set
the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the carrier of L1 is non empty set
the InternalRel of L1 is non empty Relation-like the carrier of L1 -defined the carrier of L1 -valued Element of K32(K33( the carrier of L1, the carrier of L1))
K33( the carrier of L1, the carrier of L1) is non empty set
K32(K33( the carrier of L1, the carrier of L1)) is non empty set
RelStr(# the carrier of L1, the InternalRel of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the InternalRel of f is non empty Relation-like the carrier of f -defined the carrier of f -valued Element of K32(K33( the carrier of f, the carrier of f))
K33( the carrier of f, the carrier of f) is non empty set
K32(K33( the carrier of f, the carrier of f)) is non empty set
RelStr(# the carrier of f, the InternalRel of f #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
bool the carrier of S is non empty Element of K32(K32( the carrier of S))
B2 is set
f is Element of K32( the carrier of f)
uparrow f is upper Element of K32( the carrier of f)
B2 is Element of K32(K32( the carrier of S))
the topology of S is non empty Element of K32(K32( the carrier of S))
f is Element of K32(K32( the carrier of S))
UniCl f is Element of K32(K32( the carrier of S))
B2 is set
B2 is Element of K32( the carrier of S)
uparrow B2 is upper Element of K32( the carrier of S)
sigma S is non empty Element of K32(K32( the carrier of S))
sigma f is non empty Element of K32(K32( the carrier of f))
lambda f is non empty Element of K32(K32( the carrier of f))
the topology of f is non empty Element of K32(K32( the carrier of f))
x is Element of K32( the carrier of f)
{ (uparrow b₁) where b₁ is Element of K32( the carrier of f) : ( b₁ in B0 & b₁ c= x ) } is set
y is set
x1 is Element of K32( the carrier of f)
uparrow x1 is upper Element of K32( the carrier of f)
{ b₁ where b₁ is Element of K32( the carrier of f) : ( b₁ in B0 & b₁ c= x ) } is set
x1 is set
y1 is Element of K32( the carrier of f)
y is Element of K32(K32( the carrier of S))
x1 is Element of K32(K32( the carrier of S))
u is Element of K32(K32( the carrier of S))
y1 is Element of K32(K32( the carrier of S))
c₁₅ is set
y is Element of K32( the carrier of f)
uparrow y is upper Element of K32( the carrier of f)
{ b₁ where b₁ is Element of K32( the carrier of f) : S₁[b₁] } is set
{ (uparrow b₁) where b₁ is Element of K32( the carrier of f) : S₁[b₁] } is set
union { (uparrow b₁) where b₁ is Element of K32( the carrier of f) : S₁[b₁] } is set
union u is Element of K32( the carrier of S)
uparrow (union u) is upper Element of K32( the carrier of S)
b is Element of K32(K32( the carrier of f))
union b is Element of K32( the carrier of f)
uparrow (union b) is upper Element of K32( the carrier of f)
union y1 is Element of K32( the carrier of S)
B2 is set
B2 is Element of K32( the carrier of f)
uparrow B2 is upper Element of K32( the carrier of f)
the topology of f is non empty Element of K32(K32( the carrier of f))
lambda f is non empty Element of K32(K32( the carrier of f))
sigma S is non empty Element of K32(K32( the carrier of S))
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight S is epsilon-transitive epsilon-connected ordinal cardinal set
f is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight f is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of f is non empty set
K32( the carrier of f) is non empty set
K32(K32( the carrier of f)) is non empty set
B0 is open quasi_basis Element of K32(K32( the carrier of f))
len B0 is epsilon-transitive epsilon-connected ordinal cardinal set
B2 is set
f is Element of K32( the carrier of f)
uparrow f is upper Element of K32( the carrier of f)
B2 is Relation-like Function-like set
dom B2 is set
{ (uparrow b₁) where b₁ is Element of K32( the carrier of f) : b₁ in B0 } is set
rng B2 is set
f is set
B2 is Element of K32( the carrier of f)
uparrow B2 is upper Element of K32( the carrier of f)
B2 . B2 is set
B2 is Element of K32( the carrier of f)
uparrow B2 is upper Element of K32( the carrier of f)
len { (uparrow b₁) where b₁ is Element of K32( the carrier of f) : b₁ in B0 } is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of S is non empty set
K32( the carrier of S) is non empty set
K32(K32( the carrier of S)) is non empty set
{ (len b₁) where b₁ is open quasi_basis Element of K32(K32( the carrier of S)) : verum } is set
meet { (len b₁) where b₁ is open quasi_basis Element of K32(K32( the carrier of S)) : verum } is set
L1 is non empty reflexive transitive antisymmetric up-complete V204() RelStr
the carrier of L1 is non empty set
S is Element of the carrier of L1
compactbelow S is Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty set
{ b₁ where b₁ is Element of the carrier of L1 : ( b₁ <= S & b₁ is compact ) } is set
L1 is non empty finite reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete V204() RelStr
the carrier of L1 is non empty finite set
S is Element of the carrier of L1
compactbelow S is non empty finite directed Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty finite V36() set
{ b₁ where b₁ is Element of the carrier of L1 : ( b₁ <= S & b₁ is compact ) } is set
f is Element of the carrier of L1
compactbelow f is non empty finite directed Element of K32( the carrier of L1)
{ b₁ where b₁ is Element of the carrier of L1 : ( b₁ <= f & b₁ is compact ) } is set
CompactSublatt L1 is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema V204() SubRelStr of L1
S is Element of the carrier of L1
compactbelow S is non empty finite directed Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty finite V36() set
{ b₁ where b₁ is Element of the carrier of L1 : ( b₁ <= S & b₁ is compact ) } is set
"\/" ((compactbelow S),L1) is Element of the carrier of L1
f is Element of the carrier of L1
f is Element of the carrier of L1
S is Element of the carrier of L1
the carrier of (CompactSublatt L1) is non empty set
f is Element of the carrier of L1
{S,f} is non empty finite Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty finite V36() set
"/\" ({S,f},L1) is Element of the carrier of L1
S "/\" f is Element of the carrier of L1
L1 is non empty reflexive transitive antisymmetric with_suprema with_infima V204() RelStr
{{}} is non empty trivial finite V36() 1 -element set
K33({{}},{{}}) is non empty finite set
K32(K33({{}},{{}})) is non empty finite V36() set
[{},{}] is set
{{},{}} is non empty finite V36() set
{{{},{}},{{}}} is non empty finite V36() set
{[{},{}]} is non empty trivial finite 1 -element set
L1 is Relation-like {{}} -defined {{}} -valued finite Element of K32(K33({{}},{{}}))
RelStr(# {{}},L1 #) is non empty trivial finite 1 -element strict RelStr
S is non empty RelStr
the carrier of S is non empty set
f is Element of the carrier of S
[f,f] is Element of K33( the carrier of S, the carrier of S)
K33( the carrier of S, the carrier of S) is non empty set
{f,f} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,f},{f}} is non empty finite V36() set
f is non empty trivial finite 1 -element reflexive transitive antisymmetric lower-bounded upper-bounded V98() connected up-complete /\-complete satisfying_axiom_K algebraic arithmetic with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
B0 is non empty reflexive transitive antisymmetric with_suprema with_infima V204() RelStr
L1 is non empty finite reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete satisfying_axiom_K algebraic arithmetic with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
CompactSublatt L1 is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema V204() SubRelStr of L1
the carrier of (CompactSublatt L1) is non empty set
S is non empty finite directed join-closed with_bottom CLbasis of L1
card S is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of omega
len the carrier of (CompactSublatt L1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive V204() RelStr
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
f is Element of the carrier of L1
wayabove f is Element of K32( the carrier of L1)
S is Element of K32( the carrier of L1)
uparrow S is Element of K32( the carrier of L1)
(wayabove f) \ (uparrow S) is Element of K32( the carrier of L1)
L1 is non empty reflexive V204() RelStr
the carrier of L1 is non empty set
{} L1 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element FinSequence-membered directed filtered Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty set
S is Element of the carrier of L1
(L1,({} L1),S) is Element of K32( the carrier of L1)
wayabove S is Element of K32( the carrier of L1)
uparrow ({} L1) is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element FinSequence-membered directed filtered Element of K32( the carrier of L1)
(wayabove S) \ (uparrow ({} L1)) is Element of K32( the carrier of L1)
L1 is non empty reflexive transitive antisymmetric V204() RelStr
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
S is Element of K32( the carrier of L1)
uparrow S is upper Element of K32( the carrier of L1)
f is Element of the carrier of L1
(L1,S,f) is Element of K32( the carrier of L1)
wayabove f is upper Element of K32( the carrier of L1)
(wayabove f) \ (uparrow S) is Element of K32( the carrier of L1)
B0 is set
B2 is Element of the carrier of L1
L1 is non empty finite reflexive transitive V204() RelStr
Ids L1 is non empty set
the carrier of L1 is non empty finite set
bool the carrier of L1 is non empty finite V36() Element of K32(K32( the carrier of L1))
K32( the carrier of L1) is non empty finite V36() set
K32(K32( the carrier of L1)) is non empty finite V36() set
{ b₁ where b₁ is non empty finite directed lower Element of K32( the carrier of L1) : verum } is set
S is non empty finite set
{ b₁ where b₁ is Element of S : b₁ is non empty finite directed lower Element of K32( the carrier of L1) } is set
f is set
B0 is non empty finite directed lower Element of K32( the carrier of L1)
f is set
B0 is Element of S
{ H₁(b₁) where b₁ is Element of S : S₁[b₁] } is set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
S is non empty directed join-closed with_bottom CLbasis of L1
subrelstr S is non empty strict reflexive transitive antisymmetric lower-bounded full directed with_suprema V204() SubRelStr of L1
Ids (subrelstr S) is non empty set
InclPoset (Ids (subrelstr S)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete satisfying_axiom_K algebraic with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
the carrier of (InclPoset (Ids (subrelstr S))) is non empty set
supMap (subrelstr S) is Relation-like the carrier of (InclPoset (Ids (subrelstr S))) -defined the carrier of (InclPoset (Ids (subrelstr S))) -defined the carrier of L1 -valued Function-like V29( the carrier of (InclPoset (Ids (subrelstr S))), the carrier of L1) V29( the carrier of (InclPoset (Ids (subrelstr S))), the carrier of L1) infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving Element of K32(K33( the carrier of (InclPoset (Ids (subrelstr S))), the carrier of L1))
the carrier of L1 is non empty set
K33( the carrier of (InclPoset (Ids (subrelstr S))), the carrier of L1) is non empty set
K32(K33( the carrier of (InclPoset (Ids (subrelstr S))), the carrier of L1)) is non empty set
dom (supMap (subrelstr S)) is Element of K32( the carrier of (InclPoset (Ids (subrelstr S))))
K32( the carrier of (InclPoset (Ids (subrelstr S)))) is non empty set
rng (supMap (subrelstr S)) is Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty set
len the carrier of L1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
len (Ids (subrelstr S)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete V204() RelStr
the carrier of L1 is non empty set
S is Element of the carrier of L1
wayabove S is directed upper join-closed Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty set
"/\" ((wayabove S),L1) is Element of the carrier of L1
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
S is non empty directed join-closed with_bottom CLbasis of L1
{ (L1,b₂,b₁) where b₁ is Element of the carrier of L1, b₂ is finite Element of K32( the carrier of L1) : ( b₁ in S & b₂ c= S ) } is set
len { (L1,b₂,b₁) where b₁ is Element of the carrier of L1, b₂ is finite Element of K32( the carrier of L1) : ( b₁ in S & b₂ c= S ) } is epsilon-transitive epsilon-connected ordinal cardinal set
len S is non empty epsilon-transitive epsilon-connected ordinal cardinal set
f is set
{} L1 is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element FinSequence-membered directed filtered Element of K32( the carrier of L1)
B0 is Element of the carrier of L1
(L1,({} L1),B0) is Element of K32( the carrier of L1)
wayabove B0 is directed upper join-closed Element of K32( the carrier of L1)
uparrow ({} L1) is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element FinSequence-membered directed filtered upper Element of K32( the carrier of L1)
(wayabove B0) \ (uparrow ({} L1)) is Element of K32( the carrier of L1)
S * is non empty functional FinSequence-membered M10(S)
B2 is non empty set
f is Relation-like K100() -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S *
f /. 1 is Element of S
Del (f,1) is Relation-like K100() -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (Del (f,1)) is finite set
rng f is finite Element of K32(S)
K32(S) is non empty set
B2 is Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
(L1,B2,B2) is Element of K32( the carrier of L1)
wayabove B2 is directed upper join-closed Element of K32( the carrier of L1)
uparrow B2 is upper Element of K32( the carrier of L1)
(wayabove B2) \ (uparrow B2) is Element of K32( the carrier of L1)
x is Element of B2
K33((S *),B2) is non empty set
K32(K33((S *),B2)) is non empty set
f is Relation-like S * -defined B2 -valued Function-like V29(S * ,B2) Element of K32(K33((S *),B2))
dom f is functional FinSequence-membered Element of K32((S *))
K32((S *)) is non empty set
rng f is Element of K32(B2)
K32(B2) is non empty set
B2 is set
x is finite Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
(L1,x,B2) is Element of K32( the carrier of L1)
wayabove B2 is directed upper join-closed Element of K32( the carrier of L1)
uparrow x is upper Element of K32( the carrier of L1)
(wayabove B2) \ (uparrow x) is Element of K32( the carrier of L1)
x1 is Relation-like K100() -defined Function-like finite FinSequence-like FinSubsequence-like set
rng x1 is finite set
y is Element of S
<*y*> is non empty trivial Relation-like K100() -defined S -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of S
y1 is Relation-like K100() -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
<*y*> ^ y1 is non empty Relation-like K100() -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(<*y*> ^ y1) /. 1 is Element of S
Del ((<*y*> ^ y1),1) is Relation-like K100() -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (Del ((<*y*> ^ y1),1)) is finite set
f . (<*y*> ^ y1) is set
b is Element of the carrier of L1
c₁₅ is Element of K32( the carrier of L1)
(L1,c₁₅,b) is Element of K32( the carrier of L1)
wayabove b is directed upper join-closed Element of K32( the carrier of L1)
uparrow c₁₅ is upper Element of K32( the carrier of L1)
(wayabove b) \ (uparrow c₁₅) is Element of K32( the carrier of L1)
len (S *) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson V204() TopRelStr
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
S is finite Element of K32( the carrier of L1)
uparrow S is upper Element of K32( the carrier of L1)
(uparrow S) ` is Element of K32( the carrier of L1)
downarrow S is lower Element of K32( the carrier of L1)
(downarrow S) ` is Element of K32( the carrier of L1)
{ (uparrow b₁) where b₁ is Element of the carrier of L1 : b₁ in S } is set
bool the carrier of L1 is non empty Element of K32(K32( the carrier of L1))
K32(K32( the carrier of L1)) is non empty set
f is set
B0 is Element of the carrier of L1
uparrow B0 is non empty directed filtered upper meet-closed join-closed Element of K32( the carrier of L1)
{ (downarrow b₁) where b₁ is Element of the carrier of L1 : b₁ in S } is set
B0 is set
B2 is Element of the carrier of L1
downarrow B2 is non empty directed filtered lower meet-closed join-closed Element of K32( the carrier of L1)
B0 is Element of K32(K32( the carrier of L1))
f is Element of K32(K32( the carrier of L1))
f is Element of K32(K32( the carrier of L1))
union f is Element of K32( the carrier of L1)
B2 is Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
uparrow B2 is non empty directed filtered upper meet-closed join-closed Element of K32( the carrier of L1)
{ H₁(b₁) where b₁ is Element of the carrier of L1 : b₁ in S } is set
B2 is Element of K32(K32( the carrier of L1))
union B2 is Element of K32( the carrier of L1)
B2 is Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
downarrow B2 is non empty directed filtered lower meet-closed join-closed Element of K32( the carrier of L1)
{ H₂(b₁) where b₁ is Element of the carrier of L1 : b₁ in S } is set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
the carrier of S is non empty set
K32( the carrier of S) is non empty set
K32(K32( the carrier of S)) is non empty set
f is non empty directed join-closed with_bottom CLbasis of L1
{ (L1,b₂,b₁) where b₁ is Element of the carrier of L1, b₂ is finite Element of K32( the carrier of L1) : ( b₁ in f & b₂ c= f ) } is set
the InternalRel of L1 is non empty Relation-like the carrier of L1 -defined the carrier of L1 -valued Element of K32(K33( the carrier of L1, the carrier of L1))
K33( the carrier of L1, the carrier of L1) is non empty set
K32(K33( the carrier of L1, the carrier of L1)) is non empty set
RelStr(# the carrier of L1, the InternalRel of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
bool the carrier of S is non empty Element of K32(K32( the carrier of S))
B0 is set
f is finite Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
(L1,f,B2) is Element of K32( the carrier of L1)
wayabove B2 is directed upper join-closed Element of K32( the carrier of L1)
uparrow f is upper Element of K32( the carrier of L1)
(wayabove B2) \ (uparrow f) is Element of K32( the carrier of L1)
B0 is Element of K32(K32( the carrier of S))
sigma S is non empty Element of K32(K32( the carrier of S))
{ (b₁ \ (uparrow b₂)) where b₁, b₂ is Element of K32( the carrier of S) : ( b₁ in sigma S & b₂ is finite ) } is set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S
B2 is Element of K32( the carrier of S)
x is Element of the carrier of S
f is open quasi_basis Element of K32(K32( the carrier of S))
y is Element of K32( the carrier of S)
x1 is Element of K32( the carrier of S)
y1 is Element of K32( the carrier of S)
uparrow y1 is upper Element of K32( the carrier of S)
x1 \ (uparrow y1) is Element of K32( the carrier of S)
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S -valued Element of K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S))
K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S) is non empty set
K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S) is non empty set
sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S is non empty Element of K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S))
K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S)) is non empty set
b is Element of K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S)
{ (wayabove b₁) where b₁ is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S : b₁ in b } is set
union { (wayabove b₁) where b₁ is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S : b₁ in b } is set
u is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S
c₁₅ is Element of the carrier of L1
Bottom L1 is Element of the carrier of L1
"\/" ({},L1) is Element of the carrier of L1
y is set
xS is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S
wayabove xS is directed upper join-closed Element of K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of S)
xL is Element of the carrier of L1
bL is Element of the carrier of L1
FL is Element of K32( the carrier of L1)
uparrow FL is upper Element of K32( the carrier of L1)
f is set
FFL is Element of the carrier of L1
cT is Element of the carrier of L1
cT is set
f is Relation-like Function-like set
dom f is set
rng f is set
FFL is set
cT is set
f . cT is set
z is Element of the carrier of L1
cT is Element of the carrier of L1
FFL is Element of K32( the carrier of L1)
cT is set
cT is set
f . cT is set
v is Element of the carrier of L1
z is Element of the carrier of L1
uparrow FFL is upper Element of K32( the carrier of L1)
cT is set
cT is Element of the carrier of L1
z is Element of the carrier of L1
f . z is set
y1 is Element of the carrier of L1
v is Element of the carrier of L1
wayabove bL is directed upper join-closed Element of K32( the carrier of L1)
(wayabove bL) \ (uparrow FFL) is Element of K32( the carrier of L1)
cT is Element of K32( the carrier of S)
cT is Element of K32( the carrier of S)
(L1,FFL,bL) is Element of K32( the carrier of L1)
B2 is Element of K32(K32( the carrier of S))
wayabove xL is directed upper join-closed Element of K32( the carrier of L1)
(wayabove xL) \ (uparrow FL) is Element of K32( the carrier of L1)
z is Element of the carrier of L1
v is set
f . v is set
c₂₈ is Element of the carrier of L1
y1 is Element of the carrier of L1
z is Element of the carrier of L1
z is set
the topology of S is non empty Element of K32(K32( the carrier of S))
f is set
B2 is finite Element of K32( the carrier of L1)
B2 is Element of the carrier of L1
(L1,B2,B2) is Element of K32( the carrier of L1)
wayabove B2 is directed upper join-closed Element of K32( the carrier of L1)
uparrow B2 is upper Element of K32( the carrier of L1)
(wayabove B2) \ (uparrow B2) is Element of K32( the carrier of L1)
y is Element of the carrier of S
wayabove y is directed upper join-closed Element of K32( the carrier of S)
x is finite Element of K32( the carrier of S)
uparrow x is upper Element of K32( the carrier of S)
(uparrow x) ` is Element of K32( the carrier of S)
(wayabove y) /\ ((uparrow x) `) is Element of K32( the carrier of S)
(wayabove y) \ (uparrow B2) is Element of K32( the carrier of S)
(wayabove y) \ (uparrow x) is Element of K32( the carrier of S)
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight S is epsilon-transitive epsilon-connected ordinal cardinal set
f is non empty directed join-closed with_bottom CLbasis of L1
len f is non empty epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of S is non empty set
the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the carrier of L1 is non empty set
the InternalRel of L1 is non empty Relation-like the carrier of L1 -defined the carrier of L1 -valued Element of K32(K33( the carrier of L1, the carrier of L1))
K33( the carrier of L1, the carrier of L1) is non empty set
K32(K33( the carrier of L1, the carrier of L1)) is non empty set
RelStr(# the carrier of L1, the InternalRel of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
CompactSublatt L1 is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema V204() SubRelStr of L1
the carrier of (CompactSublatt L1) is non empty set
K32( the carrier of L1) is non empty set
{ (L1,b₂,b₁) where b₁ is Element of the carrier of L1, b₂ is finite Element of K32( the carrier of L1) : ( b₁ in f & b₂ c= f ) } is set
K32( the carrier of S) is non empty set
K32(K32( the carrier of S)) is non empty set
len { (L1,b₂,b₁) where b₁ is Element of the carrier of L1, b₂ is finite Element of K32( the carrier of L1) : ( b₁ in f & b₂ c= f ) } is epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
the carrier of S is non empty set
K32( the carrier of S) is non empty set
K32(K32( the carrier of S)) is non empty set
f is open quasi_basis Element of K32(K32( the carrier of S))
{ (wayabove ("/\" (b₁,S))) where b₁ is Element of K32( the carrier of S) : b₁ in f } is set
bool the carrier of S is non empty Element of K32(K32( the carrier of S))
B2 is set
f is Element of K32( the carrier of S)
"/\" (f,S) is Element of the carrier of S
wayabove ("/\" (f,S)) is directed upper join-closed Element of K32( the carrier of S)
{ (wayabove b₁) where b₁ is Element of the carrier of S : verum } is set
B2 is Element of K32( the carrier of S)
B2 is Element of the carrier of S
f is open quasi_basis Element of K32(K32( the carrier of S))
x is Element of K32( the carrier of S)
y is Element of K32( the carrier of S)
x1 is Element of K32( the carrier of S)
y1 is Element of the carrier of S
wayabove y1 is directed upper join-closed Element of K32( the carrier of S)
"/\" (y,S) is Element of the carrier of S
wayabove ("/\" (y,S)) is directed upper join-closed Element of K32( the carrier of S)
u is directed upper join-closed Element of K32( the carrier of S)
B2 is Element of K32(K32( the carrier of S))
c₁₅ is Element of the carrier of S
wayabove c₁₅ is directed upper join-closed Element of K32( the carrier of S)
b is Element of the carrier of S
y is Element of the carrier of S
uparrow c₁₅ is non empty directed filtered upper meet-closed join-closed Element of K32( the carrier of S)
"/\" ((uparrow c₁₅),S) is Element of the carrier of S
the topology of S is non empty Element of K32(K32( the carrier of S))
B2 is set
B2 is Element of K32( the carrier of S)
"/\" (B2,S) is Element of the carrier of S
wayabove ("/\" (B2,S)) is directed upper join-closed Element of K32( the carrier of S)
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
the carrier of S is non empty set
K32( the carrier of S) is non empty set
K32(K32( the carrier of S)) is non empty set
f is open quasi_basis Element of K32(K32( the carrier of S))
{ ("/\" (b₁,S)) where b₁ is Element of K32( the carrier of S) : b₁ in f } is set
{ (wayabove ("/\" (b₁,S))) where b₁ is Element of K32( the carrier of S) : b₁ in f } is set
B0 is set
B2 is open quasi_basis Element of K32(K32( the carrier of S))
f is set
B2 is Element of K32( the carrier of S)
"/\" (B2,S) is Element of the carrier of S
B2 is Element of the carrier of S
wayabove B2 is directed upper join-closed Element of K32( the carrier of S)
B2 is directed upper join-closed Element of K32( the carrier of S)
x is Element of K32( the carrier of S)
"/\" (x,S) is Element of the carrier of S
f is Relation-like Function-like set
dom f is set
rng f is set
B2 is set
B2 is Element of K32( the carrier of S)
"/\" (B2,S) is Element of the carrier of S
wayabove ("/\" (B2,S)) is directed upper join-closed Element of K32( the carrier of S)
f . ("/\" (B2,S)) is set
x is Element of the carrier of S
wayabove x is directed upper join-closed Element of K32( the carrier of S)
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight S is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of S is non empty set
K32( the carrier of S) is non empty set
K32(K32( the carrier of S)) is non empty set
f is open quasi_basis Element of K32(K32( the carrier of S))
len f is epsilon-transitive epsilon-connected ordinal cardinal set
{ ("/\" (b₁,S)) where b₁ is Element of K32( the carrier of S) : b₁ in f } is set
B0 is set
B2 is Element of K32( the carrier of S)
"/\" (B2,S) is Element of the carrier of S
B0 is Element of K32( the carrier of S)
finsups B0 is non empty directed Element of K32( the carrier of S)
f is set
B2 is Element of K32( the carrier of S)
"/\" (B2,S) is Element of the carrier of S
B2 is Element of the carrier of S
f is Relation-like Function-like set
dom f is set
rng f is set
B2 is set
B2 is Element of K32( the carrier of S)
"/\" (B2,S) is Element of the carrier of S
f . B2 is set
x is Element of K32( the carrier of S)
"/\" (x,S) is Element of the carrier of S
len B0 is epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of L1 is non empty set
the InternalRel of L1 is non empty Relation-like the carrier of L1 -defined the carrier of L1 -valued Element of K32(K33( the carrier of L1, the carrier of L1))
K33( the carrier of L1, the carrier of L1) is non empty set
K32(K33( the carrier of L1, the carrier of L1)) is non empty set
RelStr(# the carrier of L1, the InternalRel of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
B2 is set
B2 is Element of the carrier of S
uparrow B2 is non empty directed filtered upper meet-closed join-closed Element of K32( the carrier of S)
x is Element of K32( the carrier of S)
"/\" ((uparrow B2),S) is Element of the carrier of S
"/\" (x,S) is Element of the carrier of S
len (finsups B0) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
len (finsups B0) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
len (finsups B0) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
len (finsups B0) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
K32(B0) is non empty set
"\/" ({},S) is Element of the carrier of S
{ ("\/" (b₁,S)) where b₁ is finite Element of K32(B0) : ex_sup_of b₁,S } is set
Bottom L1 is Element of the carrier of L1
"\/" ({},L1) is Element of the carrier of L1
K32( the carrier of L1) is non empty set
B2 is Element of the carrier of L1
B2 is Element of K32( the carrier of L1)
x is Element of the carrier of L1
y is finite Element of K32(B0)
"\/" (y,S) is Element of the carrier of S
x1 is finite Element of K32(B0)
"\/" (x1,S) is Element of the carrier of S
x1 \/ y is finite Element of K32(B0)
{B2,x} is non empty finite Element of K32( the carrier of L1)
"\/" ({B2,x},L1) is Element of the carrier of L1
B2 "\/" x is Element of the carrier of L1
("\/" (x1,S)) "\/" ("\/" (y,S)) is Element of the carrier of S
"\/" ((x1 \/ y),S) is Element of the carrier of S
B2 is directed join-closed Element of K32( the carrier of L1)
x is Element of the carrier of L1
y is Element of the carrier of L1
wayabove x is directed upper join-closed Element of K32( the carrier of L1)
y1 is Element of the carrier of S
x1 is Element of the carrier of S
wayabove x1 is directed upper join-closed Element of K32( the carrier of S)
u is Element of K32( the carrier of S)
"/\" (u,S) is Element of the carrier of S
b is Element of the carrier of L1
uparrow x1 is non empty directed filtered upper meet-closed join-closed Element of K32( the carrier of S)
"/\" ((uparrow x1),S) is Element of the carrier of S
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight S is epsilon-transitive epsilon-connected ordinal cardinal set
the non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight the non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
S is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete Lawson satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight S is epsilon-transitive epsilon-connected ordinal cardinal set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty RelStr
S is non empty RelStr
the carrier of L1 is non empty set
len the carrier of L1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of S is non empty set
len the carrier of S is non empty epsilon-transitive epsilon-connected ordinal cardinal set
K33( the carrier of L1, the carrier of S) is non empty set
K32(K33( the carrier of L1, the carrier of S)) is non empty set
f is Relation-like the carrier of L1 -defined the carrier of S -valued Function-like V29( the carrier of L1, the carrier of S) Element of K32(K33( the carrier of L1, the carrier of S))
dom f is Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty set
rng f is Element of K32( the carrier of S)
K32( the carrier of S) is non empty set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
S is non empty directed join-closed with_bottom CLbasis of L1
len S is non empty epsilon-transitive epsilon-connected ordinal cardinal set
subrelstr S is non empty strict reflexive transitive antisymmetric lower-bounded full directed with_suprema V204() SubRelStr of L1
Ids (subrelstr S) is non empty set
InclPoset (Ids (subrelstr S)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete satisfying_axiom_K algebraic with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
((InclPoset (Ids (subrelstr S)))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of InclPoset (Ids (subrelstr S)) : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of InclPoset (Ids (subrelstr S)) : verum } is set
CompactSublatt (InclPoset (Ids (subrelstr S))) is non empty strict reflexive transitive antisymmetric full join-inheriting with_suprema V204() SubRelStr of InclPoset (Ids (subrelstr S))
the carrier of (CompactSublatt (InclPoset (Ids (subrelstr S)))) is non empty set
len the carrier of (CompactSublatt (InclPoset (Ids (subrelstr S)))) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of (subrelstr S) is non empty set
len the carrier of (subrelstr S) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
sigma L1 is non empty Element of K32(K32( the carrier of L1))
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset (sigma L1) is non empty strict reflexive transitive antisymmetric V204() RelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 -valued Element of K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1))
K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1) is non empty set
K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the InternalRel of L1 is non empty Relation-like the carrier of L1 -defined the carrier of L1 -valued Element of K32(K33( the carrier of L1, the carrier of L1))
K33( the carrier of L1, the carrier of L1) is non empty set
K32(K33( the carrier of L1, the carrier of L1)) is non empty set
RelStr(# the carrier of L1, the InternalRel of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty Element of K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1))
K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1) is non empty set
K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1)) is non empty set
InclPoset (sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1) is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete V204() RelStr
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
sigma L1 is non empty Element of K32(K32( the carrier of L1))
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset (sigma L1) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema satisfying_axiom_of_approximation continuous V204() RelStr
((InclPoset (sigma L1))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of InclPoset (sigma L1) : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of InclPoset (sigma L1) : verum } is set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 -valued Element of K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1))
K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1) is non empty set
K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the InternalRel of L1 is non empty Relation-like the carrier of L1 -defined the carrier of L1 -valued Element of K32(K33( the carrier of L1, the carrier of L1))
K33( the carrier of L1, the carrier of L1) is non empty set
K32(K33( the carrier of L1, the carrier of L1)) is non empty set
RelStr(# the carrier of L1, the InternalRel of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty Element of K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1))
K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1) is non empty set
K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1)) is non empty set
InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete distributive with_suprema with_infima complete V204() RelStr
weight the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is epsilon-transitive epsilon-connected ordinal cardinal set
len the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of (InclPoset (sigma L1)) is non empty set
len the carrier of (InclPoset (sigma L1)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
L1 is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() RelStr
(L1) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
sigma L1 is non empty Element of K32(K32( the carrier of L1))
the carrier of L1 is non empty set
K32( the carrier of L1) is non empty set
K32(K32( the carrier of L1)) is non empty set
InclPoset (sigma L1) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema satisfying_axiom_of_approximation continuous V204() RelStr
((InclPoset (sigma L1))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of InclPoset (sigma L1) : verum } is set
meet { (len b₁) where b₁ is non empty directed join-closed with_bottom CLbasis of InclPoset (sigma L1) : verum } is set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1
weight the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is epsilon-transitive epsilon-connected ordinal cardinal set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty Element of K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1))
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty set
K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1) is non empty set
K32(K32( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1)) is non empty set
InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete distributive with_suprema with_infima complete V204() RelStr
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 -valued Element of K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1))
K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1) is non empty set
K32(K33( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete Scott with_suprema with_infima complete satisfying_axiom_of_approximation continuous V204() V206() TopAugmentation of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr
the InternalRel of L1 is non empty Relation-like the carrier of L1 -defined the carrier of L1 -valued Element of K32(K33( the carrier of L1, the carrier of L1))
K33( the carrier of L1, the carrier of L1) is non empty set
K32(K33( the carrier of L1, the carrier of L1)) is non empty set
RelStr(# the carrier of L1, the InternalRel of L1 #) is non empty strict reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima V204() RelStr