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