:: LATTICE4 semantic presentation

K215() is Element of bool K211()
K211() is set
bool K211() is non empty set
omega is set
bool omega is non empty set
bool K215() is non empty set
{} is empty set
the empty set is empty set
1 is non empty set
{{},1} is non empty set
BL is set
AF is set
the Element of BL is Element of BL
A1 is set
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
<.BL.) is non empty final meet-closed join-closed Element of bool the carrier of BL
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is Element of the carrier of BL
A1 is Element of the carrier of BL
AF "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (AF,A1) is Element of the carrier of BL
A1 is Element of the carrier of BL
AF "\/" A1 is Element of the carrier of BL
the L_join of BL . (AF,A1) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty final meet-closed join-closed Element of bool the carrier of BL
A1 is non empty final meet-closed join-closed Element of bool the carrier of BL
AF \/ A1 is non empty Element of bool the carrier of BL
<.(AF \/ A1).) is non empty final meet-closed join-closed Element of bool the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty final meet-closed join-closed Element of bool the carrier of BL
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
<.A1.) is non empty final meet-closed join-closed Element of bool the carrier of BL
{ b₁ where b₁ is Element of the carrier of BL : A1 [= b₁ } is set
<.A1.) \/ AF is non empty Element of bool the carrier of BL
<.(<.A1.) \/ AF).) is non empty final meet-closed join-closed Element of bool the carrier of BL
{ b₁ where b₁ is Element of the carrier of BL : ex b₂, b₃ being Element of the carrier of BL st
( b₂ "/\" b₃ [= b₁ & b₂ in <.A1.) & b₃ in AF ) } is set
p is Element of the carrier of BL
q is Element of the carrier of BL
B is Element of the carrier of BL
q "/\" B is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (q,B) is Element of the carrier of BL
p is Element of the carrier of BL
q is Element of the carrier of BL
p "/\" q is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (p,q) is Element of the carrier of BL
A1 "/\" q is Element of the carrier of BL
the L_meet of BL . (A1,q) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of AF is non empty set
[: the carrier of BL, the carrier of AF:] is non empty set
bool [: the carrier of BL, the carrier of AF:] is non empty set
the Element of the carrier of AF is Element of the carrier of AF
A1 is Element of the carrier of BL
p is Element of the carrier of AF
q is Element of the carrier of BL
A1 is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of AF:]
p is Element of the carrier of BL
q is Element of the carrier of BL
p "\/" q is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (p,q) is Element of the carrier of BL
A1 . (p "\/" q) is Element of the carrier of AF
the Element of the carrier of AF "\/" the Element of the carrier of AF is Element of the carrier of AF
the L_join of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_join of AF . ( the Element of the carrier of AF, the Element of the carrier of AF) is Element of the carrier of AF
A1 . p is Element of the carrier of AF
(A1 . p) "\/" the Element of the carrier of AF is Element of the carrier of AF
the L_join of AF . ((A1 . p), the Element of the carrier of AF) is Element of the carrier of AF
A1 . q is Element of the carrier of AF
(A1 . p) "\/" (A1 . q) is Element of the carrier of AF
the L_join of AF . ((A1 . p),(A1 . q)) is Element of the carrier of AF
p "/\" q is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_meet of BL . (p,q) is Element of the carrier of BL
A1 . (p "/\" q) is Element of the carrier of AF
the Element of the carrier of AF "/\" the Element of the carrier of AF is Element of the carrier of AF
the L_meet of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
the L_meet of AF . ( the Element of the carrier of AF, the Element of the carrier of AF) is Element of the carrier of AF
(A1 . p) "/\" the Element of the carrier of AF is Element of the carrier of AF
the L_meet of AF . ((A1 . p), the Element of the carrier of AF) is Element of the carrier of AF
(A1 . p) "/\" (A1 . q) is Element of the carrier of AF
the L_meet of AF . ((A1 . p),(A1 . q)) is Element of the carrier of AF
p is Element of the carrier of BL
q is Element of the carrier of BL
p "\/" q is Element of the carrier of BL
the L_join of BL . (p,q) is Element of the carrier of BL
A1 . (p "\/" q) is Element of the carrier of AF
A1 . p is Element of the carrier of AF
A1 . q is Element of the carrier of AF
(A1 . p) "\/" (A1 . q) is Element of the carrier of AF
the L_join of AF . ((A1 . p),(A1 . q)) is Element of the carrier of AF
B is Element of the carrier of BL
B1 is Element of the carrier of BL
B "/\" B1 is Element of the carrier of BL
the L_meet of BL . (B,B1) is Element of the carrier of BL
A1 . (B "/\" B1) is Element of the carrier of AF
A1 . B is Element of the carrier of AF
A1 . B1 is Element of the carrier of AF
(A1 . B) "/\" (A1 . B1) is Element of the carrier of AF
the L_meet of AF . ((A1 . B),(A1 . B1)) is Element of the carrier of AF
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of AF is non empty set
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
p is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total (BL,AF)
p . A1 is Element of the carrier of AF
p . A1 is Element of the carrier of AF
(p . A1) "\/" (p . A1) is Element of the carrier of AF
the L_join of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_join of AF . ((p . A1),(p . A1)) is Element of the carrier of AF
A1 "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (A1,A1) is Element of the carrier of BL
p . (A1 "\/" A1) is Element of the carrier of AF
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of AF is non empty set
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
p is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total (BL,AF)
p . A1 is Element of the carrier of AF
p . A1 is Element of the carrier of AF
[: the carrier of BL, the carrier of AF:] is non empty set
bool [: the carrier of BL, the carrier of AF:] is non empty set
q is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of AF:]
q . A1 is Element of the carrier of AF
q . A1 is Element of the carrier of AF
(q . A1) "\/" (q . A1) is Element of the carrier of AF
the L_join of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_join of AF . ((q . A1),(q . A1)) is Element of the carrier of AF
A1 "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (A1,A1) is Element of the carrier of BL
q . (A1 "\/" A1) is Element of the carrier of AF
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of AF is non empty set
[: the carrier of BL, the carrier of AF:] is non empty set
bool [: the carrier of BL, the carrier of AF:] is non empty set
A1 is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of AF:]
A1 is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of AF:]
rng A1 is set
p is Element of the carrier of AF
q is set
A1 . q is set
p is Element of the carrier of AF
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
the carrier of AF is non empty set
LattRel BL is Relation-like set
LattRel AF is Relation-like set
p is Relation-like Function-like set
dom p is set
field (LattRel BL) is set
field (LattRel AF) is set
rng p is set
[: the carrier of BL, the carrier of AF:] is non empty set
bool [: the carrier of BL, the carrier of AF:] is non empty set
B is Element of the carrier of BL
B1 is Element of the carrier of BL
q is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of AF:]
B "\/" B1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (B,B1) is Element of the carrier of BL
q . (B "\/" B1) is Element of the carrier of AF
q . B is Element of the carrier of AF
q . B1 is Element of the carrier of AF
(q . B) "\/" (q . B1) is Element of the carrier of AF
the L_join of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_join of AF . ((q . B),(q . B1)) is Element of the carrier of AF
q is Element of the carrier of BL
B0 is Element of the carrier of BL
B0 "\/" q is Element of the carrier of BL
the L_join of BL . (B0,q) is Element of the carrier of BL
[B1,(B "\/" B1)] is Element of the carrier of [:BL,BL:]
[:BL,BL:] is strict LattStr
the carrier of [:BL,BL:] is set
{B1,(B "\/" B1)} is non empty set
{B1} is non empty set
{{B1,(B "\/" B1)},{B1}} is non empty set
[(q . B1),(q . (B "\/" B1))] is Element of the carrier of [:AF,AF:]
[:AF,AF:] is strict LattStr
the carrier of [:AF,AF:] is set
{(q . B1),(q . (B "\/" B1))} is non empty set
{(q . B1)} is non empty set
{{(q . B1),(q . (B "\/" B1))},{(q . B1)}} is non empty set
q . q is Element of the carrier of AF
q . (B0 "\/" q) is Element of the carrier of AF
c₁₁ is Element of the carrier of BL
q . c₁₁ is Element of the carrier of AF
[(q . B1),(q . c₁₁)] is Element of the carrier of [:AF,AF:]
{(q . B1),(q . c₁₁)} is non empty set
{{(q . B1),(q . c₁₁)},{(q . B1)}} is non empty set
[B1,c₁₁] is Element of the carrier of [:BL,BL:]
{B1,c₁₁} is non empty set
{{B1,c₁₁},{B1}} is non empty set
[(q . B),(q . c₁₁)] is Element of the carrier of [:AF,AF:]
{(q . B),(q . c₁₁)} is non empty set
{(q . B)} is non empty set
{{(q . B),(q . c₁₁)},{(q . B)}} is non empty set
[B,c₁₁] is Element of the carrier of [:BL,BL:]
{B,c₁₁} is non empty set
{B} is non empty set
{{B,c₁₁},{B}} is non empty set
[(B "\/" B1),c₁₁] is Element of the carrier of [:BL,BL:]
{(B "\/" B1),c₁₁} is non empty set
{(B "\/" B1)} is non empty set
{{(B "\/" B1),c₁₁},{(B "\/" B1)}} is non empty set
[(q . (B "\/" B1)),(q . c₁₁)] is Element of the carrier of [:AF,AF:]
{(q . (B "\/" B1)),(q . c₁₁)} is non empty set
{(q . (B "\/" B1))} is non empty set
{{(q . (B "\/" B1)),(q . c₁₁)},{(q . (B "\/" B1))}} is non empty set
[B,(B "\/" B1)] is Element of the carrier of [:BL,BL:]
{B,(B "\/" B1)} is non empty set
{{B,(B "\/" B1)},{B}} is non empty set
[(q . B),(q . (B "\/" B1))] is Element of the carrier of [:AF,AF:]
{(q . B),(q . (B "\/" B1))} is non empty set
{{(q . B),(q . (B "\/" B1))},{(q . B)}} is non empty set
q . B0 is Element of the carrier of AF
B "/\" B1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_meet of BL . (B,B1) is Element of the carrier of BL
q . (B "/\" B1) is Element of the carrier of AF
(q . B) "/\" (q . B1) is Element of the carrier of AF
the L_meet of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
the L_meet of AF . ((q . B),(q . B1)) is Element of the carrier of AF
B0 is Element of the carrier of BL
q is Element of the carrier of BL
B0 "/\" q is Element of the carrier of BL
the L_meet of BL . (B0,q) is Element of the carrier of BL
[(B "/\" B1),B1] is Element of the carrier of [:BL,BL:]
[:BL,BL:] is strict LattStr
the carrier of [:BL,BL:] is set
{(B "/\" B1),B1} is non empty set
{(B "/\" B1)} is non empty set
{{(B "/\" B1),B1},{(B "/\" B1)}} is non empty set
[(q . (B "/\" B1)),(q . B1)] is Element of the carrier of [:AF,AF:]
[:AF,AF:] is strict LattStr
the carrier of [:AF,AF:] is set
{(q . (B "/\" B1)),(q . B1)} is non empty set
{(q . (B "/\" B1))} is non empty set
{{(q . (B "/\" B1)),(q . B1)},{(q . (B "/\" B1))}} is non empty set
q . (B0 "/\" q) is Element of the carrier of AF
q . q is Element of the carrier of AF
c₁₁ is Element of the carrier of BL
q . c₁₁ is Element of the carrier of AF
[(q . c₁₁),(q . B1)] is Element of the carrier of [:AF,AF:]
{(q . c₁₁),(q . B1)} is non empty set
{(q . c₁₁)} is non empty set
{{(q . c₁₁),(q . B1)},{(q . c₁₁)}} is non empty set
[c₁₁,B1] is Element of the carrier of [:BL,BL:]
{c₁₁,B1} is non empty set
{c₁₁} is non empty set
{{c₁₁,B1},{c₁₁}} is non empty set
[(q . c₁₁),(q . B)] is Element of the carrier of [:AF,AF:]
{(q . c₁₁),(q . B)} is non empty set
{{(q . c₁₁),(q . B)},{(q . c₁₁)}} is non empty set
[c₁₁,B] is Element of the carrier of [:BL,BL:]
{c₁₁,B} is non empty set
{{c₁₁,B},{c₁₁}} is non empty set
[c₁₁,(B "/\" B1)] is Element of the carrier of [:BL,BL:]
{c₁₁,(B "/\" B1)} is non empty set
{{c₁₁,(B "/\" B1)},{c₁₁}} is non empty set
[(q . c₁₁),(q . (B "/\" B1))] is Element of the carrier of [:AF,AF:]
{(q . c₁₁),(q . (B "/\" B1))} is non empty set
{{(q . c₁₁),(q . (B "/\" B1))},{(q . c₁₁)}} is non empty set
[(B "/\" B1),B] is Element of the carrier of [:BL,BL:]
{(B "/\" B1),B} is non empty set
{{(B "/\" B1),B},{(B "/\" B1)}} is non empty set
[(q . (B "/\" B1)),(q . B)] is Element of the carrier of [:AF,AF:]
{(q . (B "/\" B1)),(q . B)} is non empty set
{{(q . (B "/\" B1)),(q . B)},{(q . (B "/\" B1))}} is non empty set
q . B0 is Element of the carrier of AF
B is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total (BL,AF)
LattRel BL is Relation-like set
LattRel AF is Relation-like set
p is Relation-like the carrier of BL -defined the carrier of AF -valued Function-like non empty V19( the carrier of BL) quasi_total (BL,AF)
field (LattRel BL) is set
q is set
B is set
[q,B] is set
{q,B} is non empty set
{q} is non empty set
{{q,B},{q}} is non empty set
p . q is set
p . B is set
[(p . q),(p . B)] is set
{(p . q),(p . B)} is non empty set
{(p . q)} is non empty set
{{(p . q),(p . B)},{(p . q)}} is non empty set
B1 is Element of the carrier of BL
B0 is Element of the carrier of BL
p . B1 is Element of the carrier of AF
p . B0 is Element of the carrier of AF
B1 is Element of the carrier of BL
p . B1 is Element of the carrier of AF
B0 is Element of the carrier of BL
p . B0 is Element of the carrier of AF
dom p is set
rng p is set
field (LattRel AF) is set
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of AF is non empty set
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is Element of bool the carrier of BL
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 "/\" A1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (A1,A1) is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (A1,A1) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty final meet-closed join-closed Element of bool the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
AF is Element of Fin the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (AF,(id BL)) is Element of the carrier of BL
FinMeet (AF,(id BL)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is Element of the carrier of BL
{.AF.} is non empty Element of Fin the carrier of BL
Fin the carrier of BL is preBoolean set
(BL,{.AF.}) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin ({.AF.},(id BL)) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL $$ ({.AF.},(id BL)) is Element of the carrier of BL
(id BL) . AF is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is Element of the carrier of BL
{.AF.} is non empty Element of Fin the carrier of BL
Fin the carrier of BL is preBoolean set
(BL,{.AF.}) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet ({.AF.},(id BL)) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL $$ ({.AF.},(id BL)) is Element of the carrier of BL
(id BL) . AF is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
the carrier of AF is non empty set
A1 is Relation-like the carrier of AF -defined the carrier of BL -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,BL)
A1 is Element of the carrier of BL
p is Element of the carrier of BL
q is Element of the carrier of BL
p "\/" q is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (p,q) is Element of the carrier of BL
A1 "/\" (p "\/" q) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_meet of BL . (A1,(p "\/" q)) is Element of the carrier of BL
A1 "/\" p is Element of the carrier of BL
the L_meet of BL . (A1,p) is Element of the carrier of BL
A1 "/\" q is Element of the carrier of BL
the L_meet of BL . (A1,q) is Element of the carrier of BL
(A1 "/\" p) "\/" (A1 "/\" q) is Element of the carrier of BL
the L_join of BL . ((A1 "/\" p),(A1 "/\" q)) is Element of the carrier of BL
B is Element of the carrier of AF
A1 . B is Element of the carrier of BL
B1 is Element of the carrier of AF
A1 . B1 is Element of the carrier of BL
B0 is Element of the carrier of AF
A1 . B0 is Element of the carrier of BL
p "\/" q is Element of the carrier of BL
A1 "/\" (p "\/" q) is Element of the carrier of BL
the L_meet of BL . (A1,(p "\/" q)) is Element of the carrier of BL
B0 "\/" B1 is Element of the carrier of AF
the L_join of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_join of AF . (B0,B1) is Element of the carrier of AF
A1 . (B0 "\/" B1) is Element of the carrier of BL
A1 "/\" (A1 . (B0 "\/" B1)) is Element of the carrier of BL
the L_meet of BL . (A1,(A1 . (B0 "\/" B1))) is Element of the carrier of BL
B "/\" (B0 "\/" B1) is Element of the carrier of AF
the L_meet of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
the L_meet of AF . (B,(B0 "\/" B1)) is Element of the carrier of AF
A1 . (B "/\" (B0 "\/" B1)) is Element of the carrier of BL
B "/\" B0 is Element of the carrier of AF
the L_meet of AF . (B,B0) is Element of the carrier of AF
B "/\" B1 is Element of the carrier of AF
the L_meet of AF . (B,B1) is Element of the carrier of AF
(B "/\" B0) "\/" (B "/\" B1) is Element of the carrier of AF
the L_join of AF . ((B "/\" B0),(B "/\" B1)) is Element of the carrier of AF
A1 . ((B "/\" B0) "\/" (B "/\" B1)) is Element of the carrier of BL
A1 . (B "/\" B0) is Element of the carrier of BL
A1 . (B "/\" B1) is Element of the carrier of BL
(A1 . (B "/\" B0)) "\/" (A1 . (B "/\" B1)) is Element of the carrier of BL
the L_join of BL . ((A1 . (B "/\" B0)),(A1 . (B "/\" B1))) is Element of the carrier of BL
A1 "/\" p is Element of the carrier of BL
(A1 "/\" p) "\/" (A1 . (B "/\" B1)) is Element of the carrier of BL
the L_join of BL . ((A1 "/\" p),(A1 . (B "/\" B1))) is Element of the carrier of BL
A1 "/\" q is Element of the carrier of BL
(A1 "/\" p) "\/" (A1 "/\" q) is Element of the carrier of BL
the L_join of BL . ((A1 "/\" p),(A1 "/\" q)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of AF is non empty set
A1 is Relation-like the carrier of AF -defined the carrier of BL -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,BL)
Bottom AF is Element of the carrier of AF
A1 . (Bottom AF) is Element of the carrier of BL
p is Element of the carrier of BL
q is Element of the carrier of AF
A1 . q is Element of the carrier of BL
(A1 . (Bottom AF)) "/\" p is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((A1 . (Bottom AF)),p) is Element of the carrier of BL
(Bottom AF) "/\" q is Element of the carrier of AF
the L_meet of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_meet of AF . ((Bottom AF),q) is Element of the carrier of AF
A1 . ((Bottom AF) "/\" q) is Element of the carrier of BL
p "/\" (A1 . (Bottom AF)) is Element of the carrier of BL
the L_meet of BL . (p,(A1 . (Bottom AF))) is Element of the carrier of BL
p is Element of the carrier of BL
(A1 . (Bottom AF)) "/\" p is Element of the carrier of BL
the L_meet of BL . ((A1 . (Bottom AF)),p) is Element of the carrier of BL
q is Element of the carrier of BL
q "/\" (A1 . (Bottom AF)) is Element of the carrier of BL
the L_meet of BL . (q,(A1 . (Bottom AF))) is Element of the carrier of BL
Bottom BL is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Element of Fin the carrier of BL
A1 is Element of the carrier of BL
{.A1.} is non empty Element of Fin the carrier of BL
AF \/ {.A1.} is non empty Element of Fin the carrier of BL
A1 is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin ((AF \/ {.A1.}),A1) is Element of the carrier of BL
FinJoin (AF,A1) is Element of the carrier of BL
A1 . A1 is Element of the carrier of BL
(FinJoin (AF,A1)) "\/" (A1 . A1) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((FinJoin (AF,A1)),(A1 . A1)) is Element of the carrier of BL
the L_join of BL $$ ((AF \/ {.A1.}),A1) is Element of the carrier of BL
the L_join of BL $$ (AF,A1) is Element of the carrier of BL
( the L_join of BL $$ (AF,A1)) "\/" (A1 . A1) is Element of the carrier of BL
the L_join of BL . (( the L_join of BL $$ (AF,A1)),(A1 . A1)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
AF is Element of Fin the carrier of BL
(BL,AF) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (AF,(id BL)) is Element of the carrier of BL
A1 is Element of the carrier of BL
{.A1.} is non empty Element of Fin the carrier of BL
AF \/ {.A1.} is non empty Element of Fin the carrier of BL
(BL,(AF \/ {.A1.})) is Element of the carrier of BL
FinJoin ((AF \/ {.A1.}),(id BL)) is Element of the carrier of BL
(BL,AF) "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((BL,AF),A1) is Element of the carrier of BL
(id BL) . A1 is Element of the carrier of BL
(FinJoin (AF,(id BL))) "\/" ((id BL) . A1) is Element of the carrier of BL
the L_join of BL . ((FinJoin (AF,(id BL))),((id BL) . A1)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
AF is Element of Fin the carrier of BL
(BL,AF) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (AF,(id BL)) is Element of the carrier of BL
A1 is Element of Fin the carrier of BL
(BL,A1) is Element of the carrier of BL
FinJoin (A1,(id BL)) is Element of the carrier of BL
(BL,AF) "\/" (BL,A1) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((BL,AF),(BL,A1)) is Element of the carrier of BL
AF \/ A1 is Element of Fin the carrier of BL
(BL,(AF \/ A1)) is Element of the carrier of BL
FinJoin ((AF \/ A1),(id BL)) is Element of the carrier of BL
the L_join of BL $$ ((AF \/ A1),(id BL)) is Element of the carrier of BL
the L_join of BL $$ (AF,(id BL)) is Element of the carrier of BL
the L_join of BL $$ (A1,(id BL)) is Element of the carrier of BL
( the L_join of BL $$ (AF,(id BL))) "\/" ( the L_join of BL $$ (A1,(id BL))) is Element of the carrier of BL
the L_join of BL . (( the L_join of BL $$ (AF,(id BL))),( the L_join of BL $$ (A1,(id BL)))) is Element of the carrier of BL
(BL,AF) "\/" ( the L_join of BL $$ (A1,(id BL))) is Element of the carrier of BL
the L_join of BL . ((BL,AF),( the L_join of BL $$ (A1,(id BL)))) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of BL is non empty set
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
{}. the carrier of BL is empty Element of Fin the carrier of BL
Fin the carrier of BL is preBoolean set
Bottom BL is Element of the carrier of BL
AF is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (({}. the carrier of BL),AF) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL $$ (({}. the carrier of BL),AF) is Element of the carrier of BL
the_unity_wrt the L_join of BL is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of BL is non empty set
{}. the carrier of BL is empty Element of Fin the carrier of BL
Fin the carrier of BL is preBoolean set
(BL,({}. the carrier of BL)) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (({}. the carrier of BL),(id BL)) is Element of the carrier of BL
Bottom BL is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
Bottom BL is Element of the carrier of BL
Fin the carrier of BL is preBoolean set
AF is meet-closed join-closed Element of bool the carrier of BL
A1 is Element of Fin the carrier of BL
(BL,A1) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (A1,(id BL)) is Element of the carrier of BL
A1 is Element of the carrier of BL
{.A1.} is non empty Element of Fin the carrier of BL
A1 \/ {.A1.} is non empty Element of Fin the carrier of BL
(BL,(A1 \/ {.A1.})) is Element of the carrier of BL
FinJoin ((A1 \/ {.A1.}),(id BL)) is Element of the carrier of BL
{A1} is non empty set
A1 \/ {A1} is non empty set
(BL,A1) "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((BL,A1),A1) is Element of the carrier of BL
{}. the carrier of BL is empty Element of Fin the carrier of BL
(BL,({}. the carrier of BL)) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (({}. the carrier of BL),(id BL)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of AF is non empty set
A1 is Relation-like the carrier of AF -defined the carrier of BL -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,BL)
Top AF is Element of the carrier of AF
A1 . (Top AF) is Element of the carrier of BL
p is Element of the carrier of BL
q is Element of the carrier of AF
A1 . q is Element of the carrier of BL
(A1 . (Top AF)) "\/" p is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((A1 . (Top AF)),p) is Element of the carrier of BL
(Top AF) "\/" q is Element of the carrier of AF
the L_join of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_join of AF . ((Top AF),q) is Element of the carrier of AF
A1 . ((Top AF) "\/" q) is Element of the carrier of BL
p "\/" (A1 . (Top AF)) is Element of the carrier of BL
the L_join of BL . (p,(A1 . (Top AF))) is Element of the carrier of BL
p is Element of the carrier of BL
(A1 . (Top AF)) "\/" p is Element of the carrier of BL
the L_join of BL . ((A1 . (Top AF)),p) is Element of the carrier of BL
q is Element of the carrier of BL
q "\/" (A1 . (Top AF)) is Element of the carrier of BL
the L_join of BL . (q,(A1 . (Top AF))) is Element of the carrier of BL
Top BL is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of BL is non empty set
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
{}. the carrier of BL is empty Element of Fin the carrier of BL
Fin the carrier of BL is preBoolean set
Top BL is Element of the carrier of BL
AF is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (({}. the carrier of BL),AF) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL $$ (({}. the carrier of BL),AF) is Element of the carrier of BL
the_unity_wrt the L_meet of BL is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of BL is non empty set
{}. the carrier of BL is empty Element of Fin the carrier of BL
Fin the carrier of BL is preBoolean set
(BL,({}. the carrier of BL)) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (({}. the carrier of BL),(id BL)) is Element of the carrier of BL
Top BL is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Element of Fin the carrier of BL
A1 is Element of the carrier of BL
{.A1.} is non empty Element of Fin the carrier of BL
AF \/ {.A1.} is non empty Element of Fin the carrier of BL
A1 is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet ((AF \/ {.A1.}),A1) is Element of the carrier of BL
FinMeet (AF,A1) is Element of the carrier of BL
A1 . A1 is Element of the carrier of BL
(FinMeet (AF,A1)) "/\" (A1 . A1) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((FinMeet (AF,A1)),(A1 . A1)) is Element of the carrier of BL
the L_meet of BL $$ ((AF \/ {.A1.}),A1) is Element of the carrier of BL
the L_meet of BL $$ (AF,A1) is Element of the carrier of BL
( the L_meet of BL $$ (AF,A1)) "/\" (A1 . A1) is Element of the carrier of BL
the L_meet of BL . (( the L_meet of BL $$ (AF,A1)),(A1 . A1)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
AF is Element of Fin the carrier of BL
(BL,AF) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (AF,(id BL)) is Element of the carrier of BL
A1 is Element of the carrier of BL
{.A1.} is non empty Element of Fin the carrier of BL
AF \/ {.A1.} is non empty Element of Fin the carrier of BL
(BL,(AF \/ {.A1.})) is Element of the carrier of BL
FinMeet ((AF \/ {.A1.}),(id BL)) is Element of the carrier of BL
(BL,AF) "/\" A1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((BL,AF),A1) is Element of the carrier of BL
(id BL) . A1 is Element of the carrier of BL
(FinMeet (AF,(id BL))) "/\" ((id BL) . A1) is Element of the carrier of BL
the L_meet of BL . ((FinMeet (AF,(id BL))),((id BL) . A1)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Element of Fin the carrier of BL
A1 is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
A1 .: AF is Element of Fin the carrier of BL
A1 is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet ((A1 .: AF),A1) is Element of the carrier of BL
A1 * A1 is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (AF,(A1 * A1)) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL $$ ((A1 .: AF),A1) is Element of the carrier of BL
the L_meet of BL $$ (AF,(A1 * A1)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
AF is Element of Fin the carrier of BL
(BL,AF) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (AF,(id BL)) is Element of the carrier of BL
A1 is Element of Fin the carrier of BL
(BL,A1) is Element of the carrier of BL
FinMeet (A1,(id BL)) is Element of the carrier of BL
(BL,AF) "/\" (BL,A1) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((BL,AF),(BL,A1)) is Element of the carrier of BL
AF \/ A1 is Element of Fin the carrier of BL
(BL,(AF \/ A1)) is Element of the carrier of BL
FinMeet ((AF \/ A1),(id BL)) is Element of the carrier of BL
the L_meet of BL $$ ((AF \/ A1),(id BL)) is Element of the carrier of BL
the L_meet of BL $$ (AF,(id BL)) is Element of the carrier of BL
the L_meet of BL $$ (A1,(id BL)) is Element of the carrier of BL
( the L_meet of BL $$ (AF,(id BL))) "/\" ( the L_meet of BL $$ (A1,(id BL))) is Element of the carrier of BL
the L_meet of BL . (( the L_meet of BL $$ (AF,(id BL))),( the L_meet of BL $$ (A1,(id BL)))) is Element of the carrier of BL
(BL,AF) "/\" ( the L_meet of BL $$ (A1,(id BL))) is Element of the carrier of BL
the L_meet of BL . ((BL,AF),( the L_meet of BL $$ (A1,(id BL)))) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
Top BL is Element of the carrier of BL
Fin the carrier of BL is preBoolean set
AF is meet-closed join-closed Element of bool the carrier of BL
A1 is Element of Fin the carrier of BL
(BL,A1) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (A1,(id BL)) is Element of the carrier of BL
A1 is Element of the carrier of BL
{.A1.} is non empty Element of Fin the carrier of BL
A1 \/ {.A1.} is non empty Element of Fin the carrier of BL
(BL,(A1 \/ {.A1.})) is Element of the carrier of BL
FinMeet ((A1 \/ {.A1.}),(id BL)) is Element of the carrier of BL
{A1} is non empty set
A1 \/ {A1} is non empty set
(BL,A1) "/\" A1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((BL,A1),A1) is Element of the carrier of BL
{}. the carrier of BL is empty Element of Fin the carrier of BL
(BL,({}. the carrier of BL)) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (({}. the carrier of BL),(id BL)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
AF is Element of Fin the carrier of BL
A1 is Element of the carrier of BL
A1 is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
the L_meet of BL $$ (AF,A1) is Element of the carrier of BL
the L_join of BL . (( the L_meet of BL $$ (AF,A1)),A1) is Element of the carrier of BL
the L_join of BL [:] (A1,A1) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
the L_meet of BL $$ (AF,( the L_join of BL [:] (A1,A1))) is Element of the carrier of BL
B is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
the L_meet of BL $$ (AF,B) is Element of the carrier of BL
{}. the carrier of BL is empty Element of Fin the carrier of BL
FinMeet (({}. the carrier of BL),B) is Element of the carrier of BL
Top BL is Element of the carrier of BL
(Top BL) "\/" A1 is Element of the carrier of BL
the L_join of BL . ((Top BL),A1) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
AF is Element of Fin the carrier of BL
(BL,AF) is Element of the carrier of BL
FinMeet (AF,(id BL)) is Element of the carrier of BL
A1 is Element of the carrier of BL
(BL,AF) "\/" A1 is Element of the carrier of BL
the L_join of BL . ((BL,AF),A1) is Element of the carrier of BL
the L_join of BL [:] ((id BL),A1) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
( the L_join of BL [:] ((id BL),A1)) .: AF is Element of Fin the carrier of BL
(BL,(( the L_join of BL [:] ((id BL),A1)) .: AF)) is Element of the carrier of BL
FinMeet ((( the L_join of BL [:] ((id BL),A1)) .: AF),(id BL)) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_meet of BL $$ (AF,(id BL)) is Element of the carrier of BL
the L_join of BL . (( the L_meet of BL $$ (AF,(id BL))),A1) is Element of the carrier of BL
the L_meet of BL $$ (AF,( the L_join of BL [:] ((id BL),A1))) is Element of the carrier of BL
FinMeet (AF,( the L_join of BL [:] ((id BL),A1))) is Element of the carrier of BL
(id BL) * ( the L_join of BL [:] ((id BL),A1)) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (AF,((id BL) * ( the L_join of BL [:] ((id BL),A1)))) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative LattStr
the carrier of AF is non empty set
A1 is Relation-like the carrier of AF -defined the carrier of BL -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,BL)
A1 is Element of the carrier of AF
A1 . A1 is Element of the carrier of BL
p is Element of the carrier of AF
A1 => p is Element of the carrier of AF
A1 . (A1 => p) is Element of the carrier of BL
(A1 . A1) "/\" (A1 . (A1 => p)) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((A1 . A1),(A1 . (A1 => p))) is Element of the carrier of BL
A1 . p is Element of the carrier of BL
A1 "/\" (A1 => p) is Element of the carrier of AF
the L_meet of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_meet of AF . (A1,(A1 => p)) is Element of the carrier of AF
A1 . (A1 "/\" (A1 => p)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative LattStr
the carrier of AF is non empty set
A1 is Relation-like the carrier of AF -defined the carrier of BL -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,BL)
A1 is Element of the carrier of AF
A1 . A1 is Element of the carrier of BL
p is Element of the carrier of AF
A1 . p is Element of the carrier of BL
(A1 . A1) "/\" (A1 . p) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((A1 . A1),(A1 . p)) is Element of the carrier of BL
q is Element of the carrier of AF
A1 . q is Element of the carrier of BL
A1 => q is Element of the carrier of AF
A1 . (A1 => q) is Element of the carrier of BL
A1 "/\" p is Element of the carrier of AF
the L_meet of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_meet of AF . (A1,p) is Element of the carrier of AF
A1 . (A1 "/\" p) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative LattStr
the carrier of AF is non empty set
A1 is Relation-like the carrier of AF -defined the carrier of BL -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,BL)
A1 is Element of the carrier of BL
p is Element of the carrier of BL
q is Element of the carrier of AF
A1 . q is Element of the carrier of BL
B is Element of the carrier of AF
A1 . B is Element of the carrier of BL
q => B is Element of the carrier of AF
A1 . (q => B) is Element of the carrier of BL
B1 is Element of the carrier of BL
A1 "/\" B1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (A1,B1) is Element of the carrier of BL
A1 "/\" B1 is Element of the carrier of BL
B0 is Element of the carrier of BL
A1 "/\" B0 is Element of the carrier of BL
the L_meet of BL . (A1,B0) is Element of the carrier of BL
q is Element of the carrier of AF
A1 . q is Element of the carrier of BL
A1 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative LattStr
the carrier of A1 is non empty set
p is Relation-like the carrier of AF -defined the carrier of A1 -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,A1)
q is Element of the carrier of AF
p . q is Element of the carrier of A1
B1 is Element of the carrier of A1
(p . q) "/\" B1 is Element of the carrier of A1
the L_meet of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined the carrier of A1 -valued Function-like non empty V19([: the carrier of A1, the carrier of A1:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of A1, the carrier of A1:], the carrier of A1:]
[: the carrier of A1, the carrier of A1:] is non empty set
[:[: the carrier of A1, the carrier of A1:], the carrier of A1:] is non empty set
bool [:[: the carrier of A1, the carrier of A1:], the carrier of A1:] is non empty set
the L_meet of A1 . ((p . q),B1) is Element of the carrier of A1
B is Element of the carrier of AF
p . B is Element of the carrier of A1
q => B is Element of the carrier of AF
p . (q => B) is Element of the carrier of A1
B0 is Element of the carrier of AF
p . B0 is Element of the carrier of A1
(p . q) "/\" (p . (q => B)) is Element of the carrier of A1
the L_meet of A1 . ((p . q),(p . (q => B))) is Element of the carrier of A1
(p . q) => (p . B) is Element of the carrier of A1
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
Top BL is Element of the carrier of BL
the carrier of BL is non empty set
(Top BL) ` is Element of the carrier of BL
Bottom BL is Element of the carrier of BL
(Bottom BL) ` is Element of the carrier of BL
(Bottom BL) "\/" ((Bottom BL) `) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((Bottom BL),((Bottom BL) `)) is Element of the carrier of BL
((Bottom BL) "\/" ((Bottom BL) `)) ` is Element of the carrier of BL
((Bottom BL) `) ` is Element of the carrier of BL
((Bottom BL) `) "/\" (((Bottom BL) `) `) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_meet of BL . (((Bottom BL) `),(((Bottom BL) `) `)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
Bottom BL is Element of the carrier of BL
the carrier of BL is non empty set
(Bottom BL) ` is Element of the carrier of BL
Top BL is Element of the carrier of BL
(Top BL) ` is Element of the carrier of BL
(Top BL) "/\" ((Top BL) `) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((Top BL),((Top BL) `)) is Element of the carrier of BL
((Top BL) "/\" ((Top BL) `)) ` is Element of the carrier of BL
((Top BL) `) ` is Element of the carrier of BL
((Top BL) `) "\/" (((Top BL) `) `) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_join of BL . (((Top BL) `),(((Top BL) `) `)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented LattStr
the carrier of BL is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of AF is non empty set
A1 is Relation-like the carrier of AF -defined the carrier of BL -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,BL)
A1 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of A1 is non empty set
p is Relation-like the carrier of AF -defined the carrier of A1 -valued Function-like non empty V19( the carrier of AF) quasi_total (AF,A1)
q is Element of the carrier of AF
q ` is Element of the carrier of AF
p . (q `) is Element of the carrier of A1
p . q is Element of the carrier of A1
(p . (q `)) "/\" (p . q) is Element of the carrier of A1
the L_meet of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined the carrier of A1 -valued Function-like non empty V19([: the carrier of A1, the carrier of A1:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of A1, the carrier of A1:], the carrier of A1:]
[: the carrier of A1, the carrier of A1:] is non empty set
[:[: the carrier of A1, the carrier of A1:], the carrier of A1:] is non empty set
bool [:[: the carrier of A1, the carrier of A1:], the carrier of A1:] is non empty set
the L_meet of A1 . ((p . (q `)),(p . q)) is Element of the carrier of A1
(q `) "/\" q is Element of the carrier of AF
the L_meet of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
[: the carrier of AF, the carrier of AF:] is non empty set
[:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:] is non empty set
the L_meet of AF . ((q `),q) is Element of the carrier of AF
p . ((q `) "/\" q) is Element of the carrier of A1
Bottom AF is Element of the carrier of AF
p . (Bottom AF) is Element of the carrier of A1
Bottom A1 is Element of the carrier of A1
(p . (q `)) "\/" (p . q) is Element of the carrier of A1
the L_join of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined the carrier of A1 -valued Function-like non empty V19([: the carrier of A1, the carrier of A1:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of A1, the carrier of A1:], the carrier of A1:]
the L_join of A1 . ((p . (q `)),(p . q)) is Element of the carrier of A1
(q `) "\/" q is Element of the carrier of AF
the L_join of AF is Relation-like [: the carrier of AF, the carrier of AF:] -defined the carrier of AF -valued Function-like non empty V19([: the carrier of AF, the carrier of AF:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of AF, the carrier of AF:], the carrier of AF:]
the L_join of AF . ((q `),q) is Element of the carrier of AF
p . ((q `) "\/" q) is Element of the carrier of A1
Top AF is Element of the carrier of AF
p . (Top AF) is Element of the carrier of A1
Top A1 is Element of the carrier of A1
(p . q) ` is Element of the carrier of A1
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty Element of bool the carrier of BL
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 "/\" A1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (A1,A1) is Element of the carrier of BL
A1 ` is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
AF is Element of the carrier of BL
A1 is Element of the carrier of BL
AF "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (AF,A1) is Element of the carrier of BL
A1 is non empty (BL)
AF ` is Element of the carrier of BL
A1 ` is Element of the carrier of BL
(AF `) "/\" (A1 `) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_meet of BL . ((AF `),(A1 `)) is Element of the carrier of BL
(AF "\/" A1) ` is Element of the carrier of BL
((AF "\/" A1) `) ` is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
AF is Element of the carrier of BL
A1 is Element of the carrier of BL
AF => A1 is Element of the carrier of BL
A1 is non empty (BL)
AF ` is Element of the carrier of BL
(AF `) "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((AF `),A1) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty Element of bool the carrier of BL
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 "/\" A1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (A1,A1) is Element of the carrier of BL
A1 ` is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty (BL)
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 "/\" A1 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (A1,A1) is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 "\/" A1 is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . (A1,A1) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty Element of bool the carrier of BL
the Element of AF is Element of AF
bool the carrier of BL is non empty Element of bool (bool the carrier of BL)
bool (bool the carrier of BL) is non empty set
A1 is set
q is set
p is Element of the carrier of BL
meet A1 is set
q is non empty set
B is set
B is non empty Element of bool the carrier of BL
B1 is Element of the carrier of BL
B1 ` is Element of the carrier of BL
B0 is Element of the carrier of BL
B1 "/\" B0 is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (B1,B0) is Element of the carrier of BL
q is set
q is set
B1 is non empty (BL)
B0 is set
B0 is non empty (BL)
A1 is non empty (BL)
A1 is non empty (BL)
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty Element of bool the carrier of BL
{ (b₁ => b₂) where b₁, b₂ is Element of the carrier of BL : ( b₁ in AF & b₂ in AF ) } is set
A1 is set
p is Element of the carrier of BL
q is Element of the carrier of BL
p => q is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty Element of bool the carrier of BL
(BL,AF) is Element of bool the carrier of BL
{ (b₁ => b₂) where b₁, b₂ is Element of the carrier of BL : ( b₁ in AF & b₂ in AF ) } is set
the Element of AF is Element of AF
p is Element of the carrier of BL
p => p is Element of the carrier of BL
q is non empty set
AF is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of AF is non empty set
bool the carrier of AF is non empty set
p is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of p is non empty set
bool the carrier of p is non empty set
BL is set
A1 is non empty Element of bool the carrier of AF
(AF,A1) is non empty Element of bool the carrier of AF
{ (b₁ => b₂) where b₁, b₂ is Element of the carrier of AF : ( b₁ in A1 & b₂ in A1 ) } is set
A1 is set
B is Element of the carrier of p
B1 is Element of the carrier of p
B => B1 is Element of the carrier of p
q is non empty Element of bool the carrier of p
(p,q) is non empty Element of bool the carrier of p
{ (b₁ => b₂) where b₁, b₂ is Element of the carrier of p : ( b₁ in q & b₂ in q ) } is set
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
AF is non empty Element of bool the carrier of BL
(BL,AF) is non empty Element of bool the carrier of BL
{ (b₁ => b₂) where b₁, b₂ is Element of the carrier of BL : ( b₁ in AF & b₂ in AF ) } is set
A1 is Element of the carrier of BL
A1 is Element of the carrier of BL
p is Element of the carrier of BL
A1 => p is Element of the carrier of BL
q is Element of the carrier of BL
q ` is Element of the carrier of BL
B is Element of the carrier of BL
(q `) "\/" B is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((q `),B) is Element of the carrier of BL
A1 is Element of the carrier of BL
A1 ` is Element of the carrier of BL
p is Element of the carrier of BL
(A1 `) "\/" p is Element of the carrier of BL
the L_join of BL . ((A1 `),p) is Element of the carrier of BL
A1 => p is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
A1 is Element of the carrier of BL
AF . A1 is Element of the carrier of BL
A1 ` is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
(BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Element of the carrier of BL
{.AF.} is non empty Element of Fin the carrier of BL
AF ` is Element of the carrier of BL
A1 is Element of Fin the carrier of BL
A1 \/ {.AF.} is non empty Element of Fin the carrier of BL
FinJoin ((A1 \/ {.AF.}),(BL)) is Element of the carrier of BL
FinJoin (A1,(BL)) is Element of the carrier of BL
(FinJoin (A1,(BL))) "\/" (AF `) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((FinJoin (A1,(BL))),(AF `)) is Element of the carrier of BL
(BL) . AF is Element of the carrier of BL
(FinJoin (A1,(BL))) "\/" ((BL) . AF) is Element of the carrier of BL
the L_join of BL . ((FinJoin (A1,(BL))),((BL) . AF)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
(BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Element of Fin the carrier of BL
(BL,AF) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (AF,(id BL)) is Element of the carrier of BL
(BL,AF) ` is Element of the carrier of BL
FinMeet (AF,(BL)) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
p is Element of the carrier of BL
q is Element of the carrier of BL
the L_join of BL . (p,q) is Element of the carrier of BL
(BL) . ( the L_join of BL . (p,q)) is Element of the carrier of BL
(BL) . p is Element of the carrier of BL
(BL) . q is Element of the carrier of BL
the L_meet of BL . (((BL) . p),((BL) . q)) is Element of the carrier of BL
p "\/" q is Element of the carrier of BL
(p "\/" q) ` is Element of the carrier of BL
p ` is Element of the carrier of BL
q ` is Element of the carrier of BL
(p `) "/\" (q `) is Element of the carrier of BL
the L_meet of BL . ((p `),(q `)) is Element of the carrier of BL
the L_meet of BL . (((BL) . p),(q `)) is Element of the carrier of BL
the_unity_wrt the L_join of BL is Element of the carrier of BL
(BL) . (the_unity_wrt the L_join of BL) is Element of the carrier of BL
(the_unity_wrt the L_join of BL) ` is Element of the carrier of BL
Bottom BL is Element of the carrier of BL
(Bottom BL) ` is Element of the carrier of BL
Top BL is Element of the carrier of BL
the_unity_wrt the L_meet of BL is Element of the carrier of BL
the L_join of BL $$ (AF,(id BL)) is Element of the carrier of BL
( the L_join of BL $$ (AF,(id BL))) ` is Element of the carrier of BL
(BL) . ( the L_join of BL $$ (AF,(id BL))) is Element of the carrier of BL
(BL) * (id BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
the L_meet of BL $$ (AF,((BL) * (id BL))) is Element of the carrier of BL
the L_meet of BL $$ (AF,(BL)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
(BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Element of the carrier of BL
{.AF.} is non empty Element of Fin the carrier of BL
AF ` is Element of the carrier of BL
A1 is Element of Fin the carrier of BL
A1 \/ {.AF.} is non empty Element of Fin the carrier of BL
FinMeet ((A1 \/ {.AF.}),(BL)) is Element of the carrier of BL
FinMeet (A1,(BL)) is Element of the carrier of BL
(FinMeet (A1,(BL))) "/\" (AF `) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . ((FinMeet (A1,(BL))),(AF `)) is Element of the carrier of BL
(BL) . AF is Element of the carrier of BL
(FinMeet (A1,(BL))) "/\" ((BL) . AF) is Element of the carrier of BL
the L_meet of BL . ((FinMeet (A1,(BL))),((BL) . AF)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
Fin the carrier of BL is preBoolean set
(BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is Element of Fin the carrier of BL
(BL,AF) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (AF,(id BL)) is Element of the carrier of BL
(BL,AF) ` is Element of the carrier of BL
FinJoin (AF,(BL)) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
p is Element of the carrier of BL
q is Element of the carrier of BL
the L_meet of BL . (p,q) is Element of the carrier of BL
(BL) . ( the L_meet of BL . (p,q)) is Element of the carrier of BL
(BL) . p is Element of the carrier of BL
(BL) . q is Element of the carrier of BL
the L_join of BL . (((BL) . p),((BL) . q)) is Element of the carrier of BL
p "/\" q is Element of the carrier of BL
(p "/\" q) ` is Element of the carrier of BL
p ` is Element of the carrier of BL
q ` is Element of the carrier of BL
(p `) "\/" (q `) is Element of the carrier of BL
the L_join of BL . ((p `),(q `)) is Element of the carrier of BL
the L_join of BL . (((BL) . p),(q `)) is Element of the carrier of BL
the_unity_wrt the L_meet of BL is Element of the carrier of BL
(BL) . (the_unity_wrt the L_meet of BL) is Element of the carrier of BL
(the_unity_wrt the L_meet of BL) ` is Element of the carrier of BL
Top BL is Element of the carrier of BL
(Top BL) ` is Element of the carrier of BL
Bottom BL is Element of the carrier of BL
the_unity_wrt the L_join of BL is Element of the carrier of BL
the L_meet of BL $$ (AF,(id BL)) is Element of the carrier of BL
( the L_meet of BL $$ (AF,(id BL))) ` is Element of the carrier of BL
(BL) . ( the L_meet of BL $$ (AF,(id BL))) is Element of the carrier of BL
(BL) * (id BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
the L_join of BL $$ (AF,((BL) * (id BL))) is Element of the carrier of BL
the L_join of BL $$ (AF,(BL)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
Bottom BL is Element of the carrier of BL
Top BL is Element of the carrier of BL
Fin the carrier of BL is preBoolean set
(BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
AF is non empty meet-closed join-closed Element of bool the carrier of BL
(BL,AF) is non empty Element of bool the carrier of BL
{ (b<sub>1</sub> => b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of BL : ( b<sub>1</sub> in AF & b<sub>2</sub> in AF ) } is set
{ ((BL,b<sub>1</sub>) "\/" (FinJoin (b<sub>2</sub>,(BL)))) where b<sub>1</sub>, b<sub>2</sub> is Element of Fin the carrier of BL : ( b<sub>1</sub> c= AF & b<sub>2</sub> c= AF ) } is set
A1 is set
p is Element of Fin the carrier of BL
(BL,p) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (p,(id BL)) is Element of the carrier of BL
q is Element of Fin the carrier of BL
FinJoin (q,(BL)) is Element of the carrier of BL
(BL,p) "\/" (FinJoin (q,(BL))) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((BL,p),(FinJoin (q,(BL)))) is Element of the carrier of BL
(BL,q) is Element of the carrier of BL
FinMeet (q,(id BL)) is Element of the carrier of BL
B is Element of the carrier of BL
B1 is Element of the carrier of BL
B ` is Element of the carrier of BL
(B `) "\/" B1 is Element of the carrier of BL
the L_join of BL . ((B `),B1) is Element of the carrier of BL
A1 is Element of Fin the carrier of BL
FinJoin (A1,(BL)) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
q is Element of Fin the carrier of BL
FinJoin (q,(BL)) is Element of the carrier of BL
B is Element of the carrier of BL
{.B.} is non empty Element of Fin the carrier of BL
q \/ {.B.} is non empty Element of Fin the carrier of BL
FinJoin ((q \/ {.B.}),(BL)) is Element of the carrier of BL
{B} is non empty set
q \/ {B} is non empty set
B1 is Element of Fin the carrier of BL
(BL,B1) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (B1,(id BL)) is Element of the carrier of BL
B1 is Element of Fin the carrier of BL
(BL,B1) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (B1,(id BL)) is Element of the carrier of BL
B0 is Element of the carrier of BL
B0 ` is Element of the carrier of BL
q is Element of the carrier of BL
(B0 `) "\/" q is Element of the carrier of BL
the L_join of BL . ((B0 `),q) is Element of the carrier of BL
c<sub>11</sub> is set
a is Element of the carrier of BL
the L_join of BL [:] ((id BL),a) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
( the L_join of BL [:] ((id BL),a)) .: B1 is Element of Fin the carrier of BL
A1 is Element of the carrier of BL
A2 is Element of the carrier of BL
( the L_join of BL [:] ((id BL),a)) . A2 is Element of the carrier of BL
(id BL) . A2 is Element of the carrier of BL
the L_join of BL . (((id BL) . A2),a) is Element of the carrier of BL
A2 "\/" a is Element of the carrier of BL
the L_join of BL . (A2,a) is Element of the carrier of BL
the L_join of BL [:] ((id BL),B0) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
( the L_join of BL [:] ((id BL),B0)) .: B1 is Element of Fin the carrier of BL
c<sub>11</sub> is set
a is Element of the carrier of BL
a "\/" B0 is Element of the carrier of BL
the L_join of BL . (a,B0) is Element of the carrier of BL
A1 is Element of Fin the carrier of BL
(BL,A1) is Element of the carrier of BL
FinJoin (A1,(id BL)) is Element of the carrier of BL
A2 is Element of Fin the carrier of BL
FinJoin (A2,(BL)) is Element of the carrier of BL
(BL,A1) "\/" (FinJoin (A2,(BL))) is Element of the carrier of BL
the L_join of BL . ((BL,A1),(FinJoin (A2,(BL)))) is Element of the carrier of BL
{.B0.} is non empty Element of Fin the carrier of BL
A1 \/ {.B0.} is non empty Element of Fin the carrier of BL
A19 is non empty Element of Fin the carrier of BL
(BL,A19) is Element of the carrier of BL
FinJoin (A19,(id BL)) is Element of the carrier of BL
A29 is Element of Fin the carrier of BL
FinJoin (A29,(BL)) is Element of the carrier of BL
(BL,A19) "\/" (FinJoin (A29,(BL))) is Element of the carrier of BL
the L_join of BL . ((BL,A19),(FinJoin (A29,(BL)))) is Element of the carrier of BL
(BL,A1) "\/" B0 is Element of the carrier of BL
the L_join of BL . ((BL,A1),B0) is Element of the carrier of BL
((BL,A1) "\/" B0) "\/" (FinJoin (A2,(BL))) is Element of the carrier of BL
the L_join of BL . (((BL,A1) "\/" B0),(FinJoin (A2,(BL)))) is Element of the carrier of BL
A19 is Element of Fin the carrier of BL
(BL,A19) is Element of the carrier of BL
FinJoin (A19,(id BL)) is Element of the carrier of BL
A29 is Element of Fin the carrier of BL
FinJoin (A29,(BL)) is Element of the carrier of BL
(BL,A19) "\/" (FinJoin (A29,(BL))) is Element of the carrier of BL
the L_join of BL . ((BL,A19),(FinJoin (A29,(BL)))) is Element of the carrier of BL
q ` is Element of the carrier of BL
the L_join of BL [:] ((id BL),(q `)) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
( the L_join of BL [:] ((id BL),(q `))) .: B1 is Element of Fin the carrier of BL
c₁₁ is set
a is Element of the carrier of BL
a "\/" (q `) is Element of the carrier of BL
the L_join of BL . (a,(q `)) is Element of the carrier of BL
A1 is Element of Fin the carrier of BL
(BL,A1) is Element of the carrier of BL
FinJoin (A1,(id BL)) is Element of the carrier of BL
A2 is Element of Fin the carrier of BL
FinJoin (A2,(BL)) is Element of the carrier of BL
(BL,A1) "\/" (FinJoin (A2,(BL))) is Element of the carrier of BL
the L_join of BL . ((BL,A1),(FinJoin (A2,(BL)))) is Element of the carrier of BL
A19 is Element of Fin the carrier of BL
(BL,A19) is Element of the carrier of BL
FinJoin (A19,(id BL)) is Element of the carrier of BL
{.q.} is non empty Element of Fin the carrier of BL
A2 \/ {.q.} is non empty Element of Fin the carrier of BL
A29 is non empty Element of Fin the carrier of BL
FinJoin (A29,(BL)) is Element of the carrier of BL
(BL,A19) "\/" (FinJoin (A29,(BL))) is Element of the carrier of BL
the L_join of BL . ((BL,A19),(FinJoin (A29,(BL)))) is Element of the carrier of BL
(FinJoin (A2,(BL))) "\/" (q `) is Element of the carrier of BL
the L_join of BL . ((FinJoin (A2,(BL))),(q `)) is Element of the carrier of BL
(BL,A1) "\/" ((FinJoin (A2,(BL))) "\/" (q `)) is Element of the carrier of BL
the L_join of BL . ((BL,A1),((FinJoin (A2,(BL))) "\/" (q `))) is Element of the carrier of BL
A19 is Element of Fin the carrier of BL
(BL,A19) is Element of the carrier of BL
FinJoin (A19,(id BL)) is Element of the carrier of BL
A29 is Element of Fin the carrier of BL
FinJoin (A29,(BL)) is Element of the carrier of BL
(BL,A19) "\/" (FinJoin (A29,(BL))) is Element of the carrier of BL
the L_join of BL . ((BL,A19),(FinJoin (A29,(BL)))) is Element of the carrier of BL
(( the L_join of BL [:] ((id BL),B0)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) is Element of Fin the carrier of BL
(BL,((( the L_join of BL [:] ((id BL),B0)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1))) is Element of the carrier of BL
FinMeet (((( the L_join of BL [:] ((id BL),B0)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)),(id BL)) is Element of the carrier of BL
B ` is Element of the carrier of BL
(B0 `) ` is Element of the carrier of BL
((B0 `) `) "/\" (q `) is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
the L_meet of BL . (((B0 `) `),(q `)) is Element of the carrier of BL
B0 "/\" (q `) is Element of the carrier of BL
the L_meet of BL . (B0,(q `)) is Element of the carrier of BL
(BL,B1) "\/" (B0 "/\" (q `)) is Element of the carrier of BL
the L_join of BL . ((BL,B1),(B0 "/\" (q `))) is Element of the carrier of BL
(BL,B1) "\/" B0 is Element of the carrier of BL
the L_join of BL . ((BL,B1),B0) is Element of the carrier of BL
(BL,B1) "\/" (q `) is Element of the carrier of BL
the L_join of BL . ((BL,B1),(q `)) is Element of the carrier of BL
((BL,B1) "\/" B0) "/\" ((BL,B1) "\/" (q `)) is Element of the carrier of BL
the L_meet of BL . (((BL,B1) "\/" B0),((BL,B1) "\/" (q `))) is Element of the carrier of BL
(BL,(( the L_join of BL [:] ((id BL),B0)) .: B1)) is Element of the carrier of BL
FinMeet ((( the L_join of BL [:] ((id BL),B0)) .: B1),(id BL)) is Element of the carrier of BL
(BL,(( the L_join of BL [:] ((id BL),B0)) .: B1)) "/\" ((BL,B1) "\/" (q `)) is Element of the carrier of BL
the L_meet of BL . ((BL,(( the L_join of BL [:] ((id BL),B0)) .: B1)),((BL,B1) "\/" (q `))) is Element of the carrier of BL
(BL,(( the L_join of BL [:] ((id BL),(q `))) .: B1)) is Element of the carrier of BL
FinMeet ((( the L_join of BL [:] ((id BL),(q `))) .: B1),(id BL)) is Element of the carrier of BL
(BL,(( the L_join of BL [:] ((id BL),B0)) .: B1)) "/\" (BL,(( the L_join of BL [:] ((id BL),(q `))) .: B1)) is Element of the carrier of BL
the L_meet of BL . ((BL,(( the L_join of BL [:] ((id BL),B0)) .: B1)),(BL,(( the L_join of BL [:] ((id BL),(q `))) .: B1))) is Element of the carrier of BL
{}. the carrier of BL is empty Element of Fin the carrier of BL
FinJoin (({}. the carrier of BL),(BL)) is Element of the carrier of BL
{.(Bottom BL).} is non empty Element of Fin the carrier of BL
p is non empty Element of Fin the carrier of BL
(BL,p) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (p,(id BL)) is Element of the carrier of BL
q is set
B is non empty Element of Fin the carrier of BL
(BL,B) is Element of the carrier of BL
FinJoin (B,(id BL)) is Element of the carrier of BL
{.(Top BL).} is non empty Element of Fin the carrier of BL
B1 is non empty Element of Fin the carrier of BL
FinJoin (B1,(BL)) is Element of the carrier of BL
(BL,B) "\/" (FinJoin (B1,(BL))) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((BL,B),(FinJoin (B1,(BL)))) is Element of the carrier of BL
(Bottom BL) "\/" (Bottom BL) is Element of the carrier of BL
the L_join of BL . ((Bottom BL),(Bottom BL)) is Element of the carrier of BL
(Top BL) ` is Element of the carrier of BL
(Bottom BL) "\/" ((Top BL) `) is Element of the carrier of BL
the L_join of BL . ((Bottom BL),((Top BL) `)) is Element of the carrier of BL
(BL,B) "\/" ((Top BL) `) is Element of the carrier of BL
the L_join of BL . ((BL,B),((Top BL) `)) is Element of the carrier of BL
(BL,B1) is Element of the carrier of BL
FinMeet (B1,(id BL)) is Element of the carrier of BL
(BL,B1) ` is Element of the carrier of BL
(BL,B) "\/" ((BL,B1) `) is Element of the carrier of BL
the L_join of BL . ((BL,B),((BL,B1) `)) is Element of the carrier of BL
B is Element of Fin the carrier of BL
(BL,B) is Element of the carrier of BL
FinJoin (B,(id BL)) is Element of the carrier of BL
B1 is Element of Fin the carrier of BL
FinJoin (B1,(BL)) is Element of the carrier of BL
(BL,B) "\/" (FinJoin (B1,(BL))) is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((BL,B),(FinJoin (B1,(BL)))) is Element of the carrier of BL
(BL,{.(Bottom BL).}) is Element of the carrier of BL
FinMeet ({.(Bottom BL).},(id BL)) is Element of the carrier of BL
p is Element of Fin the carrier of BL
(BL,p) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (p,(id BL)) is Element of the carrier of BL
BL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean Heyting implicative LattStr
the carrier of BL is non empty set
bool the carrier of BL is non empty set
Bottom BL is Element of the carrier of BL
Top BL is Element of the carrier of BL
Fin the carrier of BL is preBoolean set
AF is non empty meet-closed join-closed Element of bool the carrier of BL
(BL,AF) is non empty Element of bool the carrier of BL
{ (b₁ => b₂) where b₁, b₂ is Element of the carrier of BL : ( b₁ in AF & b₂ in AF ) } is set
{ (BL,b₁) where b₁ is Element of Fin the carrier of BL : b₁ c= (BL,AF) } is set
(BL,AF) is non empty (BL)
A1 is set
p is Element of the carrier of BL
{.p.} is non empty Element of Fin the carrier of BL
(Bottom BL) "\/" p is Element of the carrier of BL
the L_join of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_join of BL . ((Bottom BL),p) is Element of the carrier of BL
(Top BL) ` is Element of the carrier of BL
((Top BL) `) "\/" p is Element of the carrier of BL
the L_join of BL . (((Top BL) `),p) is Element of the carrier of BL
q is Element of Fin the carrier of BL
(BL,q) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (q,(id BL)) is Element of the carrier of BL
A1 is set
p is Element of Fin the carrier of BL
(BL,p) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (p,(id BL)) is Element of the carrier of BL
p is non empty (BL)
A1 is non empty Element of bool the carrier of BL
B is set
B1 is Element of Fin the carrier of BL
(BL,B1) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (B1,(id BL)) is Element of the carrier of BL
B0 is set
q is Element of the carrier of BL
c<sub>11</sub> is Element of the carrier of BL
q => c<sub>11</sub> is Element of the carrier of BL
q is meet-closed join-closed Element of bool the carrier of BL
p is Element of the carrier of BL
p ` is Element of the carrier of BL
q is Element of the carrier of BL
p "/\" q is Element of the carrier of BL
the L_meet of BL is Relation-like [: the carrier of BL, the carrier of BL:] -defined the carrier of BL -valued Function-like non empty V19([: the carrier of BL, the carrier of BL:]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:]
[: the carrier of BL, the carrier of BL:] is non empty set
[:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
bool [:[: the carrier of BL, the carrier of BL:], the carrier of BL:] is non empty set
the L_meet of BL . (p,q) is Element of the carrier of BL
B is Element of Fin the carrier of BL
(BL,B) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (B,(id BL)) is Element of the carrier of BL
B1 is Element of Fin the carrier of BL
(BL,B1) is Element of the carrier of BL
FinMeet (B1,(id BL)) is Element of the carrier of BL
B1 \/ B is Element of Fin the carrier of BL
B0 is Element of Fin the carrier of BL
(BL,B0) is Element of the carrier of BL
FinMeet (B0,(id BL)) is Element of the carrier of BL
B is Element of Fin the carrier of BL
(BL,B) is Element of the carrier of BL
id BL is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
bool [: the carrier of BL, the carrier of BL:] is non empty set
id the carrier of BL is Relation-like the carrier of BL -defined the carrier of BL -valued non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinMeet (B,(id BL)) is Element of the carrier of BL
(BL) is Relation-like the carrier of BL -defined the carrier of BL -valued Function-like non empty V19( the carrier of BL) quasi_total Element of bool [: the carrier of BL, the carrier of BL:]
FinJoin (B,(BL)) is Element of the carrier of BL
B1 is Element of Fin the carrier of BL
(BL,B1) is Element of the carrier of BL
FinMeet (B1,(id BL)) is Element of the carrier of BL