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