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

1 is non empty set
bool {} is non empty finite V45() set
is non empty functional finite V45() set
F2() is non empty set
F1() is non empty set
{ F4(b1) where b1 is Element of F1() : P1[b1] } is set
{ F3(b1) where b1 is Element of F2() : b1 in { F4(b1) where b2 is Element of F1() : P1[b1] } } is set
{ F3(F4(b1)) where b1 is Element of F1() : P1[b1] } is set
Q is set
j is Element of F2()
F3(j) is set
D is Element of F1()
F4(D) is Element of F2()
Q is set
j is Element of F1()
F4(j) is Element of F2()
F3(F4(j)) is set
F1() is non empty set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
Q is non empty set
the Element of Q is Element of Q
D is Element of F1()
F2(D) 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 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),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

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 () 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
H4(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 multF of j . [f,L] is set
H4(j) . (j9,(H4(j) . (f,L))) is Element of the carrier of j
[j9,(H4(j) . (f,L))] is set
{j9,(H4(j) . (f,L))} is non empty finite set
{j9} is non empty finite set
{{j9,(H4(j) . (f,L))},{j9}} is non empty finite V45() set
the multF of j . [j9,(H4(j) . (f,L))] is set
H4(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 multF of j . [j9,f] is set
H4(j) . ((H4(j) . (j9,f)),L) is Element of the carrier of j
[(H4(j) . (j9,f)),L] is set
{(H4(j) . (j9,f)),L} is non empty finite set
{(H4(j) . (j9,f))} is non empty finite set
{{(H4(j) . (j9,f)),L},{(H4(j) . (j9,f))}} is non empty finite V45() set
the multF of j . [(H4(j) . (j9,f)),L] is set
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
H4(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
H4(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 multF of j . [f,j9] is set
j9 is Element of the carrier of j
H4(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
H4(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 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 ()
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 ()
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 * b1) where b1 is Element of the carrier of j : b1 in f } is set
"\/" ( { (j9 * b1) where b1 is Element of the carrier of j : b1 in f } ,j) is Element of the carrier of j
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
{ (b1 * j9) where b1 is Element of the carrier of j : b1 in f } is set
"\/" ( { (b1 * j9) where b1 is Element of the carrier of j : b1 in f } ,j) is Element of the carrier of j
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 () is non empty set
[: the carrier of (), the carrier of ():] is non empty V7() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_join of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_meet of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
(H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]) is non empty () ()

the carrier of F1() is non empty set
F4() is set
F3() is set
{ ("\/" ( { F2(b1,b2) where b2 is Element of the carrier of F1() : b2 in F4() } ,F1())) where b1 is Element of the carrier of F1() : b1 in F3() } is set
"\/" ( { ("\/" ( { F2(b1,b2) where b2 is Element of the carrier of F1() : b2 in F4() } ,F1())) where b1 is Element of the carrier of F1() : b1 in F3() } ,F1()) is Element of the carrier of F1()
{ F2(b1,b2) where b1, b2 is Element of the carrier of F1() : ( b1 in F3() & b2 in F4() ) } is set
"\/" ( { F2(b1,b2) where b1, b2 is Element of the carrier of F1() : ( b1 in F3() & b2 in F4() ) } ,F1()) is Element of the carrier of F1()
{ { F2(b1,b2) where b2 is Element of the carrier of F1() : b2 in F4() } where b1 is Element of the carrier of F1() : b1 in F3() } is set
bool the carrier of F1() is non empty set
{ ("\/" (b1,F1())) where b1 is Element of bool the carrier of F1() : b1 in { { F2(b1,b2) where b3 is Element of the carrier of F1() : b2 in F4() } where b2 is Element of the carrier of F1() : b1 in F3() } } is set
X is set
x is Element of bool the carrier of F1()
"\/" (x,F1()) is Element of the carrier of F1()
x9 is Element of the carrier of F1()
{ F2(x9,b1) where b1 is Element of the carrier of F1() : b1 in F4() } is set
X is set
x is Element of the carrier of F1()
{ F2(x,b1) where b1 is Element of the carrier of F1() : b1 in F4() } is set
"\/" ( { F2(x,b1) where b1 is Element of the carrier of F1() : b1 in F4() } ,F1()) is Element of the carrier of F1()
x9 is set
a9 is Element of the carrier of F1()
F2(x,a9) is Element of the carrier of F1()
union { { F2(b1,b2) where b2 is Element of the carrier of F1() : b2 in F4() } where b1 is Element of the carrier of F1() : b1 in F3() } is set
X is set
x is Element of the carrier of F1()
x9 is Element of the carrier of F1()
F2(x,x9) is Element of the carrier of F1()
{ F2(x,b1) where b1 is Element of the carrier of F1() : b1 in F4() } is set
X is set
x is set
x9 is Element of the carrier of F1()
{ F2(x9,b1) where b1 is Element of the carrier of F1() : b1 in F4() } is set
a9 is Element of the carrier of F1()
F2(x9,a9) is Element of the carrier of F1()
bool H1(F1()) is non empty Element of bool (bool H1(F1()))
bool H1(F1()) is non empty set
bool (bool H1(F1())) is non empty set
X is set
x is Element of the carrier of F1()
{ F2(x,b1) where b1 is Element of the carrier of F1() : b1 in F4() } is set
x9 is set
a9 is Element of the carrier of F1()
F2(x,a9) is Element of the carrier of F1()

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
{ (b1 * b2) where b1, b2 is Element of the carrier of Q : ( b1 in j & b2 in D ) } is set
"\/" ( { (b1 * b2) where b1, b2 is Element of the carrier of Q : ( b1 in j & b2 in D ) } ,Q) is Element of the carrier of Q
{ (a1 * b1) where b1 is Element of the carrier of Q : b1 in D } is set
"\/" ( { (a1 * b1) where b1 is Element of the carrier of Q : b1 in D } ,Q) is Element of the carrier of Q
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 * b1) where b1 is Element of the carrier of Q : b1 in D } is set
"\/" ( { (j9 * b1) where b1 is Element of the carrier of Q : b1 in D } ,Q) is Element of the carrier of Q
{ H5(b1) where b1 is Element of the carrier of Q : S1[b1] } is set
{ H6(b1) where b1 is Element of the carrier of Q : S1[b1] } is set
{ ("\/" ( { H7(b1,b2) where b2 is Element of the carrier of Q : b2 in D } ,Q)) where b1 is Element of the carrier of Q : b1 in j } is set
"\/" ( { ("\/" ( { H7(b1,b2) where b2 is Element of the carrier of Q : b2 in D } ,Q)) where b1 is Element of the carrier of Q : b1 in j } ,Q) is Element of the carrier of Q
{ H7(b1,b2) where b1, b2 is Element of the carrier of Q : ( b1 in j & b2 in D ) } is set
"\/" ( { H7(b1,b2) where b1, b2 is Element of the carrier of Q : ( b1 in j & b2 in D ) } ,Q) is Element of the carrier of Q

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
{ (b1 * j9) where b1 is Element of the carrier of Q : b1 in {j,D} } is set
{ (j9 * b1) where b1 is Element of the carrier of Q : b1 in {j,D} } is set
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
"\/" ( { (b1 * j9) where b1 is Element of the carrier of Q : b1 in {j,D} } ,Q) is Element of the carrier of Q
"\/" ( { (j9 * b1) where b1 is Element of the carrier of Q : b1 in {j,D} } ,Q) is Element of the carrier of Q
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 () is non empty set
the Element of the carrier of () is Element of the carrier of ()
[: the carrier of (), the carrier of ():] is non empty V7() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_join of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_meet of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
(H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():], the Element of the carrier of ()) is non empty () ()

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
{ (b1 * b2) where b1, b2 is Element of the carrier of Q : ( b1 in j & b2 in D ) } is set
"\/" ( { (b1 * b2) where b1, b2 is Element of the carrier of Q : ( b1 in j & b2 in D ) } ,Q) is Element of the carrier of Q
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 () is non empty set
the Element of the carrier of () is Element of the carrier of ()
[: the carrier of (), the carrier of ():] is non empty V7() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_join of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_meet of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
(H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) V21([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():], the Element of the carrier of ()) is non empty () ()
j9 is non empty () ()
Q is non empty unital ()

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
{ H5(b1) where b1 is Element of the carrier of j : S1[b1] } is set
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 * () is Element of the carrier of j
the multF of j . (D,()) is Element of the carrier of j
[D,()] is set
{D,()} is non empty finite set
{D} is non empty finite set
{{D,()},{D}} is non empty finite V45() set
the multF of j . [D,()] is set
{ H5(b1) where b1 is Element of the carrier of j : S1[b1] } is set

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

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