:: LOPCLSET semantic presentation

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V31() V35() finite finite-yielding V40() cardinal {} -element set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V31() V35() finite finite-yielding V40() cardinal {} -element set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V31() V35() finite finite-yielding V40() cardinal {} -element set

K116() is non trivial V31() non finite cardinal limit_cardinal set

K19(K116()) is non empty non trivial cup-closed diff-closed preBoolean non finite set

1 is non empty set

union {} is finite set

BL is non empty TopStruct

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

{ b

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

bool the carrier of BL is non empty cup-closed diff-closed preBoolean Element of K19(K19( the carrier of BL))

c

f is Element of K19( the carrier of BL)

BL is non empty TopSpace-like TopStruct

(BL) is Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

{} BL is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper V31() V35() finite finite-yielding V40() cardinal {} -element open closed Element of K19( the carrier of BL)

BL is non empty TopSpace-like TopStruct

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

T is Element of K19( the carrier of BL)

c

BL is non empty TopSpace-like TopStruct

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

T is Element of K19( the carrier of BL)

c

BL is non empty TopSpace-like TopStruct

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

T is Element of K19( the carrier of BL)

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

BL is non empty TopSpace-like TopStruct

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

T is Element of (BL)

c

T \/ c

f is Element of K19( the carrier of BL)

p is Element of K19( the carrier of BL)

f \/ p is Element of K19( the carrier of BL)

T \/ c

T /\ c

f is Element of K19( the carrier of BL)

p is Element of K19( the carrier of BL)

f /\ p is Element of K19( the carrier of BL)

T /\ c

BL is non empty TopSpace-like TopStruct

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

T is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

c

f is Element of (BL)

T . (c

[c

{c

{c

{{c

T . [c

(BL,c

T is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

c

f is Element of (BL)

T . (c

[c

{c

{c

{{c

T . [c

(BL,c

BL is non empty TopSpace-like TopStruct

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of LattStr(# (BL),(BL),(BL) #) is non empty set

T is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

f is Element of (BL)

c

p is Element of (BL)

T "\/" c

the L_join of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_join of LattStr(# (BL),(BL),(BL) #) . (T,c

[T,c

{T,c

{T} is non empty trivial finite 1 -element set

{{T,c

the L_join of LattStr(# (BL),(BL),(BL) #) . [T,c

(BL,f,p) is Element of (BL)

BL is non empty TopSpace-like TopStruct

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of LattStr(# (BL),(BL),(BL) #) is non empty set

T is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

f is Element of (BL)

c

p is Element of (BL)

T "/\" c

the L_meet of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_meet of LattStr(# (BL),(BL),(BL) #) . (T,c

[T,c

{T,c

{T} is non empty trivial finite 1 -element set

{{T,c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [T,c

(BL,f,p) is Element of (BL)

BL is non empty TopSpace-like TopStruct

{} BL is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper V31() V35() finite finite-yielding V40() cardinal {} -element open closed Element of K19( the carrier of BL)

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

BL is non empty TopSpace-like TopStruct

[#] BL is non empty non proper open closed Element of K19( the carrier of BL)

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

BL is non empty TopSpace-like TopStruct

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

T is Element of (BL)

T ` is Element of K19( the carrier of BL)

the carrier of BL \ T is set

c

BL is non empty TopSpace-like TopStruct

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of LattStr(# (BL),(BL),(BL) #) is non empty set

c

f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

c

the L_join of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_join of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{c

{{c

the L_join of LattStr(# (BL),(BL),(BL) #) . [c

f "\/" c

the L_join of LattStr(# (BL),(BL),(BL) #) . (f,c

[f,c

{f,c

{f} is non empty trivial finite 1 -element set

{{f,c

the L_join of LattStr(# (BL),(BL),(BL) #) . [f,c

p is Element of (BL)

q is Element of (BL)

(BL,q,p) is Element of (BL)

c

f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

p is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

f "\/" p is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

the L_join of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_join of LattStr(# (BL),(BL),(BL) #) . (f,p) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

[f,p] is set

{f,p} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,p},{f}} is non empty finite V40() set

the L_join of LattStr(# (BL),(BL),(BL) #) . [f,p] is set

c

the L_join of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{c

{{c

the L_join of LattStr(# (BL),(BL),(BL) #) . [c

c

the L_join of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{{c

the L_join of LattStr(# (BL),(BL),(BL) #) . [c

(c

the L_join of LattStr(# (BL),(BL),(BL) #) . ((c

[(c

{(c

{(c

{{(c

the L_join of LattStr(# (BL),(BL),(BL) #) . [(c

q is Element of (BL)

Y is Element of (BL)

D is Element of (BL)

D is Element of (BL)

D is Element of (BL)

(BL,q,D) is Element of (BL)

(BL,Y,D) is Element of (BL)

(BL,q,(BL,Y,D)) is Element of (BL)

(BL,q,Y) is Element of (BL)

(BL,(BL,q,Y),D) is Element of (BL)

(BL,D,D) is Element of (BL)

c

f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

c

the L_meet of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_meet of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{c

{{c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [c

(c

the L_join of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

the L_join of LattStr(# (BL),(BL),(BL) #) . ((c

[(c

{(c

{(c

{{(c

the L_join of LattStr(# (BL),(BL),(BL) #) . [(c

p is Element of (BL)

q is Element of (BL)

Y is Element of (BL)

(BL,Y,q) is Element of (BL)

(BL,p,q) is Element of (BL)

(BL,(BL,p,q),q) is Element of (BL)

c

f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

c

the L_meet of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_meet of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{c

{{c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [c

f "/\" c

the L_meet of LattStr(# (BL),(BL),(BL) #) . (f,c

[f,c

{f,c

{f} is non empty trivial finite 1 -element set

{{f,c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [f,c

p is Element of (BL)

q is Element of (BL)

(BL,q,p) is Element of (BL)

c

f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

p is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

f "/\" p is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

the L_meet of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_meet of LattStr(# (BL),(BL),(BL) #) . (f,p) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

[f,p] is set

{f,p} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,p},{f}} is non empty finite V40() set

the L_meet of LattStr(# (BL),(BL),(BL) #) . [f,p] is set

c

the L_meet of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{c

{{c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [c

c

the L_meet of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{{c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [c

(c

the L_meet of LattStr(# (BL),(BL),(BL) #) . ((c

[(c

{(c

{(c

{{(c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [(c

q is Element of (BL)

Y is Element of (BL)

D is Element of (BL)

D is Element of (BL)

D is Element of (BL)

(BL,q,D) is Element of (BL)

(BL,Y,D) is Element of (BL)

(BL,q,(BL,Y,D)) is Element of (BL)

(BL,q,Y) is Element of (BL)

(BL,(BL,q,Y),D) is Element of (BL)

(BL,D,D) is Element of (BL)

c

f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)

c

the L_join of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)) is Relation-like non empty set

K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #))) is non empty cup-closed diff-closed preBoolean set

the L_join of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{c

{{c

the L_join of LattStr(# (BL),(BL),(BL) #) . [c

c

the L_meet of LattStr(# (BL),(BL),(BL) #) is Relation-like K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)) -defined the carrier of LattStr(# (BL),(BL),(BL) #) -valued Function-like non empty V14(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #))) quasi_total Element of K19(K20(K20( the carrier of LattStr(# (BL),(BL),(BL) #), the carrier of LattStr(# (BL),(BL),(BL) #)), the carrier of LattStr(# (BL),(BL),(BL) #)))

the L_meet of LattStr(# (BL),(BL),(BL) #) . (c

[c

{c

{{c

the L_meet of LattStr(# (BL),(BL),(BL) #) . [c

p is Element of (BL)

q is Element of (BL)

Y is Element of (BL)

(BL,p,Y) is Element of (BL)

(BL,p,q) is Element of (BL)

(BL,p,(BL,p,q)) is Element of (BL)

BL is non empty TopSpace-like TopStruct

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

BL is non empty TopSpace-like TopStruct

(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of (BL) is non empty set

T is Element of the carrier of (BL)

c

T "\/" c

the L_join of (BL) is Relation-like K20( the carrier of (BL), the carrier of (BL)) -defined the carrier of (BL) -valued Function-like non empty V14(K20( the carrier of (BL), the carrier of (BL))) quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))

K20( the carrier of (BL), the carrier of (BL)) is Relation-like non empty set

K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)) is Relation-like non empty set

K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL))) is non empty cup-closed diff-closed preBoolean set

the L_join of (BL) . (T,c

[T,c

{T,c

{T} is non empty trivial finite 1 -element set

{{T,c

the L_join of (BL) . [T,c

T \/ c

BL is non empty TopSpace-like TopStruct

(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of (BL) is non empty set

T is Element of the carrier of (BL)

c

T "/\" c

the L_meet of (BL) is Relation-like K20( the carrier of (BL), the carrier of (BL)) -defined the carrier of (BL) -valued Function-like non empty V14(K20( the carrier of (BL), the carrier of (BL))) quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))

K20( the carrier of (BL), the carrier of (BL)) is Relation-like non empty set

K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)) is Relation-like non empty set

K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL))) is non empty cup-closed diff-closed preBoolean set

the L_meet of (BL) . (T,c

[T,c

{T,c

{T} is non empty trivial finite 1 -element set

{{T,c

the L_meet of (BL) . [T,c

T /\ c

BL is non empty TopSpace-like TopStruct

(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of (BL) is non empty set

BL is non empty TopSpace-like TopStruct

(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of (BL) is non empty set

c

f is Element of the carrier of (BL)

p is Element of the carrier of (BL)

f "\/" p is Element of the carrier of (BL)

the L_join of (BL) is Relation-like K20( the carrier of (BL), the carrier of (BL)) -defined the carrier of (BL) -valued Function-like non empty V14(K20( the carrier of (BL), the carrier of (BL))) quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))

K20( the carrier of (BL), the carrier of (BL)) is Relation-like non empty set

K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)) is Relation-like non empty set

K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL))) is non empty cup-closed diff-closed preBoolean set

the L_join of (BL) . (f,p) is Element of the carrier of (BL)

[f,p] is set

{f,p} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,p},{f}} is non empty finite V40() set

the L_join of (BL) . [f,p] is set

c

the L_meet of (BL) is Relation-like K20( the carrier of (BL), the carrier of (BL)) -defined the carrier of (BL) -valued Function-like non empty V14(K20( the carrier of (BL), the carrier of (BL))) quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))

the L_meet of (BL) . (c

[c

{c

{c

{{c

the L_meet of (BL) . [c

c

the L_meet of (BL) . (c

[c

{c

{{c

the L_meet of (BL) . [c

c

the L_meet of (BL) . (c

[c

{c

{{c

the L_meet of (BL) . [c

(c

the L_join of (BL) . ((c

[(c

{(c

{(c

{{(c

the L_join of (BL) . [(c

Y is Element of (BL)

D is Element of (BL)

D is Element of (BL)

D is Element of (BL)

B is Element of (BL)

G is Element of (BL)

(BL,Y,D) is Element of (BL)

(BL,Y,D) is Element of (BL)

(BL,D,D) is Element of (BL)

(BL,Y,(BL,D,D)) is Element of (BL)

(BL,Y,D) is Element of (BL)

(BL,(BL,Y,D),(BL,Y,D)) is Element of (BL)

(BL,B,G) is Element of (BL)

{} BL is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper V31() V35() finite finite-yielding V40() cardinal {} -element open closed Element of K19( the carrier of BL)

[#] BL is non empty non proper open closed Element of K19( the carrier of BL)

f is Element of the carrier of (BL)

p is Element of the carrier of (BL)

f "\/" p is Element of the carrier of (BL)

the L_join of (BL) is Relation-like K20( the carrier of (BL), the carrier of (BL)) -defined the carrier of (BL) -valued Function-like non empty V14(K20( the carrier of (BL), the carrier of (BL))) quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))

K20( the carrier of (BL), the carrier of (BL)) is Relation-like non empty set

K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)) is Relation-like non empty set

K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL))) is non empty cup-closed diff-closed preBoolean set

the L_join of (BL) . (f,p) is Element of the carrier of (BL)

[f,p] is set

{f,p} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,p},{f}} is non empty finite V40() set

the L_join of (BL) . [f,p] is set

p "\/" f is Element of the carrier of (BL)

the L_join of (BL) . (p,f) is Element of the carrier of (BL)

[p,f] is set

{p,f} is non empty finite set

{p} is non empty trivial finite 1 -element set

{{p,f},{p}} is non empty finite V40() set

the L_join of (BL) . [p,f] is set

q is Element of (BL)

([#] BL) \/ q is non empty Element of K19( the carrier of BL)

c

p is Element of the carrier of (BL)

c

the L_meet of (BL) is Relation-like K20( the carrier of (BL), the carrier of (BL)) -defined the carrier of (BL) -valued Function-like non empty V14(K20( the carrier of (BL), the carrier of (BL))) quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))

K20( the carrier of (BL), the carrier of (BL)) is Relation-like non empty set

K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)) is Relation-like non empty set

K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL))) is non empty cup-closed diff-closed preBoolean set

the L_meet of (BL) . (c

[c

{c

{c

{{c

the L_meet of (BL) . [c

p "/\" c

the L_meet of (BL) . (p,c

[p,c

{p,c

{p} is non empty trivial finite 1 -element set

{{p,c

the L_meet of (BL) . [p,c

q is Element of (BL)

{} /\ q is Relation-like finite Element of K19( the carrier of BL)

Bottom (BL) is Element of the carrier of (BL)

Top (BL) is Element of the carrier of (BL)

p is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr

the carrier of p is non empty set

q is Element of the carrier of p

Y is Element of (BL)

Y ` is Element of K19( the carrier of BL)

the carrier of BL \ Y is set

D is Element of the carrier of p

D "\/" q is Element of the carrier of p

the L_join of p is Relation-like K20( the carrier of p, the carrier of p) -defined the carrier of p -valued Function-like non empty V14(K20( the carrier of p, the carrier of p)) quasi_total commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of p, the carrier of p), the carrier of p))

K20( the carrier of p, the carrier of p) is Relation-like non empty set

K20(K20( the carrier of p, the carrier of p), the carrier of p) is Relation-like non empty set

K19(K20(K20( the carrier of p, the carrier of p), the carrier of p)) is non empty cup-closed diff-closed preBoolean set

the L_join of p . (D,q) is Element of the carrier of p

[D,q] is set

{D,q} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,q},{D}} is non empty finite V40() set

the L_join of p . [D,q] is set

Y \/ (Y `) is Element of K19( the carrier of BL)

Top p is Element of the carrier of p

D "/\" q is Element of the carrier of p

the L_meet of p is Relation-like K20( the carrier of p, the carrier of p) -defined the carrier of p -valued Function-like non empty V14(K20( the carrier of p, the carrier of p)) quasi_total commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of p, the carrier of p), the carrier of p))

the L_meet of p . (D,q) is Element of the carrier of p

the L_meet of p . [D,q] is set

Y /\ (Y `) is Element of K19( the carrier of BL)

Bottom p is Element of the carrier of p

BL is non empty TopSpace-like TopStruct

[#] BL is non empty non proper open closed Element of K19( the carrier of BL)

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of (BL) is non empty set

BL is non empty TopSpace-like TopStruct

{} BL is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper V31() V35() finite finite-yielding V40() cardinal {} -element open closed Element of K19( the carrier of BL)

the carrier of BL is non empty set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

K20((BL),(BL)) is Relation-like non empty set

K20(K20((BL),(BL)),(BL)) is Relation-like non empty set

K19(K20(K20((BL),(BL)),(BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like K20((BL),(BL)) -defined (BL) -valued Function-like non empty V14(K20((BL),(BL))) quasi_total Element of K19(K20(K20((BL),(BL)),(BL)))

LattStr(# (BL),(BL),(BL) #) is non empty strict LattStr

the carrier of (BL) is non empty set

the non empty TopSpace-like TopStruct is non empty TopSpace-like TopStruct

( the non empty TopSpace-like TopStruct ) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

( the non empty TopSpace-like TopStruct ) is non empty Element of K19(K19( the carrier of the non empty TopSpace-like TopStruct ))

the carrier of the non empty TopSpace-like TopStruct is non empty set

K19( the carrier of the non empty TopSpace-like TopStruct ) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of the non empty TopSpace-like TopStruct )) is non empty cup-closed diff-closed preBoolean set

{ b

( the non empty TopSpace-like TopStruct ) is Relation-like K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )) -defined ( the non empty TopSpace-like TopStruct ) -valued Function-like non empty V14(K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct ))) quasi_total Element of K19(K20(K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )),( the non empty TopSpace-like TopStruct )))

K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )) is Relation-like non empty set

K20(K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )),( the non empty TopSpace-like TopStruct )) is Relation-like non empty set

K19(K20(K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )),( the non empty TopSpace-like TopStruct ))) is non empty cup-closed diff-closed preBoolean set

( the non empty TopSpace-like TopStruct ) is Relation-like K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )) -defined ( the non empty TopSpace-like TopStruct ) -valued Function-like non empty V14(K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct ))) quasi_total Element of K19(K20(K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )),( the non empty TopSpace-like TopStruct )))

LattStr(# ( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct ) #) is non empty strict LattStr

T is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of T is non empty set

[#] the non empty TopSpace-like TopStruct is non empty non proper open closed Element of K19( the carrier of the non empty TopSpace-like TopStruct )

{} the non empty TopSpace-like TopStruct is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper V31() V35() finite finite-yielding V40() cardinal {} -element open closed Element of K19( the carrier of the non empty TopSpace-like TopStruct )

c

f is Element of the carrier of T

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

{ b

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

bool the carrier of BL is non empty cup-closed diff-closed preBoolean Element of K19(K19( the carrier of BL))

c

f is non empty final meet-closed join-closed Element of K19( the carrier of BL)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is Element of K19(K19( the carrier of BL))

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

c

f is Element of the carrier of BL

Bottom BL is Element of the carrier of BL

p is Element of the carrier of BL

q is non empty final meet-closed join-closed Element of K19( the carrier of BL)

f is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of f is non empty non trivial set

K19( the carrier of f) is non empty cup-closed diff-closed preBoolean set

BL is set

T is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(T) is non empty Element of K19(K19( the carrier of T))

the carrier of T is non empty non trivial set

K19( the carrier of T) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of T)) is non empty cup-closed diff-closed preBoolean set

{ b

p is non empty final meet-closed join-closed Element of K19( the carrier of f)

c

(f) is non empty Element of K19(K19( the carrier of f))

K19(K19( the carrier of f)) is non empty cup-closed diff-closed preBoolean set

{ b

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

T is Element of the carrier of BL

{ b

c

f is non empty final meet-closed join-closed Element of K19( the carrier of BL)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

{ b

T is Relation-like Function-like set

dom T is set

c

T . c

{ b

T is Relation-like Function-like set

dom T is set

c

dom c

f is set

T . f is set

p is Element of the carrier of BL

{ b

c

BL is set

T is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of T is non empty non trivial set

(T) is Relation-like Function-like set

K19( the carrier of T) is non empty cup-closed diff-closed preBoolean set

c

(T) . c

{ b

f is non empty final meet-closed join-closed Element of K19( the carrier of T)

{ b

f is non empty final meet-closed join-closed Element of K19( the carrier of T)

f is non empty final meet-closed join-closed Element of K19( the carrier of T)

p is non empty final meet-closed join-closed Element of K19( the carrier of T)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like Function-like set

T is Element of the carrier of BL

(BL) . T is set

c

f is non empty final meet-closed join-closed Element of K19( the carrier of BL)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

T is Element of the carrier of BL

c

T "\/" c

the L_join of BL is Relation-like K20( the carrier of BL, the carrier of BL) -defined the carrier of BL -valued Function-like non empty V14(K20( the carrier of BL, the carrier of BL)) quasi_total commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL))

K20( the carrier of BL, the carrier of BL) is Relation-like non empty set

K20(K20( the carrier of BL, the carrier of BL), the carrier of BL) is Relation-like non empty set

K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

the L_join of BL . (T,c

[T,c

{T,c

{T} is non empty trivial finite 1 -element set

{{T,c

the L_join of BL . [T,c

f is non empty final meet-closed join-closed Element of K19( the carrier of BL)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

(BL) is Relation-like Function-like set

T is Element of the carrier of BL

(BL) . T is set

c

T "/\" c

the L_meet of BL is Relation-like K20( the carrier of BL, the carrier of BL) -defined the carrier of BL -valued Function-like non empty V14(K20( the carrier of BL, the carrier of BL)) quasi_total commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL))

K20( the carrier of BL, the carrier of BL) is Relation-like non empty set

K20(K20( the carrier of BL, the carrier of BL), the carrier of BL) is Relation-like non empty set

K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

the L_meet of BL . (T,c

[T,c

{T,c

{T} is non empty trivial finite 1 -element set

{{T,c

the L_meet of BL . [T,c

(BL) . (T "/\" c

(BL) . c

((BL) . T) /\ ((BL) . c

f is set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

q is non empty final meet-closed join-closed Element of K19( the carrier of BL)

f is set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

p is non empty final meet-closed join-closed Element of K19( the carrier of BL)

q is non empty final meet-closed join-closed Element of K19( the carrier of BL)

p is non empty final meet-closed join-closed Element of K19( the carrier of BL)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

(BL) is Relation-like Function-like set

T is Element of the carrier of BL

(BL) . T is set

c

T "\/" c

the L_join of BL is Relation-like K20( the carrier of BL, the carrier of BL) -defined the carrier of BL -valued Function-like non empty V14(K20( the carrier of BL, the carrier of BL)) quasi_total commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL))

K20( the carrier of BL, the carrier of BL) is Relation-like non empty set

K20(K20( the carrier of BL, the carrier of BL), the carrier of BL) is Relation-like non empty set

K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

the L_join of BL . (T,c

[T,c

{T,c

{T} is non empty trivial finite 1 -element set

{{T,c

the L_join of BL . [T,c

(BL) . (T "\/" c

(BL) . c

((BL) . T) \/ ((BL) . c

f is set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

q is non empty final meet-closed join-closed Element of K19( the carrier of BL)

f is set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

p is non empty final meet-closed join-closed Element of K19( the carrier of BL)

q is non empty final meet-closed join-closed Element of K19( the carrier of BL)

p is non empty final meet-closed join-closed Element of K19( the carrier of BL)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is Relation-like Function-like set

the carrier of BL is non empty non trivial set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

K19((BL)) is non empty cup-closed diff-closed preBoolean set

K19(K19((BL))) is non empty cup-closed diff-closed preBoolean set

K20( the carrier of BL,(bool (BL))) is Relation-like non empty set

K19(K20( the carrier of BL,(bool (BL)))) is non empty cup-closed diff-closed preBoolean set

T is Relation-like Function-like set

dom T is set

rng T is set

c

f is set

T . f is set

{ b

c

f is Element of the carrier of BL

c

{ b

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

K19((BL)) is non empty cup-closed diff-closed preBoolean set

K19(K19((BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))

K20( the carrier of BL,(bool (BL))) is Relation-like non empty set

K19(K20( the carrier of BL,(bool (BL)))) is non empty cup-closed diff-closed preBoolean set

rng (BL) is non empty Element of K19((bool (BL)))

K19((bool (BL))) is non empty cup-closed diff-closed preBoolean set

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is set

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

K19((BL)) is non empty cup-closed diff-closed preBoolean set

K19(K19((BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))

K20( the carrier of BL,(bool (BL))) is Relation-like non empty set

K19(K20( the carrier of BL,(bool (BL)))) is non empty cup-closed diff-closed preBoolean set

rng (BL) is non empty Element of K19((bool (BL)))

K19((bool (BL))) is non empty cup-closed diff-closed preBoolean set

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is non empty set

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

K19((BL)) is non empty cup-closed diff-closed preBoolean set

K19(K19((BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))

K20( the carrier of BL,(bool (BL))) is Relation-like non empty set

K19(K20( the carrier of BL,(bool (BL)))) is non empty cup-closed diff-closed preBoolean set

rng (BL) is non empty Element of K19((bool (BL)))

K19((bool (BL))) is non empty cup-closed diff-closed preBoolean set

BL is set

T is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(T) is non empty set

(T) is non empty Element of K19(K19( the carrier of T))

the carrier of T is non empty non trivial set

K19( the carrier of T) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of T)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (T) is non empty cup-closed diff-closed preBoolean Element of K19(K19((T)))

K19((T)) is non empty cup-closed diff-closed preBoolean set

K19(K19((T))) is non empty cup-closed diff-closed preBoolean set

(T) is Relation-like the carrier of T -defined bool (T) -valued Function-like non empty V14( the carrier of T) quasi_total Element of K19(K20( the carrier of T,(bool (T))))

K20( the carrier of T,(bool (T))) is Relation-like non empty set

K19(K20( the carrier of T,(bool (T)))) is non empty cup-closed diff-closed preBoolean set

rng (T) is non empty Element of K19((bool (T)))

K19((bool (T))) is non empty cup-closed diff-closed preBoolean set

dom (T) is non empty Element of K19( the carrier of T)

c

(T) . c

f is Element of the carrier of T

(T) . f is Element of bool (T)

c

(T) . c

dom (T) is non empty Element of K19( the carrier of T)

c

(T) . c

f is Element of the carrier of T

(T) . f is Element of bool (T)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

K19((BL)) is non empty cup-closed diff-closed preBoolean set

K19(K19((BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty set

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

(BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))

K20( the carrier of BL,(bool (BL))) is Relation-like non empty set

K19(K20( the carrier of BL,(bool (BL)))) is non empty cup-closed diff-closed preBoolean set

rng (BL) is non empty Element of K19((bool (BL)))

K19((bool (BL))) is non empty cup-closed diff-closed preBoolean set

{ (union b

f is set

p is Element of K19(K19((BL)))

union p is Element of K19((BL))

f is Element of K19(K19((BL)))

TopStruct(# (BL),f #) is non empty strict TopStruct

the carrier of TopStruct(# (BL),f #) is non empty set

the topology of TopStruct(# (BL),f #) is Element of K19(K19( the carrier of TopStruct(# (BL),f #)))

K19( the carrier of TopStruct(# (BL),f #)) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of TopStruct(# (BL),f #))) is non empty cup-closed diff-closed preBoolean set

Top BL is Element of the carrier of BL

{ b

Y is set

D is non empty final meet-closed join-closed Element of K19( the carrier of BL)

bool { b

K19( { b

K19(K19( { b

{ { b

Y is Element of K19(K19((BL)))

D is Element of K19(K19((BL)))

union D is Element of K19((BL))

D is set

D is non empty final meet-closed join-closed Element of K19( the carrier of BL)

(BL) . (Top BL) is Element of bool (BL)

q is Element of K19(K19( the carrier of TopStruct(# (BL),f #)))

union q is Element of K19( the carrier of TopStruct(# (BL),f #))

K19((BL)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

K19(K19((BL))) is non empty cup-closed diff-closed preBoolean set

D is set

D is Element of K19((BL))

union D is set

D is Element of K19((BL))

D is Element of K19(K19((BL)))

union D is Element of K19((BL))

union (union D) is set

{ (union b

union { (union b

D is set

D is Element of K19(K19((BL)))

union D is Element of K19((BL))

D is set

D is Element of K19((BL))

union D is set

B is Element of K19((BL))

union B is set

q is Element of K19( the carrier of TopStruct(# (BL),f #))

Y is Element of K19( the carrier of TopStruct(# (BL),f #))

q /\ Y is Element of K19( the carrier of TopStruct(# (BL),f #))

D is Element of K19(K19((BL)))

union D is Element of K19((BL))

D is Element of K19(K19((BL)))

union D is Element of K19((BL))

(union D) /\ (union D) is Element of K19((BL))

INTERSECTION (D,D) is set

union (INTERSECTION (D,D)) is set

D is set

B is set

G is set

B /\ G is set

B \/ G is set

D is Element of K19(K19((BL)))

B is Element of K19(K19((BL)))

G is set

DD is set

DD is set

DD /\ DD is set

b is Element of the carrier of BL

(BL) . b is Element of bool (BL)

D is Element of the carrier of BL

(BL) . D is Element of bool (BL)

{ b

{ b

b "/\" D is Element of the carrier of BL

the L_meet of BL is Relation-like K20( the carrier of BL, the carrier of BL) -defined the carrier of BL -valued Function-like non empty V14(K20( the carrier of BL, the carrier of BL)) quasi_total commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL))

K20( the carrier of BL, the carrier of BL) is Relation-like non empty set

K20(K20( the carrier of BL, the carrier of BL), the carrier of BL) is Relation-like non empty set

K19(K20(K20( the carrier of BL, the carrier of BL), the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

the L_meet of BL . (b,D) is Element of the carrier of BL

[b,D] is set

{b,D} is non empty finite set

{b} is non empty trivial finite 1 -element set

{{b,D},{b}} is non empty finite V40() set

the L_meet of BL . [b,D] is set

{ b

D1 is set

D1 is non empty final meet-closed join-closed Element of K19( the carrier of BL)

F is non empty final meet-closed join-closed Element of K19( the carrier of BL)

D1 is set

D1 is non empty final meet-closed join-closed Element of K19( the carrier of BL)

F is non empty final meet-closed join-closed Element of K19( the carrier of BL)

F1 is non empty final meet-closed join-closed Element of K19( the carrier of BL)

(BL) . (b "/\" D) is Element of bool (BL)

p is strict TopSpace-like TopStruct

the carrier of p is set

the topology of p is non empty Element of K19(K19( the carrier of p))

K19( the carrier of p) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of p)) is non empty cup-closed diff-closed preBoolean set

T is strict TopSpace-like TopStruct

the carrier of T is set

the topology of T is non empty Element of K19(K19( the carrier of T))

K19( the carrier of T) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of T)) is non empty cup-closed diff-closed preBoolean set

c

the carrier of c

the topology of c

K19( the carrier of c

K19(K19( the carrier of c

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

(BL) is strict TopSpace-like TopStruct

the carrier of (BL) is set

(BL) is non empty Element of K19(K19( the carrier of BL))

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

c

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

K19((BL)) is non empty cup-closed diff-closed preBoolean set

K19(K19((BL))) is non empty cup-closed diff-closed preBoolean set

(BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))

K20( the carrier of BL,(bool (BL))) is Relation-like non empty set

K19(K20( the carrier of BL,(bool (BL)))) is non empty cup-closed diff-closed preBoolean set

T is Element of the carrier of BL

(BL) . T is Element of bool (BL)

BL is non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean LattStr

the carrier of BL is non empty non trivial set

K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set

(BL) is non empty Element of K19(K19( the carrier of BL))

K19(K19( the carrier of BL)) is non empty cup-closed diff-closed preBoolean set

{ b

bool (BL) is non empty cup-closed diff-closed preBoolean Element of K19(K19((BL)))

K19((BL)) is non empty