omega is set
K19(omega) is non empty set
{} is empty set
the empty set is empty set
1 is non empty set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
H is TopSpace-like TopStruct
the carrier of H is set
K19( the carrier of H) is non empty set
p9 is Element of K19( the carrier of H)
p9 ` is Element of K19( the carrier of H)
the carrier of H \ p9 is set
q9 is Element of K19( the carrier of H)
(p9 `) \/ q9 is Element of K19( the carrier of H)
Int ((p9 `) \/ q9) is open Element of K19( the carrier of H)
p9 /\ (Int ((p9 `) \/ q9)) is Element of K19( the carrier of H)
p9 /\ ((p9 `) \/ q9) is Element of K19( the carrier of H)
p9 /\ (p9 `) is Element of K19( the carrier of H)
p9 /\ q9 is Element of K19( the carrier of H)
(p9 /\ (p9 `)) \/ (p9 /\ q9) is Element of K19( the carrier of H)
{} \/ (p9 /\ q9) is set
H is TopSpace-like TopStruct
the carrier of H is set
K19( the carrier of H) is non empty set
p9 is Element of K19( the carrier of H)
p9 ` is Element of K19( the carrier of H)
the carrier of H \ p9 is set
q9 is Element of K19( the carrier of H)
(p9 `) \/ q9 is Element of K19( the carrier of H)
Int ((p9 `) \/ q9) is open Element of K19( the carrier of H)
r is Element of K19( the carrier of H)
p9 /\ r is Element of K19( the carrier of H)
r \/ (p9 `) is Element of K19( the carrier of H)
(p9 /\ r) \/ (p9 `) is Element of K19( the carrier of H)
p9 \/ (p9 `) is Element of K19( the carrier of H)
(p9 \/ (p9 `)) /\ (r \/ (p9 `)) is Element of K19( the carrier of H)
[#] H is non proper open closed dense Element of K19( the carrier of H)
([#] H) /\ (r \/ (p9 `)) is Element of K19( the carrier of H)
q9 \/ (p9 `) is Element of K19( the carrier of H)
Int r is open Element of K19( the carrier of H)
H is TopStruct
the topology of H is Element of K19(K19( the carrier of H))
the carrier of H is set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
H is TopSpace-like TopStruct
(H) is Element of K19(K19( the carrier of H))
the carrier of H is set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
H is non empty TopSpace-like TopStruct
the carrier of H is non empty set
K19( the carrier of H) is non empty set
(H) is non empty Element of K19(K19( the carrier of H))
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
p9 is Element of (H)
q9 is Element of (H)
p9 \/ q9 is set
A is Element of K19( the carrier of H)
r is Element of K19( the carrier of H)
p9 \/ q9 is Element of K19( the carrier of H)
p9 /\ q9 is set
A is Element of K19( the carrier of H)
r is Element of K19( the carrier of H)
p9 /\ q9 is Element of K19( the carrier of H)
H is non empty TopSpace-like TopStruct
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
H is non empty TopSpace-like TopStruct
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of LattStr(# (H),(H),(H) #) is non empty set
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) is Relation-like K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)) -defined the carrier of LattStr(# (H),(H),(H) #) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #)))
K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)) is non empty set
K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #)) is non empty set
K19(K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #))) is non empty set
the L_join of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
r \/ q9 is set
r "\/" q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (r,q9) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) is Relation-like K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)) -defined the carrier of LattStr(# (H),(H),(H) #) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #)))
the L_meet of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "/\" r) "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . ((q9 "/\" r),r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "/\" r) \/ r is set
q9 /\ r is set
(q9 /\ r) \/ r is set
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" (q9 "\/" r) is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,(q9 "\/" r)) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 /\ (q9 "\/" r) is set
q9 \/ r is set
q9 /\ (q9 \/ r) is set
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
A is Element of the carrier of LattStr(# (H),(H),(H) #)
r "/\" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (r,A) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" (r "/\" A) is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,(r "/\" A)) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 /\ (r "/\" A) is set
r /\ A is set
q9 /\ (r /\ A) is set
q9 /\ r is set
(q9 /\ r) /\ A is set
q9 "/\" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "/\" r) /\ A is set
(q9 "/\" r) "/\" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . ((q9 "/\" r),A) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
r /\ q9 is set
r "/\" q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (r,q9) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
A is Element of the carrier of LattStr(# (H),(H),(H) #)
r "\/" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (r,A) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "\/" (r "\/" A) is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (q9,(r "\/" A)) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 \/ (r "\/" A) is set
r \/ A is set
q9 \/ (r \/ A) is set
q9 \/ r is set
(q9 \/ r) \/ A is set
q9 "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "\/" r) \/ A is set
(q9 "\/" r) "\/" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . ((q9 "\/" r),A) is Element of the carrier of LattStr(# (H),(H),(H) #)
H is non empty TopSpace-like TopStruct
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
r is non empty TopSpace-like TopStruct
(r) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(r) is non empty Element of K19(K19( the carrier of r))
the carrier of r is non empty set
K19( the carrier of r) is non empty set
K19(K19( the carrier of r)) is non empty set
the topology of r is non empty Element of K19(K19( the carrier of r))
(r) is Relation-like K20((r),(r)) -defined (r) -valued Function-like quasi_total Element of K19(K20(K20((r),(r)),(r)))
K20((r),(r)) is non empty set
K20(K20((r),(r)),(r)) is non empty set
K19(K20(K20((r),(r)),(r))) is non empty set
(r) is Relation-like K20((r),(r)) -defined (r) -valued Function-like quasi_total Element of K19(K20(K20((r),(r)),(r)))
LattStr(# (r),(r),(r) #) is non empty strict LattStr
the carrier of (r) is non empty set
p9 is Element of the carrier of (H)
q9 is Element of the carrier of (H)
p9 "\/" q9 is Element of the carrier of (H)
the L_join of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_join of (H) . (p9,q9) is Element of the carrier of (H)
p9 \/ q9 is set
A is Element of the carrier of (r)
x is Element of the carrier of (r)
A "/\" x is Element of the carrier of (r)
the L_meet of (r) is Relation-like K20( the carrier of (r), the carrier of (r)) -defined the carrier of (r) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (r), the carrier of (r)), the carrier of (r)))
K20( the carrier of (r), the carrier of (r)) is non empty set
K20(K20( the carrier of (r), the carrier of (r)), the carrier of (r)) is non empty set
K19(K20(K20( the carrier of (r), the carrier of (r)), the carrier of (r))) is non empty set
the L_meet of (r) . (A,x) is Element of the carrier of (r)
A /\ x is set
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
p9 is Element of the carrier of (H)
q9 is Element of the carrier of (H)
p9 "\/" q9 is Element of the carrier of (H)
the L_join of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_join of (H) . (p9,q9) is Element of the carrier of (H)
p9 \/ q9 is set
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
p9 is Element of the carrier of (H)
q9 is Element of the carrier of (H)
r is Element of (H)
A is Element of (H)
(H,r,A) is Element of (H)
p9 "\/" q9 is Element of the carrier of (H)
the L_join of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_join of (H) . (p9,q9) is Element of the carrier of (H)
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
q9 is Element of the carrier of (H)
r is Element of the carrier of (H)
A is Element of (H)
A ` is Element of K19( the carrier of H)
the carrier of H \ A is set
x is Element of (H)
(A `) \/ x is Element of K19( the carrier of H)
Int ((A `) \/ x) is open Element of K19( the carrier of H)
x9 is Element of (H)
C is Element of the carrier of (H)
q9 "/\" C is Element of the carrier of (H)
the L_meet of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_meet of (H) . (q9,C) is Element of the carrier of (H)
q9 "/\" C is Element of the carrier of (H)
(H,A,x9) is Element of (H)
A /\ C is Element of K19( the carrier of H)
X is Element of the carrier of (H)
q9 "/\" X is Element of the carrier of (H)
the L_meet of (H) . (q9,X) is Element of the carrier of (H)
Y is Element of (H)
p9 is Element of K19( the carrier of H)
q9 "/\" X is Element of the carrier of (H)
A /\ p9 is Element of K19( the carrier of H)
(H,A,Y) is Element of (H)
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
Bottom (H) is Element of the carrier of (H)
the carrier of (H) is non empty set
q9 is Element of the carrier of (H)
r is Element of the carrier of (H)
q9 "/\" r is Element of the carrier of (H)
the L_meet of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_meet of (H) . (q9,r) is Element of the carrier of (H)
q9 /\ r is set
r "/\" q9 is Element of the carrier of (H)
the L_meet of (H) . (r,q9) is Element of the carrier of (H)
r is Element of the carrier of (H)
q9 "/\" r is Element of the carrier of (H)
the L_meet of (H) . (q9,r) is Element of the carrier of (H)
A is Element of the carrier of (H)
A "/\" q9 is Element of the carrier of (H)
the L_meet of (H) . (A,q9) is Element of the carrier of (H)
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
p9 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
H is non empty TopSpace-like TopStruct
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
(H) is non empty Element of K19(K19( the carrier of H))
the carrier of H is non empty set
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
the topology of H is non empty Element of K19(K19( the carrier of H))
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
Top (H) is Element of the carrier of (H)
the carrier of (H) is non empty set
r is Element of the carrier of (H)
q9 is Element of the carrier of (H)
q9 "\/" r is Element of the carrier of (H)
the L_join of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_join of (H) . (q9,r) is Element of the carrier of (H)
A is Element of (H)
the carrier of H \/ A is non empty set
r "\/" q9 is Element of the carrier of (H)
the L_join of (H) . (r,q9) is Element of the carrier of (H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
(H) is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
p9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
q9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
q9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
(H) is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( b1 in (H) & a1 in b1 ) } is set
p9 is Relation-like Function-like set
dom p9 is set
q9 is Element of the carrier of H
p9 . q9 is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( b1 in (H) & q9 in b1 ) } is set
p9 is Relation-like Function-like set
dom p9 is set
q9 is Relation-like Function-like set
dom q9 is set
r is set
p9 . r is set
A is Element of the carrier of H
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( b1 in (H) & A in b1 ) } is set
q9 . r is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
(H) is Relation-like Function-like set
(H) is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
p9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
q9 is Element of the carrier of H
(H) . q9 is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( b1 in (H) & q9 in b1 ) } is set
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
(H) is Relation-like Function-like set
K19( the carrier of H) is non empty set
p9 is Element of the carrier of H
(H) . p9 is set
q9 is set
(H) is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( b1 in (H) & p9 in b1 ) } is set
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is Relation-like Function-like set
rng (H) is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is set
(H) is Relation-like Function-like set
rng (H) is set
dom (H) is set
the carrier of H is non empty set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like set
rng (H) is set
the carrier of H is non empty set
p9 is set
dom (H) is set
q9 is set
(H) . q9 is set
r is Element of the carrier of H
A is Element of the carrier of H
(H) . A is set
q9 is Element of the carrier of H
(H) . q9 is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
(H) is Relation-like Function-like set
p9 is Element of the carrier of H
(H) . p9 is set
q9 is Element of the carrier of H
p9 "\/" q9 is Element of the carrier of H
the L_join of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_join of H . (p9,q9) is Element of the carrier of H
(H) . (p9 "\/" q9) is set
(H) . q9 is set
((H) . p9) \/ ((H) . q9) is set
x is set
K19( the carrier of H) is non empty set
x9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
A is set
x is non empty final meet-closed join-closed Element of K19( the carrier of H)
x9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
x is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
(H) is Relation-like Function-like set
p9 is Element of the carrier of H
(H) . p9 is set
q9 is Element of the carrier of H
p9 "/\" q9 is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_meet of H . (p9,q9) is Element of the carrier of H
(H) . (p9 "/\" q9) is set
(H) . q9 is set
((H) . p9) /\ ((H) . q9) is set
x is set
K19( the carrier of H) is non empty set
x9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
A is set
x is non empty final meet-closed join-closed Element of K19( the carrier of H)
x9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
x is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
p9 is Element of the carrier of H
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : p9 in b1 } is set
K19(K19( the carrier of H)) is non empty set
bool the carrier of H is non empty Element of K19(K19( the carrier of H))
r is set
A is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
p9 is Element of the carrier of H
(H,p9) is Element of K19(K19( the carrier of H))
K19( the carrier of H) is non empty set
K19(K19( the carrier of H)) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : p9 in b1 } is set
<.p9.) is non empty final meet-closed join-closed Element of K19( the carrier of H)
{ b1 where b1 is Element of the carrier of H : p9 [= b1 } is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
p9 is Element of the carrier of H
(H,p9) is non empty Element of K19(K19( the carrier of H))
K19(K19( the carrier of H)) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : p9 in b1 } is set
q9 is set
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
p9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
q9 is Element of the carrier of H
(H,q9) is non empty Element of K19(K19( the carrier of H))
K19(K19( the carrier of H)) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : q9 in b1 } is set
r is Element of the carrier of H
(H,r) is non empty Element of K19(K19( the carrier of H))
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : r in b1 } is set
(H,q9) \ (H,r) is Element of K19(K19( the carrier of H))
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
p9 is Element of the carrier of H
(H,p9) is non empty Element of K19(K19( the carrier of H))
K19(K19( the carrier of H)) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : p9 in b1 } is set
q9 is Element of the carrier of H
(H,q9) is non empty Element of K19(K19( the carrier of H))
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : q9 in b1 } is set
(H,p9) \ (H,q9) is Element of K19(K19( the carrier of H))
r is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
p9 is Element of the carrier of H
(H,p9) is non empty Element of K19(K19( the carrier of H))
K19(K19( the carrier of H)) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : p9 in b1 } is set
q9 is Element of the carrier of H
(H,q9) is non empty Element of K19(K19( the carrier of H))
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : q9 in b1 } is set
(H,p9) \ (H,q9) is Element of K19(K19( the carrier of H))
r is set
A is Element of K19(K19( the carrier of H))
union A is Element of K19( the carrier of H)
x is Element of K19( the carrier of H)
the Element of A is Element of A
C is set
X is Element of the carrier of H
C is non empty Element of K19( the carrier of H)
Y is Element of the carrier of H
X "/\" Y is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_meet of H . (X,Y) is Element of the carrier of H
p9 is set
q9 is set
p9 is set
x9 is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
p9 is Element of the carrier of H
<.p9.) is non empty final meet-closed join-closed Element of K19( the carrier of H)
{ b1 where b1 is Element of the carrier of H : p9 [= b1 } is set
(H,p9) is non empty Element of K19(K19( the carrier of H))
K19(K19( the carrier of H)) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : p9 in b1 } is set
q9 is Element of the carrier of H
(H,q9) is non empty Element of K19(K19( the carrier of H))
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : q9 in b1 } is set
(H,p9) \ (H,q9) is Element of K19(K19( the carrier of H))
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
(H) is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
p9 is Element of the carrier of H
q9 is Element of the carrier of H
(H,p9) is non empty Element of K19(K19( the carrier of H))
K19(K19( the carrier of H)) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : p9 in b1 } is set
(H,q9) is non empty Element of K19(K19( the carrier of H))
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : q9 in b1 } is set
(H,p9) \ (H,q9) is Element of K19(K19( the carrier of H))
A is set
A is set
x is non empty final meet-closed join-closed Element of K19( the carrier of H)
x9 is Element of the carrier of H
C is Element of the carrier of H
x9 "\/" C is Element of the carrier of H
the L_join of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_join of H . (x9,C) is Element of the carrier of H
<.C.) is non empty final meet-closed join-closed Element of K19( the carrier of H)
{ b1 where b1 is Element of the carrier of H : C [= b1 } is set
<.C.) \/ x is non empty Element of K19( the carrier of H)
<.(<.C.) \/ x).) is non empty final meet-closed join-closed Element of K19( the carrier of H)
<.x9.) is non empty final meet-closed join-closed Element of K19( the carrier of H)
{ b1 where b1 is Element of the carrier of H : x9 [= b1 } is set
<.x9.) \/ x is non empty Element of K19( the carrier of H)
<.(<.x9.) \/ x).) is non empty final meet-closed join-closed Element of K19( the carrier of H)
p9 is Element of the carrier of H
x9 "/\" p9 is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
the L_meet of H . (x9,p9) is Element of the carrier of H
q9 is Element of the carrier of H
C "/\" q9 is Element of the carrier of H
the L_meet of H . (C,q9) is Element of the carrier of H
p9 "/\" q9 is Element of the carrier of H
the L_meet of H . (p9,q9) is Element of the carrier of H
C "/\" (p9 "/\" q9) is Element of the carrier of H
the L_meet of H . (C,(p9 "/\" q9)) is Element of the carrier of H
x9 "/\" (p9 "/\" q9) is Element of the carrier of H
the L_meet of H . (x9,(p9 "/\" q9)) is Element of the carrier of H
(x9 "/\" (p9 "/\" q9)) "\/" (C "/\" (p9 "/\" q9)) is Element of the carrier of H
the L_join of H . ((x9 "/\" (p9 "/\" q9)),(C "/\" (p9 "/\" q9))) is Element of the carrier of H
(x9 "\/" C) "/\" (p9 "/\" q9) is Element of the carrier of H
the L_meet of H . ((x9 "\/" C),(p9 "/\" q9)) is Element of the carrier of H
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
K19( the carrier of H) is non empty set
(H) is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
p9 is Element of the carrier of H
q9 is Element of the carrier of H
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
A is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
(H) is Relation-like Function-like set
p9 is Element of the carrier of H
(H) . p9 is set
q9 is Element of the carrier of H
(H) . q9 is set
K19( the carrier of H) is non empty set
(H) is set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
A is non empty final meet-closed join-closed Element of K19( the carrier of H)
r is non empty final meet-closed join-closed Element of K19( the carrier of H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is Relation-like Function-like set
p9 is set
dom (H) is set
q9 is set
(H) . p9 is set
(H) . q9 is set
the carrier of H is non empty set
r is Element of the carrier of H
A is Element of the carrier of H
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
p9 is Element of (H)
q9 is Element of (H)
p9 \/ q9 is set
the carrier of H is non empty set
r is Element of the carrier of H
(H) . r is set
A is Element of the carrier of H
(H) . A is set
A "\/" r is Element of the carrier of H
the L_join of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_join of H . (A,r) is Element of the carrier of H
(H) . (A "\/" r) is set
p9 /\ q9 is set
the carrier of H is non empty set
r is Element of the carrier of H
(H) . r is set
A is Element of the carrier of H
(H) . A is set
A "/\" r is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_meet of H . (A,r) is Element of the carrier of H
(H) . (A "/\" r) is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of LattStr(# (H),(H),(H) #) is non empty set
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) is Relation-like K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)) -defined the carrier of LattStr(# (H),(H),(H) #) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #)))
K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)) is non empty set
K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #)) is non empty set
K19(K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #))) is non empty set
the L_join of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
r \/ q9 is set
r "\/" q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (r,q9) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) is Relation-like K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)) -defined the carrier of LattStr(# (H),(H),(H) #) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of LattStr(# (H),(H),(H) #), the carrier of LattStr(# (H),(H),(H) #)), the carrier of LattStr(# (H),(H),(H) #)))
the L_meet of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "/\" r) "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . ((q9 "/\" r),r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "/\" r) \/ r is set
q9 /\ r is set
(q9 /\ r) \/ r is set
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" (q9 "\/" r) is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,(q9 "\/" r)) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 /\ (q9 "\/" r) is set
q9 \/ r is set
q9 /\ (q9 \/ r) is set
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
A is Element of the carrier of LattStr(# (H),(H),(H) #)
r "/\" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (r,A) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" (r "/\" A) is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,(r "/\" A)) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 /\ (r "/\" A) is set
r /\ A is set
q9 /\ (r /\ A) is set
q9 /\ r is set
(q9 /\ r) /\ A is set
q9 "/\" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "/\" r) /\ A is set
(q9 "/\" r) "/\" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . ((q9 "/\" r),A) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "/\" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
r /\ q9 is set
r "/\" q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_meet of LattStr(# (H),(H),(H) #) . (r,q9) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 is Element of the carrier of LattStr(# (H),(H),(H) #)
r is Element of the carrier of LattStr(# (H),(H),(H) #)
A is Element of the carrier of LattStr(# (H),(H),(H) #)
r "\/" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (r,A) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 "\/" (r "\/" A) is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (q9,(r "\/" A)) is Element of the carrier of LattStr(# (H),(H),(H) #)
q9 \/ (r "\/" A) is set
r \/ A is set
q9 \/ (r \/ A) is set
q9 \/ r is set
(q9 \/ r) \/ A is set
q9 "\/" r is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . (q9,r) is Element of the carrier of LattStr(# (H),(H),(H) #)
(q9 "\/" r) \/ A is set
(q9 "\/" r) "\/" A is Element of the carrier of LattStr(# (H),(H),(H) #)
the L_join of LattStr(# (H),(H),(H) #) . ((q9 "\/" r),A) is Element of the carrier of LattStr(# (H),(H),(H) #)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
r is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(r) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(r) is non empty set
(r) is Relation-like Function-like one-to-one set
rng (r) is set
(r) is Relation-like K20((r),(r)) -defined (r) -valued Function-like quasi_total Element of K19(K20(K20((r),(r)),(r)))
K20((r),(r)) is non empty set
K20(K20((r),(r)),(r)) is non empty set
K19(K20(K20((r),(r)),(r))) is non empty set
(r) is Relation-like K20((r),(r)) -defined (r) -valued Function-like quasi_total Element of K19(K20(K20((r),(r)),(r)))
LattStr(# (r),(r),(r) #) is non empty strict LattStr
the carrier of (r) is non empty set
p9 is Element of the carrier of (H)
q9 is Element of the carrier of (H)
p9 "\/" q9 is Element of the carrier of (H)
the L_join of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_join of (H) . (p9,q9) is Element of the carrier of (H)
p9 \/ q9 is set
A is Element of the carrier of (r)
x is Element of the carrier of (r)
A "/\" x is Element of the carrier of (r)
the L_meet of (r) is Relation-like K20( the carrier of (r), the carrier of (r)) -defined the carrier of (r) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (r), the carrier of (r)), the carrier of (r)))
K20( the carrier of (r), the carrier of (r)) is non empty set
K20(K20( the carrier of (r), the carrier of (r)), the carrier of (r)) is non empty set
K19(K20(K20( the carrier of (r), the carrier of (r)), the carrier of (r))) is non empty set
the L_meet of (r) . (A,x) is Element of the carrier of (r)
A /\ x is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
p9 is Element of the carrier of (H)
q9 is Element of the carrier of (H)
p9 "\/" q9 is Element of the carrier of (H)
the L_join of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_join of (H) . (p9,q9) is Element of the carrier of (H)
p9 \/ q9 is set
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is Relation-like Function-like one-to-one set
the carrier of H is non empty set
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
dom (H) is set
K20( the carrier of H, the carrier of (H)) is non empty set
K19(K20( the carrier of H, the carrier of (H))) is non empty set
p9 is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like quasi_total Element of K19(K20( the carrier of H, the carrier of (H)))
q9 is Element of the carrier of H
r is Element of the carrier of H
q9 "\/" r is Element of the carrier of H
the L_join of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_join of H . (q9,r) is Element of the carrier of H
p9 . (q9 "\/" r) is Element of the carrier of (H)
p9 . q9 is Element of the carrier of (H)
p9 . r is Element of the carrier of (H)
(p9 . q9) \/ (p9 . r) is set
(p9 . q9) "\/" (p9 . r) is Element of the carrier of (H)
the L_join of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
K20( the carrier of (H), the carrier of (H)) is non empty set
K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)) is non empty set
K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H))) is non empty set
the L_join of (H) . ((p9 . q9),(p9 . r)) is Element of the carrier of (H)
q9 "/\" r is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
the L_meet of H . (q9,r) is Element of the carrier of H
p9 . (q9 "/\" r) is Element of the carrier of (H)
(p9 . q9) /\ (p9 . r) is set
(p9 . q9) "/\" (p9 . r) is Element of the carrier of (H)
the L_meet of (H) is Relation-like K20( the carrier of (H), the carrier of (H)) -defined the carrier of (H) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of (H), the carrier of (H)), the carrier of (H)))
the L_meet of (H) . ((p9 . q9),(p9 . r)) is Element of the carrier of (H)
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of H is non empty set
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
K20( the carrier of H, the carrier of (H)) is non empty set
K19(K20( the carrier of H, the carrier of (H))) is non empty set
(H) is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like one-to-one quasi_total Homomorphism of H,(H)
rng (H) is set
p9 is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like quasi_total Element of K19(K20( the carrier of H, the carrier of (H)))
H is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
(H) is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like one-to-one quasi_total bijective Homomorphism of H,(H)
the carrier of H is non empty set
the carrier of (H) 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 V90() Heyting implicative 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 set
K19(K19( the carrier of the non empty TopSpace-like TopStruct )) is non empty set
the topology of the non empty TopSpace-like TopStruct is non empty Element of K19(K19( the carrier of the non empty TopSpace-like TopStruct ))
( 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 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 non empty set
K20(K20(( the non empty TopSpace-like TopStruct ),( the non empty TopSpace-like TopStruct )),( the non empty TopSpace-like TopStruct )) is 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 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 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
Top ( the non empty TopSpace-like TopStruct ) is Element of the carrier of ( the non empty TopSpace-like TopStruct )
the carrier of ( the non empty TopSpace-like TopStruct ) is non empty set
Bottom ( the non empty TopSpace-like TopStruct ) is Element of the carrier of ( the non empty TopSpace-like TopStruct )
q9 is Element of the carrier of ( the non empty TopSpace-like TopStruct )
r is Element of the carrier of ( the non empty TopSpace-like TopStruct )
H 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 V90() Heyting implicative LattStr
the carrier of H is non empty non trivial set
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
(H) is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like one-to-one quasi_total bijective Homomorphism of H,(H)
Top H is Element of the carrier of H
(H) . (Top H) is Element of the carrier of (H)
(H) is set
K19( the carrier of H) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
p9 is set
q9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
p9 is set
q9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
H 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 V90() Heyting implicative LattStr
the carrier of H is non empty non trivial set
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
(H) is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like one-to-one quasi_total bijective Homomorphism of H,(H)
Bottom H is Element of the carrier of H
(H) . (Bottom H) is Element of the carrier of (H)
the Element of (H) . (Bottom H) is Element of (H) . (Bottom H)
K19( the carrier of H) is non empty set
q9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
H 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 V90() Heyting implicative LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is set
the carrier of H is non empty non trivial set
K19( the carrier of H) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
bool (H) is non empty Element of K19(K19((H)))
K19((H)) is non empty set
K19(K19((H))) is non empty set
p9 is set
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
(H) is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like one-to-one quasi_total bijective Homomorphism of H,(H)
q9 is Element of the carrier of H
(H) . q9 is Element of the carrier of (H)
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( b1 in (H) & q9 in b1 ) } is set
r is set
A is non empty final meet-closed join-closed Element of K19( the carrier of H)
H 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 V90() Heyting implicative LattStr
(H) is set
the carrier of H is non empty non trivial set
K19( the carrier of H) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
p9 is Element of the carrier of H
q9 is Element of the carrier of H
p9 is non empty final meet-closed join-closed Element of K19( the carrier of H)
H 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 V90() Heyting implicative LattStr
(H) is non empty set
the carrier of H is non empty non trivial set
K19( the carrier of H) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
K19((H)) is non empty set
{ (union b1) where b1 is Element of K19((H)) : verum } is set
bool (H) is non empty Element of K19(K19((H)))
K19((H)) is non empty set
K19(K19((H))) is non empty set
r is set
A is Element of K19((H))
union A is set
union (bool (H)) is Element of K19((H))
r is Element of K19(K19((H)))
TopStruct(# (H),r #) is non empty strict TopStruct
the carrier of TopStruct(# (H),r #) is non empty set
the topology of TopStruct(# (H),r #) is Element of K19(K19( the carrier of TopStruct(# (H),r #)))
K19( the carrier of TopStruct(# (H),r #)) is non empty set
K19(K19( the carrier of TopStruct(# (H),r #))) is non empty set
p9 is strict TopStruct
the carrier of p9 is set
the topology of p9 is Element of K19(K19( the carrier of p9))
K19( the carrier of p9) is non empty set
K19(K19( the carrier of p9)) is non empty set
q9 is strict TopStruct
the carrier of q9 is set
the topology of q9 is Element of K19(K19( the carrier of q9))
K19( the carrier of q9) is non empty set
K19(K19( the carrier of q9)) is non empty set
H 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 V90() Heyting implicative LattStr
(H) is strict TopStruct
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
K19((H)) is non empty set
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
the carrier of H is non empty non trivial set
(H) is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like one-to-one quasi_total bijective Homomorphism of H,(H)
Top H is Element of the carrier of H
(H) . (Top H) is Element of the carrier of (H)
{((H) . (Top H))} is non empty Element of K19( the carrier of (H))
K19( the carrier of (H)) is non empty set
the topology of (H) is Element of K19(K19( the carrier of (H)))
the carrier of (H) is set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
{ (union b1) where b1 is Element of K19((H)) : verum } is set
(H) is non empty set
K19( the carrier of H) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
p9 is Element of K19((H))
union p9 is set
r is Element of K19(K19( the carrier of (H)))
{ b1 where b1 is Element of K19((H)) : S1[b1] } is set
{ (union b1) where b1 is Element of K19((H)) : b1 in { b1 where b2 is Element of K19((H)) : S1[b1] } } is set
x9 is set
C is Element of K19((H))
union C is set
x9 is set
C is Element of K19((H))
union C is set
X is Element of K19((H))
union X is set
K19(K19((H))) is non empty set
x9 is Element of K19(K19((H)))
union x9 is Element of K19((H))
union (union x9) is set
union r is Element of K19( the carrier of (H))
r is Element of K19( the carrier of (H))
A is Element of K19( the carrier of (H))
r /\ A is Element of K19( the carrier of (H))
x is Element of K19((H))
union x is set
x9 is Element of K19((H))
union x9 is set
INTERSECTION (x,x9) is set
C is set
X is set
Y is set
X /\ Y is set
p9 is Element of the carrier of H
(H) . p9 is Element of the carrier of (H)
q9 is Element of the carrier of H
(H) . q9 is Element of the carrier of (H)
p9 "/\" q9 is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_meet of H . (p9,q9) is Element of the carrier of H
(H) . (p9 "/\" q9) is Element of the carrier of (H)
(union x) /\ (union x9) is set
C is Element of K19((H))
union C is set
H 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 V90() Heyting implicative LattStr
(H) is non empty strict TopSpace-like TopStruct
((H)) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
((H)) is non empty Element of K19(K19( the carrier of (H)))
the carrier of (H) is non empty set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
the topology of (H) is non empty Element of K19(K19( the carrier of (H)))
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
K20(((H)),((H))) is non empty set
K20(K20(((H)),((H))),((H))) is non empty set
K19(K20(K20(((H)),((H))),((H)))) is non empty set
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
LattStr(# ((H)),((H)),((H)) #) is non empty strict LattStr
the carrier of ((H)) is non empty set
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
K19((H)) is non empty set
{ (union b1) where b1 is Element of K19((H)) : verum } is set
H 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 V90() Heyting implicative LattStr
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
(H) is non empty strict TopSpace-like TopStruct
((H)) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
((H)) is non empty Element of K19(K19( the carrier of (H)))
the carrier of (H) is non empty set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
the topology of (H) is non empty Element of K19(K19( the carrier of (H)))
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
K20(((H)),((H))) is non empty set
K20(K20(((H)),((H))),((H))) is non empty set
K19(K20(K20(((H)),((H))),((H)))) is non empty set
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
LattStr(# ((H)),((H)),((H)) #) is non empty strict LattStr
the carrier of ((H)) is non empty set
p9 is set
K19((H)) is non empty set
{p9} is non empty set
r is Element of K19((H))
union r is set
{ (union b1) where b1 is Element of K19((H)) : verum } is set
H 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 V90() Heyting implicative LattStr
(H) is Relation-like Function-like one-to-one set
the carrier of H is non empty non trivial set
(H) is non empty strict TopSpace-like TopStruct
((H)) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
((H)) is non empty Element of K19(K19( the carrier of (H)))
the carrier of (H) is non empty set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
the topology of (H) is non empty Element of K19(K19( the carrier of (H)))
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
K20(((H)),((H))) is non empty set
K20(K20(((H)),((H))),((H))) is non empty set
K19(K20(K20(((H)),((H))),((H)))) is non empty set
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
LattStr(# ((H)),((H)),((H)) #) is non empty strict LattStr
the carrier of ((H)) is non empty set
(H) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(H) is non empty set
rng (H) is set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
K20((H),(H)) is non empty set
K20(K20((H),(H)),(H)) is non empty set
K19(K20(K20((H),(H)),(H))) is non empty set
(H) is Relation-like K20((H),(H)) -defined (H) -valued Function-like quasi_total Element of K19(K20(K20((H),(H)),(H)))
LattStr(# (H),(H),(H) #) is non empty strict LattStr
the carrier of (H) is non empty set
K20( the carrier of H, the carrier of (H)) is non empty set
K19(K20( the carrier of H, the carrier of (H))) is non empty set
(H) is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like one-to-one quasi_total bijective Homomorphism of H,(H)
K20( the carrier of H, the carrier of ((H))) is non empty set
K19(K20( the carrier of H, the carrier of ((H)))) is non empty set
q9 is Relation-like the carrier of H -defined the carrier of (H) -valued Function-like quasi_total Element of K19(K20( the carrier of H, the carrier of (H)))
r is Relation-like the carrier of H -defined the carrier of ((H)) -valued Function-like quasi_total Element of K19(K20( the carrier of H, the carrier of ((H))))
A is Element of the carrier of H
x is Element of the carrier of H
A "\/" x is Element of the carrier of H
the L_join of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_join of H . (A,x) is Element of the carrier of H
r . (A "\/" x) is Element of the carrier of ((H))
(H) . A is Element of the carrier of (H)
(H) . x is Element of the carrier of (H)
((H) . A) \/ ((H) . x) is set
r . A is Element of the carrier of ((H))
r . x is Element of the carrier of ((H))
(r . A) "\/" (r . x) is Element of the carrier of ((H))
the L_join of ((H)) is Relation-like K20( the carrier of ((H)), the carrier of ((H))) -defined the carrier of ((H)) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of ((H)), the carrier of ((H))), the carrier of ((H))))
K20( the carrier of ((H)), the carrier of ((H))) is non empty set
K20(K20( the carrier of ((H)), the carrier of ((H))), the carrier of ((H))) is non empty set
K19(K20(K20( the carrier of ((H)), the carrier of ((H))), the carrier of ((H)))) is non empty set
the L_join of ((H)) . ((r . A),(r . x)) is Element of the carrier of ((H))
A "/\" x is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
the L_meet of H . (A,x) is Element of the carrier of H
r . (A "/\" x) is Element of the carrier of ((H))
((H) . A) /\ ((H) . x) is set
(r . A) "/\" (r . x) is Element of the carrier of ((H))
the L_meet of ((H)) is Relation-like K20( the carrier of ((H)), the carrier of ((H))) -defined the carrier of ((H)) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of ((H)), the carrier of ((H))), the carrier of ((H))))
the L_meet of ((H)) . ((r . A),(r . x)) is Element of the carrier of ((H))
H 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 V90() Heyting implicative LattStr
the carrier of H is non empty non trivial set
(H) is non empty strict TopSpace-like TopStruct
((H)) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
((H)) is non empty Element of K19(K19( the carrier of (H)))
the carrier of (H) is non empty set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
the topology of (H) is non empty Element of K19(K19( the carrier of (H)))
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
K20(((H)),((H))) is non empty set
K20(K20(((H)),((H))),((H))) is non empty set
K19(K20(K20(((H)),((H))),((H)))) is non empty set
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
LattStr(# ((H)),((H)),((H)) #) is non empty strict LattStr
the carrier of ((H)) is non empty set
(H) is Relation-like the carrier of H -defined the carrier of ((H)) -valued Function-like one-to-one quasi_total Homomorphism of H,((H))
p9 is Element of the carrier of H
(H) . p9 is Element of the carrier of ((H))
q9 is Element of the carrier of H
p9 => q9 is Element of the carrier of H
(H) . (p9 => q9) is Element of the carrier of ((H))
(H) . q9 is Element of the carrier of ((H))
((H) . p9) => ((H) . q9) is Element of the carrier of ((H))
(H) is non empty set
(H) is Relation-like Function-like one-to-one set
rng (H) is set
K19((H)) is non empty set
{ (union b1) where b1 is Element of K19((H)) : verum } is set
r is Element of the carrier of ((H))
A is Element of K19((H))
union A is set
((H) . p9) "/\" r is Element of the carrier of ((H))
the L_meet of ((H)) is Relation-like K20( the carrier of ((H)), the carrier of ((H))) -defined the carrier of ((H)) -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of ((H)), the carrier of ((H))), the carrier of ((H))))
K20( the carrier of ((H)), the carrier of ((H))) is non empty set
K20(K20( the carrier of ((H)), the carrier of ((H))), the carrier of ((H))) is non empty set
K19(K20(K20( the carrier of ((H)), the carrier of ((H))), the carrier of ((H)))) is non empty set
the L_meet of ((H)) . (((H) . p9),r) is Element of the carrier of ((H))
((H) . p9) /\ (union A) is set
{((H) . p9)} is non empty Element of K19( the carrier of ((H)))
K19( the carrier of ((H))) is non empty set
INTERSECTION ({((H) . p9)},A) is set
union (INTERSECTION ({((H) . p9)},A)) is set
x is set
x9 is Element of the carrier of H
(H) . x9 is Element of the carrier of ((H))
((H) . p9) /\ x is set
((H) . p9) /\ ((H) . x9) is set
p9 "/\" x9 is Element of the carrier of H
the L_meet of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total commutative associative idempotent Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))
K20( the carrier of H, the carrier of H) is non empty set
K20(K20( the carrier of H, the carrier of H), the carrier of H) is non empty set
K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is non empty set
the L_meet of H . (p9,x9) is Element of the carrier of H
(H) . (p9 "/\" x9) is Element of the carrier of ((H))
p9 "/\" (p9 => q9) is Element of the carrier of H
the L_meet of H . (p9,(p9 => q9)) is Element of the carrier of H
(H) . (p9 "/\" (p9 => q9)) is Element of the carrier of ((H))
((H) . p9) "/\" ((H) . (p9 => q9)) is Element of the carrier of ((H))
the L_meet of ((H)) . (((H) . p9),((H) . (p9 => q9))) is Element of the carrier of ((H))
H 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 V90() Heyting implicative LattStr
(H) is non empty strict TopSpace-like TopStruct
((H)) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
((H)) is non empty Element of K19(K19( the carrier of (H)))
the carrier of (H) is non empty set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
the topology of (H) is non empty Element of K19(K19( the carrier of (H)))
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
K20(((H)),((H))) is non empty set
K20(K20(((H)),((H))),((H))) is non empty set
K19(K20(K20(((H)),((H))),((H)))) is non empty set
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
LattStr(# ((H)),((H)),((H)) #) is non empty strict LattStr
(H) is Relation-like the carrier of H -defined the carrier of ((H)) -valued Function-like one-to-one quasi_total Homomorphism of H,((H))
the carrier of H is non empty non trivial set
the carrier of ((H)) is non empty set
p9 is Element of the carrier of H
q9 is Element of the carrier of H
p9 => q9 is Element of the carrier of H
(H) . (p9 => q9) is Element of the carrier of ((H))
(H) . p9 is Element of the carrier of ((H))
(H) . q9 is Element of the carrier of ((H))
((H) . p9) => ((H) . q9) is Element of the carrier of ((H))
H 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 V90() Heyting implicative LattStr
(H) is non empty strict TopSpace-like TopStruct
((H)) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
((H)) is non empty Element of K19(K19( the carrier of (H)))
the carrier of (H) is non empty set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
the topology of (H) is non empty Element of K19(K19( the carrier of (H)))
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
K20(((H)),((H))) is non empty set
K20(K20(((H)),((H))),((H))) is non empty set
K19(K20(K20(((H)),((H))),((H)))) is non empty set
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
LattStr(# ((H)),((H)),((H)) #) is non empty strict LattStr
(H) is Relation-like the carrier of H -defined the carrier of ((H)) -valued Function-like one-to-one quasi_total Homomorphism of H,((H))
the carrier of H is non empty non trivial set
the carrier of ((H)) is non empty set
Top H is Element of the carrier of H
(H) . (Top H) is Element of the carrier of ((H))
(H) is non empty set
K19( the carrier of H) is non empty set
{ b1 where b1 is non empty final meet-closed join-closed Element of K19( the carrier of H) : ( not b1 = the carrier of H & b1 is prime ) } is set
Top ((H)) is Element of the carrier of ((H))
H 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 V90() Heyting implicative LattStr
(H) is non empty strict TopSpace-like TopStruct
((H)) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative LattStr
((H)) is non empty Element of K19(K19( the carrier of (H)))
the carrier of (H) is non empty set
K19( the carrier of (H)) is non empty set
K19(K19( the carrier of (H))) is non empty set
the topology of (H) is non empty Element of K19(K19( the carrier of (H)))
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
K20(((H)),((H))) is non empty set
K20(K20(((H)),((H))),((H))) is non empty set
K19(K20(K20(((H)),((H))),((H)))) is non empty set
((H)) is Relation-like K20(((H)),((H))) -defined ((H)) -valued Function-like quasi_total Element of K19(K20(K20(((H)),((H))),((H))))
LattStr(# ((H)),((H)),((H)) #) is non empty strict LattStr
(H) is Relation-like the carrier of H -defined the carrier of ((H)) -valued Function-like one-to-one quasi_total Homomorphism of H,((H))
the carrier of H is non empty non trivial set
the carrier of ((H)) is non empty set
Bottom H is Element of the carrier of H
(H) . (Bottom H) is Element of the carrier of ((H))
Bottom ((H)) is Element of the carrier of ((H))