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

the carrier of F

K32( the carrier of F

K32(K32( the carrier of F

{ b

{ (uparrow b

union { (uparrow b

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

the carrier of F

K32( the carrier of F

K32(K32( the carrier of F

{ b

{ (downarrow b

union { (downarrow b

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

meet { (len b

[#] 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

meet { (len b

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

meet { (len b

[#] 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

meet { (len b

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

B2 is Element of the carrier of S

f is Element of the carrier of S

K32(B0) is non empty set

{ ("\/" (b

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

meet { (len b

{ (len b

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

meet { b

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

meet { b

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

meet { b

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

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

meet B2 is Element of K32( the carrier of L1)

meet { b

len (rng S) is epsilon-transitive epsilon-connected ordinal cardinal set

{ (len b

meet { (len b

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

meet { b

S . B2 is Element of the carrier of (BoolePoset the carrier of L1)

{ b

meet { b

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

meet { b

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

meet { (len b

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

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

y is set

x1 is Element of K32( the carrier of f)

uparrow x1 is upper Element of K32( the carrier of f)

{ b

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

y is Element of K32( the carrier of f)

uparrow y is upper Element of K32( the carrier of f)

{ b

{ (uparrow b

union { (uparrow b

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

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

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

meet { (len b

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

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

f is Element of the carrier of L1

compactbelow f is non empty finite directed Element of K32( the carrier of L1)

{ b

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

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

meet { (len b

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

S is non empty finite set

{ b

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

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

len { (L1,b

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

(L1,c

wayabove b is directed upper join-closed Element of K32( the carrier of L1)

uparrow c

(wayabove b) \ (uparrow c

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

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

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

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

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

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

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

union { (wayabove b

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

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

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

meet { (len b

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

K32( the carrier of S) is non empty set

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

len { (L1,b

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

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

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

wayabove c

b is Element of the carrier of S

y is Element of the carrier of S

uparrow c

"/\" ((uparrow c

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

{ (wayabove ("/\" (b

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

meet { (len b

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

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

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

meet { (len b

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

meet { (len b

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

meet { (len b

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

meet { (len b

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

meet { (len b

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

meet { (len b

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