:: QUANTAL1 semantic presentation

K143() is set

bool K143() is non empty set

K147() is Element of bool K143()

K142() is set

bool K142() is non empty set

{} is empty V7() non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V45() set

the empty V7() non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V45() set is empty V7() non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V45() set

1 is non empty set

bool {} is non empty finite V45() set

{{}} is non empty functional finite V45() set

F

F

{ F

{ F

{ F

Q is set

j is Element of F

F

D is Element of F

F

Q is set

j is Element of F

F

F

F

{ F

Q is non empty set

the Element of Q is Element of Q

D is Element of F

F

Q is non empty LattStr

the carrier of Q is non empty set

the L_join of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

[: the carrier of Q, the carrier of Q:] is non empty V7() set

[:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty V7() set

bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty set

the L_meet of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) is non empty strict LattStr

j is non empty LattStr

the carrier of j is non empty set

the L_join of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

[: the carrier of j, the carrier of j:] is non empty V7() set

[:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty V7() set

bool [:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set

the L_meet of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

LattStr(# the carrier of j, the L_join of j, the L_meet of j #) is non empty strict LattStr

D is Element of the carrier of Q

j9 is Element of the carrier of Q

D "\/" j9 is Element of the carrier of Q

the L_join of Q . (D,j9) is Element of the carrier of Q

[D,j9] is set

{D,j9} is non empty finite set

{D} is non empty finite set

{{D,j9},{D}} is non empty finite V45() set

the L_join of Q . [D,j9] is set

D "/\" j9 is Element of the carrier of Q

the L_meet of Q . (D,j9) is Element of the carrier of Q

the L_meet of Q . [D,j9] is set

f is Element of the carrier of j

L is Element of the carrier of j

f "\/" L is Element of the carrier of j

the L_join of j . (f,L) is Element of the carrier of j

[f,L] is set

{f,L} is non empty finite set

{f} is non empty finite set

{{f,L},{f}} is non empty finite V45() set

the L_join of j . [f,L] is set

f "/\" L is Element of the carrier of j

the L_meet of j . (f,L) is Element of the carrier of j

the L_meet of j . [f,L] is set

Q is non empty LattStr

the carrier of Q is non empty set

the L_join of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

[: the carrier of Q, the carrier of Q:] is non empty V7() set

[:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty V7() set

bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty set

the L_meet of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) is non empty strict LattStr

j is non empty LattStr

the carrier of j is non empty set

the L_join of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

[: the carrier of j, the carrier of j:] is non empty V7() set

[:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty V7() set

bool [:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set

the L_meet of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

LattStr(# the carrier of j, the L_join of j, the L_meet of j #) is non empty strict LattStr

D is Element of the carrier of Q

j9 is Element of the carrier of j

f is set

L is Element of the carrier of j

X is Element of the carrier of Q

L is Element of the carrier of Q

X is Element of the carrier of j

L is Element of the carrier of j

X is Element of the carrier of Q

L is Element of the carrier of Q

X is Element of the carrier of j

Q is non empty LattStr

the carrier of Q is non empty set

bool the carrier of Q is non empty set

Q is non empty LattStr

the carrier of Q is non empty set

bool the carrier of Q is non empty set

j is Element of bool the carrier of Q

bool j is non empty set

{} j is empty V7() non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V45() Element of bool j

"\/" (({} j),Q) is Element of the carrier of Q

D is Element of the carrier of Q

the non empty set is non empty set

[: the non empty set , the non empty set :] is non empty V7() set

[:[: the non empty set , the non empty set :], the non empty set :] is non empty V7() set

bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set

the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]

( the non empty set , the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]) is () ()

the carrier of ( the non empty set , the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]) is set

the non empty set is non empty set

[: the non empty set , the non empty set :] is non empty V7() set

[:[: the non empty set , the non empty set :], the non empty set :] is non empty V7() set

bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set

the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]

the Element of the non empty set is Element of the non empty set

( the non empty set , the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set ) is () ()

the carrier of ( the non empty set , the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the non empty V7() V10([: the non empty set , the non empty set :]) V11( the non empty set ) Function-like V17([: the non empty set , the non empty set :]) V21([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set ) is set

Q is non empty multMagma

Q is non empty multMagma

the set is set

{ the set } is non empty finite set

[:{ the set },{ the set }:] is non empty V7() finite set

[:[:{ the set },{ the set }:],{ the set }:] is non empty V7() finite set

bool [:[:{ the set },{ the set }:],{ the set }:] is non empty finite V45() set

the non empty V7() V10([:{ the set },{ the set }:]) V11({ the set }) Function-like V17([:{ the set },{ the set }:]) V21([:{ the set },{ the set }:],{ the set }) finite Element of bool [:[:{ the set },{ the set }:],{ the set }:] is non empty V7() V10([:{ the set },{ the set }:]) V11({ the set }) Function-like V17([:{ the set },{ the set }:]) V21([:{ the set },{ the set }:],{ the set }) finite Element of bool [:[:{ the set },{ the set }:],{ the set }:]

multMagma(# { the set }, the non empty V7() V10([:{ the set },{ the set }:]) V11({ the set }) Function-like V17([:{ the set },{ the set }:]) V21([:{ the set },{ the set }:],{ the set }) finite Element of bool [:[:{ the set },{ the set }:],{ the set }:] #) is non empty strict multMagma

D is non empty strict multMagma

the carrier of D is non empty set

j9 is Element of the carrier of D

f is Element of the carrier of D

j9 * f is Element of the carrier of D

the multF of D is non empty V7() V10([: the carrier of D, the carrier of D:]) V11( the carrier of D) Function-like V17([: the carrier of D, the carrier of D:]) V21([: the carrier of D, the carrier of D:], the carrier of D) Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]

[: the carrier of D, the carrier of D:] is non empty V7() set

[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty V7() set

bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set

the multF of D . (j9,f) is Element of the carrier of D

[j9,f] is set

{j9,f} is non empty finite set

{j9} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the multF of D . [j9,f] is set

j9 is Element of the carrier of D

f is Element of the carrier of D

f * j9 is Element of the carrier of D

the multF of D is non empty V7() V10([: the carrier of D, the carrier of D:]) V11( the carrier of D) Function-like V17([: the carrier of D, the carrier of D:]) V21([: the carrier of D, the carrier of D:], the carrier of D) Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]

[: the carrier of D, the carrier of D:] is non empty V7() set

[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty V7() set

bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set

the multF of D . (f,j9) is Element of the carrier of D

[f,j9] is set

{f,j9} is non empty finite set

{f} is non empty finite set

{{f,j9},{f}} is non empty finite V45() set

the multF of D . [f,j9] is set

BooleLatt {} is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V142() complemented Boolean complete LattStr

j is non empty ()

the carrier of j is non empty set

the L_join of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

[: the carrier of j, the carrier of j:] is non empty V7() set

[:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty V7() set

bool [:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set

the L_meet of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

LattStr(# the carrier of j, the L_join of j, the L_meet of j #) is non empty strict LattStr

the Element of the carrier of j is Element of the carrier of j

the carrier of (BooleLatt {}) is non empty set

j9 is Element of the carrier of j

f is Element of the carrier of j

the multF of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

j9 is Element of the carrier of j

f is Element of the carrier of j

L is Element of the carrier of j

H

[f,L] is set

{f,L} is non empty finite set

{f} is non empty finite set

{{f,L},{f}} is non empty finite V45() set

the multF of j . [f,L] is set

H

[j9,(H

{j9,(H

{j9} is non empty finite set

{{j9,(H

the multF of j . [j9,(H

H

[j9,f] is set

{j9,f} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the multF of j . [j9,f] is set

H

[(H

{(H

{(H

{{(H

the multF of j . [(H

j9 is Element of the carrier of j

f is Element of the carrier of j

L is Element of the carrier of j

f "/\" L is Element of the carrier of j

the L_meet of j . (f,L) is Element of the carrier of j

[f,L] is set

{f,L} is non empty finite set

{f} is non empty finite set

{{f,L},{f}} is non empty finite V45() set

the L_meet of j . [f,L] is set

j9 "/\" (f "/\" L) is Element of the carrier of j

the L_meet of j . (j9,(f "/\" L)) is Element of the carrier of j

[j9,(f "/\" L)] is set

{j9,(f "/\" L)} is non empty finite set

{j9} is non empty finite set

{{j9,(f "/\" L)},{j9}} is non empty finite V45() set

the L_meet of j . [j9,(f "/\" L)] is set

j9 "/\" f is Element of the carrier of j

the L_meet of j . (j9,f) is Element of the carrier of j

[j9,f] is set

{j9,f} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the L_meet of j . [j9,f] is set

(j9 "/\" f) "/\" L is Element of the carrier of j

the L_meet of j . ((j9 "/\" f),L) is Element of the carrier of j

[(j9 "/\" f),L] is set

{(j9 "/\" f),L} is non empty finite set

{(j9 "/\" f)} is non empty finite set

{{(j9 "/\" f),L},{(j9 "/\" f)}} is non empty finite V45() set

the L_meet of j . [(j9 "/\" f),L] is set

X is Element of the carrier of j

x is Element of the carrier of j

X "\/" x is Element of the carrier of j

the L_join of j . (X,x) is Element of the carrier of j

[X,x] is set

{X,x} is non empty finite set

{X} is non empty finite set

{{X,x},{X}} is non empty finite V45() set

the L_join of j . [X,x] is set

X "/\" (X "\/" x) is Element of the carrier of j

the L_meet of j . (X,(X "\/" x)) is Element of the carrier of j

[X,(X "\/" x)] is set

{X,(X "\/" x)} is non empty finite set

{{X,(X "\/" x)},{X}} is non empty finite V45() set

the L_meet of j . [X,(X "\/" x)] is set

j9 is Element of the carrier of j

f is Element of the carrier of j

H

[j9,f] is set

{j9,f} is non empty finite set

{j9} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the multF of j . [j9,f] is set

H

[f,j9] is set

{f,j9} is non empty finite set

{f} is non empty finite set

{{f,j9},{f}} is non empty finite V45() set

the multF of j . [f,j9] is set

j9 is Element of the carrier of j

H

[ the Element of the carrier of j,j9] is set

{ the Element of the carrier of j,j9} is non empty finite set

{ the Element of the carrier of j} is non empty finite set

{{ the Element of the carrier of j,j9},{ the Element of the carrier of j}} is non empty finite V45() set

the multF of j . [ the Element of the carrier of j,j9] is set

j9 is Element of the carrier of j

H

[j9, the Element of the carrier of j] is set

{j9, the Element of the carrier of j} is non empty finite set

{j9} is non empty finite set

{{j9, the Element of the carrier of j},{j9}} is non empty finite V45() set

the multF of j . [j9, the Element of the carrier of j] is set

j9 is Element of the carrier of j

the Element of the carrier of j * j9 is Element of the carrier of j

the multF of j . ( the Element of the carrier of j,j9) is Element of the carrier of j

[ the Element of the carrier of j,j9] is set

{ the Element of the carrier of j,j9} is non empty finite set

{ the Element of the carrier of j} is non empty finite set

{{ the Element of the carrier of j,j9},{ the Element of the carrier of j}} is non empty finite V45() set

the multF of j . [ the Element of the carrier of j,j9] is set

j9 is Element of the carrier of j

j9 * the Element of the carrier of j is Element of the carrier of j

the multF of j . (j9, the Element of the carrier of j) is Element of the carrier of j

[j9, the Element of the carrier of j] is set

{j9, the Element of the carrier of j} is non empty finite set

{j9} is non empty finite set

{{j9, the Element of the carrier of j},{j9}} is non empty finite V45() set

the multF of j . [j9, the Element of the carrier of j] is set

j9 is set

f is Element of the carrier of (BooleLatt {})

L is Element of the carrier of j

X is Element of the carrier of j

x is Element of the carrier of j

x9 is Element of the carrier of (BooleLatt {})

j9 is set

j9 is Element of the carrier of j

f is set

"\/" (f,j) is Element of the carrier of j

j9 * ("\/" (f,j)) is Element of the carrier of j

the multF of j . (j9,("\/" (f,j))) is Element of the carrier of j

[j9,("\/" (f,j))] is set

{j9,("\/" (f,j))} is non empty finite set

{j9} is non empty finite set

{{j9,("\/" (f,j))},{j9}} is non empty finite V45() set

the multF of j . [j9,("\/" (f,j))] is set

{ (j9 * b

"\/" ( { (j9 * b

j9 is Element of the carrier of j

f is set

"\/" (f,j) is Element of the carrier of j

("\/" (f,j)) * j9 is Element of the carrier of j

the multF of j . (("\/" (f,j)),j9) is Element of the carrier of j

[("\/" (f,j)),j9] is set

{("\/" (f,j)),j9} is non empty finite set

{("\/" (f,j))} is non empty finite set

{{("\/" (f,j)),j9},{("\/" (f,j))}} is non empty finite V45() set

the multF of j . [("\/" (f,j)),j9] is set

{ (b

"\/" ( { (b

j9 is Element of the carrier of j

f is Element of the carrier of j

j9 "/\" f is Element of the carrier of j

the L_meet of j . (j9,f) is Element of the carrier of j

[j9,f] is set

{j9,f} is non empty finite set

{j9} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the L_meet of j . [j9,f] is set

(j9 "/\" f) "\/" f is Element of the carrier of j

the L_join of j . ((j9 "/\" f),f) is Element of the carrier of j

[(j9 "/\" f),f] is set

{(j9 "/\" f),f} is non empty finite set

{(j9 "/\" f)} is non empty finite set

{{(j9 "/\" f),f},{(j9 "/\" f)}} is non empty finite V45() set

the L_join of j . [(j9 "/\" f),f] is set

L is Element of the carrier of j

X is Element of the carrier of j

L "/\" X is Element of the carrier of j

the L_meet of j . (L,X) is Element of the carrier of j

[L,X] is set

{L,X} is non empty finite set

{L} is non empty finite set

{{L,X},{L}} is non empty finite V45() set

the L_meet of j . [L,X] is set

X "/\" L is Element of the carrier of j

the L_meet of j . (X,L) is Element of the carrier of j

[X,L] is set

{X,L} is non empty finite set

{X} is non empty finite set

{{X,L},{X}} is non empty finite V45() set

the L_meet of j . [X,L] is set

j9 is Element of the carrier of j

f is Element of the carrier of j

j9 "\/" f is Element of the carrier of j

the L_join of j . (j9,f) is Element of the carrier of j

[j9,f] is set

{j9,f} is non empty finite set

{j9} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the L_join of j . [j9,f] is set

f "\/" j9 is Element of the carrier of j

the L_join of j . (f,j9) is Element of the carrier of j

[f,j9] is set

{f,j9} is non empty finite set

{f} is non empty finite set

{{f,j9},{f}} is non empty finite V45() set

the L_join of j . [f,j9] is set

L is Element of the carrier of j

X is Element of the carrier of j

x is Element of the carrier of j

X "\/" x is Element of the carrier of j

the L_join of j . (X,x) is Element of the carrier of j

[X,x] is set

{X,x} is non empty finite set

{X} is non empty finite set

{{X,x},{X}} is non empty finite V45() set

the L_join of j . [X,x] is set

L "\/" (X "\/" x) is Element of the carrier of j

the L_join of j . (L,(X "\/" x)) is Element of the carrier of j

[L,(X "\/" x)] is set

{L,(X "\/" x)} is non empty finite set

{L} is non empty finite set

{{L,(X "\/" x)},{L}} is non empty finite V45() set

the L_join of j . [L,(X "\/" x)] is set

L "\/" X is Element of the carrier of j

the L_join of j . (L,X) is Element of the carrier of j

[L,X] is set

{L,X} is non empty finite set

{{L,X},{L}} is non empty finite V45() set

the L_join of j . [L,X] is set

(L "\/" X) "\/" x is Element of the carrier of j

the L_join of j . ((L "\/" X),x) is Element of the carrier of j

[(L "\/" X),x] is set

{(L "\/" X),x} is non empty finite set

{(L "\/" X)} is non empty finite set

{{(L "\/" X),x},{(L "\/" X)}} is non empty finite V45() set

the L_join of j . [(L "\/" X),x] is set

Q is non empty set

[:Q,Q:] is non empty V7() set

[:[:Q,Q:],Q:] is non empty V7() set

bool [:[:Q,Q:],Q:] is non empty set

j is non empty V7() V10([:Q,Q:]) V11(Q) Function-like V17([:Q,Q:]) V21([:Q,Q:],Q) Element of bool [:[:Q,Q:],Q:]

D is non empty V7() V10([:Q,Q:]) V11(Q) Function-like V17([:Q,Q:]) V21([:Q,Q:],Q) Element of bool [:[:Q,Q:],Q:]

j9 is non empty V7() V10([:Q,Q:]) V11(Q) Function-like V17([:Q,Q:]) V21([:Q,Q:],Q) Element of bool [:[:Q,Q:],Q:]

(Q,j,D,j9) is () ()

the carrier of (BooleLatt {}) is non empty set

[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):] is non empty V7() set

[:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty V7() set

bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty set

the non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

the L_join of (BooleLatt {}) is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

the L_meet of (BooleLatt {}) is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

(H

F

the carrier of F

F

F

{ ("\/" ( { F

"\/" ( { ("\/" ( { F

{ F

"\/" ( { F

{ { F

bool the carrier of F

{ ("\/" (b

X is set

x is Element of bool the carrier of F

"\/" (x,F

x9 is Element of the carrier of F

{ F

X is set

x is Element of the carrier of F

{ F

"\/" ( { F

x9 is set

a9 is Element of the carrier of F

F

union { { F

X is set

x is Element of the carrier of F

x9 is Element of the carrier of F

F

{ F

X is set

x is set

x9 is Element of the carrier of F

{ F

a9 is Element of the carrier of F

F

bool H

bool H

bool (bool H

X is set

x is Element of the carrier of F

{ F

x9 is set

a9 is Element of the carrier of F

F

Q is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete () () ()

the carrier of Q is non empty set

j is set

"\/" (j,Q) is Element of the carrier of Q

D is set

"\/" (D,Q) is Element of the carrier of Q

("\/" (j,Q)) * ("\/" (D,Q)) is Element of the carrier of Q

the multF of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

[: the carrier of Q, the carrier of Q:] is non empty V7() set

[:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty V7() set

bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty set

the multF of Q . (("\/" (j,Q)),("\/" (D,Q))) is Element of the carrier of Q

[("\/" (j,Q)),("\/" (D,Q))] is set

{("\/" (j,Q)),("\/" (D,Q))} is non empty finite set

{("\/" (j,Q))} is non empty finite set

{{("\/" (j,Q)),("\/" (D,Q))},{("\/" (j,Q))}} is non empty finite V45() set

the multF of Q . [("\/" (j,Q)),("\/" (D,Q))] is set

{ (b

"\/" ( { (b

{ (a

"\/" ( { (a

j9 is Element of the carrier of Q

j9 * ("\/" (D,Q)) is Element of the carrier of Q

the multF of Q . (j9,("\/" (D,Q))) is Element of the carrier of Q

[j9,("\/" (D,Q))] is set

{j9,("\/" (D,Q))} is non empty finite set

{j9} is non empty finite set

{{j9,("\/" (D,Q))},{j9}} is non empty finite V45() set

the multF of Q . [j9,("\/" (D,Q))] is set

{ (j9 * b

"\/" ( { (j9 * b

{ H

{ H

{ ("\/" ( { H

"\/" ( { ("\/" ( { H

{ H

"\/" ( { H

Q is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete () () ()

the carrier of Q is non empty set

j is Element of the carrier of Q

D is Element of the carrier of Q

j "\/" D is Element of the carrier of Q

the L_join of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

[: the carrier of Q, the carrier of Q:] is non empty V7() set

[:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty V7() set

bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty set

the L_join of Q . (j,D) is Element of the carrier of Q

[j,D] is set

{j,D} is non empty finite set

{j} is non empty finite set

{{j,D},{j}} is non empty finite V45() set

the L_join of Q . [j,D] is set

j9 is Element of the carrier of Q

(j "\/" D) * j9 is Element of the carrier of Q

the multF of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

the multF of Q . ((j "\/" D),j9) is Element of the carrier of Q

[(j "\/" D),j9] is set

{(j "\/" D),j9} is non empty finite set

{(j "\/" D)} is non empty finite set

{{(j "\/" D),j9},{(j "\/" D)}} is non empty finite V45() set

the multF of Q . [(j "\/" D),j9] is set

j * j9 is Element of the carrier of Q

the multF of Q . (j,j9) is Element of the carrier of Q

[j,j9] is set

{j,j9} is non empty finite set

{{j,j9},{j}} is non empty finite V45() set

the multF of Q . [j,j9] is set

D * j9 is Element of the carrier of Q

the multF of Q . (D,j9) is Element of the carrier of Q

[D,j9] is set

{D,j9} is non empty finite set

{D} is non empty finite set

{{D,j9},{D}} is non empty finite V45() set

the multF of Q . [D,j9] is set

(j * j9) "\/" (D * j9) is Element of the carrier of Q

the L_join of Q . ((j * j9),(D * j9)) is Element of the carrier of Q

[(j * j9),(D * j9)] is set

{(j * j9),(D * j9)} is non empty finite set

{(j * j9)} is non empty finite set

{{(j * j9),(D * j9)},{(j * j9)}} is non empty finite V45() set

the L_join of Q . [(j * j9),(D * j9)] is set

j9 * (j "\/" D) is Element of the carrier of Q

the multF of Q . (j9,(j "\/" D)) is Element of the carrier of Q

[j9,(j "\/" D)] is set

{j9,(j "\/" D)} is non empty finite set

{j9} is non empty finite set

{{j9,(j "\/" D)},{j9}} is non empty finite V45() set

the multF of Q . [j9,(j "\/" D)] is set

j9 * j is Element of the carrier of Q

the multF of Q . (j9,j) is Element of the carrier of Q

[j9,j] is set

{j9,j} is non empty finite set

{{j9,j},{j9}} is non empty finite V45() set

the multF of Q . [j9,j] is set

j9 * D is Element of the carrier of Q

the multF of Q . (j9,D) is Element of the carrier of Q

[j9,D] is set

{j9,D} is non empty finite set

{{j9,D},{j9}} is non empty finite V45() set

the multF of Q . [j9,D] is set

(j9 * j) "\/" (j9 * D) is Element of the carrier of Q

the L_join of Q . ((j9 * j),(j9 * D)) is Element of the carrier of Q

[(j9 * j),(j9 * D)] is set

{(j9 * j),(j9 * D)} is non empty finite set

{(j9 * j)} is non empty finite set

{{(j9 * j),(j9 * D)},{(j9 * j)}} is non empty finite V45() set

the L_join of Q . [(j9 * j),(j9 * D)] is set

{j,D} is non empty finite Element of bool the carrier of Q

bool the carrier of Q is non empty set

{ (b

{ (j9 * b

X is set

x is Element of the carrier of Q

x * j9 is Element of the carrier of Q

the multF of Q . (x,j9) is Element of the carrier of Q

[x,j9] is set

{x,j9} is non empty finite set

{x} is non empty finite set

{{x,j9},{x}} is non empty finite V45() set

the multF of Q . [x,j9] is set

{(j * j9),(D * j9)} is non empty finite Element of bool the carrier of Q

X is set

x is Element of the carrier of Q

j9 * x is Element of the carrier of Q

the multF of Q . (j9,x) is Element of the carrier of Q

[j9,x] is set

{j9,x} is non empty finite set

{{j9,x},{j9}} is non empty finite V45() set

the multF of Q . [j9,x] is set

{(j9 * j),(j9 * D)} is non empty finite Element of bool the carrier of Q

"\/" ({j,D},Q) is Element of the carrier of Q

"\/" ( { (b

"\/" ( { (j9 * b

Q is non empty set

[:Q,Q:] is non empty V7() set

[:[:Q,Q:],Q:] is non empty V7() set

bool [:[:Q,Q:],Q:] is non empty set

j is non empty V7() V10([:Q,Q:]) V11(Q) Function-like V17([:Q,Q:]) V21([:Q,Q:],Q) Element of bool [:[:Q,Q:],Q:]

D is non empty V7() V10([:Q,Q:]) V11(Q) Function-like V17([:Q,Q:]) V21([:Q,Q:],Q) Element of bool [:[:Q,Q:],Q:]

j9 is non empty V7() V10([:Q,Q:]) V11(Q) Function-like V17([:Q,Q:]) V21([:Q,Q:],Q) Element of bool [:[:Q,Q:],Q:]

f is Element of Q

(Q,j,D,j9,f) is () ()

the carrier of (BooleLatt {}) is non empty set

the Element of the carrier of (BooleLatt {}) is Element of the carrier of (BooleLatt {})

[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):] is non empty V7() set

[:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty V7() set

bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty set

the non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

the L_join of (BooleLatt {}) is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

the L_meet of (BooleLatt {}) is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

(H

Q is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ()

the carrier of Q is non empty set

bool the carrier of Q is non empty set

j is Element of bool the carrier of Q

D is Element of bool the carrier of Q

"\/" (j,Q) is Element of the carrier of Q

"\/" (D,Q) is Element of the carrier of Q

("\/" (j,Q)) * ("\/" (D,Q)) is Element of the carrier of Q

the multF of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

[: the carrier of Q, the carrier of Q:] is non empty V7() set

[:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty V7() set

bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty set

the multF of Q . (("\/" (j,Q)),("\/" (D,Q))) is Element of the carrier of Q

[("\/" (j,Q)),("\/" (D,Q))] is set

{("\/" (j,Q)),("\/" (D,Q))} is non empty finite set

{("\/" (j,Q))} is non empty finite set

{{("\/" (j,Q)),("\/" (D,Q))},{("\/" (j,Q))}} is non empty finite V45() set

the multF of Q . [("\/" (j,Q)),("\/" (D,Q))] is set

{ (b

"\/" ( { (b

j9 is Element of the carrier of Q

f is Element of the carrier of Q

j9 "\/" f is Element of the carrier of Q

the L_join of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

the L_join of Q . (j9,f) is Element of the carrier of Q

[j9,f] is set

{j9,f} is non empty finite set

{j9} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the L_join of Q . [j9,f] is set

L is Element of the carrier of Q

(j9 "\/" f) * L is Element of the carrier of Q

the multF of Q . ((j9 "\/" f),L) is Element of the carrier of Q

[(j9 "\/" f),L] is set

{(j9 "\/" f),L} is non empty finite set

{(j9 "\/" f)} is non empty finite set

{{(j9 "\/" f),L},{(j9 "\/" f)}} is non empty finite V45() set

the multF of Q . [(j9 "\/" f),L] is set

j9 * L is Element of the carrier of Q

the multF of Q . (j9,L) is Element of the carrier of Q

[j9,L] is set

{j9,L} is non empty finite set

{{j9,L},{j9}} is non empty finite V45() set

the multF of Q . [j9,L] is set

f * L is Element of the carrier of Q

the multF of Q . (f,L) is Element of the carrier of Q

[f,L] is set

{f,L} is non empty finite set

{f} is non empty finite set

{{f,L},{f}} is non empty finite V45() set

the multF of Q . [f,L] is set

(j9 * L) "\/" (f * L) is Element of the carrier of Q

the L_join of Q . ((j9 * L),(f * L)) is Element of the carrier of Q

[(j9 * L),(f * L)] is set

{(j9 * L),(f * L)} is non empty finite set

{(j9 * L)} is non empty finite set

{{(j9 * L),(f * L)},{(j9 * L)}} is non empty finite V45() set

the L_join of Q . [(j9 * L),(f * L)] is set

x9 is Element of the carrier of Q

X is Element of the carrier of Q

x is Element of the carrier of Q

X "\/" x is Element of the carrier of Q

the L_join of Q . (X,x) is Element of the carrier of Q

[X,x] is set

{X,x} is non empty finite set

{X} is non empty finite set

{{X,x},{X}} is non empty finite V45() set

the L_join of Q . [X,x] is set

x9 * (X "\/" x) is Element of the carrier of Q

the multF of Q . (x9,(X "\/" x)) is Element of the carrier of Q

[x9,(X "\/" x)] is set

{x9,(X "\/" x)} is non empty finite set

{x9} is non empty finite set

{{x9,(X "\/" x)},{x9}} is non empty finite V45() set

the multF of Q . [x9,(X "\/" x)] is set

x9 * X is Element of the carrier of Q

the multF of Q . (x9,X) is Element of the carrier of Q

[x9,X] is set

{x9,X} is non empty finite set

{{x9,X},{x9}} is non empty finite V45() set

the multF of Q . [x9,X] is set

x9 * x is Element of the carrier of Q

the multF of Q . (x9,x) is Element of the carrier of Q

[x9,x] is set

{x9,x} is non empty finite set

{{x9,x},{x9}} is non empty finite V45() set

the multF of Q . [x9,x] is set

(x9 * X) "\/" (x9 * x) is Element of the carrier of Q

the L_join of Q . ((x9 * X),(x9 * x)) is Element of the carrier of Q

[(x9 * X),(x9 * x)] is set

{(x9 * X),(x9 * x)} is non empty finite set

{(x9 * X)} is non empty finite set

{{(x9 * X),(x9 * x)},{(x9 * X)}} is non empty finite V45() set

the L_join of Q . [(x9 * X),(x9 * x)] is set

the carrier of (BooleLatt {}) is non empty set

the Element of the carrier of (BooleLatt {}) is Element of the carrier of (BooleLatt {})

[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):] is non empty V7() set

[:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty V7() set

bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty set

the non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):] is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

the L_join of (BooleLatt {}) is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

the L_meet of (BooleLatt {}) is non empty V7() V10([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V11( the carrier of (BooleLatt {})) Function-like V17([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):]) V21([: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {})) Element of bool [:[: the carrier of (BooleLatt {}), the carrier of (BooleLatt {}):], the carrier of (BooleLatt {}):]

(H

j9 is non empty () ()

Q is non empty unital ()

j is non empty associative join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete () () ()

Bottom j is Element of the carrier of j

the carrier of j is non empty set

"\/" ({},j) is Element of the carrier of j

D is Element of the carrier of j

D is Element of the carrier of j

f is Element of the carrier of j

{ H

j9 is Element of the carrier of j

j9 * f is Element of the carrier of j

the multF of j is non empty V7() V10([: the carrier of j, the carrier of j:]) V11( the carrier of j) Function-like V17([: the carrier of j, the carrier of j:]) V21([: the carrier of j, the carrier of j:], the carrier of j) Element of bool [:[: the carrier of j, the carrier of j:], the carrier of j:]

[: the carrier of j, the carrier of j:] is non empty V7() set

[:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty V7() set

bool [:[: the carrier of j, the carrier of j:], the carrier of j:] is non empty set

the multF of j . (j9,f) is Element of the carrier of j

[j9,f] is set

{j9,f} is non empty finite set

{j9} is non empty finite set

{{j9,f},{j9}} is non empty finite V45() set

the multF of j . [j9,f] is set

D is Element of the carrier of j

D * (Bottom j) is Element of the carrier of j

the multF of j . (D,(Bottom j)) is Element of the carrier of j

[D,(Bottom j)] is set

{D,(Bottom j)} is non empty finite set

{D} is non empty finite set

{{D,(Bottom j)},{D}} is non empty finite V45() set

the multF of j . [D,(Bottom j)] is set

{ H

Q is non empty associative join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete () () ()

the carrier of Q is non empty set

j is Element of the carrier of Q

D is Element of the carrier of Q

j9 is Element of the carrier of Q

j * j9 is Element of the carrier of Q

the multF of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

[: the carrier of Q, the carrier of Q:] is non empty V7() set

[:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty V7() set

bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty set

the multF of Q . (j,j9) is Element of the carrier of Q

[j,j9] is set

{j,j9} is non empty finite set

{j} is non empty finite set

{{j,j9},{j}} is non empty finite V45() set

the multF of Q . [j,j9] is set

D * j9 is Element of the carrier of Q

the multF of Q . (D,j9) is Element of the carrier of Q

[D,j9] is set

{D,j9} is non empty finite set

{D} is non empty finite set

{{D,j9},{D}} is non empty finite V45() set

the multF of Q . [D,j9] is set

j9 * j is Element of the carrier of Q

the multF of Q . (j9,j) is Element of the carrier of Q

[j9,j] is set

{j9,j} is non empty finite set

{j9} is non empty finite set

{{j9,j},{j9}} is non empty finite V45() set

the multF of Q . [j9,j] is set

j9 * D is Element of the carrier of Q

the multF of Q . (j9,D) is Element of the carrier of Q

[j9,D] is set

{j9,D} is non empty finite set

{{j9,D},{j9}} is non empty finite V45() set

the multF of Q . [j9,D] is set

(j * j9) "\/" (D * j9) is Element of the carrier of Q

the L_join of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

the L_join of Q . ((j * j9),(D * j9)) is Element of the carrier of Q

[(j * j9),(D * j9)] is set

{(j * j9),(D * j9)} is non empty finite set

{(j * j9)} is non empty finite set

{{(j * j9),(D * j9)},{(j * j9)}} is non empty finite V45() set

the L_join of Q . [(j * j9),(D * j9)] is set

j "\/" D is Element of the carrier of Q

the L_join of Q . (j,D) is Element of the carrier of Q

[j,D] is set

{j,D} is non empty finite set

{{j,D},{j}} is non empty finite V45() set

the L_join of Q . [j,D] is set

(j "\/" D) * j9 is Element of the carrier of Q

the multF of Q . ((j "\/" D),j9) is Element of the carrier of Q

[(j "\/" D),j9] is set

{(j "\/" D),j9} is non empty finite set

{(j "\/" D)} is non empty finite set

{{(j "\/" D),j9},{(j "\/" D)}} is non empty finite V45() set

the multF of Q . [(j "\/" D),j9] is set

(j9 * j) "\/" (j9 * D) is Element of the carrier of Q

the L_join of Q . ((j9 * j),(j9 * D)) is Element of the carrier of Q

[(j9 * j),(j9 * D)] is set

{(j9 * j),(j9 * D)} is non empty finite set

{(j9 * j)} is non empty finite set

{{(j9 * j),(j9 * D)},{(j9 * j)}} is non empty finite V45() set

the L_join of Q . [(j9 * j),(j9 * D)] is set

j9 * (j "\/" D) is Element of the carrier of Q

the multF of Q . (j9,(j "\/" D)) is Element of the carrier of Q

[j9,(j "\/" D)] is set

{j9,(j "\/" D)} is non empty finite set

{{j9,(j "\/" D)},{j9}} is non empty finite V45() set

the multF of Q . [j9,(j "\/" D)] is set

Q is non empty associative join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete () () ()

the carrier of Q is non empty set

j is Element of the carrier of Q

D is Element of the carrier of Q

j9 is Element of the carrier of Q

j * j9 is Element of the carrier of Q

the multF of Q is non empty V7() V10([: the carrier of Q, the carrier of Q:]) V11( the carrier of Q) Function-like V17([: the carrier of Q, the carrier of Q:]) V21([: the carrier of Q, the carrier of Q:], the carrier of Q) Element of bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:]

[: the carrier of Q, the carrier of Q:] is non empty V7() set

[:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty V7() set

bool [:[: the carrier of Q, the carrier of Q:], the carrier of Q:] is non empty set

the multF of Q . (j,j9) is Element of the carrier of Q

[j,j9] is set

{j,j9} is non empty finite set

{j} is non empty finite set

{{j,j9},{j}} is non empty finite V45() set

the multF of Q . [j,j9] is set

f is Element of the carrier of Q

D * f is Element of the carrier of Q

the multF of Q . (D,f) is Element of the carrier of Q

[D,f] is set

{D,f} is non empty finite set

{D} is non empty finite set

{{D,f},{D}} is non empty finite V45() set

the multF of Q . [D,f] is set

D * j9 is Element of the carrier of Q

the multF of Q . (D,j9) is Element of the carrier of Q

[D,j9] is set

{D,j9} is non empty finite set

{{D,j9},{D}} is non empty finite V45() set

the multF of Q . [D,j9] is set

Q is non empty set

[:Q,Q:] is non empty V7() set

bool [:Q,Q:] is non empty set

j is non empty V7() V10(Q) V11(Q) Function-like V17(Q) V21(Q,Q) Element of bool [:Q,Q:]

j * j is non empty V7() V10(Q) V11(Q) Function-like V17(Q) V21(Q,Q) Element of bool [:Q,Q:]

D is Element of Q

j . D is Element of Q

j . (j . D) is Element of Q

Q is non empty LattStr

the carrier of Q is non empty set

[: the carrier of Q, the carrier of Q:] is non empty V7() set

bool