:: WAYBEL31 semantic presentation

K96() is set

K32(K96()) is non empty set

K32(omega) is non empty non trivial non finite set
K32(K100()) is non empty non trivial non finite set

F1() is RelStr
the carrier of F1() is set
K32( the carrier of F1()) is non empty set
K32(K32( the carrier of F1())) is non empty set
{ b1 where b1 is Element of K32( the carrier of F1()) : P1[b1] } is set
{ (uparrow b1) where b1 is Element of K32( the carrier of F1()) : P1[b1] } is set
union { (uparrow b1) where b1 is Element of K32( the carrier of F1()) : P1[b1] } is set
L1 is Element of K32(K32( the carrier of F1()))
union L1 is Element of K32( the carrier of F1())
uparrow (union L1) is Element of K32( the carrier of F1())
S is set
f is set
B0 is Element of K32( the carrier of F1())
uparrow B0 is Element of K32( the carrier of F1())
B2 is Element of the carrier of F1()
f is Element of the carrier of F1()
S is set
f is Element of the carrier of F1()
B0 is Element of the carrier of F1()
B2 is set
f is Element of K32( the carrier of F1())
uparrow f is Element of K32( the carrier of F1())
F1() is RelStr
the carrier of F1() is set
K32( the carrier of F1()) is non empty set
K32(K32( the carrier of F1())) is non empty set
{ b1 where b1 is Element of K32( the carrier of F1()) : P1[b1] } is set
{ () where b1 is Element of K32( the carrier of F1()) : P1[b1] } is set
union { () where b1 is Element of K32( the carrier of F1()) : P1[b1] } is set
L1 is Element of K32(K32( the carrier of F1()))
union L1 is Element of K32( the carrier of F1())
downarrow (union L1) is Element of K32( the carrier of F1())
S is set
f is set
B0 is Element of K32( the carrier of F1())
downarrow B0 is Element of K32( the carrier of F1())
B2 is Element of the carrier of F1()
f is Element of the carrier of F1()
S is set
f is Element of the carrier of F1()
B0 is Element of the carrier of F1()
B2 is set
f is Element of K32( the carrier of F1())
downarrow f is Element of K32( the carrier of F1())

S is non empty directed join-closed with_bottom CLbasis of L1

Ids () is non empty set

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set

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

B2 is non empty directed join-closed with_bottom CLbasis of L1

B2 is set

f is set
B2 is non empty directed join-closed with_bottom CLbasis of L1

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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 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 b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set

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

B0 is non empty directed join-closed with_bottom CLbasis of L1

B2 is set
f is set
B2 is non empty directed join-closed with_bottom CLbasis of L1

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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set

the carrier of () is non empty set

f is set
B0 is non empty directed join-closed with_bottom CLbasis of L1

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

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
() /\ f is Element of K32( the carrier of S)
"\/" ((() /\ f),S) is Element of the carrier of S
union (() /\ 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

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
{ ("\/" (b1,S)) where b1 is finite Element of K32(B0) : ex_sup_of b1,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
{ ("\/" (b1,S)) where b1 is finite Element of K32(B0) : ex_sup_of b1,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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of S : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of S : verum } is set
{ (len b1) where b1 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))

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)

f is set
B0 is non empty directed join-closed with_bottom CLbasis 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

the carrier of S is non empty set

L1 is non empty TopSpace-like T_0 TopStruct

the carrier of L1 is non empty 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
{ b1 where b1 is Element of the topology of L1 : a1 in b1 } is set
meet { b1 where b1 is Element of the topology of L1 : a1 in b1 } is set

the carrier of (BoolePoset the carrier of L1) is non empty set
S is set
{ b1 where b1 is Element of the topology of L1 : S in b1 } is set
meet { b1 where b1 is Element of the topology of L1 : S in b1 } 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
{ b1 where b1 is Element of the topology of L1 : B2 in b1 } is set
meet { b1 where b1 is Element of the topology of L1 : B2 in b1 } 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
{ b1 where b1 is Element of the topology of L1 : f in b1 } 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
{ H2(b1) where b1 is Element of B0 : S1[b1] } is set
meet B2 is Element of K32( the carrier of L1)
meet { b1 where b1 is Element of the topology of L1 : f in b1 } is set

{ (len b1) where b1 is open quasi_basis Element of K32(K32( the carrier of L1)) : verum } is set
meet { (len b1) where b1 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)
{ b1 where b1 is Element of the topology of L1 : f in b1 } is set
meet { b1 where b1 is Element of the topology of L1 : f in b1 } is set
S . B2 is Element of the carrier of (BoolePoset the carrier of L1)
{ b1 where b1 is Element of the topology of L1 : B2 in b1 } is set
meet { b1 where b1 is Element of the topology of L1 : B2 in b1 } 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))

f is set
B2 is set
S . B2 is set
B2 is Element of the carrier of L1
{ b1 where b1 is Element of the topology of L1 : B2 in b1 } is set
meet { b1 where b1 is Element of the topology of L1 : B2 in b1 } 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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of S : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of S : verum } is set
the carrier of S is non empty set

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

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

the carrier of () is non empty 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

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 b1) where b1 is Element of K32( the carrier of f) : b1 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 b1) where b1 is Element of K32( the carrier of f) : ( b1 in B0 & b1 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)
{ b1 where b1 is Element of K32( the carrier of f) : ( b1 in B0 & b1 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))
c15 is set
y is Element of K32( the carrier of f)
uparrow y is upper Element of K32( the carrier of f)
{ b1 where b1 is Element of K32( the carrier of f) : S1[b1] } is set
{ (uparrow b1) where b1 is Element of K32( the carrier of f) : S1[b1] } is set
union { (uparrow b1) where b1 is Element of K32( the carrier of f) : S1[b1] } is set
union u is Element of K32( the carrier of S)
uparrow () 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 () 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))

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

B2 is set
f is Element of K32( the carrier of f)
uparrow f is upper Element of K32( the carrier of f)

dom B2 is set
{ (uparrow b1) where b1 is Element of K32( the carrier of f) : b1 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 b1) where b1 is Element of K32( the carrier of f) : b1 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 b1) where b1 is open quasi_basis Element of K32(K32( the carrier of S)) : verum } is set
meet { (len b1) where b1 is open quasi_basis Element of K32(K32( the carrier of S)) : verum } is set

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
{ b1 where b1 is Element of the carrier of L1 : ( b1 <= S & b1 is compact ) } is set

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
{ b1 where b1 is Element of the carrier of L1 : ( b1 <= S & b1 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)
{ b1 where b1 is Element of the carrier of L1 : ( b1 <= f & b1 is compact ) } is 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
{ b1 where b1 is Element of the carrier of L1 : ( b1 <= S & b1 is compact ) } is set
"\/" ((),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 () 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

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

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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set

the carrier of () is non empty set
S is non empty finite directed join-closed with_bottom CLbasis of L1

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)
() \ () is Element of K32( the carrier of L1)
L1 is non empty reflexive V204() RelStr
the carrier of L1 is non empty set

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 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)
() \ () 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
{ b1 where b1 is non empty finite directed lower Element of K32( the carrier of L1) : verum } is set
S is non empty finite set
{ b1 where b1 is Element of S : b1 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
{ H1(b1) where b1 is Element of S : S1[b1] } is set

S is non empty directed join-closed with_bottom CLbasis of L1

Ids () is non empty set

the carrier of (InclPoset (Ids ())) is non empty set
supMap () is Relation-like the carrier of (InclPoset (Ids ())) -defined the carrier of (InclPoset (Ids ())) -defined the carrier of L1 -valued Function-like V29( the carrier of (InclPoset (Ids ())), the carrier of L1) V29( the carrier of (InclPoset (Ids ())), 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 ())), the carrier of L1))
the carrier of L1 is non empty set
K33( the carrier of (InclPoset (Ids ())), the carrier of L1) is non empty set
K32(K33( the carrier of (InclPoset (Ids ())), the carrier of L1)) is non empty set
dom (supMap ()) is Element of K32( the carrier of (InclPoset (Ids ())))
K32( the carrier of (InclPoset (Ids ()))) is non empty set
rng (supMap ()) is Element of K32( the carrier of L1)
K32( the carrier of L1) is non empty set

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
"/\" ((),L1) is Element of the carrier of L1

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,b2,b1) where b1 is Element of the carrier of L1, b2 is finite Element of K32( the carrier of L1) : ( b1 in S & b2 c= S ) } is set
len { (L1,b2,b1) where b1 is Element of the carrier of L1, b2 is finite Element of K32( the carrier of L1) : ( b1 in S & b2 c= S ) } is epsilon-transitive epsilon-connected ordinal cardinal set

f is set

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)

(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 /. 1 is Element of S

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) \ () is Element of K32( the carrier of L1)

rng x1 is finite set
y is Element of S

(<*y*> ^ y1) /. 1 is Element of S

rng (Del ((<*y*> ^ y1),1)) is finite set
f . (<*y*> ^ y1) is set
b is Element of the carrier of L1
c15 is Element of K32( the carrier of L1)
(L1,c15,b) is Element of K32( the carrier of L1)
wayabove b is directed upper join-closed Element of K32( the carrier of L1)
uparrow c15 is upper Element of K32( the carrier of L1)
() \ (uparrow c15) is Element of K32( the carrier of L1)

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)
() ` is Element of K32( the carrier of L1)
downarrow S is lower Element of K32( the carrier of L1)
() ` is Element of K32( the carrier of L1)
{ (uparrow b1) where b1 is Element of the carrier of L1 : b1 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)
{ () where b1 is Element of the carrier of L1 : b1 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)
{ H1(b1) where b1 is Element of the carrier of L1 : b1 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)
{ H2(b1) where b1 is Element of the carrier of L1 : b1 in S } is set

the carrier of L1 is non empty set
K32( the carrier of L1) is non empty 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 non empty directed join-closed with_bottom CLbasis of L1
{ (L1,b2,b1) where b1 is Element of the carrier of L1, b2 is finite Element of K32( the carrier of L1) : ( b1 in f & b2 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) \ () 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))
{ (b1 \ (uparrow b2)) where b1, b2 is Element of K32( the carrier of S) : ( b1 in sigma S & b2 is finite ) } is set

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)

{ } is set
union { } is set

c15 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

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

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
c28 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)
() ` is Element of K32( the carrier of S)
() /\ (() `) is Element of K32( the carrier of S)
() \ (uparrow B2) is Element of K32( the carrier of S)
() \ () is Element of K32( the carrier of S)

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set

f is non empty directed join-closed with_bottom CLbasis of L1

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

the carrier of () is non empty set
K32( the carrier of L1) is non empty set
{ (L1,b2,b1) where b1 is Element of the carrier of L1, b2 is finite Element of K32( the carrier of L1) : ( b1 in f & b2 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,b2,b1) where b1 is Element of the carrier of L1, b2 is finite Element of K32( the carrier of L1) : ( b1 in f & b2 c= f ) } 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))
{ (wayabove ("/\" (b1,S))) where b1 is Element of K32( the carrier of S) : b1 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 b1) where b1 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))
c15 is Element of the carrier of S
wayabove c15 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 c15 is non empty directed filtered upper meet-closed join-closed Element of K32( the carrier of S)
"/\" ((uparrow c15),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)

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))
{ ("/\" (b1,S)) where b1 is Element of K32( the carrier of S) : b1 in f } is set
{ (wayabove ("/\" (b1,S))) where b1 is Element of K32( the carrier of S) : b1 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

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)

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is 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))

{ ("/\" (b1,S)) where b1 is Element of K32( the carrier of S) : b1 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

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

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

K32(B0) is non empty set
"\/" ({},S) is Element of the carrier of S
{ ("\/" (b1,S)) where b1 is finite Element of K32(B0) : ex_sup_of b1,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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set

L1 is non empty RelStr
S is non empty RelStr
the carrier of L1 is non empty set

the carrier of S is non empty 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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 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

Ids () is non empty set

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of InclPoset (Ids ()) : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of InclPoset (Ids ()) : verum } is set

the carrier of (CompactSublatt (InclPoset (Ids ()))) is non empty set
len the carrier of (CompactSublatt (InclPoset (Ids ()))) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of () is non empty 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

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

InclPoset () is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V98() up-complete /\-complete with_suprema with_infima complete V204() RelStr

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of L1 : verum } is set
meet { (len b1) where b1 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

{ (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of InclPoset (sigma L1) : verum } is set
meet { (len b1) where b1 is non empty directed join-closed with_bottom CLbasis of InclPoset (sigma L1) : verum } 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