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

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

( b

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

q . c

[(q . B1),(q . c

{(q . B1),(q . c

{{(q . B1),(q . c

[B1,c

{B1,c

{{B1,c

[(q . B),(q . c

{(q . B),(q . c

{(q . B)} is non empty set

{{(q . B),(q . c

[B,c

{B,c

{B} is non empty set

{{B,c

[(B "\/" B1),c

{(B "\/" B1),c

{(B "\/" B1)} is non empty set

{{(B "\/" B1),c

[(q . (B "\/" B1)),(q . c

{(q . (B "\/" B1)),(q . c

{(q . (B "\/" B1))} is non empty set

{{(q . (B "\/" B1)),(q . c

[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

q . c

[(q . c

{(q . c

{(q . c

{{(q . c

[c

{c

{c

{{c

[(q . c

{(q . c

{{(q . c

[c

{c

{{c

[c

{c

{{c

[(q . c

{(q . c

{{(q . c

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