:: 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₂() is non empty set
F₁() is non empty set
{ F₄(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
{ F₃(b₁) where b₁ is Element of F₂() : b₁ in { F₄(b₁) where b₂ is Element of F₁() : P₁[b₁] } } is set
{ F₃(F₄(b₁)) where b₁ is Element of F₁() : P₁[b₁] } is set
Q is set
j is Element of F₂()
F₃(j) is set
D is Element of F₁()
F₄(D) is Element of F₂()
Q is set
j is Element of F₁()
F₄(j) is Element of F₂()
F₃(F₄(j)) is set
F₁() is non empty set
{ F₂(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
Q is non empty set
the Element of Q is Element of Q
D is Element of F₁()
F₂(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 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₄(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
H₄(j) . (j9,(H₄(j) . (f,L))) is Element of the carrier of j
[j9,(H₄(j) . (f,L))] is set
{j9,(H₄(j) . (f,L))} is non empty finite set
{j9} is non empty finite set
{{j9,(H₄(j) . (f,L))},{j9}} is non empty finite V45() set
the multF of j . [j9,(H₄(j) . (f,L))] is set
H₄(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
H₄(j) . ((H₄(j) . (j9,f)),L) is Element of the carrier of j
[(H₄(j) . (j9,f)),L] is set
{(H₄(j) . (j9,f)),L} is non empty finite set
{(H₄(j) . (j9,f))} is non empty finite set
{{(H₄(j) . (j9,f)),L},{(H₄(j) . (j9,f))}} is non empty finite V45() set
the multF of j . [(H₄(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
H₄(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
H₄(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
H₄(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
H₄(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 (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₁) where b₁ is Element of the carrier of j : b₁ in f } is set
"\/" ( { (j9 * b₁) where b₁ is Element of the carrier of j : b₁ 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
{ (b₁ * j9) where b₁ is Element of the carrier of j : b₁ in f } is set
"\/" ( { (b₁ * j9) where b₁ is Element of the carrier of j : b₁ 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 (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₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}), 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 () ()
F₁() is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ()
the carrier of F₁() is non empty set
F₄() is set
F₃() is set
{ ("\/" ( { F₂(b₁,b₂) where b₂ is Element of the carrier of F₁() : b₂ in F₄() } ,F₁())) where b₁ is Element of the carrier of F₁() : b₁ in F₃() } is set
"\/" ( { ("\/" ( { F₂(b₁,b₂) where b₂ is Element of the carrier of F₁() : b₂ in F₄() } ,F₁())) where b₁ is Element of the carrier of F₁() : b₁ in F₃() } ,F₁()) is Element of the carrier of F₁()
{ F₂(b₁,b₂) where b₁, b₂ is Element of the carrier of F₁() : ( b₁ in F₃() & b₂ in F₄() ) } is set
"\/" ( { F₂(b₁,b₂) where b₁, b₂ is Element of the carrier of F₁() : ( b₁ in F₃() & b₂ in F₄() ) } ,F₁()) is Element of the carrier of F₁()
{ { F₂(b₁,b₂) where b₂ is Element of the carrier of F₁() : b₂ in F₄() } where b₁ is Element of the carrier of F₁() : b₁ in F₃() } is set
bool the carrier of F₁() is non empty set
{ ("\/" (b₁,F₁())) where b₁ is Element of bool the carrier of F₁() : b₁ in { { F₂(b₁,b₂) where b₃ is Element of the carrier of F₁() : b₂ in F₄() } where b₂ is Element of the carrier of F₁() : b₁ in F₃() } } is set
X is set
x is Element of bool the carrier of F₁()
"\/" (x,F₁()) is Element of the carrier of F₁()
x9 is Element of the carrier of F₁()
{ F₂(x9,b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₄() } is set
X is set
x is Element of the carrier of F₁()
{ F₂(x,b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₄() } is set
"\/" ( { F₂(x,b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₄() } ,F₁()) is Element of the carrier of F₁()
x9 is set
a9 is Element of the carrier of F₁()
F₂(x,a9) is Element of the carrier of F₁()
union { { F₂(b₁,b₂) where b₂ is Element of the carrier of F₁() : b₂ in F₄() } where b₁ is Element of the carrier of F₁() : b₁ in F₃() } is set
X is set
x is Element of the carrier of F₁()
x9 is Element of the carrier of F₁()
F₂(x,x9) is Element of the carrier of F₁()
{ F₂(x,b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₄() } is set
X is set
x is set
x9 is Element of the carrier of F₁()
{ F₂(x9,b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₄() } is set
a9 is Element of the carrier of F₁()
F₂(x9,a9) is Element of the carrier of F₁()
bool H₁(F₁()) is non empty Element of bool (bool H₁(F₁()))
bool H₁(F₁()) is non empty set
bool (bool H₁(F₁())) is non empty set
X is set
x is Element of the carrier of F₁()
{ F₂(x,b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₄() } is set
x9 is set
a9 is Element of the carrier of F₁()
F₂(x,a9) is Element of the carrier of 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₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in j & b₂ in D ) } is set
"\/" ( { (b₁ * b₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in j & b₂ in D ) } ,Q) is Element of the carrier of Q
{ (a₁ * b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (a₁ * b₁) where b₁ is Element of the carrier of Q : b₁ 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 * b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (j9 * b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₆(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ ("\/" ( { H₇(b₁,b₂) where b₂ is Element of the carrier of Q : b₂ in D } ,Q)) where b₁ is Element of the carrier of Q : b₁ in j } is set
"\/" ( { ("\/" ( { H₇(b₁,b₂) where b₂ is Element of the carrier of Q : b₂ in D } ,Q)) where b₁ is Element of the carrier of Q : b₁ in j } ,Q) is Element of the carrier of Q
{ H₇(b₁,b₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in j & b₂ in D ) } is set
"\/" ( { H₇(b₁,b₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in j & b₂ in D ) } ,Q) is Element of the carrier of Q
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) where b₁ is Element of the carrier of Q : b₁ in {j,D} } is set
{ (j9 * b₁) where b₁ is Element of the carrier of Q : b₁ 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
"\/" ( { (b₁ * j9) where b₁ is Element of the carrier of Q : b₁ in {j,D} } ,Q) is Element of the carrier of Q
"\/" ( { (j9 * b₁) where b₁ is Element of the carrier of Q : b₁ 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 (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₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}), 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 {}):], the Element of the carrier of (BooleLatt {})) is non empty () ()
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₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in j & b₂ in D ) } is set
"\/" ( { (b₁ * b₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in j & b₂ 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 (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₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}), 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 {}):], the Element of the carrier of (BooleLatt {})) is non empty () ()
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₅(b₁) where b₁ is Element of the carrier of j : S₁[b₁] } 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 * (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₅(b₁) where b₁ is Element of the carrier of j : S₁[b₁] } 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
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 [: the carrier of Q, the carrier of Q:] is non empty set
Q is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of Q is non empty set
[: the carrier of Q, the carrier of Q:] is non empty V7() set
bool [: the carrier of Q, the carrier of Q:] is non empty set
id the carrier of Q is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like one-to-one V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
j is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
D is Element of the carrier of Q
j . D is Element of the carrier of Q
D is Element of the carrier of Q
j . D is Element of the carrier of Q
D is Element of the carrier of Q
j9 is Element of the carrier of Q
j . D is Element of the carrier of Q
j . j9 is Element of the carrier of Q
Q is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of Q is non empty set
[: the carrier of Q, the carrier of Q:] is non empty V7() set
bool [: the carrier of Q, the carrier of Q:] is non empty set
bool the carrier of Q is non empty set
j is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
D is Element of bool the carrier of Q
"\/" (D,Q) is Element of the carrier of Q
j . ("\/" (D,Q)) is Element of the carrier of Q
{ (j . b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (j . b₁) where b₁ is Element of the carrier of Q : b₁ 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
j . f is Element of the carrier of Q
D is Element of bool the carrier of Q
"\/" (D,Q) is Element of the carrier of Q
j . ("\/" (D,Q)) is Element of the carrier of Q
{ (j . b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (j . b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
Q is non empty ()
the carrier of Q is non empty set
[: the carrier of Q, the carrier of Q:] is non empty V7() set
bool [: the carrier of Q, the carrier of Q:] is non empty set
Q is non empty ()
the carrier of Q is non empty set
j is Element of the carrier of Q
D is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= D } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= D } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j * b₁ [= D } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : j * b₁ [= D } ,Q) is Element of the carrier of Q
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
j * D 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,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 multF of Q . [j,D] is set
j9 is Element of the carrier of Q
(Q,j,j9) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j * b₁ [= j9 } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : j * b₁ [= j9 } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j * b₁ [= j9 } is set
L is set
X is Element of the carrier of Q
j * X is Element of the carrier of Q
the multF of Q . (j,X) is Element of the carrier of Q
[j,X] is set
{j,X} is non empty finite set
{{j,X},{j}} is non empty finite V45() set
the multF of Q . [j,X] is set
bool the carrier of Q is non empty set
L is Element of bool the carrier of Q
L is Element of bool the carrier of Q
"\/" (L,Q) is Element of the carrier of Q
j * ("\/" (L,Q)) is Element of the carrier of Q
the multF of Q . (j,("\/" (L,Q))) is Element of the carrier of Q
[j,("\/" (L,Q))] is set
{j,("\/" (L,Q))} is non empty finite set
{{j,("\/" (L,Q))},{j}} is non empty finite V45() set
the multF of Q . [j,("\/" (L,Q))] is set
X is Element of the carrier of Q
j * X is Element of the carrier of Q
the multF of Q . (j,X) is Element of the carrier of Q
[j,X] is set
{j,X} is non empty finite set
{{j,X},{j}} is non empty finite V45() set
the multF of Q . [j,X] is set
x is Element of the carrier of Q
j * x is Element of the carrier of Q
the multF of Q . (j,x) is Element of the carrier of Q
[j,x] is set
{j,x} is non empty finite set
{{j,x},{j}} is non empty finite V45() set
the multF of Q . [j,x] is set
X is Element of the carrier of Q
j * X is Element of the carrier of Q
the multF of Q . (j,X) is Element of the carrier of Q
[j,X] is set
{j,X} is non empty finite set
{{j,X},{j}} is non empty finite V45() set
the multF of Q . [j,X] is set
x is Element of the carrier of Q
j * x is Element of the carrier of Q
the multF of Q . (j,x) is Element of the carrier of Q
[j,x] is set
{j,x} is non empty finite set
{{j,x},{j}} is non empty finite V45() set
the multF of Q . [j,x] is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₂[b₁] } is set
{ (j * b₁) where b₁ is Element of the carrier of Q : b₁ in L } is set
X is Element of the carrier of Q
x is Element of the carrier of Q
j * x is Element of the carrier of Q
the multF of Q . (j,x) is Element of the carrier of Q
[j,x] is set
{j,x} is non empty finite set
{{j,x},{j}} is non empty finite V45() set
the multF of Q . [j,x] is set
"\/" ( { (j * b₁) where b₁ is Element of the carrier of Q : b₁ in L } ,Q) is Element of the carrier of Q
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
j * D 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,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 multF of Q . [j,D] is set
j9 is Element of the carrier of Q
(Q,D,j9) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j9 } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j9 } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j9 } is set
L is set
X is Element of the carrier of Q
X * D is Element of the carrier of Q
the multF of Q . (X,D) is Element of the carrier of Q
[X,D] is set
{X,D} is non empty finite set
{X} is non empty finite set
{{X,D},{X}} is non empty finite V45() set
the multF of Q . [X,D] is set
bool the carrier of Q is non empty set
L is Element of bool the carrier of Q
L is Element of bool the carrier of Q
"\/" (L,Q) is Element of the carrier of Q
("\/" (L,Q)) * D is Element of the carrier of Q
the multF of Q . (("\/" (L,Q)),D) is Element of the carrier of Q
[("\/" (L,Q)),D] is set
{("\/" (L,Q)),D} is non empty finite set
{("\/" (L,Q))} is non empty finite set
{{("\/" (L,Q)),D},{("\/" (L,Q))}} is non empty finite V45() set
the multF of Q . [("\/" (L,Q)),D] is set
X is Element of the carrier of Q
X * D is Element of the carrier of Q
the multF of Q . (X,D) is Element of the carrier of Q
[X,D] is set
{X,D} is non empty finite set
{X} is non empty finite set
{{X,D},{X}} is non empty finite V45() set
the multF of Q . [X,D] is set
x is Element of the carrier of Q
x * D is Element of the carrier of Q
the multF of Q . (x,D) is Element of the carrier of Q
[x,D] is set
{x,D} is non empty finite set
{x} is non empty finite set
{{x,D},{x}} is non empty finite V45() set
the multF of Q . [x,D] is set
X is Element of the carrier of Q
X * D is Element of the carrier of Q
the multF of Q . (X,D) is Element of the carrier of Q
[X,D] is set
{X,D} is non empty finite set
{X} is non empty finite set
{{X,D},{X}} is non empty finite V45() set
the multF of Q . [X,D] is set
x is Element of the carrier of Q
x * D is Element of the carrier of Q
the multF of Q . (x,D) is Element of the carrier of Q
[x,D] is set
{x,D} is non empty finite set
{x} is non empty finite set
{{x,D},{x}} is non empty finite V45() set
the multF of Q . [x,D] is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₂[b₁] } is set
{ (b₁ * D) where b₁ is Element of the carrier of Q : b₁ in L } is set
X is Element of the carrier of Q
x is Element of the carrier of Q
x * D is Element of the carrier of Q
the multF of Q . (x,D) is Element of the carrier of Q
[x,D] is set
{x,D} is non empty finite set
{x} is non empty finite set
{{x,D},{x}} is non empty finite V45() set
the multF of Q . [x,D] is set
"\/" ( { (b₁ * D) where b₁ is Element of the carrier of Q : b₁ in L } ,Q) is Element of the carrier of Q
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
D is Element of the carrier of Q
j9 is Element of the carrier of Q
j is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } ,Q) is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } ,Q) is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j9 * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : j9 * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } is set
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } is set
f is set
L is Element of the carrier of Q
L * 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 . (L,j9) is Element of the carrier of Q
[L,j9] is set
{L,j9} is non empty finite set
{L} is non empty finite set
{{L,j9},{L}} is non empty finite V45() set
the multF of Q . [L,j9] is set
L * D is Element of the carrier of Q
the multF of Q . (L,D) is Element of the carrier of Q
[L,D] is set
{L,D} is non empty finite set
{{L,D},{L}} is non empty finite V45() set
the multF of Q . [L,D] is set
{ b₁ where b₁ is Element of the carrier of Q : j9 * b₁ [= j } is set
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } is set
f is set
L is Element of the carrier of Q
j9 * L 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 . (j9,L) is Element of the carrier of Q
[j9,L] is set
{j9,L} is non empty finite set
{j9} is non empty finite set
{{j9,L},{j9}} is non empty finite V45() set
the multF of Q . [j9,L] is set
D * L is Element of the carrier of Q
the multF of Q . (D,L) is Element of the carrier of Q
[D,L] is set
{D,L} is non empty finite set
{D} is non empty finite set
{{D,L},{D}} is non empty finite V45() set
the multF of Q . [D,L] 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
[: the carrier of Q, the carrier of Q:] is non empty V7() set
bool [: the carrier of Q, the carrier of Q:] is non empty set
j is Element of the carrier of Q
D is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
j9 is Element of the carrier of Q
f is Element of the carrier of Q
D . j9 is Element of the carrier of Q
D . f is Element of the carrier of Q
(Q,f,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * f [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * f [= j } ,Q) is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } ,Q) is Element of the carrier of Q
(Q,(Q,j9,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j9,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j9,j) [= j } ,Q) is Element of the carrier of Q
(Q,(Q,f,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,f,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,f,j) [= j } ,Q) is Element of the carrier of Q
Q is non empty ()
the carrier of Q is non empty 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
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 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 . (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 * 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} is non empty finite set
{{j9,D},{j9}} is non empty finite V45() set
the multF of Q . [j9,D] is set
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } ,Q) is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j9 * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : j9 * b₁ [= j } ,Q) is Element of the carrier of Q
D is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } ,Q) is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } is set
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } is set
L is set
X is Element of the carrier of Q
X * D 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 . (X,D) is Element of the carrier of Q
[X,D] is set
{X,D} is non empty finite set
{X} is non empty finite set
{{X,D},{X}} is non empty finite V45() set
the multF of Q . [X,D] is set
D * X is Element of the carrier of Q
the multF of Q . (D,X) is Element of the carrier of Q
[D,X] is set
{D,X} is non empty finite set
{D} is non empty finite set
{{D,X},{D}} is non empty finite V45() set
the multF of Q . [D,X] is set
L is set
X is Element of the carrier of Q
D * X 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 . (D,X) is Element of the carrier of Q
[D,X] is set
{D,X} is non empty finite set
{D} is non empty finite set
{{D,X},{D}} is non empty finite V45() set
the multF of Q . [D,X] is set
X * D is Element of the carrier of Q
the multF of Q . (X,D) is Element of the carrier of Q
[X,D] is set
{X,D} is non empty finite set
{X} is non empty finite set
{{X,D},{X}} is non empty finite V45() set
the multF of Q . [X,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
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } ,Q) is Element of the carrier of Q
(Q,(Q,D,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } ,Q) is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,(Q,D,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,D,j) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,D,j) * b₁ [= j } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ [= D } is set
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } is set
j9 is set
f is Element of the carrier of Q
(Q,f,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * f [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * f [= j } ,Q) is Element of the carrier of Q
(Q,f,j) * f 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 . ((Q,f,j),f) is Element of the carrier of Q
[(Q,f,j),f] is set
{(Q,f,j),f} is non empty finite set
{(Q,f,j)} is non empty finite set
{{(Q,f,j),f},{(Q,f,j)}} is non empty finite V45() set
the multF of Q . [(Q,f,j),f] is set
f * (Q,f,j) is Element of the carrier of Q
the multF of Q . (f,(Q,f,j)) is Element of the carrier of Q
[f,(Q,f,j)] is set
{f,(Q,f,j)} is non empty finite set
{f} is non empty finite set
{{f,(Q,f,j)},{f}} is non empty finite V45() set
the multF of Q . [f,(Q,f,j)] is set
f * (Q,D,j) is Element of the carrier of Q
the multF of Q . (f,(Q,D,j)) is Element of the carrier of Q
[f,(Q,D,j)] is set
{f,(Q,D,j)} is non empty finite set
{{f,(Q,D,j)},{f}} is non empty finite V45() set
the multF of Q . [f,(Q,D,j)] is set
{ b₁ where b₁ is Element of the carrier of Q : (Q,D,j) * b₁ [= j } is set
j9 is set
f is Element of the carrier of Q
(Q,f,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : f * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : f * b₁ [= j } ,Q) is Element of the carrier of Q
f * (Q,f,j) 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 . (f,(Q,f,j)) is Element of the carrier of Q
[f,(Q,f,j)] is set
{f,(Q,f,j)} is non empty finite set
{f} is non empty finite set
{{f,(Q,f,j)},{f}} is non empty finite V45() set
the multF of Q . [f,(Q,f,j)] is set
(Q,f,j) * f is Element of the carrier of Q
the multF of Q . ((Q,f,j),f) is Element of the carrier of Q
[(Q,f,j),f] is set
{(Q,f,j),f} is non empty finite set
{(Q,f,j)} is non empty finite set
{{(Q,f,j),f},{(Q,f,j)}} is non empty finite V45() set
the multF of Q . [(Q,f,j),f] is set
(Q,D,j) * f is Element of the carrier of Q
the multF of Q . ((Q,D,j),f) is Element of the carrier of Q
[(Q,D,j),f] is set
{(Q,D,j),f} is non empty finite set
{(Q,D,j)} is non empty finite set
{{(Q,D,j),f},{(Q,D,j)}} is non empty finite V45() set
the multF of Q . [(Q,D,j),f] is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ [= D } ,Q) is Element of the carrier of Q
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
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } ,Q) is Element of the carrier of Q
(Q,(Q,D,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } ,Q) is Element of the carrier of Q
(Q,(Q,(Q,D,j),j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,(Q,D,j),j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,(Q,D,j),j) [= j } ,Q) is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,(Q,D,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,D,j) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,D,j) * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,(Q,(Q,D,j),j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,(Q,D,j),j) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,(Q,D,j),j) * b₁ [= j } ,Q) is Element of the carrier of Q
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
D is Element of the carrier of Q
j is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j } ,Q) is Element of the carrier of Q
(Q,(Q,D,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } ,Q) is Element of the carrier of Q
j9 is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } ,Q) is Element of the carrier of Q
(Q,(Q,j9,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j9,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j9,j) [= j } ,Q) is Element of the carrier of Q
(Q,(Q,D,j),j) * (Q,(Q,j9,j),j) 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 . ((Q,(Q,D,j),j),(Q,(Q,j9,j),j)) is Element of the carrier of Q
[(Q,(Q,D,j),j),(Q,(Q,j9,j),j)] is set
{(Q,(Q,D,j),j),(Q,(Q,j9,j),j)} is non empty finite set
{(Q,(Q,D,j),j)} is non empty finite set
{{(Q,(Q,D,j),j),(Q,(Q,j9,j),j)},{(Q,(Q,D,j),j)}} is non empty finite V45() set
the multF of Q . [(Q,(Q,D,j),j),(Q,(Q,j9,j),j)] 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
(Q,(D * j9),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (D * j9) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (D * j9) [= j } ,Q) is Element of the carrier of Q
(Q,(Q,(D * j9),j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,(D * j9),j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,(D * j9),j) [= j } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,a₁,j) [= j } is set
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j) [= j } is set
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j9,j) [= j } is set
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in H₅(D) & b₂ in H₅(j9) ) } is set
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,(D * j9),j) [= j } is set
f is set
{ H₆(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
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 multF 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 multF of Q . [X,x] is set
{ H₇(H₆(b₁)) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
a9 is Element of the carrier of Q
a is Element of the carrier of Q
(X * x) * a is Element of the carrier of Q
the multF of Q . ((X * x),a) is Element of the carrier of Q
[(X * x),a] is set
{(X * x),a} is non empty finite set
{(X * x)} is non empty finite set
{{(X * x),a},{(X * x)}} is non empty finite V45() set
the multF of Q . [(X * x),a] is set
a * (D * j9) is Element of the carrier of Q
the multF of Q . (a,(D * j9)) is Element of the carrier of Q
[a,(D * j9)] is set
{a,(D * j9)} is non empty finite set
{a} is non empty finite set
{{a,(D * j9)},{a}} is non empty finite V45() set
the multF of Q . [a,(D * j9)] is set
(Q,x,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : x * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : x * b₁ [= j } ,Q) is Element of the carrier of Q
a9 is Element of the carrier of Q
a9 * (Q,j9,j) is Element of the carrier of Q
the multF of Q . (a9,(Q,j9,j)) is Element of the carrier of Q
[a9,(Q,j9,j)] is set
{a9,(Q,j9,j)} is non empty finite set
{a9} is non empty finite set
{{a9,(Q,j9,j)},{a9}} is non empty finite V45() set
the multF of Q . [a9,(Q,j9,j)] is set
a * D is Element of the carrier of Q
the multF of Q . (a,D) is Element of the carrier of Q
[a,D] is set
{a,D} is non empty finite set
{{a,D},{a}} is non empty finite V45() set
the multF of Q . [a,D] is set
(a * D) * j9 is Element of the carrier of Q
the multF of Q . ((a * D),j9) is Element of the carrier of Q
[(a * D),j9] is set
{(a * D),j9} is non empty finite set
{(a * D)} is non empty finite set
{{(a * D),j9},{(a * D)}} is non empty finite V45() set
the multF of Q . [(a * D),j9] is set
x * (a * D) is Element of the carrier of Q
the multF of Q . (x,(a * D)) is Element of the carrier of Q
[x,(a * D)] is set
{x,(a * D)} is non empty finite set
{x} is non empty finite set
{{x,(a * D)},{x}} is non empty finite V45() set
the multF of Q . [x,(a * D)] is set
x * a is Element of the carrier of Q
the multF of Q . (x,a) is Element of the carrier of Q
[x,a] is set
{x,a} is non empty finite set
{{x,a},{x}} is non empty finite V45() set
the multF of Q . [x,a] is set
(x * a) * D is Element of the carrier of Q
the multF of Q . ((x * a),D) is Element of the carrier of Q
[(x * a),D] is set
{(x * a),D} is non empty finite set
{(x * a)} is non empty finite set
{{(x * a),D},{(x * a)}} is non empty finite V45() set
the multF of Q . [(x * a),D] is set
(Q,X,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : X * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : X * b₁ [= j } ,Q) is Element of the carrier of Q
a9 is Element of the carrier of Q
a9 * (Q,D,j) is Element of the carrier of Q
the multF of Q . (a9,(Q,D,j)) is Element of the carrier of Q
[a9,(Q,D,j)] is set
{a9,(Q,D,j)} is non empty finite set
{a9} is non empty finite set
{{a9,(Q,D,j)},{a9}} is non empty finite V45() set
the multF of Q . [a9,(Q,D,j)] is set
X * (x * a) is Element of the carrier of Q
the multF of Q . (X,(x * a)) is Element of the carrier of Q
[X,(x * a)] is set
{X,(x * a)} is non empty finite set
{{X,(x * a)},{X}} is non empty finite V45() set
the multF of Q . [X,(x * a)] is set
{ H₇(b₁) where b₁ is Element of the carrier of Q : b₁ in { H₆(b₁) where b₂ is Element of the carrier of Q : S₁[b₁] } } is set
(X * x) * (Q,(D * j9),j) is Element of the carrier of Q
the multF of Q . ((X * x),(Q,(D * j9),j)) is Element of the carrier of Q
[(X * x),(Q,(D * j9),j)] is set
{(X * x),(Q,(D * j9),j)} is non empty finite set
{(X * x)} is non empty finite set
{{(X * x),(Q,(D * j9),j)},{(X * x)}} is non empty finite V45() set
the multF of Q . [(X * x),(Q,(D * j9),j)] is set
"\/" ( { H₇(H₆(b₁)) where b₁ is Element of the carrier of Q : S₁[b₁] } ,Q) is Element of the carrier of Q
"\/" ( { (b₁ * b₂) where b₁, b₂ is Element of the carrier of Q : ( b₁ in H₅(D) & b₂ in H₅(j9) ) } ,Q) is Element of the carrier of Q
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
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_unity_wrt the multF of Q is Element of the carrier of Q
j is Element of the carrier of Q
(Q,j,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= j } ,Q) is Element of the carrier of Q
(Q,j,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : j * b₁ [= j } ,Q) is Element of the carrier of Q
f is Element of the carrier of Q
f * (Q,j,j) is Element of the carrier of Q
the multF of Q . (f,(Q,j,j)) is Element of the carrier of Q
[f,(Q,j,j)] is set
{f,(Q,j,j)} is non empty finite set
{f} is non empty finite set
{{f,(Q,j,j)},{f}} is non empty finite V45() set
the multF of Q . [f,(Q,j,j)] is set
(Q,j,j) * f is Element of the carrier of Q
the multF of Q . ((Q,j,j),f) is Element of the carrier of Q
[(Q,j,j),f] is set
{(Q,j,j),f} is non empty finite set
{(Q,j,j)} is non empty finite set
{{(Q,j,j),f},{(Q,j,j)}} is non empty finite V45() set
the multF of Q . [(Q,j,j),f] is set
L is Element of the carrier of Q
L * (f * (Q,j,j)) is Element of the carrier of Q
the multF of Q . (L,(f * (Q,j,j))) is Element of the carrier of Q
[L,(f * (Q,j,j))] is set
{L,(f * (Q,j,j))} is non empty finite set
{L} is non empty finite set
{{L,(f * (Q,j,j))},{L}} is non empty finite V45() set
the multF of Q . [L,(f * (Q,j,j))] is set
L * f is Element of the carrier of Q
the multF of Q . (L,f) is Element of the carrier of Q
[L,f] is set
{L,f} is non empty finite set
{{L,f},{L}} is non empty finite V45() set
the multF of Q . [L,f] is set
(L * f) * (Q,j,j) is Element of the carrier of Q
the multF of Q . ((L * f),(Q,j,j)) is Element of the carrier of Q
[(L * f),(Q,j,j)] is set
{(L * f),(Q,j,j)} is non empty finite set
{(L * f)} is non empty finite set
{{(L * f),(Q,j,j)},{(L * f)}} is non empty finite V45() set
the multF of Q . [(L * f),(Q,j,j)] is set
(Q,(Q,j,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j,j) [= j } ,Q) is Element of the carrier of Q
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₂[b₁] } is set
(Q,(f * (Q,j,j)),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (f * (Q,j,j)) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (f * (Q,j,j)) [= j } ,Q) is Element of the carrier of Q
(Q,(Q,(f * (Q,j,j)),j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,(f * (Q,j,j)),j) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,(f * (Q,j,j)),j) * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,f,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * f [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * f [= j } ,Q) is Element of the carrier of Q
(Q,(Q,f,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,f,j) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,f,j) * b₁ [= j } ,Q) is Element of the carrier of Q
L is Element of the carrier of Q
((Q,j,j) * f) * L is Element of the carrier of Q
the multF of Q . (((Q,j,j) * f),L) is Element of the carrier of Q
[((Q,j,j) * f),L] is set
{((Q,j,j) * f),L} is non empty finite set
{((Q,j,j) * f)} is non empty finite set
{{((Q,j,j) * f),L},{((Q,j,j) * f)}} is non empty finite V45() set
the multF of Q . [((Q,j,j) * f),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,L},{f}} is non empty finite V45() set
the multF of Q . [f,L] is set
(Q,j,j) * (f * L) is Element of the carrier of Q
the multF of Q . ((Q,j,j),(f * L)) is Element of the carrier of Q
[(Q,j,j),(f * L)] is set
{(Q,j,j),(f * L)} is non empty finite set
{{(Q,j,j),(f * L)},{(Q,j,j)}} is non empty finite V45() set
the multF of Q . [(Q,j,j),(f * L)] is set
(Q,(Q,j,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,j,j) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,j,j) * b₁ [= j } ,Q) is Element of the carrier of Q
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₃[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₄[b₁] } is set
(Q,((Q,j,j) * f),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : ((Q,j,j) * f) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : ((Q,j,j) * f) * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,(Q,((Q,j,j) * f),j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,((Q,j,j) * f),j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,((Q,j,j) * f),j) [= j } ,Q) is Element of the carrier of Q
(Q,f,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : f * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : f * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,(Q,f,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,f,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,f,j) [= j } ,Q) is Element of the carrier of Q
f is Element of the carrier of Q
H₄(Q) . (f,(Q,j,j)) is Element of the carrier of Q
[f,(Q,j,j)] is set
{f,(Q,j,j)} is non empty finite set
{f} is non empty finite set
{{f,(Q,j,j)},{f}} is non empty finite V45() set
the multF of Q . [f,(Q,j,j)] is set
H₄(Q) . (f,(Q,j,j)) is Element of the carrier of Q
f * (Q,j,j) is Element of the carrier of Q
the multF of Q . (f,(Q,j,j)) is Element of the carrier of Q
(Q,j,j) * (Q,j,j) is Element of the carrier of Q
the multF of Q . ((Q,j,j),(Q,j,j)) is Element of the carrier of Q
[(Q,j,j),(Q,j,j)] is set
{(Q,j,j),(Q,j,j)} is non empty finite set
{{(Q,j,j),(Q,j,j)},{(Q,j,j)}} is non empty finite V45() set
the multF of Q . [(Q,j,j),(Q,j,j)] is set
f is Element of the carrier of Q
H₄(Q) . ((Q,j,j),f) is Element of the carrier of Q
[(Q,j,j),f] is set
{(Q,j,j),f} is non empty finite set
{(Q,j,j)} is non empty finite set
{{(Q,j,j),f},{(Q,j,j)}} is non empty finite V45() set
the multF of Q . [(Q,j,j),f] is set
H₄(Q) . ((Q,j,j),f) is Element of the carrier of Q
(Q,j,j) * f is Element of the carrier of Q
the multF of Q . ((Q,j,j),f) is Element of the carrier of Q
[(Q,j,j),f] is set
{(Q,j,j),f} is non empty finite set
{{(Q,j,j),f},{(Q,j,j)}} is non empty finite V45() set
the multF of Q . [(Q,j,j),f] 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
(Q,D,j9) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j9 } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= j9 } ,Q) is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j9 * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : j9 * b₁ [= j } ,Q) is Element of the carrier of Q
D * (Q,j9,j) 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 . (D,(Q,j9,j)) is Element of the carrier of Q
[D,(Q,j9,j)] is set
{D,(Q,j9,j)} is non empty finite set
{D} is non empty finite set
{{D,(Q,j9,j)},{D}} is non empty finite V45() set
the multF of Q . [D,(Q,j9,j)] is set
(Q,(D * (Q,j9,j)),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (D * (Q,j9,j)) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (D * (Q,j9,j)) [= j } ,Q) is Element of the carrier of Q
(Q,D,j9) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j9 } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : D * b₁ [= j9 } ,Q) is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= j } ,Q) is Element of the carrier of Q
(Q,j9,j) * D is Element of the carrier of Q
the multF of Q . ((Q,j9,j),D) is Element of the carrier of Q
[(Q,j9,j),D] is set
{(Q,j9,j),D} is non empty finite set
{(Q,j9,j)} is non empty finite set
{{(Q,j9,j),D},{(Q,j9,j)}} is non empty finite V45() set
the multF of Q . [(Q,j9,j),D] is set
(Q,((Q,j9,j) * D),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : ((Q,j9,j) * D) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : ((Q,j9,j) * D) * b₁ [= j } ,Q) is Element of the carrier of Q
(Q,(Q,j9,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j9,j) [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j9,j) [= j } ,Q) is Element of the carrier of Q
f is Element of the carrier of Q
f * D is Element of the carrier of Q
the multF of Q . (f,D) is Element of the carrier of Q
[f,D] is set
{f,D} is non empty finite set
{f} is non empty finite set
{{f,D},{f}} is non empty finite V45() set
the multF of Q . [f,D] is set
f * (D * (Q,j9,j)) is Element of the carrier of Q
the multF of Q . (f,(D * (Q,j9,j))) is Element of the carrier of Q
[f,(D * (Q,j9,j))] is set
{f,(D * (Q,j9,j))} is non empty finite set
{{f,(D * (Q,j9,j))},{f}} is non empty finite V45() set
the multF of Q . [f,(D * (Q,j9,j))] is set
(f * D) * (Q,j9,j) is Element of the carrier of Q
the multF of Q . ((f * D),(Q,j9,j)) is Element of the carrier of Q
[(f * D),(Q,j9,j)] is set
{(f * D),(Q,j9,j)} is non empty finite set
{(f * D)} is non empty finite set
{{(f * D),(Q,j9,j)},{(f * D)}} is non empty finite V45() set
the multF of Q . [(f * D),(Q,j9,j)] is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₂[b₁] } is set
(Q,(Q,j9,j),j) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,j9,j) * b₁ [= j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,j9,j) * b₁ [= j } ,Q) is Element of the carrier of Q
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,f},{D}} is non empty finite V45() set
the multF of Q . [D,f] is set
((Q,j9,j) * D) * f is Element of the carrier of Q
the multF of Q . (((Q,j9,j) * D),f) is Element of the carrier of Q
[((Q,j9,j) * D),f] is set
{((Q,j9,j) * D),f} is non empty finite set
{((Q,j9,j) * D)} is non empty finite set
{{((Q,j9,j) * D),f},{((Q,j9,j) * D)}} is non empty finite V45() set
the multF of Q . [((Q,j9,j) * D),f] is set
(Q,j9,j) * (D * f) is Element of the carrier of Q
the multF of Q . ((Q,j9,j),(D * f)) is Element of the carrier of Q
[(Q,j9,j),(D * f)] is set
{(Q,j9,j),(D * f)} is non empty finite set
{{(Q,j9,j),(D * f)},{(Q,j9,j)}} is non empty finite V45() set
the multF of Q . [(Q,j9,j),(D * f)] is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₃[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : S₄[b₁] } 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 , 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 , the Element of the non empty set ) is set
Q is non empty ()
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
the of Q is Element of the carrier of Q
D is Element of the carrier of Q
(Q,D, the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= the of Q } ,Q) is Element of the carrier of Q
(Q,D, the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : D * b₁ [= the of Q } ,Q) is Element of the carrier of Q
D is Element of the carrier of Q
(Q,D, the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= the of Q } ,Q) is Element of the carrier of Q
(Q,(Q,D, the of Q), the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : (Q,D, the of Q) * b₁ [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : (Q,D, the of Q) * b₁ [= the of Q } ,Q) is Element of the carrier of Q
(Q,D, the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : D * b₁ [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : D * b₁ [= the of Q } ,Q) is Element of the carrier of Q
(Q,(Q,D, the of Q), the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D, the of Q) [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D, the of Q) [= the of Q } ,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
L is Element of Q
(Q,j,D,j9,f,L) 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 Element of the carrier of (BooleLatt {}) is Element of 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₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}), 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 {}):], the Element of the carrier of (BooleLatt {}), the Element of the carrier of (BooleLatt {})) is non empty () ()
Q is ()
the of Q is Element of the carrier of Q
the carrier of Q is set
Q is non empty ()
(Q) is Element of the carrier of Q
the carrier of Q is non empty set
the of Q is Element of the carrier of Q
(Q,(Q),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q) [= (Q) } ,Q) is Element of the carrier of Q
j is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty ()
the carrier of Q is non empty set
[: the carrier of Q, the carrier of Q:] is non empty V7() set
bool [: the carrier of Q, the carrier of Q:] is non empty set
j is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
D is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
j9 is Element of the carrier of Q
D . j9 is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
j is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
D is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
j9 is Element of the carrier of Q
j . j9 is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
D . j9 is Element of the carrier of Q
Q is non empty ()
the carrier of Q is non empty set
[: the carrier of Q, the carrier of Q:] is non empty V7() set
bool [: the carrier of Q, the carrier of Q:] is non empty set
j is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
(Q) is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
(Q) * j is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
Q is non empty ()
the carrier of Q is non empty set
[: 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
j 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:]
(Q) is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
bool [: the carrier of Q, the carrier of Q:] is non empty set
(Q) * j 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:]
Q is non empty unital 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
(Q,j) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
(Q,(Q,j)) is Element of the carrier of Q
(Q,(Q,j),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j, the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : j * b₁ [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : j * b₁ [= the of Q } ,Q) is Element of the carrier of Q
(Q,j, the of Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= the of Q } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= the of Q } ,Q) is Element of the carrier of Q
Q is non empty unital 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
(Q,D) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,D,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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 set
"\/" (j,Q) is Element of the carrier of Q
(Q,("\/" (j,Q))) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,("\/" (j,Q)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" (j,Q)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" (j,Q)) [= (Q) } ,Q) is Element of the carrier of Q
{ (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } is set
"/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } } ,Q) is Element of the carrier of Q
{ (("/\" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } ,Q)) * b₁) where b₁ is Element of the carrier of Q : b₁ in j } is set
D is Element of the carrier of Q
j9 is Element of the carrier of Q
("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)) * 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 . (("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),j9) is Element of the carrier of Q
[("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),j9] is set
{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),j9} is non empty finite set
{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))} is non empty finite set
{{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),j9},{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))}} is non empty finite V45() set
the multF of Q . [("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),j9] is set
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
"\/" ( { (("/\" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } ,Q)) * b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q) is Element of the carrier of Q
("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)) * ("\/" (j,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 . (("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),("\/" (j,Q))) is Element of the carrier of Q
[("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),("\/" (j,Q))] is set
{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),("\/" (j,Q))} is non empty finite set
{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))} is non empty finite set
{{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),("\/" (j,Q))},{("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))}} is non empty finite V45() set
the multF of Q . [("/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),("\/" (j,Q))] is set
D is Element of the carrier of Q
j9 is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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 set
"/\" (j,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than j } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than j } ,Q) is Element of the carrier of Q
(Q,("/\" (j,Q))) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,("/\" (j,Q)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ("/\" (j,Q)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ("/\" (j,Q)) [= (Q) } ,Q) is Element of the carrier of Q
{ (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } is set
"\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q) is Element of the carrier of Q
{ (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } } is set
"/\" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in { (Q,b₁) where b₃ is Element of the carrier of Q : b₁ in j } } } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in { (Q,b₁) where b₃ is Element of the carrier of Q : b₁ in j } } } ,Q) is Element of the carrier of Q
D is Element of the carrier of Q
(Q,D) is Element of the carrier of Q
(Q,D,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } ,Q) is Element of the carrier of Q
(Q,(Q,D)) is Element of the carrier of Q
(Q,(Q,D),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D) [= (Q) } ,Q) is Element of the carrier of Q
D is set
j9 is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
f is Element of the carrier of Q
(Q,f) is Element of the carrier of Q
(Q,f,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * f [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * f [= (Q) } ,Q) is Element of the carrier of Q
(Q,("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))) is Element of the carrier of Q
(Q,("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } ,Q)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in j } ,Q)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,(Q,("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q)))) is Element of the carrier of Q
(Q,(Q,("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in j } ,Q))) [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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
(Q,j) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) 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
(Q,(j "\/" D)) is Element of the carrier of Q
(Q,(j "\/" D),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (j "\/" D) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (j "\/" D) [= (Q) } ,Q) is Element of the carrier of Q
(Q,D) is Element of the carrier of Q
(Q,D,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) "/\" (Q,D) is Element of the carrier of Q
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:]
the L_meet of Q . ((Q,j),(Q,D)) is Element of the carrier of Q
[(Q,j),(Q,D)] is set
{(Q,j),(Q,D)} is non empty finite set
{(Q,j)} is non empty finite set
{{(Q,j),(Q,D)},{(Q,j)}} is non empty finite V45() set
the L_meet of Q . [(Q,j),(Q,D)] is set
j "/\" D is Element of the carrier of Q
the L_meet of Q . (j,D) is Element of the carrier of Q
the L_meet of Q . [j,D] is set
(Q,(j "/\" D)) is Element of the carrier of Q
(Q,(j "/\" D),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (j "/\" D) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (j "/\" D) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) "\/" (Q,D) is Element of the carrier of Q
the L_join of Q . ((Q,j),(Q,D)) is Element of the carrier of Q
the L_join of Q . [(Q,j),(Q,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
{ (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in {j,D} } is set
{(Q,j),(Q,D)} is non empty finite Element of bool the carrier of Q
j9 is set
f is Element of the carrier of Q
(Q,f) is Element of the carrier of Q
(Q,f,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * f [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * f [= (Q) } ,Q) is Element of the carrier of Q
j9 is set
"\/" ({j,D},Q) is Element of the carrier of Q
"/\" ({(Q,j),(Q,D)},Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than {(Q,j),(Q,D)} } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than {(Q,j),(Q,D)} } ,Q) is Element of the carrier of Q
"\/" ({(Q,j),(Q,D)},Q) is Element of the carrier of Q
"/\" ({j,D},Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than {j,D} } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than {j,D} } ,Q) is Element of the carrier of Q
Q is non empty unital 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
(Q,j) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
D is Element of the carrier of Q
(Q,D) is Element of the carrier of Q
(Q,D,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,D) 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 . ((Q,j),(Q,D)) is Element of the carrier of Q
[(Q,j),(Q,D)] is set
{(Q,j),(Q,D)} is non empty finite set
{(Q,j)} is non empty finite set
{{(Q,j),(Q,D)},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,D)] is set
(Q,((Q,j) * (Q,D))) is Element of the carrier of Q
(Q,((Q,j) * (Q,D)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,D)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,D)) [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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 set
"\/" (D,Q) is Element of the carrier of Q
j * ("\/" (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,("\/" (D,Q))) is Element of the carrier of Q
[j,("\/" (D,Q))] is set
{j,("\/" (D,Q))} is non empty finite set
{j} is non empty finite set
{{j,("\/" (D,Q))},{j}} is non empty finite V45() set
the multF of Q . [j,("\/" (D,Q))] is set
{ (j * b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (j * b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
"/\" (D,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than D } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than D } ,Q) is Element of the carrier of Q
(Q,j,("/\" (D,Q))) is Element of the carrier of Q
(Q,j) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
(Q,("/\" (D,Q))) is Element of the carrier of Q
(Q,("/\" (D,Q)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ("/\" (D,Q)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ("/\" (D,Q)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,("/\" (D,Q))) is Element of the carrier of Q
the multF of Q . ((Q,j),(Q,("/\" (D,Q)))) is Element of the carrier of Q
[(Q,j),(Q,("/\" (D,Q)))] is set
{(Q,j),(Q,("/\" (D,Q)))} is non empty finite set
{(Q,j)} is non empty finite set
{{(Q,j),(Q,("/\" (D,Q)))},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,("/\" (D,Q)))] is set
(Q,((Q,j) * (Q,("/\" (D,Q))))) is Element of the carrier of Q
(Q,((Q,j) * (Q,("/\" (D,Q)))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,("/\" (D,Q)))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,("/\" (D,Q)))) [= (Q) } ,Q) is Element of the carrier of Q
{ (Q,j,b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"/\" ( { (Q,j,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,j,b₁) where b₂ is Element of the carrier of Q : b₁ in D } } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,j,b₁) where b₂ is Element of the carrier of Q : b₁ in D } } ,Q) is Element of the carrier of Q
{ H₆(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : b₁ in { H₆(b₁) where b₂ is Element of the carrier of Q : S₁[b₁] } } is set
{ H₅(H₆(b₁)) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₇(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₆(b₁) where b₁ is Element of the carrier of Q : b₁ in { H₇(b₁) where b₂ is Element of the carrier of Q : S₁[b₁] } } is set
{ H₆(H₇(b₁)) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
j9 is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,j9) is Element of the carrier of Q
the multF of Q . ((Q,j),(Q,j9)) is Element of the carrier of Q
[(Q,j),(Q,j9)] is set
{(Q,j),(Q,j9)} is non empty finite set
{{(Q,j),(Q,j9)},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,j9)] is set
(Q,((Q,j) * (Q,j9))) is Element of the carrier of Q
(Q,((Q,j) * (Q,j9)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,j9)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,j9)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j,j9) is Element of the carrier of Q
{ H₈(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₉(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
(Q,j) * ("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)) is Element of the carrier of Q
the multF of Q . ((Q,j),("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))) is Element of the carrier of Q
[(Q,j),("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))] is set
{(Q,j),("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))} is non empty finite set
{{(Q,j),("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))] is set
(Q,((Q,j) * ("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)))) is Element of the carrier of Q
(Q,((Q,j) * ("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * ("\/" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in D } ,Q))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * ("\/" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in D } ,Q))) [= (Q) } ,Q) is Element of the carrier of Q
{ ((Q,j) * (Q,b₁)) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { ((Q,j) * (Q,b₁)) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
(Q,("\/" ( { ((Q,j) * (Q,b₁)) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))) is Element of the carrier of Q
(Q,("\/" ( { ((Q,j) * (Q,b₁)) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" ( { ((Q,j) * (Q,b₁)) where b₂ is Element of the carrier of Q : b₁ in D } ,Q)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" ( { ((Q,j) * (Q,b₁)) where b₂ is Element of the carrier of Q : b₁ in D } ,Q)) [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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 set
"\/" (D,Q) is Element of the carrier of Q
("\/" (D,Q)) * j 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 . (("\/" (D,Q)),j) is Element of the carrier of Q
[("\/" (D,Q)),j] is set
{("\/" (D,Q)),j} is non empty finite set
{("\/" (D,Q))} is non empty finite set
{{("\/" (D,Q)),j},{("\/" (D,Q))}} is non empty finite V45() set
the multF of Q . [("\/" (D,Q)),j] is set
{ (b₁ * j) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (b₁ * j) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
"/\" (D,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than D } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than D } ,Q) is Element of the carrier of Q
(Q,("/\" (D,Q)),j) is Element of the carrier of Q
(Q,("/\" (D,Q))) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,("/\" (D,Q)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ("/\" (D,Q)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ("/\" (D,Q)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
(Q,("/\" (D,Q))) * (Q,j) is Element of the carrier of Q
the multF of Q . ((Q,("/\" (D,Q))),(Q,j)) is Element of the carrier of Q
[(Q,("/\" (D,Q))),(Q,j)] is set
{(Q,("/\" (D,Q))),(Q,j)} is non empty finite set
{(Q,("/\" (D,Q)))} is non empty finite set
{{(Q,("/\" (D,Q))),(Q,j)},{(Q,("/\" (D,Q)))}} is non empty finite V45() set
the multF of Q . [(Q,("/\" (D,Q))),(Q,j)] is set
(Q,((Q,("/\" (D,Q))) * (Q,j))) is Element of the carrier of Q
(Q,((Q,("/\" (D,Q))) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,("/\" (D,Q))) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,("/\" (D,Q))) * (Q,j)) [= (Q) } ,Q) is Element of the carrier of Q
{ (Q,b₁,j) where b₁ is Element of the carrier of Q : b₁ in D } is set
"/\" ( { (Q,b₁,j) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,b₁,j) where b₂ is Element of the carrier of Q : b₁ in D } } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ is_less_than { (Q,b₁,j) where b₂ is Element of the carrier of Q : b₁ in D } } ,Q) is Element of the carrier of Q
{ H₆(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Q : b₁ in { H₆(b₁) where b₂ is Element of the carrier of Q : S₁[b₁] } } is set
{ H₅(H₆(b₁)) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₇(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₆(b₁) where b₁ is Element of the carrier of Q : b₁ in { H₇(b₁) where b₂ is Element of the carrier of Q : S₁[b₁] } } is set
{ H₆(H₇(b₁)) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
j9 is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
(Q,j9) * (Q,j) is Element of the carrier of Q
the multF of Q . ((Q,j9),(Q,j)) is Element of the carrier of Q
[(Q,j9),(Q,j)] is set
{(Q,j9),(Q,j)} is non empty finite set
{(Q,j9)} is non empty finite set
{{(Q,j9),(Q,j)},{(Q,j9)}} is non empty finite V45() set
the multF of Q . [(Q,j9),(Q,j)] is set
(Q,((Q,j9) * (Q,j))) is Element of the carrier of Q
(Q,((Q,j9) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j9) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j9) * (Q,j)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
{ H₈(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ H₉(b₁) where b₁ is Element of the carrier of Q : S₁[b₁] } is set
{ (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)) * (Q,j) is Element of the carrier of Q
the multF of Q . (("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)),(Q,j)) is Element of the carrier of Q
[("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)),(Q,j)] is set
{("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)),(Q,j)} is non empty finite set
{("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))} is non empty finite set
{{("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)),(Q,j)},{("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))}} is non empty finite V45() set
the multF of Q . [("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)),(Q,j)] is set
(Q,(("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)) * (Q,j))) is Element of the carrier of Q
(Q,(("\/" ( { (Q,b₁) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (("\/" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in D } ,Q)) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (("\/" ( { (Q,b₁) where b₂ is Element of the carrier of Q : b₁ in D } ,Q)) * (Q,j)) [= (Q) } ,Q) is Element of the carrier of Q
{ ((Q,b₁) * (Q,j)) where b₁ is Element of the carrier of Q : b₁ in D } is set
"\/" ( { ((Q,b₁) * (Q,j)) where b₁ is Element of the carrier of Q : b₁ in D } ,Q) is Element of the carrier of Q
(Q,("\/" ( { ((Q,b₁) * (Q,j)) where b₁ is Element of the carrier of Q : b₁ in D } ,Q))) is Element of the carrier of Q
(Q,("\/" ( { ((Q,b₁) * (Q,j)) where b₁ is Element of the carrier of Q : b₁ in D } ,Q)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" ( { ((Q,b₁) * (Q,j)) where b₂ is Element of the carrier of Q : b₁ in D } ,Q)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ("\/" ( { ((Q,b₁) * (Q,j)) where b₂ is Element of the carrier of Q : b₁ in D } ,Q)) [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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
(Q,j,D) is Element of the carrier of Q
(Q,j) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
(Q,D) is Element of the carrier of Q
(Q,D,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,D) 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 . ((Q,j),(Q,D)) is Element of the carrier of Q
[(Q,j),(Q,D)] is set
{(Q,j),(Q,D)} is non empty finite set
{(Q,j)} is non empty finite set
{{(Q,j),(Q,D)},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,D)] is set
(Q,((Q,j) * (Q,D))) is Element of the carrier of Q
(Q,((Q,j) * (Q,D)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,D)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,D)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,D,j) is Element of the carrier of Q
(Q,D) * (Q,j) is Element of the carrier of Q
the multF of Q . ((Q,D),(Q,j)) is Element of the carrier of Q
[(Q,D),(Q,j)] is set
{(Q,D),(Q,j)} is non empty finite set
{(Q,D)} is non empty finite set
{{(Q,D),(Q,j)},{(Q,D)}} is non empty finite V45() set
the multF of Q . [(Q,D),(Q,j)] is set
(Q,((Q,D) * (Q,j))) is Element of the carrier of Q
(Q,((Q,D) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,D) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,D) * (Q,j)) [= (Q) } ,Q) 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_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:]
the L_meet 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_meet of Q . [D,j9] is set
(Q,j,(D "/\" j9)) is Element of the carrier of Q
(Q,(D "/\" j9)) is Element of the carrier of Q
(Q,(D "/\" j9),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (D "/\" j9) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (D "/\" j9) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,(D "/\" j9)) is Element of the carrier of Q
the multF of Q . ((Q,j),(Q,(D "/\" j9))) is Element of the carrier of Q
[(Q,j),(Q,(D "/\" j9))] is set
{(Q,j),(Q,(D "/\" j9))} is non empty finite set
{{(Q,j),(Q,(D "/\" j9))},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,(D "/\" j9))] is set
(Q,((Q,j) * (Q,(D "/\" j9)))) is Element of the carrier of Q
(Q,((Q,j) * (Q,(D "/\" j9))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,(D "/\" j9))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,(D "/\" j9))) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j,j9) is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,j9) is Element of the carrier of Q
the multF of Q . ((Q,j),(Q,j9)) is Element of the carrier of Q
[(Q,j),(Q,j9)] is set
{(Q,j),(Q,j9)} is non empty finite set
{{(Q,j),(Q,j9)},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,j9)] is set
(Q,((Q,j) * (Q,j9))) is Element of the carrier of Q
(Q,((Q,j) * (Q,j9)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,j9)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,j9)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j,D) "/\" (Q,j,j9) is Element of the carrier of Q
the L_meet of Q . ((Q,j,D),(Q,j,j9)) is Element of the carrier of Q
[(Q,j,D),(Q,j,j9)] is set
{(Q,j,D),(Q,j,j9)} is non empty finite set
{(Q,j,D)} is non empty finite set
{{(Q,j,D),(Q,j,j9)},{(Q,j,D)}} is non empty finite V45() set
the L_meet of Q . [(Q,j,D),(Q,j,j9)] is set
(Q,(D "/\" j9),j) is Element of the carrier of Q
(Q,(D "/\" j9)) * (Q,j) is Element of the carrier of Q
the multF of Q . ((Q,(D "/\" j9)),(Q,j)) is Element of the carrier of Q
[(Q,(D "/\" j9)),(Q,j)] is set
{(Q,(D "/\" j9)),(Q,j)} is non empty finite set
{(Q,(D "/\" j9))} is non empty finite set
{{(Q,(D "/\" j9)),(Q,j)},{(Q,(D "/\" j9))}} is non empty finite V45() set
the multF of Q . [(Q,(D "/\" j9)),(Q,j)] is set
(Q,((Q,(D "/\" j9)) * (Q,j))) is Element of the carrier of Q
(Q,((Q,(D "/\" j9)) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,(D "/\" j9)) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,(D "/\" j9)) * (Q,j)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j9,j) is Element of the carrier of Q
(Q,j9) * (Q,j) is Element of the carrier of Q
the multF of Q . ((Q,j9),(Q,j)) is Element of the carrier of Q
[(Q,j9),(Q,j)] is set
{(Q,j9),(Q,j)} is non empty finite set
{(Q,j9)} is non empty finite set
{{(Q,j9),(Q,j)},{(Q,j9)}} is non empty finite V45() set
the multF of Q . [(Q,j9),(Q,j)] is set
(Q,((Q,j9) * (Q,j))) is Element of the carrier of Q
(Q,((Q,j9) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j9) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j9) * (Q,j)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,D,j) "/\" (Q,j9,j) is Element of the carrier of Q
the L_meet of Q . ((Q,D,j),(Q,j9,j)) is Element of the carrier of Q
[(Q,D,j),(Q,j9,j)] is set
{(Q,D,j),(Q,j9,j)} is non empty finite set
{(Q,D,j)} is non empty finite set
{{(Q,D,j),(Q,j9,j)},{(Q,D,j)}} is non empty finite V45() set
the L_meet of Q . [(Q,D,j),(Q,j9,j)] is set
(Q,D) "\/" (Q,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 . ((Q,D),(Q,j9)) is Element of the carrier of Q
[(Q,D),(Q,j9)] is set
{(Q,D),(Q,j9)} is non empty finite set
{{(Q,D),(Q,j9)},{(Q,D)}} is non empty finite V45() set
the L_join of Q . [(Q,D),(Q,j9)] is set
(Q,j) * ((Q,D) "\/" (Q,j9)) is Element of the carrier of Q
the multF of Q . ((Q,j),((Q,D) "\/" (Q,j9))) is Element of the carrier of Q
[(Q,j),((Q,D) "\/" (Q,j9))] is set
{(Q,j),((Q,D) "\/" (Q,j9))} is non empty finite set
{{(Q,j),((Q,D) "\/" (Q,j9))},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),((Q,D) "\/" (Q,j9))] is set
(Q,((Q,j) * ((Q,D) "\/" (Q,j9)))) is Element of the carrier of Q
(Q,((Q,j) * ((Q,D) "\/" (Q,j9))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * ((Q,D) "\/" (Q,j9))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * ((Q,D) "\/" (Q,j9))) [= (Q) } ,Q) is Element of the carrier of Q
((Q,j) * (Q,D)) "\/" ((Q,j) * (Q,j9)) is Element of the carrier of Q
the L_join of Q . (((Q,j) * (Q,D)),((Q,j) * (Q,j9))) is Element of the carrier of Q
[((Q,j) * (Q,D)),((Q,j) * (Q,j9))] is set
{((Q,j) * (Q,D)),((Q,j) * (Q,j9))} is non empty finite set
{((Q,j) * (Q,D))} is non empty finite set
{{((Q,j) * (Q,D)),((Q,j) * (Q,j9))},{((Q,j) * (Q,D))}} is non empty finite V45() set
the L_join of Q . [((Q,j) * (Q,D)),((Q,j) * (Q,j9))] is set
(Q,(((Q,j) * (Q,D)) "\/" ((Q,j) * (Q,j9)))) is Element of the carrier of Q
(Q,(((Q,j) * (Q,D)) "\/" ((Q,j) * (Q,j9))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,j) * (Q,D)) "\/" ((Q,j) * (Q,j9))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,j) * (Q,D)) "\/" ((Q,j) * (Q,j9))) [= (Q) } ,Q) is Element of the carrier of Q
((Q,D) "\/" (Q,j9)) * (Q,j) is Element of the carrier of Q
the multF of Q . (((Q,D) "\/" (Q,j9)),(Q,j)) is Element of the carrier of Q
[((Q,D) "\/" (Q,j9)),(Q,j)] is set
{((Q,D) "\/" (Q,j9)),(Q,j)} is non empty finite set
{((Q,D) "\/" (Q,j9))} is non empty finite set
{{((Q,D) "\/" (Q,j9)),(Q,j)},{((Q,D) "\/" (Q,j9))}} is non empty finite V45() set
the multF of Q . [((Q,D) "\/" (Q,j9)),(Q,j)] is set
(Q,(((Q,D) "\/" (Q,j9)) * (Q,j))) is Element of the carrier of Q
(Q,(((Q,D) "\/" (Q,j9)) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,D) "\/" (Q,j9)) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,D) "\/" (Q,j9)) * (Q,j)) [= (Q) } ,Q) is Element of the carrier of Q
((Q,D) * (Q,j)) "\/" ((Q,j9) * (Q,j)) is Element of the carrier of Q
the L_join of Q . (((Q,D) * (Q,j)),((Q,j9) * (Q,j))) is Element of the carrier of Q
[((Q,D) * (Q,j)),((Q,j9) * (Q,j))] is set
{((Q,D) * (Q,j)),((Q,j9) * (Q,j))} is non empty finite set
{((Q,D) * (Q,j))} is non empty finite set
{{((Q,D) * (Q,j)),((Q,j9) * (Q,j))},{((Q,D) * (Q,j))}} is non empty finite V45() set
the L_join of Q . [((Q,D) * (Q,j)),((Q,j9) * (Q,j))] is set
(Q,(((Q,D) * (Q,j)) "\/" ((Q,j9) * (Q,j)))) is Element of the carrier of Q
(Q,(((Q,D) * (Q,j)) "\/" ((Q,j9) * (Q,j))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,D) * (Q,j)) "\/" ((Q,j9) * (Q,j))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,D) * (Q,j)) "\/" ((Q,j9) * (Q,j))) [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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
(Q,j,j9) is Element of the carrier of Q
(Q,j) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,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 . ((Q,j),(Q,j9)) is Element of the carrier of Q
[(Q,j),(Q,j9)] is set
{(Q,j),(Q,j9)} is non empty finite set
{(Q,j)} is non empty finite set
{{(Q,j),(Q,j9)},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,j9)] is set
(Q,((Q,j) * (Q,j9))) is Element of the carrier of Q
(Q,((Q,j) * (Q,j9)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,j9)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,j9)) [= (Q) } ,Q) is Element of the carrier of Q
f is Element of the carrier of Q
(Q,D,f) is Element of the carrier of Q
(Q,D) is Element of the carrier of Q
(Q,D,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } ,Q) is Element of the carrier of Q
(Q,f) is Element of the carrier of Q
(Q,f,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * f [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * f [= (Q) } ,Q) is Element of the carrier of Q
(Q,D) * (Q,f) is Element of the carrier of Q
the multF of Q . ((Q,D),(Q,f)) is Element of the carrier of Q
[(Q,D),(Q,f)] is set
{(Q,D),(Q,f)} is non empty finite set
{(Q,D)} is non empty finite set
{{(Q,D),(Q,f)},{(Q,D)}} is non empty finite V45() set
the multF of Q . [(Q,D),(Q,f)] is set
(Q,((Q,D) * (Q,f))) is Element of the carrier of Q
(Q,((Q,D) * (Q,f)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,D) * (Q,f)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,D) * (Q,f)) [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital 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
(Q,j,D) is Element of the carrier of Q
(Q,j) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
(Q,D) is Element of the carrier of Q
(Q,D,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * D [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,D) 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 . ((Q,j),(Q,D)) is Element of the carrier of Q
[(Q,j),(Q,D)] is set
{(Q,j),(Q,D)} is non empty finite set
{(Q,j)} is non empty finite set
{{(Q,j),(Q,D)},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,D)] is set
(Q,((Q,j) * (Q,D))) is Element of the carrier of Q
(Q,((Q,j) * (Q,D)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,D)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,D)) [= (Q) } ,Q) is Element of the carrier of Q
j9 is Element of the carrier of Q
(Q,(Q,j,D),j9) is Element of the carrier of Q
(Q,(Q,j,D)) is Element of the carrier of Q
(Q,(Q,j,D),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j,D) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,j,D) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j9) is Element of the carrier of Q
(Q,j9,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j9 [= (Q) } ,Q) is Element of the carrier of Q
(Q,(Q,j,D)) * (Q,j9) is Element of the carrier of Q
the multF of Q . ((Q,(Q,j,D)),(Q,j9)) is Element of the carrier of Q
[(Q,(Q,j,D)),(Q,j9)] is set
{(Q,(Q,j,D)),(Q,j9)} is non empty finite set
{(Q,(Q,j,D))} is non empty finite set
{{(Q,(Q,j,D)),(Q,j9)},{(Q,(Q,j,D))}} is non empty finite V45() set
the multF of Q . [(Q,(Q,j,D)),(Q,j9)] is set
(Q,((Q,(Q,j,D)) * (Q,j9))) is Element of the carrier of Q
(Q,((Q,(Q,j,D)) * (Q,j9)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,(Q,j,D)) * (Q,j9)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,(Q,j,D)) * (Q,j9)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,D,j9) is Element of the carrier of Q
(Q,D) * (Q,j9) is Element of the carrier of Q
the multF of Q . ((Q,D),(Q,j9)) is Element of the carrier of Q
[(Q,D),(Q,j9)] is set
{(Q,D),(Q,j9)} is non empty finite set
{(Q,D)} is non empty finite set
{{(Q,D),(Q,j9)},{(Q,D)}} is non empty finite V45() set
the multF of Q . [(Q,D),(Q,j9)] is set
(Q,((Q,D) * (Q,j9))) is Element of the carrier of Q
(Q,((Q,D) * (Q,j9)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,D) * (Q,j9)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,D) * (Q,j9)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j,(Q,D,j9)) is Element of the carrier of Q
(Q,(Q,D,j9)) is Element of the carrier of Q
(Q,(Q,D,j9),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j9) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q,D,j9) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,(Q,D,j9)) is Element of the carrier of Q
the multF of Q . ((Q,j),(Q,(Q,D,j9))) is Element of the carrier of Q
[(Q,j),(Q,(Q,D,j9))] is set
{(Q,j),(Q,(Q,D,j9))} is non empty finite set
{{(Q,j),(Q,(Q,D,j9))},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,(Q,D,j9))] is set
(Q,((Q,j) * (Q,(Q,D,j9)))) is Element of the carrier of Q
(Q,((Q,j) * (Q,(Q,D,j9))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,(Q,D,j9))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,(Q,D,j9))) [= (Q) } ,Q) is Element of the carrier of Q
((Q,j) * (Q,D)) * (Q,j9) is Element of the carrier of Q
the multF of Q . (((Q,j) * (Q,D)),(Q,j9)) is Element of the carrier of Q
[((Q,j) * (Q,D)),(Q,j9)] is set
{((Q,j) * (Q,D)),(Q,j9)} is non empty finite set
{((Q,j) * (Q,D))} is non empty finite set
{{((Q,j) * (Q,D)),(Q,j9)},{((Q,j) * (Q,D))}} is non empty finite V45() set
the multF of Q . [((Q,j) * (Q,D)),(Q,j9)] is set
(Q,(((Q,j) * (Q,D)) * (Q,j9))) is Element of the carrier of Q
(Q,(((Q,j) * (Q,D)) * (Q,j9)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,j) * (Q,D)) * (Q,j9)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (((Q,j) * (Q,D)) * (Q,j9)) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * ((Q,D) * (Q,j9)) is Element of the carrier of Q
the multF of Q . ((Q,j),((Q,D) * (Q,j9))) is Element of the carrier of Q
[(Q,j),((Q,D) * (Q,j9))] is set
{(Q,j),((Q,D) * (Q,j9))} is non empty finite set
{{(Q,j),((Q,D) * (Q,j9))},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),((Q,D) * (Q,j9))] is set
(Q,((Q,j) * ((Q,D) * (Q,j9)))) is Element of the carrier of Q
(Q,((Q,j) * ((Q,D) * (Q,j9))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * ((Q,D) * (Q,j9))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * ((Q,D) * (Q,j9))) [= (Q) } ,Q) is Element of the carrier of Q
Q is non empty unital associative join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete () () () () () () ()
the carrier of Q is non empty set
(Q) is Element of the carrier of Q
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
(Q,(Q),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q) [= (Q) } ,Q) is Element of the carrier of Q
j is Element of the carrier of Q
j * (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)) is Element of the carrier of Q
[j,(Q)] is set
{j,(Q)} is non empty finite set
{j} is non empty finite set
{{j,(Q)},{j}} is non empty finite V45() set
the multF of Q . [j,(Q)] is set
(Q) * j is Element of the carrier of Q
the multF of Q . ((Q),j) is Element of the carrier of Q
[(Q),j] is set
{(Q),j} is non empty finite set
{(Q)} is non empty finite set
{{(Q),j},{(Q)}} is non empty finite V45() set
the multF of Q . [(Q),j] is set
the_unity_wrt H₄(Q) is Element of the carrier of Q
Q is non empty unital associative join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete () () () () () () ()
the carrier of Q is non empty set
(Q) is Element of the carrier of Q
the of Q is Element of the carrier of Q
j is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
(Q,j) is Element of the carrier of Q
(Q,j,(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * j [= (Q) } ,Q) is Element of the carrier of Q
(Q,(Q)) is Element of the carrier of Q
(Q,(Q),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * (Q) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * (Q) [= (Q) } ,Q) is Element of the carrier of Q
(Q,j) * (Q,(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 . ((Q,j),(Q,(Q))) is Element of the carrier of Q
[(Q,j),(Q,(Q))] is set
{(Q,j),(Q,(Q))} is non empty finite set
{(Q,j)} is non empty finite set
{{(Q,j),(Q,(Q))},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q,(Q))] is set
(Q,((Q,j) * (Q,(Q)))) is Element of the carrier of Q
(Q,((Q,j) * (Q,(Q))),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,(Q))) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,j) * (Q,(Q))) [= (Q) } ,Q) is Element of the carrier of Q
(Q,(Q),j) is Element of the carrier of Q
(Q,(Q)) * (Q,j) is Element of the carrier of Q
the multF of Q . ((Q,(Q)),(Q,j)) is Element of the carrier of Q
[(Q,(Q)),(Q,j)] is set
{(Q,(Q)),(Q,j)} is non empty finite set
{(Q,(Q))} is non empty finite set
{{(Q,(Q)),(Q,j)},{(Q,(Q))}} is non empty finite V45() set
the multF of Q . [(Q,(Q)),(Q,j)] is set
(Q,((Q,(Q)) * (Q,j))) is Element of the carrier of Q
(Q,((Q,(Q)) * (Q,j)),(Q)) is Element of the carrier of Q
{ b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,(Q)) * (Q,j)) [= (Q) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of Q : b₁ * ((Q,(Q)) * (Q,j)) [= (Q) } ,Q) is Element of the carrier of Q
(Q) is Element of the carrier of Q
(Q,j) * (Q) is Element of the carrier of Q
the multF of Q . ((Q,j),(Q)) is Element of the carrier of Q
[(Q,j),(Q)] is set
{(Q,j),(Q)} is non empty finite set
{{(Q,j),(Q)},{(Q,j)}} is non empty finite V45() set
the multF of Q . [(Q,j),(Q)] is set
(Q) * (Q,j) is Element of the carrier of Q
the multF of Q . ((Q),(Q,j)) is Element of the carrier of Q
[(Q),(Q,j)] is set
{(Q),(Q,j)} is non empty finite set
{(Q)} is non empty finite set
{{(Q),(Q,j)},{(Q)}} is non empty finite V45() set
the multF of Q . [(Q),(Q,j)] 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
[: the carrier of Q, the carrier of Q:] is non empty V7() set
bool [: the carrier of Q, the carrier of Q:] is non empty set
j is non empty V7() V10( the carrier of Q) V11( the carrier of Q) Function-like V17( the carrier of Q) V21( the carrier of Q, the carrier of Q) Element of bool [: the carrier of Q, the carrier of Q:]
rng j is non empty Element of bool the carrier of Q
bool the carrier of Q is non empty set
dom j is non empty Element of bool the carrier of Q
D is non empty Element of bool the carrier of Q
[:H₁(Q),D:] is non empty V7() set
bool [:H₁(Q),D:] is non empty set
bool D is non empty set
j9 is non empty V7() V10(H₁(Q)) V11(D) Function-like V17(H₁(Q)) V21(H₁(Q),D) Element of bool [:H₁(Q),D:]
bool D is non empty Element of bool (bool D)
bool (bool D) is non empty set
[:(bool D),D:] is non empty V7() set
bool [:(bool D),D:] is non empty set
f is non empty V7() V10( bool D) V11(D) Function-like V17( bool D) V21( bool D,D) Element of bool [:(bool D),D:]
dom f is non empty Element of bool (bool D)
bool (bool D) is non empty set
L is Element of bool (bool D)
f .: L is Element of bool D
f . (f .: L) is Element of D
union L is Element of bool D
f . (union L) is Element of D
{ (j . b₁) where b₁ is Element of the carrier of Q : b₁ in f .: L } is set
{ (j . b₁) where b₁ is Element of the carrier of Q : b₁ in union L } is set
a is Element of the carrier of Q
a9 is Element of the carrier of Q
j . a9 is Element of the carrier of Q
x is set
x is Element of bool D
"\/" (x,Q) is Element of the carrier of Q
j . ("\/" (x,Q)) is Element of the carrier of Q
Y is Element of the carrier of Q
f . x is Element of D
j . Y is Element of the carrier of Q
"\/" ( { (j . b₁) where b₁ is Element of the carrier of Q : b₁ in union L } ,Q) is Element of the carrier of Q
"\/" ( { (j . b₁) where b₁ is Element of the carrier of Q : b₁ in f .: L } ,Q) is Element of the carrier of Q
a is Element of the carrier of Q
a9 is Element of the carrier of Q
j . a9 is Element of the carrier of Q
x is set
f . x is set
x is Element of bool D
Y is Element of bool the carrier of Q
{ (j . b₁) where b₁ is Element of the carrier of Q : b₁ in Y } is set
z is set
b is Element of the carrier of Q
j . b is Element of the carrier of Q
"\/" (Y,Q) is Element of the carrier of Q
j . ("\/" (Y,Q)) is Element of the carrier of Q
"\/" ( { (j . b₁) where b₁ is Element of the carrier of Q : b₁ in Y } ,Q) is Element of the carrier of Q
j . ("\/" ( { (j . b₁) where b₁ is Element of the carrier of Q : b₁ in union L } ,Q)) is Element of the carrier of Q
a9 is Element of bool the carrier of Q
"\/" (a9,Q) is Element of the carrier of Q
j . ("\/" (a9,Q)) is Element of the carrier of Q
j . (j . ("\/" (a9,Q))) is Element of the carrier of Q
x9 is Element of bool the carrier of Q
"\/" (x9,Q) is Element of the carrier of Q
j . ("\/" (x9,Q)) is Element of the carrier of Q
a9 is Element of bool the carrier of Q
"\/" (a9,Q) is Element of the carrier of Q
j . ("\/" (a9,Q)) is Element of the carrier of Q
L is Element of D
{L} is non empty finite Element of bool D
f . {L} is Element of D
X is set
j . X is set
x is Element of the carrier of Q
{x} is non empty finite Element of bool the carrier of Q
x9 is Element of bool the carrier of Q
"\/" (x9,Q) is Element of the carrier of Q
j . ("\/" (x9,Q)) is Element of the carrier of Q
a9 is Element of the carrier of Q
j . a9 is Element of the carrier of Q
j . (j . a9) is Element of the carrier of Q
L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of L is non empty set
bool the carrier of L is non empty set
X is Element of bool the carrier of L
"\/" (X,L) is Element of the carrier of L
"\/" (X,Q) is Element of the carrier of Q
j . ("\/" (X,Q)) is Element of the carrier of Q
f . X is set