:: OPENLATT semantic presentation

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

{ b

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

{ b

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

{ b

{ b

p9 is Relation-like Function-like set

dom p9 is set

q9 is Element of the carrier of H

p9 . q9 is set

{ b

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

{ b

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

{ b

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

{ b

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

{ b

{ b

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

{ b

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

{ b

<.p9.) is non empty final meet-closed join-closed Element of K19( the carrier of H)

{ b

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

{ b

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

{ b

r is Element of the carrier of H

(H,r) is non empty Element of K19(K19( the carrier of H))

{ b

(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

{ b

q9 is Element of the carrier of H

(H,q9) is non empty Element of K19(K19( the carrier of H))

{ b

(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

{ b

q9 is Element of the carrier of H

(H,q9) is non empty Element of K19(K19( the carrier of H))

{ b

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

{ b

(H,p9) is non empty Element of K19(K19( the carrier of H))

K19(K19( the carrier of H)) is non empty set

{ b

q9 is Element of the carrier of H

(H,q9) is non empty Element of K19(K19( the carrier of H))

{ b

(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

{ b

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

{ b

(H,q9) is non empty Element of K19(K19( the carrier of H))

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

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

{ b

(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 b

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 b

(H) is non empty set

K19( the carrier of H) is non empty set

{ b

p9 is Element of K19((H))

union p9 is set

r is Element of K19(K19( the carrier of (H)))

{ b

{ (union b

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 b

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 b

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)