:: 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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
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₃ is set
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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
{} 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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
T is Element of K19( the carrier of BL)
c₃ is 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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
T is Element of K19( the carrier of BL)
c₃ is 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
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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
T is Element of (BL)
c₃ is Element of (BL)
T \/ c₃ is set
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₃ is Element of K19( the carrier of BL)
T /\ c₃ is set
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₃ is 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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
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₃ is Element of (BL)
f is Element of (BL)
T . (c₃,f) is Element of (BL)
[c₃,f] is set
{c₃,f} is non empty finite set
{c₃} is non empty trivial finite 1 -element set
{{c₃,f},{c₃}} is non empty finite V40() set
T . [c₃,f] is set
(BL,c₃,f) is Element of (BL)
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₃ is Element of (BL)
f is Element of (BL)
T . (c₃,f) is Element of (BL)
[c₃,f] is set
{c₃,f} is non empty finite set
{c₃} is non empty trivial finite 1 -element set
{{c₃,f},{c₃}} is non empty finite V40() set
T . [c₃,f] is set
(BL,c₃,f) 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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is 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)))
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₃ is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
p is Element of (BL)
T "\/" c₃ 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) #) . (T,c₃) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[T,c₃] is set
{T,c₃} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c₃},{T}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [T,c₃] is set
(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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is 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)))
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₃ is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
p is Element of (BL)
T "/\" c₃ 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) #) . (T,c₃) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[T,c₃] is set
{T,c₃} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c₃},{T}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [T,c₃] is set
(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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is set
T is Element of (BL)
T ` is Element of K19( the carrier of BL)
the carrier of BL \ T is set
c<sub>3</sub> is Element of K19( the carrier 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<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of BL) : ( b<sub>1</sub> is open & b<sub>1</sub> is closed ) } is 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)))
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<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
c<sub>3</sub> "\/" f 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) #) . (c<sub>3</sub>,f) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,f] is set
{c<sub>3</sub>,f} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,f},{c<sub>3</sub>}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,f] is set
f "\/" c<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_join of LattStr(# (BL),(BL),(BL) #) . (f,c<sub>3</sub>) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[f,c<sub>3</sub>] is set
{f,c<sub>3</sub>} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,c<sub>3</sub>},{f}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [f,c<sub>3</sub>] is set
p is Element of (BL)
q is Element of (BL)
(BL,q,p) is Element of (BL)
c<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
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<sub>3</sub> "\/" (f "\/" p) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_join of LattStr(# (BL),(BL),(BL) #) . (c<sub>3</sub>,(f "\/" p)) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,(f "\/" p)] is set
{c<sub>3</sub>,(f "\/" p)} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,(f "\/" p)},{c<sub>3</sub>}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,(f "\/" p)] is set
c<sub>3</sub> "\/" f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_join of LattStr(# (BL),(BL),(BL) #) . (c<sub>3</sub>,f) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,f] is set
{c<sub>3</sub>,f} is non empty finite set
{{c<sub>3</sub>,f},{c<sub>3</sub>}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,f] is set
(c<sub>3</sub> "\/" f) "\/" p is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_join of LattStr(# (BL),(BL),(BL) #) . ((c<sub>3</sub> "\/" f),p) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[(c<sub>3</sub> "\/" f),p] is set
{(c<sub>3</sub> "\/" f),p} is non empty finite set
{(c<sub>3</sub> "\/" f)} is non empty trivial finite 1 -element set
{{(c<sub>3</sub> "\/" f),p},{(c<sub>3</sub> "\/" f)}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [(c<sub>3</sub> "\/" f),p] is set
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<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
c<sub>3</sub> "/\" f 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) #) . (c<sub>3</sub>,f) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,f] is set
{c<sub>3</sub>,f} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,f},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,f] is set
(c<sub>3</sub> "/\" f) "\/" f 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) #)))
the L_join of LattStr(# (BL),(BL),(BL) #) . ((c<sub>3</sub> "/\" f),f) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[(c<sub>3</sub> "/\" f),f] is set
{(c<sub>3</sub> "/\" f),f} is non empty finite set
{(c<sub>3</sub> "/\" f)} is non empty trivial finite 1 -element set
{{(c<sub>3</sub> "/\" f),f},{(c<sub>3</sub> "/\" f)}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [(c<sub>3</sub> "/\" f),f] is set
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<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
c<sub>3</sub> "/\" f 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) #) . (c<sub>3</sub>,f) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,f] is set
{c<sub>3</sub>,f} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,f},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,f] is set
f "/\" c<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_meet of LattStr(# (BL),(BL),(BL) #) . (f,c<sub>3</sub>) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[f,c<sub>3</sub>] is set
{f,c<sub>3</sub>} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,c<sub>3</sub>},{f}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [f,c<sub>3</sub>] is set
p is Element of (BL)
q is Element of (BL)
(BL,q,p) is Element of (BL)
c<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
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<sub>3</sub> "/\" (f "/\" p) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_meet of LattStr(# (BL),(BL),(BL) #) . (c<sub>3</sub>,(f "/\" p)) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,(f "/\" p)] is set
{c<sub>3</sub>,(f "/\" p)} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,(f "/\" p)},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,(f "/\" p)] is set
c<sub>3</sub> "/\" f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_meet of LattStr(# (BL),(BL),(BL) #) . (c<sub>3</sub>,f) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,f] is set
{c<sub>3</sub>,f} is non empty finite set
{{c<sub>3</sub>,f},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,f] is set
(c<sub>3</sub> "/\" f) "/\" p is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
the L_meet of LattStr(# (BL),(BL),(BL) #) . ((c<sub>3</sub> "/\" f),p) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[(c<sub>3</sub> "/\" f),p] is set
{(c<sub>3</sub> "/\" f),p} is non empty finite set
{(c<sub>3</sub> "/\" f)} is non empty trivial finite 1 -element set
{{(c<sub>3</sub> "/\" f),p},{(c<sub>3</sub> "/\" f)}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [(c<sub>3</sub> "/\" f),p] is set
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<sub>3</sub> is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
f is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
c<sub>3</sub> "\/" f 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) #) . (c<sub>3</sub>,f) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,f] is set
{c<sub>3</sub>,f} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,f},{c<sub>3</sub>}} is non empty finite V40() set
the L_join of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,f] is set
c<sub>3</sub> "/\" (c<sub>3</sub> "\/" f) 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) #)))
the L_meet of LattStr(# (BL),(BL),(BL) #) . (c<sub>3</sub>,(c<sub>3</sub> "\/" f)) is Element of the carrier of LattStr(# (BL),(BL),(BL) #)
[c<sub>3</sub>,(c<sub>3</sub> "\/" f)] is set
{c<sub>3</sub>,(c<sub>3</sub> "\/" f)} is non empty finite set
{{c<sub>3</sub>,(c<sub>3</sub> "\/" f)},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of LattStr(# (BL),(BL),(BL) #) . [c<sub>3</sub>,(c<sub>3</sub> "\/" f)] is set
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<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of BL) : ( b<sub>1</sub> is open & b<sub>1</sub> is closed ) } is 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)))
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<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of BL) : ( b<sub>1</sub> is open & b<sub>1</sub> is closed ) } is 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)))
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<sub>3</sub> is Element of the carrier of (BL)
T "\/" c<sub>3</sub> 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) . (T,c<sub>3</sub>) is Element of the carrier of (BL)
[T,c<sub>3</sub>] is set
{T,c<sub>3</sub>} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c<sub>3</sub>},{T}} is non empty finite V40() set
the L_join of (BL) . [T,c<sub>3</sub>] is set
T \/ c<sub>3</sub> is 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<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of BL) : ( b<sub>1</sub> is open & b<sub>1</sub> is closed ) } is 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)))
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<sub>3</sub> is Element of the carrier of (BL)
T "/\" c<sub>3</sub> 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 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<sub>3</sub>) is Element of the carrier of (BL)
[T,c<sub>3</sub>] is set
{T,c<sub>3</sub>} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c<sub>3</sub>},{T}} is non empty finite V40() set
the L_meet of (BL) . [T,c<sub>3</sub>] is set
T /\ c<sub>3</sub> is 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<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of BL) : ( b<sub>1</sub> is open & b<sub>1</sub> is closed ) } is 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)))
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<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of BL) : ( b<sub>1</sub> is open & b<sub>1</sub> is closed ) } is 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)))
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<sub>3</sub> is Element of 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
c<sub>3</sub> "/\" (f "\/" p) 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 Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))
the L_meet of (BL) . (c<sub>3</sub>,(f "\/" p)) is Element of the carrier of (BL)
[c<sub>3</sub>,(f "\/" p)] is set
{c<sub>3</sub>,(f "\/" p)} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,(f "\/" p)},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of (BL) . [c<sub>3</sub>,(f "\/" p)] is set
c<sub>3</sub> "/\" f is Element of the carrier of (BL)
the L_meet of (BL) . (c<sub>3</sub>,f) is Element of the carrier of (BL)
[c<sub>3</sub>,f] is set
{c<sub>3</sub>,f} is non empty finite set
{{c<sub>3</sub>,f},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of (BL) . [c<sub>3</sub>,f] is set
c<sub>3</sub> "/\" p is Element of the carrier of (BL)
the L_meet of (BL) . (c<sub>3</sub>,p) is Element of the carrier of (BL)
[c<sub>3</sub>,p] is set
{c<sub>3</sub>,p} is non empty finite set
{{c<sub>3</sub>,p},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of (BL) . [c<sub>3</sub>,p] is set
(c<sub>3</sub> "/\" f) "\/" (c<sub>3</sub> "/\" p) is Element of the carrier of (BL)
the L_join of (BL) . ((c<sub>3</sub> "/\" f),(c<sub>3</sub> "/\" p)) is Element of the carrier of (BL)
[(c<sub>3</sub> "/\" f),(c<sub>3</sub> "/\" p)] is set
{(c<sub>3</sub> "/\" f),(c<sub>3</sub> "/\" p)} is non empty finite set
{(c<sub>3</sub> "/\" f)} is non empty trivial finite 1 -element set
{{(c<sub>3</sub> "/\" f),(c<sub>3</sub> "/\" p)},{(c<sub>3</sub> "/\" f)}} is non empty finite V40() set
the L_join of (BL) . [(c<sub>3</sub> "/\" f),(c<sub>3</sub> "/\" p)] is set
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<sub>3</sub> is Element of the carrier of (BL)
p is Element of the carrier of (BL)
c<sub>3</sub> "/\" p 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 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<sub>3</sub>,p) is Element of the carrier of (BL)
[c<sub>3</sub>,p] is set
{c<sub>3</sub>,p} is non empty finite set
{c<sub>3</sub>} is non empty trivial finite 1 -element set
{{c<sub>3</sub>,p},{c<sub>3</sub>}} is non empty finite V40() set
the L_meet of (BL) . [c<sub>3</sub>,p] is set
p "/\" c<sub>3</sub> is Element of the carrier of (BL)
the L_meet of (BL) . (p,c<sub>3</sub>) is Element of the carrier of (BL)
[p,c<sub>3</sub>] is set
{p,c<sub>3</sub>} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,c<sub>3</sub>},{p}} is non empty finite V40() set
the L_meet of (BL) . [p,c<sub>3</sub>] is set
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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is 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)))
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₁ where b₁ is Element of K19( the carrier of BL) : ( b₁ is open & b₁ is closed ) } is 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)))
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₁ where b₁ is Element of K19( the carrier of the non empty TopSpace-like TopStruct ) : ( b₁ is open & b₁ is closed ) } is 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 )))
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₃ is Element of the carrier of T
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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₃ is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
c₃ is Element of the carrier of BL
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of T) : b₁ is being_ultrafilter } is set
p is non empty final meet-closed join-closed Element of K19( the carrier of f)
c₃ is set
(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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of f) : b₁ is being_ultrafilter } is 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
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
T is Element of the carrier of BL
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & T in b₁ ) } is set
c₃ is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & a₁ in b₁ ) } is set
T is Relation-like Function-like set
dom T is set
c₃ is Element of the carrier of BL
T . c₃ is set
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & c₃ in b₁ ) } is set
T is Relation-like Function-like set
dom T is set
c₃ is Relation-like Function-like set
dom c₃ is set
f is set
T . f is set
p is Element of the carrier of BL
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & p in b₁ ) } is set
c₃ . f is 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
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₃ is Element of the carrier of T
(T) . c₃ is set
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of T) : ( b₁ is being_ultrafilter & c₃ in b₁ ) } is set
f is non empty final meet-closed join-closed Element of K19( the carrier of T)
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of T) : ( b₁ is being_ultrafilter & c₃ in b₁ ) } is set
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₃ 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)
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₃ is Element of the carrier of BL
T "\/" c₃ 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 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₃) is Element of the carrier of BL
[T,c₃] is set
{T,c₃} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c₃},{T}} is non empty finite V40() set
the L_join of BL . [T,c₃] is set
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₃ is Element of the carrier of BL
T "/\" c₃ 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 . (T,c₃) is Element of the carrier of BL
[T,c₃] is set
{T,c₃} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c₃},{T}} is non empty finite V40() set
the L_meet of BL . [T,c₃] is set
(BL) . (T "/\" c₃) is set
(BL) . c₃ is set
((BL) . T) /\ ((BL) . c₃) is set
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₃ is Element of the carrier of BL
T "\/" c₃ 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 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₃) is Element of the carrier of BL
[T,c₃] is set
{T,c₃} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,c₃},{T}} is non empty finite V40() set
the L_join of BL . [T,c₃] is set
(BL) . (T "\/" c₃) is set
(BL) . c₃ is set
((BL) . T) \/ ((BL) . c₃) is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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₃ is set
f is set
T . f is set
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & f in b₁ ) } is set
c₃ 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))))
f is Element of the carrier of BL
c₃ . f is Element of bool (BL)
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & f in b₁ ) } is 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 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of T) : b₁ is being_ultrafilter } is set
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₃ is set
(T) . c₃ is set
f is Element of the carrier of T
(T) . f is Element of bool (T)
c₃ is Element of the carrier of T
(T) . c₃ is Element of bool (T)
dom (T) is non empty Element of K19( the carrier of T)
c₃ is Element of the carrier of T
(T) . c₃ is Element of bool (T)
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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₁) where b₁ is Element of K19(K19((BL))) : b₁ c= (BL) } is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & Top BL in b₁ ) } is set
Y is set
D is non empty final meet-closed join-closed Element of K19( the carrier of BL)
bool { b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & Top BL in b₁ ) } is non empty cup-closed diff-closed preBoolean Element of K19(K19( { b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & Top BL in b₁ ) } ))
K19( { b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & Top BL in b₁ ) } ) is non empty cup-closed diff-closed preBoolean set
K19(K19( { b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & Top BL in b₁ ) } )) is non empty cup-closed diff-closed preBoolean set
{ { b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & Top BL in b₁ ) } } is non empty trivial finite 1 -element set
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₁ where b₁ is Element of K19((BL)) : union b₁ in q } is set
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₁) where b₁ is Element of K19((BL)) : b₁ in D } is set
union { (union b₁) where b₁ is Element of K19((BL)) : b₁ in D } is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & b in b₁ ) } is set
{ b₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & D in b₁ ) } is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : ( b₁ is being_ultrafilter & b "/\" D in b₁ ) } is set
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₃ is strict TopSpace-like TopStruct
the carrier of c₃ is set
the topology of c₃ is non empty Element of K19(K19( the carrier of c₃))
K19( the carrier of c₃) is non empty cup-closed diff-closed preBoolean set
K19(K19( the carrier of c₃)) 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 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is 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
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₃ is non empty final meet-closed join-closed 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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) \ ((BL) . T) is Element of K19(K19( the carrier of BL))
T ` is Element of the carrier of BL
(BL) . (T `) is Element of bool (BL)
c₃ is set
f is non empty final meet-closed join-closed Element of K19( the carrier of BL)
c₃ is set
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 non empty strict TopSpace-like TopStruct
((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)))
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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is 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))))
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 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 strict 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 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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
T is Element of K19( the carrier of (BL))
{T} is non empty trivial finite 1 -element set
union {T} is set
{ (union b₁) where b₁ is Element of K19(K19((BL))) : b₁ c= (BL) } is set
the topology of (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
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 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))))
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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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 Element of the carrier of BL
(BL) . T is Element of bool (BL)
c₃ is Element of the carrier of BL
(BL) . c₃ is Element of bool (BL)
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 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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 one-to-one 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 (BL) is set
(BL) is non empty strict 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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is set
the Element of ((BL)) is Element of ((BL))
c₃ is Element of K19( the carrier of (BL))
the topology of (BL) is non empty Element of K19(K19( the carrier of (BL)))
{ (union b₁) where b₁ is Element of K19(K19((BL))) : b₁ c= (BL) } is set
f is Element of K19(K19((BL)))
union f is Element of K19((BL))
c₃ ` is Element of K19( the carrier of (BL))
the carrier of (BL) \ c<sub>3</sub> is set
p is Element of K19(K19((BL)))
union p is Element of K19((BL))
f \/ p is Element of K19(K19((BL)))
union (f \/ p) is Element of K19((BL))
c<sub>3</sub> \/ (c<sub>3</sub> `) is Element of K19( the carrier of (BL))
[#] (BL) is non empty non proper open closed Element of K19( the carrier of (BL))
union (bool (BL)) is Element of K19((BL))
BL is non empty set
Fin BL is non empty cup-closed diff-closed preBoolean set
the Element of BL is Element of BL
{. the Element of BL.} is non empty trivial finite 1 -element Element of Fin BL
BL is non empty set
Fin 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
the carrier of BL is non empty non trivial set
K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set
Bottom BL is Element of the carrier of BL
Fin the carrier of BL is non empty cup-closed diff-closed preBoolean set
T is non empty Element of K19( the carrier of BL)
<.T.) is non empty final meet-closed join-closed Element of K19( the carrier of BL)
{ (FinMeet b₁) where b₁ is finite Element of Fin the carrier of BL : ( b₁ c= T & not b₁ = {} ) } is set
{ b₁ where b₁ is Element of the carrier of BL : ex b₂ being Element of the carrier of BL st
( b₂ in { (FinMeet b₁) where b₃ is finite Element of Fin the carrier of BL : ( b₁ c= T & not b₁ = {} ) } & b₂ [= b₁ ) } is set
p is set
q is Element of the carrier of BL
Y is Element of the carrier of BL
Fin T is non empty cup-closed diff-closed preBoolean set
p is finite Element of Fin T
K19(T) is non empty cup-closed diff-closed preBoolean set
q is finite Element of Fin the carrier of BL
FinMeet q is Element of the carrier of BL
Y is Element of the carrier of BL
p is non empty Element of K19( the carrier of BL)
q is Element of the carrier of BL
Y is Element of the carrier of BL
q "/\" Y 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 . (q,Y) is Element of the carrier of BL
[q,Y] is set
{q,Y} is non empty finite set
{q} is non empty trivial finite 1 -element set
{{q,Y},{q}} is non empty finite V40() set
the L_meet of BL . [q,Y] is set
D is Element of the carrier of BL
D is Element of the carrier of BL
D is Element of the carrier of BL
D is Element of the carrier of BL
B is Element of the carrier of BL
B is Element of the carrier of BL
D "/\" B is Element of the carrier of BL
the L_meet of BL . (D,B) is Element of the carrier of BL
[D,B] is set
{D,B} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,B},{D}} is non empty finite V40() set
the L_meet of BL . [D,B] is set
D "/\" D is Element of the carrier of BL
the L_meet of BL . (D,D) is Element of the carrier of BL
[D,D] is set
{D,D} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,D},{D}} is non empty finite V40() set
the L_meet of BL . [D,D] is set
G is finite Element of Fin the carrier of BL
FinMeet G is Element of the carrier of BL
DD is finite Element of Fin the carrier of BL
FinMeet DD is Element of the carrier of BL
G \/ DD is finite Element of Fin the carrier of BL
FinMeet (G \/ DD) is Element of the carrier of BL
q is Element of the carrier of BL
Y is Element of the carrier of BL
D is Element of the carrier of BL
D is Element of the carrier of BL
D is Element of the carrier of BL
D is Element of the carrier of BL
q is set
{q} is non empty trivial finite 1 -element set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL, the carrier of BL))
K20( the carrier of BL, the carrier of BL) is Relation-like non empty set
K19(K20( the carrier of BL, the carrier of BL)) is non empty cup-closed diff-closed preBoolean set
(id the carrier of BL) . q is set
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(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
Y is finite Element of Fin the carrier of BL
the L_meet of BL $$ (Y,(id the carrier of BL)) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL, the carrier of BL))
FinMeet (Y,(id BL)) is Element of the carrier of BL
FinMeet Y is Element of the carrier of BL
D is Element of the carrier of BL
q is Element of the carrier of BL
Y is Element of the carrier of BL
q is Element of the carrier of BL
Y is finite Element of Fin the carrier of BL
FinMeet Y is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of BL is non empty set
K19( the carrier of BL) is non empty cup-closed diff-closed preBoolean set
Bottom BL is Element of the carrier of BL
T 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 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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 one-to-one 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
Bottom BL is Element of the carrier of BL
(BL) . (Bottom BL) is Element of bool (BL)
the Element of (BL) . (Bottom BL) is Element of (BL) . (Bottom BL)
c₃ 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 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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 one-to-one 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
Top BL is Element of the carrier of BL
(BL) . (Top BL) is Element of bool (BL)
Bottom BL is Element of the carrier of BL
(Bottom BL) ` is Element of the carrier of BL
(BL) . ((Bottom BL) `) is Element of bool (BL)
(BL) . (Bottom BL) is Element of bool (BL)
(BL) \ ((BL) . (Bottom BL)) is Element of K19(K19( the carrier of BL))
(BL) \ {} is Element of K19(K19( the carrier of BL))
BL is set
union BL is set
Fin BL is non empty cup-closed diff-closed preBoolean 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of T) : b₁ is being_ultrafilter } is set
(T) is non empty set
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 one-to-one 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
K19((T)) is non empty cup-closed diff-closed preBoolean set
c₃ is finite Element of Fin BL
the Element of c₃ is Element of c₃
p is Element of the carrier of T
(T) . p is Element of bool (T)
{ (b₁ `) where b<sub>1</sub> is Element of the carrier of T : (T) . b<sub>1</sub> in BL } is set
p ` is Element of the carrier of T
Y is Element of the carrier of T
D is set
D is Element of the carrier of T
D ` is Element of the carrier of T
(T) . D is Element of bool (T)
D is non empty Element of K19( the carrier of T)
<.D.) is non empty final meet-closed join-closed Element of K19( the carrier of T)
Fin the carrier of T is non empty cup-closed diff-closed preBoolean set
Bottom T is Element of the carrier of T
D is non empty finite Element of Fin the carrier of T
FinMeet D is Element of the carrier of T
dom (T) is non empty Element of K19( the carrier of T)
(T) .: D is finite Element of Fin (bool (T))
Fin (bool (T)) is non empty cup-closed diff-closed preBoolean set
(T) . (Bottom T) is Element of bool (T)
the Element of (T) . (Bottom T) is Element of (T) . (Bottom T)
{} (T) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper V31() V35() finite finite-yielding V40() cardinal {} -element Element of K19((T))
DD is non empty final meet-closed join-closed Element of K19( the carrier of T)
K20((bool (T)),(bool (T))) is Relation-like non empty set
K20(K20((bool (T)),(bool (T))),(bool (T))) is Relation-like non empty set
K19(K20(K20((bool (T)),(bool (T))),(bool (T)))) is non empty cup-closed diff-closed preBoolean set
G is Relation-like K20((bool (T)),(bool (T))) -defined bool (T) -valued Function-like non empty V14(K20((bool (T)),(bool (T)))) quasi_total Element of K19(K20(K20((bool (T)),(bool (T))),(bool (T))))
DD is Element of K19((T))
DD is Element of K19((T))
G . (DD,DD) is Element of bool (T)
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . (DD,DD) is Element of bool (T)
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . (DD,DD) is Element of K19((T))
DD /\ DD is Element of K19((T))
G . (DD,DD) is Element of K19((T))
DD is Element of K19((T))
DD is Element of K19((T))
b is Element of K19((T))
G . (DD,b) is Element of bool (T)
[DD,b] is set
{DD,b} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,b},{DD}} is non empty finite V40() set
G . [DD,b] is set
G . (DD,(G . (DD,b))) is Element of bool (T)
[DD,(G . (DD,b))] is set
{DD,(G . (DD,b))} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,(G . (DD,b))},{DD}} is non empty finite V40() set
G . [DD,(G . (DD,b))] is set
G . (DD,DD) is Element of bool (T)
[DD,DD] is set
{DD,DD} is non empty finite set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . ((G . (DD,DD)),b) is Element of bool (T)
[(G . (DD,DD)),b] is set
{(G . (DD,DD)),b} is non empty finite set
{(G . (DD,DD))} is non empty trivial finite 1 -element set
{{(G . (DD,DD)),b},{(G . (DD,DD))}} is non empty finite V40() set
G . [(G . (DD,DD)),b] is set
G . (DD,b) is Element of K19((T))
G . (DD,(G . (DD,b))) is Element of K19((T))
[DD,(G . (DD,b))] is set
{DD,(G . (DD,b))} is non empty finite set
{{DD,(G . (DD,b))},{DD}} is non empty finite V40() set
G . [DD,(G . (DD,b))] is set
DD /\ b is Element of K19((T))
G . (DD,(DD /\ b)) is Element of K19((T))
[DD,(DD /\ b)] is set
{DD,(DD /\ b)} is non empty finite set
{{DD,(DD /\ b)},{DD}} is non empty finite V40() set
G . [DD,(DD /\ b)] is set
DD /\ (DD /\ b) is Element of K19((T))
DD /\ DD is Element of K19((T))
(DD /\ DD) /\ b is Element of K19((T))
G . ((DD /\ DD),b) is Element of K19((T))
[(DD /\ DD),b] is set
{(DD /\ DD),b} is non empty finite set
{(DD /\ DD)} is non empty trivial finite 1 -element set
{{(DD /\ DD),b},{(DD /\ DD)}} is non empty finite V40() set
G . [(DD /\ DD),b] is set
G . (DD,DD) is Element of K19((T))
G . ((G . (DD,DD)),b) is Element of K19((T))
[(G . (DD,DD)),b] is set
{(G . (DD,DD)),b} is non empty finite set
{(G . (DD,DD))} is non empty trivial finite 1 -element set
{{(G . (DD,DD)),b},{(G . (DD,DD))}} is non empty finite V40() set
G . [(G . (DD,DD)),b] is set
DD is Element of K19((T))
G . (DD,DD) is Element of bool (T)
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . (DD,DD) is Element of K19((T))
DD /\ DD is Element of K19((T))
the L_meet of T is Relation-like K20( the carrier of T, the carrier of T) -defined the carrier of T -valued Function-like non empty V14(K20( the carrier of T, the carrier of T)) quasi_total commutative associative idempotent having_a_unity Element of K19(K20(K20( the carrier of T, the carrier of T), the carrier of T))
K20( the carrier of T, the carrier of T) is Relation-like non empty set
K20(K20( the carrier of T, the carrier of T), the carrier of T) is Relation-like non empty set
K19(K20(K20( the carrier of T, the carrier of T), the carrier of T)) is non empty cup-closed diff-closed preBoolean set
DD is Element of the carrier of T
DD is Element of the carrier of T
the L_meet of T . (DD,DD) is Element of the carrier of T
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
the L_meet of T . [DD,DD] is set
(T) . ( the L_meet of T . (DD,DD)) is Element of bool (T)
(T) . DD is Element of bool (T)
(T) . DD is Element of bool (T)
G . (((T) . DD),((T) . DD)) is Element of bool (T)
[((T) . DD),((T) . DD)] is set
{((T) . DD),((T) . DD)} is non empty finite set
{((T) . DD)} is non empty trivial finite 1 -element set
{{((T) . DD),((T) . DD)},{((T) . DD)}} is non empty finite V40() set
G . [((T) . DD),((T) . DD)] is set
DD "/\" DD is Element of the carrier of T
(T) . (DD "/\" DD) is Element of bool (T)
((T) . DD) /\ ((T) . DD) is Element of bool (T)
B is non empty Element of K19(K19((T)))
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V14( the carrier of T) quasi_total Element of K19(K20( the carrier of T, the carrier of T))
K19(K20( the carrier of T, the carrier of T)) is non empty cup-closed diff-closed preBoolean set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V14( the carrier of T) quasi_total Element of K19(K20( the carrier of T, the carrier of T))
(T) . (FinMeet D) is Element of bool (T)
FinMeet (D,(id the carrier of T)) is Element of the carrier of T
(T) . (FinMeet (D,(id the carrier of T))) is Element of bool (T)
the L_meet of T $$ (D,(id the carrier of T)) is Element of the carrier of T
(T) . ( the L_meet of T $$ (D,(id the carrier of T))) is Element of bool (T)
(T) * (id the carrier of T) is Relation-like the carrier of T -defined bool (T) -valued Function-like one-to-one non empty V14( the carrier of T) quasi_total Element of K19(K20( the carrier of T,(bool (T))))
G $$ (D,((T) * (id the carrier of T))) is Element of bool (T)
G $$ (D,(T)) is Element of bool (T)
id (bool (T)) is Relation-like bool (T) -defined bool (T) -valued Function-like one-to-one non empty V14( bool (T)) quasi_total Element of K19(K20((bool (T)),(bool (T))))
K19(K20((bool (T)),(bool (T)))) is non empty cup-closed diff-closed preBoolean set
(id (bool (T))) * (T) is Relation-like the carrier of T -defined bool (T) -valued Function-like one-to-one non empty V14( the carrier of T) quasi_total Element of K19(K20( the carrier of T,(bool (T))))
G $$ (D,((id (bool (T))) * (T))) is Element of bool (T)
DD is finite Element of Fin (bool (T))
G $$ (DD,(id (bool (T)))) is Element of bool (T)
{}. (bool (T)) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V31() V35() finite finite-yielding V40() cardinal {} -element Element of Fin (bool (T))
G $$ (({}. (bool (T))),(id (bool (T)))) is Element of bool (T)
DD is non empty Element of K19(K19((T)))
meet DD is Element of K19((T))
DD is finite Element of Fin (bool (T))
G $$ (DD,(id (bool (T)))) is Element of bool (T)
b is Element of K19((T))
{.b.} is non empty trivial finite 1 -element Element of Fin K19((T))
Fin K19((T)) is non empty cup-closed diff-closed preBoolean set
DD \/ {.b.} is non empty finite Element of Fin K19((T))
G $$ ((DD \/ {.b.}),(id (bool (T)))) is Element of bool (T)
D is non empty Element of K19(K19((T)))
meet D is Element of K19((T))
{b} is non empty trivial finite 1 -element set
DD \/ {b} is non empty finite set
(id (bool (T))) . b is Element of bool (T)
D1 is non empty Element of K19(K19((T)))
(id (bool (T))) . b is Element of bool (T)
G . ((G $$ (DD,(id (bool (T))))),((id (bool (T))) . b)) is Element of bool (T)
[(G $$ (DD,(id (bool (T))))),((id (bool (T))) . b)] is set
{(G $$ (DD,(id (bool (T))))),((id (bool (T))) . b)} is non empty finite set
{(G $$ (DD,(id (bool (T)))))} is non empty trivial finite 1 -element set
{{(G $$ (DD,(id (bool (T))))),((id (bool (T))) . b)},{(G $$ (DD,(id (bool (T)))))}} is non empty finite V40() set
G . [(G $$ (DD,(id (bool (T))))),((id (bool (T))) . b)] is set
G . ((G $$ (DD,(id (bool (T))))),b) is Element of K19((T))
[(G $$ (DD,(id (bool (T))))),b] is set
{(G $$ (DD,(id (bool (T))))),b} is non empty finite set
{{(G $$ (DD,(id (bool (T))))),b},{(G $$ (DD,(id (bool (T)))))}} is non empty finite V40() set
G . [(G $$ (DD,(id (bool (T))))),b] is set
(G $$ (DD,(id (bool (T))))) /\ b is Element of K19((T))
D1 is non empty Element of K19(K19((T)))
meet D1 is Element of K19((T))
(meet D1) /\ b is Element of K19((T))
meet {b} is set
(meet D1) /\ (meet {b}) is Element of K19((T))
meet B is Element of K19((T))
COMPLEMENT B is Element of K19(K19((T)))
union (COMPLEMENT B) is Element of K19((T))
[#] (T) is non empty non proper Element of K19((T))
([#] (T)) \ {} is Element of K19((T))
DD is set
b is Element of K19((T))
b ` is Element of K19((T))
(T) \ b is set
D is set
(T) . D is set
D1 is Element of the carrier of T
D1 ` is Element of the carrier of T
(D1 `) ` is Element of the carrier of T
D1 is Element of the carrier of T
D1 ` is Element of the carrier of T
(T) . D1 is Element of bool (T)
(T) . D1 is Element of bool (T)
((T) . D1) ` is Element of K19((T))
(T) \ ((T) . D1) is set
(T) . (D1 `) is Element of bool (T)
(D1 `) ` is Element of the carrier of T
(T) . ((D1 `) `) is Element of bool (T)
{ H₂(b₁) where b₁ is Element of K19((T)) : b₁ in B } is set
{ (b₁ `) where b<sub>1</sub> is Element of K19((T)) : b<sub>1</sub> in B } is set
DD is set
b is Element of K19((T))
b ` is Element of K19((T))
(T) \ b is set
(b `) ` is Element of K19((T))
(T) \ (b `) is set
DD is set
b is Element of K19((T))
b ` is Element of K19((T))
(T) \ b is set
(b `) ` is Element of K19((T))
(T) \ (b `) is set
D is non empty final meet-closed join-closed Element of K19( the carrier of T)
B is set
dom (T) is non empty Element of K19( the carrier of T)
G is set
(T) . G is set
DD is Element of the carrier of T
DD ` 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
(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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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 one-to-one 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 strict 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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is set
T is set
c₃ is Element of K19( the carrier of (BL))
[#] (BL) is non empty non proper open closed Element of K19( the carrier of (BL))
p is Element of the carrier of BL
(BL) . p is Element of bool (BL)
c₃ ` is Element of K19( the carrier of (BL))
the carrier of (BL) \ c<sub>3</sub> is set
p ` is Element of the carrier of BL
(BL) . (p `) 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
(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<sub>1</sub> where b<sub>1</sub> is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b<sub>1</sub> is being_ultrafilter } is set
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 one-to-one 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 strict 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<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of (BL)) : ( b<sub>1</sub> is open & b<sub>1</sub> is closed ) } is set
T is set
the topology of (BL) is non empty Element of K19(K19( the carrier of (BL)))
{ (union b<sub>1</sub>) where b<sub>1</sub> is Element of K19(K19((BL))) : b<sub>1</sub> c= (BL) } is set
c<sub>3</sub> is Element of K19( the carrier of (BL))
c<sub>3</sub> ` is Element of K19( the carrier of (BL))
the carrier of (BL) \ c₃ is set
f is Element of K19(K19((BL)))
union f is Element of K19((BL))
p is Element of K19(K19((BL)))
union p is Element of K19((BL))
f \/ p is Element of K19(K19((BL)))
[#] (BL) is non empty non proper open closed Element of K19( the carrier of (BL))
c₃ \/ (c₃ `) is Element of K19( the carrier of (BL))
union (f \/ p) is Element of K19((BL))
Fin (f \/ p) is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin (f \/ p)
union Y is set
f /\ Y is finite Element of K19(K19((BL)))
(f \/ p) /\ Y is finite Element of K19(K19((BL)))
p /\ Y is finite Element of K19(K19((BL)))
(f /\ Y) \/ (p /\ Y) is finite Element of K19(K19((BL)))
D is set
(c<sub>3</sub> `) /\ c₃ is Element of K19( the carrier of (BL))
D /\ c₃ is Element of K19( the carrier of (BL))
union (f /\ Y) is Element of K19((BL))
Bottom BL is Element of the carrier of BL
(BL) . (Bottom BL) is Element of bool (BL)
D is non empty Element of K19(K19((BL)))
D is non empty Element of K19(K19((BL)))
union D is Element of K19((BL))
(union f) /\ (union Y) is Element of K19((BL))
id (BL) is Relation-like (BL) -defined (BL) -valued Function-like one-to-one non empty V14((BL)) quasi_total Element of K19(K20((BL),(BL)))
K20((BL),(BL)) is Relation-like non empty set
K19(K20((BL),(BL))) is non empty cup-closed diff-closed preBoolean set
dom (id (BL)) is non empty Element of K19((BL))
K19((BL)) is non empty cup-closed diff-closed preBoolean set
dom (BL) is non empty Element of K19( the carrier of BL)
(id (BL)) * (BL) is Relation-like the carrier of BL -defined (BL) -valued Function-like one-to-one Element of K19(K20( the carrier of BL,(BL)))
K20( the carrier of BL,(BL)) is Relation-like non empty set
K19(K20( the carrier of BL,(BL))) is non empty cup-closed diff-closed preBoolean set
(BL) " D is Element of K19( the carrier of BL)
card ((BL) " D) is V31() cardinal set
(id (BL)) " D is Element of K19((BL))
card ((id (BL)) " D) is V31() cardinal set
card D is non empty V31() cardinal set
Fin the carrier of BL is non empty cup-closed diff-closed preBoolean set
B is finite Element of Fin the carrier of BL
(BL) .: B is finite Element of Fin (bool (BL))
Fin (bool (BL)) is non empty cup-closed diff-closed preBoolean set
K20((bool (BL)),(bool (BL))) is Relation-like non empty set
K20(K20((bool (BL)),(bool (BL))),(bool (BL))) is Relation-like non empty set
K19(K20(K20((bool (BL)),(bool (BL))),(bool (BL)))) is non empty cup-closed diff-closed preBoolean set
G is Relation-like K20((bool (BL)),(bool (BL))) -defined bool (BL) -valued Function-like non empty V14(K20((bool (BL)),(bool (BL)))) quasi_total Element of K19(K20(K20((bool (BL)),(bool (BL))),(bool (BL))))
DD is Element of K19((BL))
DD is Element of K19((BL))
G . (DD,DD) is Element of bool (BL)
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . (DD,DD) is Element of bool (BL)
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . (DD,DD) is Element of K19((BL))
DD \/ DD is Element of K19((BL))
G . (DD,DD) is Element of K19((BL))
DD is Element of K19((BL))
DD is Element of K19((BL))
b is Element of K19((BL))
G . (DD,b) is Element of bool (BL)
[DD,b] is set
{DD,b} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,b},{DD}} is non empty finite V40() set
G . [DD,b] is set
G . (DD,(G . (DD,b))) is Element of bool (BL)
[DD,(G . (DD,b))] is set
{DD,(G . (DD,b))} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,(G . (DD,b))},{DD}} is non empty finite V40() set
G . [DD,(G . (DD,b))] is set
G . (DD,DD) is Element of bool (BL)
[DD,DD] is set
{DD,DD} is non empty finite set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . ((G . (DD,DD)),b) is Element of bool (BL)
[(G . (DD,DD)),b] is set
{(G . (DD,DD)),b} is non empty finite set
{(G . (DD,DD))} is non empty trivial finite 1 -element set
{{(G . (DD,DD)),b},{(G . (DD,DD))}} is non empty finite V40() set
G . [(G . (DD,DD)),b] is set
G . (DD,b) is Element of K19((BL))
G . (DD,(G . (DD,b))) is Element of K19((BL))
[DD,(G . (DD,b))] is set
{DD,(G . (DD,b))} is non empty finite set
{{DD,(G . (DD,b))},{DD}} is non empty finite V40() set
G . [DD,(G . (DD,b))] is set
DD \/ b is Element of K19((BL))
G . (DD,(DD \/ b)) is Element of K19((BL))
[DD,(DD \/ b)] is set
{DD,(DD \/ b)} is non empty finite set
{{DD,(DD \/ b)},{DD}} is non empty finite V40() set
G . [DD,(DD \/ b)] is set
DD \/ (DD \/ b) is Element of K19((BL))
DD \/ DD is Element of K19((BL))
(DD \/ DD) \/ b is Element of K19((BL))
G . ((DD \/ DD),b) is Element of K19((BL))
[(DD \/ DD),b] is set
{(DD \/ DD),b} is non empty finite set
{(DD \/ DD)} is non empty trivial finite 1 -element set
{{(DD \/ DD),b},{(DD \/ DD)}} is non empty finite V40() set
G . [(DD \/ DD),b] is set
G . (DD,DD) is Element of K19((BL))
G . ((G . (DD,DD)),b) is Element of K19((BL))
[(G . (DD,DD)),b] is set
{(G . (DD,DD)),b} is non empty finite set
{(G . (DD,DD))} is non empty trivial finite 1 -element set
{{(G . (DD,DD)),b},{(G . (DD,DD))}} is non empty finite V40() set
G . [(G . (DD,DD)),b] is set
DD is Element of K19((BL))
G . (DD,DD) is Element of bool (BL)
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
G . [DD,DD] is set
G . (DD,DD) is Element of K19((BL))
DD \/ DD is Element of K19((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 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
DD is Element of the carrier of BL
DD is Element of the carrier of BL
the L_join of BL . (DD,DD) is Element of the carrier of BL
[DD,DD] is set
{DD,DD} is non empty finite set
{DD} is non empty trivial finite 1 -element set
{{DD,DD},{DD}} is non empty finite V40() set
the L_join of BL . [DD,DD] is set
(BL) . ( the L_join of BL . (DD,DD)) is Element of bool (BL)
(BL) . DD is Element of bool (BL)
(BL) . DD is Element of bool (BL)
G . (((BL) . DD),((BL) . DD)) is Element of bool (BL)
[((BL) . DD),((BL) . DD)] is set
{((BL) . DD),((BL) . DD)} is non empty finite set
{((BL) . DD)} is non empty trivial finite 1 -element set
{{((BL) . DD),((BL) . DD)},{((BL) . DD)}} is non empty finite V40() set
G . [((BL) . DD),((BL) . DD)] is set
DD "\/" DD is Element of the carrier of BL
(BL) . (DD "\/" DD) is Element of bool (BL)
((BL) . DD) \/ ((BL) . DD) is Element of bool (BL)
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL, the carrier of BL))
K19(K20( the carrier of BL, the carrier of BL)) is non empty cup-closed diff-closed preBoolean set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL, the carrier of BL))
FinJoin B is Element of the carrier of BL
(BL) . (FinJoin B) is Element of bool (BL)
FinJoin (B,(id the carrier of BL)) is Element of the carrier of BL
(BL) . (FinJoin (B,(id the carrier of BL))) is Element of bool (BL)
the L_join of BL $$ (B,(id the carrier of BL)) is Element of the carrier of BL
(BL) . ( the L_join of BL $$ (B,(id the carrier of BL))) is Element of bool (BL)
(BL) * (id the carrier of BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))
G $$ (B,((BL) * (id the carrier of BL))) is Element of bool (BL)
G $$ (B,(BL)) is Element of bool (BL)
id (bool (BL)) is Relation-like bool (BL) -defined bool (BL) -valued Function-like one-to-one non empty V14( bool (BL)) quasi_total Element of K19(K20((bool (BL)),(bool (BL))))
K19(K20((bool (BL)),(bool (BL)))) is non empty cup-closed diff-closed preBoolean set
(id (bool (BL))) * (BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))
G $$ (B,((id (bool (BL))) * (BL))) is Element of bool (BL)
DD is finite Element of Fin (bool (BL))
G $$ (DD,(id (bool (BL)))) is Element of bool (BL)
{}. (bool (BL)) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V31() V35() finite finite-yielding V40() cardinal {} -element Element of Fin (bool (BL))
G $$ (({}. (bool (BL))),(id (bool (BL)))) is Element of bool (BL)
DD is non empty Element of K19(K19((BL)))
union DD is Element of K19((BL))
DD is finite Element of Fin (bool (BL))
G $$ (DD,(id (bool (BL)))) is Element of bool (BL)
b is Element of K19((BL))
{.b.} is non empty trivial finite 1 -element Element of Fin K19((BL))
Fin K19((BL)) is non empty cup-closed diff-closed preBoolean set
DD \/ {.b.} is non empty finite Element of Fin K19((BL))
G $$ ((DD \/ {.b.}),(id (bool (BL)))) is Element of bool (BL)
D is non empty Element of K19(K19((BL)))
union D is Element of K19((BL))
{b} is non empty trivial finite 1 -element set
DD \/ {b} is non empty finite set
(id (bool (BL))) . b is Element of bool (BL)
D1 is non empty Element of K19(K19((BL)))
(id (bool (BL))) . b is Element of bool (BL)
G . ((G $$ (DD,(id (bool (BL))))),((id (bool (BL))) . b)) is Element of bool (BL)
[(G $$ (DD,(id (bool (BL))))),((id (bool (BL))) . b)] is set
{(G $$ (DD,(id (bool (BL))))),((id (bool (BL))) . b)} is non empty finite set
{(G $$ (DD,(id (bool (BL)))))} is non empty trivial finite 1 -element set
{{(G $$ (DD,(id (bool (BL))))),((id (bool (BL))) . b)},{(G $$ (DD,(id (bool (BL)))))}} is non empty finite V40() set
G . [(G $$ (DD,(id (bool (BL))))),((id (bool (BL))) . b)] is set
G . ((G $$ (DD,(id (bool (BL))))),b) is Element of K19((BL))
[(G $$ (DD,(id (bool (BL))))),b] is set
{(G $$ (DD,(id (bool (BL))))),b} is non empty finite set
{{(G $$ (DD,(id (bool (BL))))),b},{(G $$ (DD,(id (bool (BL)))))}} is non empty finite V40() set
G . [(G $$ (DD,(id (bool (BL))))),b] is set
(G $$ (DD,(id (bool (BL))))) \/ b is Element of K19((BL))
D1 is non empty Element of K19(K19((BL)))
union D1 is Element of K19((BL))
(union D1) \/ b is Element of K19((BL))
union {b} is set
(union D1) \/ (union {b}) is 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 Relation-like Function-like one-to-one set
the carrier of BL is non empty non trivial set
(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(BL) is non empty strict TopSpace-like TopStruct
((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)))
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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is 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))))
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 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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
(BL) is Relation-like the carrier of BL -defined bool (BL) -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL,(bool (BL))))
T 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))))
rng T is non empty Element of K19((bool (BL)))
K19((bool (BL))) is non empty cup-closed diff-closed preBoolean set
(BL) is non empty set
rng (BL) is non empty Element of K19((bool (BL)))
K20( the carrier of BL, the carrier of (BL)) is Relation-like non empty set
K19(K20( the carrier of BL, the carrier of (BL))) is non empty cup-closed diff-closed preBoolean set
f is Relation-like the carrier of BL -defined the carrier of (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL, the carrier of (BL)))
p is Element of the carrier of BL
q is Element of the carrier of BL
p "\/" q 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 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 . (p,q) is Element of the carrier of BL
[p,q] is set
{p,q} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,q},{p}} is non empty finite V40() set
the L_join of BL . [p,q] is set
f . (p "\/" q) is Element of the carrier of (BL)
f . p is Element of the carrier of (BL)
f . q is Element of the carrier of (BL)
(f . p) \/ (f . q) is set
(f . p) "\/" (f . q) 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),(f . q)) is Element of the carrier of (BL)
[(f . p),(f . q)] is set
{(f . p),(f . q)} is non empty finite set
{(f . p)} is non empty trivial finite 1 -element set
{{(f . p),(f . q)},{(f . p)}} is non empty finite V40() set
the L_join of (BL) . [(f . p),(f . q)] is set
p "/\" q 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))
the L_meet of BL . (p,q) is Element of the carrier of BL
the L_meet of BL . [p,q] is set
f . (p "/\" q) is Element of the carrier of (BL)
(f . p) /\ (f . q) is set
(f . p) "/\" (f . q) 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 Element of K19(K20(K20( the carrier of (BL), the carrier of (BL)), the carrier of (BL)))
the L_meet of (BL) . ((f . p),(f . q)) is Element of the carrier of (BL)
the L_meet of (BL) . [(f . p),(f . q)] is 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 join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(BL) is non empty strict TopSpace-like TopStruct
((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)))
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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is 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))))
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 Relation-like the carrier of BL -defined the carrier of (BL) -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total Homomorphism of BL,(BL)
the carrier of BL is non empty non trivial set
rng (BL) is non empty Element of K19( the carrier of (BL))
K19( the carrier of (BL)) is non empty cup-closed diff-closed preBoolean set
(BL) is non empty 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₁ where b₁ is non empty final meet-closed join-closed Element of K19( the carrier of BL) : b₁ is being_ultrafilter } is set
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 one-to-one 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
the carrier of BL is non empty non trivial set
(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(BL) is non empty strict TopSpace-like TopStruct
((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)))
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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is 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))))
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
K20( the carrier of BL, the carrier of (BL)) is Relation-like non empty set
K19(K20( the carrier of BL, the carrier of (BL))) is non empty cup-closed diff-closed preBoolean set
(BL) is Relation-like the carrier of BL -defined the carrier of (BL) -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total Homomorphism of BL,(BL)
rng (BL) is non empty Element of K19( the carrier of (BL))
K19( the carrier of (BL)) is non empty cup-closed diff-closed preBoolean set
T is Relation-like the carrier of BL -defined the carrier of (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Element of K19(K20( the carrier of BL, 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 non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(BL) is non empty strict TopSpace-like TopStruct
((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)))
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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is 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))))
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 non trivial set
the carrier of (BL) is non empty set
(BL) is Relation-like the carrier of BL -defined the carrier of (BL) -valued Function-like one-to-one non empty V14( the carrier of BL) quasi_total onto bijective Homomorphism of BL,(BL)
T is Relation-like the carrier of BL -defined the carrier of (BL) -valued Function-like non empty V14( the carrier of BL) quasi_total Homomorphism of BL,(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 non empty strict TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
(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
(T) is non empty Element of K19(K19( the carrier of T))
the carrier of T is non empty 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₁ where b₁ is Element of K19( the carrier of T) : ( b₁ is open & b₁ is closed ) } is set
(T) is Relation-like K20((T),(T)) -defined (T) -valued Function-like non empty V14(K20((T),(T))) quasi_total Element of K19(K20(K20((T),(T)),(T)))
K20((T),(T)) is Relation-like non empty set
K20(K20((T),(T)),(T)) is Relation-like non empty set
K19(K20(K20((T),(T)),(T))) is non empty cup-closed diff-closed preBoolean set
(T) is Relation-like K20((T),(T)) -defined (T) -valued Function-like non empty V14(K20((T),(T))) quasi_total Element of K19(K20(K20((T),(T)),(T)))
LattStr(# (T),(T),(T) #) is non empty strict LattStr
(BL) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
((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)))
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₁ where b₁ is Element of K19( the carrier of (BL)) : ( b₁ is open & b₁ is closed ) } is 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))))
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