:: WAYBEL22 semantic presentation

K172() is V42() countable denumerable Element of bool K168()
K168() is set
bool K168() is non empty set
K120() is V42() countable denumerable set
bool K120() is non empty set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V106() Cardinal-yielding set
1 is non empty set
{{},1} is non empty set
bool K172() is non empty set
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set
X is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of X is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
L is set
union L is set
"/\" ((union L),X) is Element of the carrier of X
{ ("/\" (b₁,X)) where b₁ is Element of bool the carrier of X : b₁ in L } is set
"/\" ( { ("/\" (b₁,X)) where b₁ is Element of bool the carrier of X : b₁ in L } ,X) is Element of the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : S₁[b₁] } is set
Mg is set
f is Element of bool the carrier of X
f is Element of bool the carrier of X
{ ("/\" (b₁,X)) where b₁ is Element of bool the carrier of X : S₁[b₁] } is set
"/\" ( { ("/\" (b₁,X)) where b₁ is Element of bool the carrier of X : S₁[b₁] } ,X) is Element of the carrier of X
union { b₁ where b₁ is Element of bool the carrier of X : S₁[b₁] } is set
"/\" ((union { b₁ where b₁ is Element of bool the carrier of X : S₁[b₁] } ),X) is Element of the carrier of X
X is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of X is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
L is set
union L is set
"\/" ((union L),X) is Element of the carrier of X
{ ("\/" (b₁,X)) where b₁ is Element of bool the carrier of X : b₁ in L } is set
"\/" ( { ("\/" (b₁,X)) where b₁ is Element of bool the carrier of X : b₁ in L } ,X) is Element of the carrier of X
{ b₁ where b₁ is Element of bool the carrier of X : S₁[b₁] } is set
Mg is set
f is Element of bool the carrier of X
f is Element of bool the carrier of X
{ ("\/" (b₁,X)) where b₁ is Element of bool the carrier of X : S₁[b₁] } is set
"\/" ( { ("\/" (b₁,X)) where b₁ is Element of bool the carrier of X : S₁[b₁] } ,X) is Element of the carrier of X
union { b₁ where b₁ is Element of bool the carrier of X : S₁[b₁] } is set
"\/" ((union { b₁ where b₁ is Element of bool the carrier of X : S₁[b₁] } ),X) is Element of the carrier of X
X is non empty V67() V68() V69() upper-bounded with_infima RelStr
Filt X is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of X : verum } is set
InclPoset (Filt X) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (InclPoset (Filt X)) is non empty set
bool the carrier of (InclPoset (Filt X)) is non empty set
L is non empty directed Element of bool the carrier of (InclPoset (Filt X))
"\/" (L,(InclPoset (Filt X))) is Element of the carrier of (InclPoset (Filt X))
union L is set
X ~ is non empty strict V67() V68() V69() lower-bounded with_suprema RelStr
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
the InternalRel of X ~ is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
RelStr(# the carrier of X,( the InternalRel of X ~) #) is strict RelStr
Ids (X ~) is set
the carrier of (X ~) is non empty set
bool the carrier of (X ~) is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of (X ~) : verum } is set
X is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of X is non empty set
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of L is non empty set
G is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of G is non empty set
Mg is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V27( the carrier of X) quasi_total CLHomomorphism of X,L
f is non empty Relation-like the carrier of L -defined the carrier of G -valued Function-like V27( the carrier of L) quasi_total CLHomomorphism of L,G
f * Mg is non empty Relation-like the carrier of X -defined the carrier of G -valued Function-like V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of G:]
[: the carrier of X, the carrier of G:] is non empty Relation-like set
bool [: the carrier of X, the carrier of G:] is non empty set
X is non empty RelStr
id X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
bool the carrier of X is non empty set
L is Element of bool the carrier of X
(id X) .: L is Element of bool the carrier of X
"/\" (((id X) .: L),X) is Element of the carrier of X
"/\" (L,X) is Element of the carrier of X
(id X) . ("/\" (L,X)) is Element of the carrier of X
X is non empty RelStr
id X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
bool the carrier of X is non empty set
L is Element of bool the carrier of X
(id X) .: L is Element of bool the carrier of X
"\/" (((id X) .: L),X) is Element of the carrier of X
"\/" (L,X) is Element of the carrier of X
(id X) . ("\/" (L,X)) is Element of the carrier of X
X is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
id X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
X is non empty V67() V68() V69() upper-bounded with_infima RelStr
Filt X is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of X : verum } is set
InclPoset (Filt X) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
BoolePoset the carrier of X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset the carrier of X) is non empty set
the InternalRel of (BoolePoset the carrier of X) is Relation-like the carrier of (BoolePoset the carrier of X) -defined the carrier of (BoolePoset the carrier of X) -valued Element of bool [: the carrier of (BoolePoset the carrier of X), the carrier of (BoolePoset the carrier of X):]
[: the carrier of (BoolePoset the carrier of X), the carrier of (BoolePoset the carrier of X):] is non empty Relation-like set
bool [: the carrier of (BoolePoset the carrier of X), the carrier of (BoolePoset the carrier of X):] is non empty set
the carrier of (InclPoset (Filt X)) is non empty set
the InternalRel of (InclPoset (Filt X)) is Relation-like the carrier of (InclPoset (Filt X)) -defined the carrier of (InclPoset (Filt X)) -valued Element of bool [: the carrier of (InclPoset (Filt X)), the carrier of (InclPoset (Filt X)):]
[: the carrier of (InclPoset (Filt X)), the carrier of (InclPoset (Filt X)):] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt X)), the carrier of (InclPoset (Filt X)):] is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
InclPoset (bool the carrier of X) is non empty strict V67() V68() V69() RelStr
RelIncl (bool the carrier of X) is Relation-like bool the carrier of X -defined bool the carrier of X -valued V19() V22() V26() V27( bool the carrier of X) quasi_total Element of bool [:(bool the carrier of X),(bool the carrier of X):]
[:(bool the carrier of X),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of X),(bool the carrier of X):] is non empty set
RelStr(# (bool the carrier of X),(RelIncl (bool the carrier of X)) #) is strict RelStr
RelIncl (Filt X) is Relation-like Filt X -defined Filt X -valued V19() V22() V26() V27( Filt X) quasi_total Element of bool [:(Filt X),(Filt X):]
[:(Filt X),(Filt X):] is non empty Relation-like set
bool [:(Filt X),(Filt X):] is non empty set
RelStr(# (Filt X),(RelIncl (Filt X)) #) is strict RelStr
f is set
F is non empty filtered upper Element of bool the carrier of X
field the InternalRel of (InclPoset (Filt X)) is set
f is set
F is set
g is set
[F,g] is set
{F,g} is non empty set
{F} is non empty set
{{F,g},{F}} is non empty set
G is non empty filtered upper Element of bool the carrier of X
GF is non empty filtered upper Element of bool the carrier of X
the InternalRel of (BoolePoset the carrier of X) |_2 the carrier of (InclPoset (Filt X)) is Relation-like set
the InternalRel of (BoolePoset the carrier of X) /\ [: the carrier of (InclPoset (Filt X)), the carrier of (InclPoset (Filt X)):] is Relation-like the carrier of (BoolePoset the carrier of X) -defined the carrier of (BoolePoset the carrier of X) -valued Element of bool [: the carrier of (BoolePoset the carrier of X), the carrier of (BoolePoset the carrier of X):]
F is set
g is set
G is set
[g,G] is set
{g,G} is non empty set
{g} is non empty set
{{g,G},{g}} is non empty set
GF is non empty filtered upper Element of bool the carrier of X
FG is non empty filtered upper Element of bool the carrier of X
g is set
G is set
[g,G] is set
{g,G} is non empty set
{g} is non empty set
{{g,G},{g}} is non empty set
GF is non empty filtered upper Element of bool the carrier of X
FG is non empty filtered upper Element of bool the carrier of X
f is SubRelStr of BoolePoset the carrier of X
g is set
G is non empty filtered upper Element of bool the carrier of X
F is V67() V68() V69() full SubRelStr of BoolePoset the carrier of X
the carrier of F is set
bool the carrier of F is non empty set
g is directed Element of bool the carrier of F
"\/" (g,(BoolePoset the carrier of X)) is Element of the carrier of (BoolePoset the carrier of X)
G is set
GF is Element of bool (bool the carrier of X)
FG is Element of bool the carrier of X
Xsf is Element of bool the carrier of X
FG \/ Xsf is Element of bool the carrier of X
Xs is Element of the carrier of F
Xs is Element of the carrier of F
s is Element of the carrier of F
Y is non empty filtered upper Element of bool the carrier of X
bool the carrier of (BoolePoset the carrier of X) is non empty set
FG is Element of bool the carrier of (BoolePoset the carrier of X)
"\/" (FG,(BoolePoset the carrier of X)) is Element of the carrier of (BoolePoset the carrier of X)
union g is set
Xs is Element of bool the carrier of X
s is non empty filtered upper Element of bool the carrier of X
Xs is Element of bool the carrier of X
Xs is Element of bool the carrier of X
Xs is Element of bool the carrier of X
Top X is Element of the carrier of X
"/\" ({},X) is Element of the carrier of X
Xs is non empty filtered upper Element of bool the carrier of X
the carrier of F is set
bool the carrier of F is non empty set
g is Element of bool the carrier of F
"/\" (g,(BoolePoset the carrier of X)) is Element of the carrier of (BoolePoset the carrier of X)
[#] X is non empty non proper directed filtered lower upper Element of bool the carrier of X
Top (BoolePoset the carrier of X) is Element of the carrier of (BoolePoset the carrier of X)
"/\" ({},(BoolePoset the carrier of X)) is Element of the carrier of (BoolePoset the carrier of X)
bool the carrier of (BoolePoset the carrier of X) is non empty set
Xsf is Element of bool the carrier of (BoolePoset the carrier of X)
"/\" (Xsf,(BoolePoset the carrier of X)) is Element of the carrier of (BoolePoset the carrier of X)
meet g is set
GF is Element of bool (bool the carrier of X)
Xs is Element of bool the carrier of X
Xs is non empty filtered upper Element of bool the carrier of X
FG is Element of bool the carrier of X
Xs is Element of bool the carrier of X
Top X is Element of the carrier of X
"/\" ({},X) is Element of the carrier of X
Xs is set
Xs is non empty filtered upper Element of bool the carrier of X
X is non empty V67() V68() V69() upper-bounded with_infima RelStr
Filt X is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of X : verum } is set
InclPoset (Filt X) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
BoolePoset the carrier of X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
X is non empty V67() V68() V69() upper-bounded RelStr
Filt X is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of X : verum } is set
InclPoset (Filt X) is non empty strict V67() V68() V69() RelStr
the carrier of (InclPoset (Filt X)) is non empty set
L is Element of the carrier of (InclPoset (Filt X))
RelIncl (Filt X) is Relation-like Filt X -defined Filt X -valued V19() V22() V26() V27( Filt X) quasi_total Element of bool [:(Filt X),(Filt X):]
[:(Filt X),(Filt X):] is non empty Relation-like set
bool [:(Filt X),(Filt X):] is non empty set
RelStr(# (Filt X),(RelIncl (Filt X)) #) is strict RelStr
G is non empty filtered upper Element of bool the carrier of X
the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
G is set
the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr is non empty set
[:G, the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr :] is Relation-like set
bool [:G, the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr :] is non empty set
the Relation-like G -defined the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr -valued Function-like V27(G) quasi_total Element of bool [:G, the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr :] is Relation-like G -defined the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr -valued Function-like V27(G) quasi_total Element of bool [:G, the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr :]
f is non empty Relation-like the carrier of L -defined the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr -valued Function-like V27( the carrier of L) quasi_total CLHomomorphism of L, the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
f | G is Relation-like the carrier of L -defined G -defined the carrier of L -defined the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr -valued Function-like Element of bool [: the carrier of L, the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr :]
[: the carrier of L, the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr :] is non empty Relation-like set
bool [: the carrier of L, the carrier of the non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr :] is non empty set
dom (f | G) is Element of bool G
bool G is non empty set
dom f is non empty Element of bool the carrier of L
(dom f) /\ G is Element of bool the carrier of L
X is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of X is non empty set
id X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
L is set
id L is Relation-like L -defined L -valued Function-like one-to-one V27(L) quasi_total Element of bool [:L,L:]
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
bool the carrier of X is non empty set
(id X) | L is Relation-like the carrier of X -defined L -defined the carrier of X -defined the carrier of X -valued Function-like Element of bool [: the carrier of X, the carrier of X:]
dom (id L) is Element of bool L
bool L is non empty set
rng (id L) is Element of bool L
[:L, the carrier of X:] is Relation-like set
bool [:L, the carrier of X:] is non empty set
Mg is Relation-like L -defined the carrier of X -valued Function-like V27(L) quasi_total Element of bool [:L, the carrier of X:]
f is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total CLHomomorphism of X,X
f | L is Relation-like the carrier of X -defined L -defined the carrier of X -defined the carrier of X -valued Function-like Element of bool [: the carrier of X, the carrier of X:]
g is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total CLHomomorphism of X,X
g | L is Relation-like the carrier of X -defined L -defined the carrier of X -defined the carrier of X -valued Function-like Element of bool [: the carrier of X, the carrier of X:]
X is set
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
bool the carrier of (BoolePoset X) is non empty Element of bool (bool the carrier of (BoolePoset X))
G is set
Mg is Element of the carrier of (BoolePoset X)
uparrow Mg is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Mg) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Mg) is non empty upper Element of bool the carrier of (BoolePoset X)
f is Element of X
{f} is non empty set
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
L is set
G is Element of the carrier of (BoolePoset X)
uparrow G is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),G) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),G) is non empty upper Element of bool the carrier of (BoolePoset X)
Mg is Element of X
{Mg} is non empty set
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
card (X) is cardinal set
card X is cardinal set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
InclPoset (bool X) is non empty strict V67() V68() V69() RelStr
RelIncl (bool X) is Relation-like bool X -defined bool X -valued V19() V22() V26() V27( bool X) quasi_total Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
RelStr(# (bool X),(RelIncl (bool X)) #) is strict RelStr
G is set
{G} is non empty set
f is Element of the carrier of (BoolePoset X)
uparrow f is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),f) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),f) is non empty upper Element of bool the carrier of (BoolePoset X)
Mg is Element of X
{Mg} is non empty set
G is Relation-like Function-like set
dom G is set
rng G is set
Mg is set
f is set
G . Mg is set
G . f is set
Mg is Element of the carrier of (BoolePoset X)
g is Element of X
{g} is non empty set
uparrow Mg is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Mg) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Mg) is non empty upper Element of bool the carrier of (BoolePoset X)
f is Element of the carrier of (BoolePoset X)
Lg is Element of X
{Lg} is non empty set
uparrow f is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),f) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),f) is non empty upper Element of bool the carrier of (BoolePoset X)
Mg is set
f is set
G . f is set
Mg is Element of the carrier of (BoolePoset X)
g is Element of X
{g} is non empty set
uparrow Mg is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Mg) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Mg) is non empty upper Element of bool the carrier of (BoolePoset X)
f is Element of the carrier of (BoolePoset X)
uparrow f is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),f) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),f) is non empty upper Element of bool the carrier of (BoolePoset X)
g is Element of X
{g} is non empty set
g is Element of X
{g} is non empty set
G . g is set
Lg is Element of the carrier of (BoolePoset X)
Mg is Element of X
{Mg} is non empty set
uparrow Lg is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Lg) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Lg) is non empty upper Element of bool the carrier of (BoolePoset X)
X is set
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
bool X is non empty set
L is non empty filtered upper Element of bool the carrier of (BoolePoset X)
{ ("/\" ( { (uparrow b₂) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,(InclPoset (Filt (BoolePoset X))))) where b₁ is Element of bool X : b₁ in L } is set
"\/" ( { ("/\" ( { (uparrow b₂) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,(InclPoset (Filt (BoolePoset X))))) where b₁ is Element of bool X : b₁ in L } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
RelIncl (Filt (BoolePoset X)) is Relation-like Filt (BoolePoset X) -defined Filt (BoolePoset X) -valued V19() V22() V26() V27( Filt (BoolePoset X)) quasi_total Element of bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):]
[:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty Relation-like set
bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty set
RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) is strict RelStr
f is set
F is Element of bool X
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in F ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in F ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
BooleLatt X is non empty V161() V168() V175() complete L17()
LattPOSet (BooleLatt X) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (BooleLatt X) is non empty set
K432((BooleLatt X)) is Relation-like the carrier of (BooleLatt X) -defined the carrier of (BooleLatt X) -valued V19() V22() V26() V27( the carrier of (BooleLatt X)) quasi_total Element of bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):]
[: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty Relation-like set
bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty set
RelStr(# the carrier of (BooleLatt X),K432((BooleLatt X)) #) is strict RelStr
the carrier of (LattPOSet (BooleLatt X)) is non empty set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
f is set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in f ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in f ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
bool the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
f is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
F is set
g is Element of L
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in g ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in g ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Top (InclPoset (Filt (BoolePoset X))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" ({},(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
GF is set
FG is Element of the carrier of (BoolePoset X)
uparrow FG is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),FG) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),FG) is non empty upper Element of bool the carrier of (BoolePoset X)
Xsf is Element of X
{Xsf} is non empty set
GF is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
Xsf is set
Xs is Element of the carrier of (BoolePoset X)
uparrow Xs is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xs) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xs) is non empty upper Element of bool the carrier of (BoolePoset X)
Xs is Element of X
{Xs} is non empty set
FG is Element of the carrier of (BoolePoset X)
"/\" (GF,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
meet GF is set
union { ("/\" ( { (uparrow b₂) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,(InclPoset (Filt (BoolePoset X))))) where b₁ is Element of bool X : b₁ in L } is set
union f is set
Lg is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
F is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
g is Element of bool X
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in g ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in g ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
FG is set
Xsf is Element of the carrier of (BoolePoset X)
uparrow Xsf is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsf) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsf) is non empty upper Element of bool the carrier of (BoolePoset X)
Xs is Element of X
{Xs} is non empty set
Top (InclPoset (Filt (BoolePoset X))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" ({},(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Bottom (BoolePoset X) is Element of the carrier of (BoolePoset X)
"\/" ({},(BoolePoset X)) is Element of the carrier of (BoolePoset X)
uparrow (Bottom (BoolePoset X)) is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),(Bottom (BoolePoset X))) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),(Bottom (BoolePoset X))) is non empty upper Element of bool the carrier of (BoolePoset X)
FG is set
Xsf is Element of X
{Xsf} is non empty set
Xs is Element of the carrier of (BoolePoset X)
uparrow Xs is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xs) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xs) is non empty upper Element of bool the carrier of (BoolePoset X)
FG is set
Xsf is Element of the carrier of (BoolePoset X)
uparrow Xsf is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsf) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsf) is non empty upper Element of bool the carrier of (BoolePoset X)
Xs is Element of X
{Xs} is non empty set
FG is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" (FG,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
meet FG is set
Xsf is set
Xs is non empty filtered upper Element of bool the carrier of (BoolePoset X)
Xs is Element of Xs
s is Element of the carrier of (BoolePoset X)
Y is set
Xsi is Element of X
{Xsi} is non empty set
Xsi is Element of the carrier of (BoolePoset X)
uparrow Xsi is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsi) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsi) is non empty upper Element of bool the carrier of (BoolePoset X)
G is Element of L
uparrow G is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),G) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),G) is non empty upper Element of bool the carrier of (BoolePoset X)
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
[:(X), the carrier of L:] is Relation-like set
bool [:(X), the carrier of L:] is non empty set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty set
bool X is non empty set
G is Relation-like (X) -defined the carrier of L -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of L:]
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in a₁ } is set
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in a₁ } ,L) is Element of the carrier of L
f is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
g is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
Mg is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
g . Mg is Element of the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Mg } is set
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Mg } ,L) is Element of the carrier of L
f is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
g is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
Lg is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
f is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Lg . f is Element of the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in f } is set
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in f } ,L) is Element of the carrier of L
Mg is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
Mg . f is Element of the carrier of L
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
[:(X), the carrier of L:] is Relation-like set
bool [:(X), the carrier of L:] is non empty set
G is Relation-like (X) -defined the carrier of L -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of L:]
(X,L,G) is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty set
Mg is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
f is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
(X,L,G) . Mg is set
(X,L,G) . f is set
bool X is non empty set
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Mg } is set
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in f } is set
(X,L,G) . Mg is Element of the carrier of L
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Mg } ,L) is Element of the carrier of L
f is set
F is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in F ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in F ) } ,L) is Element of the carrier of L
(X,L,G) . f is Element of the carrier of L
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in f } ,L) is Element of the carrier of L
f is Element of the carrier of L
F is Element of the carrier of L
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
Top (InclPoset (Filt (BoolePoset X))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" ({},(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
[:(X), the carrier of L:] is Relation-like set
bool [:(X), the carrier of L:] is non empty set
Top L is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
G is Relation-like (X) -defined the carrier of L -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of L:]
(X,L,G) is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty set
(X,L,G) . (Top (InclPoset (Filt (BoolePoset X)))) is Element of the carrier of L
bool X is non empty set
g is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in g } is set
Mg is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Mg ) } is set
f is set
F is Element of the carrier of (BoolePoset X)
uparrow F is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),F) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),F) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow F) is set
g is Element of X
{g} is non empty set
(X,L,G) . g is Element of the carrier of L
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in g } ,L) is Element of the carrier of L
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Mg ) } ,L) is Element of the carrier of L
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
[:(X), the carrier of L:] is Relation-like set
bool [:(X), the carrier of L:] is non empty set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
G is Relation-like (X) -defined the carrier of L -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of L:]
(X,L,G) is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty set
bool the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
g is Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
Mg is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
bool X is non empty set
{ { ("/\" ( { (G . (uparrow b₃)) where b₃ is Element of the carrier of (BoolePoset X) : ex b₄ being Element of X st
( b₃ = {b₄} & b₄ in b₂ ) } ,L)) where b₂ is Element of bool X : b₂ in b₁ } where b₁ is Element of Mg : verum } is set
"\/" (g,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
f is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in f } is set
union g is set
g is set
G is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in G ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in G ) } ,L) is Element of the carrier of L
GF is set
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in GF } is set
union { { ("/\" ( { (G . (uparrow b₃)) where b₃ is Element of the carrier of (BoolePoset X) : ex b₄ being Element of X st
( b₃ = {b₄} & b₄ in b₂ ) } ,L)) where b₂ is Element of bool X : b₂ in b₁ } where b₁ is Element of Mg : verum } is set
G is set
GF is Element of Mg
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in GF } is set
FG is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in FG ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in FG ) } ,L) is Element of the carrier of L
bool the carrier of L is non empty set
{ ("\/" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in { { ("/\" ( { (G . (uparrow b₃)) where b₄ is Element of the carrier of (BoolePoset X) : ex b₅ being Element of X st
( b₃ = {b₄} & b₄ in b₂ ) } ,L)) where b₃ is Element of bool X : b₂ in b₁ } where b₂ is Element of Mg : verum } } is set
(X,L,G) .: g is Element of bool the carrier of L
"\/" (((X,L,G) .: g),L) is Element of the carrier of L
(X,L,G) . ("\/" (g,(InclPoset (Filt (BoolePoset X))))) is Element of the carrier of L
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
G is set
GF is Element of Mg
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in GF } is set
FG is set
Xsf is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsf ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsf ) } ,L) is Element of the carrier of L
"\/" ((union { { ("/\" ( { (G . (uparrow b₃)) where b₃ is Element of the carrier of (BoolePoset X) : ex b₄ being Element of X st
( b₃ = {b₄} & b₄ in b₂ ) } ,L)) where b₂ is Element of bool X : b₂ in b₁ } where b₁ is Element of Mg : verum } ),L) is Element of the carrier of L
"\/" ( { ("\/" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in { { ("/\" ( { (G . (uparrow b₃)) where b₄ is Element of the carrier of (BoolePoset X) : ex b₅ being Element of X st
( b₃ = {b₄} & b₄ in b₂ ) } ,L)) where b₃ is Element of bool X : b₂ in b₁ } where b₂ is Element of Mg : verum } } ,L) is Element of the carrier of L
G is set
GF is set
(X,L,G) . GF is set
FG is Element of g
Xsf is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Xsf } is set
Xs is set
s is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in s ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in s ) } ,L) is Element of the carrier of L
Xs is Element of bool the carrier of L
(X,L,G) . Xsf is Element of the carrier of L
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Xsf } ,L) is Element of the carrier of L
GF is Element of bool the carrier of L
"\/" (GF,L) is Element of the carrier of L
FG is Element of g
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in FG } is set
Xsf is Element of Mg
Xs is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
(X,L,G) . Xs is Element of the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Xs } is set
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Xs } ,L) is Element of the carrier of L
(X,L,G) . f is Element of the carrier of L
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in f } ,L) is Element of the carrier of L
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
[:(X), the carrier of L:] is Relation-like set
bool [:(X), the carrier of L:] is non empty set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
G is Relation-like (X) -defined the carrier of L -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of L:]
(X,L,G) is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total directed-sups-preserving Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty set
RelIncl (Filt (BoolePoset X)) is Relation-like Filt (BoolePoset X) -defined Filt (BoolePoset X) -valued V19() V22() V26() V27( Filt (BoolePoset X)) quasi_total Element of bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):]
[:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty Relation-like set
bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty set
RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) is strict RelStr
bool the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
F is Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
(X,L,G) .: F is Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" (((X,L,G) .: F),L) is Element of the carrier of L
"/\" (F,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
(X,L,G) . ("/\" (F,(InclPoset (Filt (BoolePoset X))))) is Element of the carrier of L
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
InclPoset (bool X) is non empty strict V67() V68() V69() RelStr
RelIncl (bool X) is Relation-like bool X -defined bool X -valued V19() V22() V26() V27( bool X) quasi_total Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
RelStr(# (bool X),(RelIncl (bool X)) #) is strict RelStr
Top L is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
Top (InclPoset (Filt (BoolePoset X))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" ({},(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in a₂ ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in a₂ ) } ,L) is Element of the carrier of L
g is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in a₁ } is set
id g is non empty Relation-like g -defined g -valued Function-like one-to-one V27(g) quasi_total Element of bool [:g,g:]
[:g,g:] is non empty Relation-like set
bool [:g,g:] is non empty set
G is non empty Relation-like non-empty non empty-yielding g -defined Function-like V27(g) set
g --> the carrier of L is non empty Relation-like non-empty non empty-yielding g -defined { the carrier of L} -valued Function-like constant V27(g) quasi_total Element of bool [:g,{ the carrier of L}:]
{ the carrier of L} is non empty set
[:g,{ the carrier of L}:] is non empty Relation-like set
bool [:g,{ the carrier of L}:] is non empty set
GF is set
G . GF is set
(g --> the carrier of L) . GF is set
FG is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in FG ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in FG ) } ,L) is Element of the carrier of L
Xsf is Element of the carrier of L
GF is non empty Relation-like non-empty non empty-yielding g -defined Function-like V27(g) Function-yielding V106() ManySortedFunction of G,g --> the carrier of L
FG is Element of g
GF . FG is non empty Relation-like G . FG -defined the carrier of L -valued Function-like V27(G . FG) quasi_total Element of bool [:(G . FG), the carrier of L:]
G . FG is non empty set
[:(G . FG), the carrier of L:] is non empty Relation-like set
bool [:(G . FG), the carrier of L:] is non empty set
rng (GF . FG) is non empty Element of bool the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in FG } is set
(g --> the carrier of L) . FG is non empty Element of { the carrier of L}
[:(G . FG),((g --> the carrier of L) . FG):] is non empty Relation-like set
bool [:(G . FG),((g --> the carrier of L) . FG):] is non empty set
Xs is non empty Relation-like G . FG -defined (g --> the carrier of L) . FG -valued Function-like V27(G . FG) quasi_total Element of bool [:(G . FG),((g --> the carrier of L) . FG):]
Xsf is set
dom (GF . FG) is non empty Element of bool (G . FG)
bool (G . FG) is non empty set
Xs is set
(GF . FG) . Xs is set
s is non empty Relation-like G . FG -defined (g --> the carrier of L) . FG -valued Function-like V27(G . FG) quasi_total Element of bool [:(G . FG),((g --> the carrier of L) . FG):]
s . Xs is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } ,L) is Element of the carrier of L
Xsi is non empty filtered upper Element of bool the carrier of (BoolePoset X)
Y is Element of bool X
Xs is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } ,L) is Element of the carrier of L
Xs . Xs is set
meet g is set
FG is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in FG } is set
dom GF is non empty Element of bool g
bool g is non empty set
Xs is set
s is set
(X,L,G) . s is set
Xsi is Element of g
GF . Xsi is non empty Relation-like G . Xsi -defined the carrier of L -valued Function-like V27(G . Xsi) quasi_total Element of bool [:(G . Xsi), the carrier of L:]
G . Xsi is non empty set
[:(G . Xsi), the carrier of L:] is non empty Relation-like set
bool [:(G . Xsi), the carrier of L:] is non empty set
rng (GF . Xsi) is non empty Element of bool the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Xsi } is set
Y is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
(X,L,G) . Y is Element of the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Y } is set
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in Y } ,L) is Element of the carrier of L
Xs is non empty Relation-like non-empty non empty-yielding g -defined Function-like V27(g) Function-yielding V106() ManySortedFunction of G,g --> the carrier of L
Xs . Xsi is non empty Relation-like G . Xsi -defined the carrier of L -valued Function-like V27(G . Xsi) quasi_total Element of bool [:(G . Xsi), the carrier of L:]
\\/ ((Xs . Xsi),L) is Element of the carrier of L
\// (Xs,L) is non empty Relation-like dom Xs -defined the carrier of L -valued Function-like V27( dom Xs) quasi_total Element of bool [:(dom Xs), the carrier of L:]
dom Xs is non empty set
[:(dom Xs), the carrier of L:] is non empty Relation-like set
bool [:(dom Xs), the carrier of L:] is non empty set
rng (\// (Xs,L)) is non empty Element of bool the carrier of L
s is Element of g
Xs . s is non empty Relation-like G . s -defined the carrier of L -valued Function-like V27(G . s) quasi_total Element of bool [:(G . s), the carrier of L:]
G . s is non empty set
[:(G . s), the carrier of L:] is non empty Relation-like set
bool [:(G . s), the carrier of L:] is non empty set
\\/ ((Xs . s),L) is Element of the carrier of L
GF . s is non empty Relation-like G . s -defined the carrier of L -valued Function-like V27(G . s) quasi_total Element of bool [:(G . s), the carrier of L:]
rng (GF . s) is non empty Element of bool the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in s } is set
(X,L,G) . s is Element of the carrier of L
rng (Xs . s) is non empty Element of bool the carrier of L
"\/" ((rng (Xs . s)),L) is Element of the carrier of L
//\ ((\// (Xs,L)),L) is Element of the carrier of L
doms Xs is Relation-like non-empty Function-like set
product (doms Xs) is non empty functional with_common_domain product-like set
Xs is non empty functional set
(product (doms Xs)) --> g is non empty Relation-like non-empty non empty-yielding product (doms Xs) -defined bool the carrier of (InclPoset (Filt (BoolePoset X))) -valued Function-like constant V27( product (doms Xs)) quasi_total Element of bool [:(product (doms Xs)),(bool the carrier of (InclPoset (Filt (BoolePoset X)))):]
[:(product (doms Xs)),(bool the carrier of (InclPoset (Filt (BoolePoset X)))):] is non empty Relation-like set
bool [:(product (doms Xs)),(bool the carrier of (InclPoset (Filt (BoolePoset X)))):] is non empty set
Y is non empty Relation-like Xs -defined Function-like V27(Xs) set
Xs --> the carrier of L is non empty Relation-like non-empty non empty-yielding Xs -defined { the carrier of L} -valued Function-like constant V27(Xs) quasi_total Element of bool [:Xs,{ the carrier of L}:]
[:Xs,{ the carrier of L}:] is non empty Relation-like set
bool [:Xs,{ the carrier of L}:] is non empty set
Frege Xs is non empty Relation-like non-empty non empty-yielding product (doms Xs) -defined Function-like V27( product (doms Xs)) Function-yielding V106() ManySortedFunction of (product (doms Xs)) --> g,(product (doms Xs)) --> the carrier of L
(product (doms Xs)) --> g is non empty Relation-like non-empty non empty-yielding product (doms Xs) -defined bool the carrier of (InclPoset (Filt (BoolePoset X))) -valued {g} -valued Function-like constant V27( product (doms Xs)) quasi_total Element of bool [:(product (doms Xs)),{g}:]
{g} is non empty set
[:(product (doms Xs)),{g}:] is non empty Relation-like set
bool [:(product (doms Xs)),{g}:] is non empty set
(product (doms Xs)) --> the carrier of L is non empty Relation-like non-empty non empty-yielding product (doms Xs) -defined { the carrier of L} -valued Function-like constant V27( product (doms Xs)) quasi_total Element of bool [:(product (doms Xs)),{ the carrier of L}:]
[:(product (doms Xs)),{ the carrier of L}:] is non empty Relation-like set
bool [:(product (doms Xs)),{ the carrier of L}:] is non empty set
Xsi is non empty Relation-like Xs -defined Function-like V27(Xs) Function-yielding V106() ManySortedFunction of Y,Xs --> the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in a₁ . b₁ ) } ,L)) where b₁ is Element of g : b₁ in dom (Xsi . a₁) } is set
dom Xsi is non empty functional Element of bool Xs
bool Xs is non empty set
dom Xs is non empty Element of bool g
Xsi is Relation-like Function-like Element of Xs
Y . Xsi is set
Xsi . Xsi is Relation-like Y . Xsi -defined the carrier of L -valued Function-like V27(Y . Xsi) quasi_total Element of bool [:(Y . Xsi), the carrier of L:]
[:(Y . Xsi), the carrier of L:] is Relation-like set
bool [:(Y . Xsi), the carrier of L:] is non empty set
dom (Xsi . Xsi) is Element of bool (Y . Xsi)
bool (Y . Xsi) is non empty set
Xsif is set
rng (Xsi . Xsi) is Element of bool the carrier of L
u is set
(Xsi . Xsi) . u is set
Xs . u is Relation-like Function-like set
Xsi . u is set
(Xs . u) . (Xsi . u) is set
x is Element of g
G . x is non empty set
(g --> the carrier of L) . x is non empty Element of { the carrier of L}
[:(G . x),((g --> the carrier of L) . x):] is non empty Relation-like set
bool [:(G . x),((g --> the carrier of L) . x):] is non empty set
Xs . x is non empty Relation-like G . x -defined the carrier of L -valued Function-like V27(G . x) quasi_total Element of bool [:(G . x), the carrier of L:]
[:(G . x), the carrier of L:] is non empty Relation-like set
bool [:(G . x), the carrier of L:] is non empty set
x is non empty Relation-like G . x -defined (g --> the carrier of L) . x -valued Function-like V27(G . x) quasi_total Element of bool [:(G . x),((g --> the carrier of L) . x):]
dom (Xs . x) is non empty Element of bool (G . x)
bool (G . x) is non empty set
Xsi . x is set
x . (Xsi . x) is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } ,L) is Element of the carrier of L
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in Xsi . b₁ ) } ,L)) where b₁ is Element of g : b₁ in dom (Xsi . Xsi) } is set
u is Element of g
Xsi . u is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . u ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . u ) } ,L) is Element of the carrier of L
x is Element of g
G . x is non empty set
(g --> the carrier of L) . x is non empty Element of { the carrier of L}
[:(G . x),((g --> the carrier of L) . x):] is non empty Relation-like set
bool [:(G . x),((g --> the carrier of L) . x):] is non empty set
Xs . x is non empty Relation-like G . x -defined the carrier of L -valued Function-like V27(G . x) quasi_total Element of bool [:(G . x), the carrier of L:]
[:(G . x), the carrier of L:] is non empty Relation-like set
bool [:(G . x), the carrier of L:] is non empty set
x is non empty Relation-like G . x -defined (g --> the carrier of L) . x -valued Function-like V27(G . x) quasi_total Element of bool [:(G . x),((g --> the carrier of L) . x):]
dom (Xs . x) is non empty Element of bool (G . x)
bool (G . x) is non empty set
Xsi . x is set
x . (Xsi . x) is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } ,L) is Element of the carrier of L
s is set
/\\ ((Frege Xs),L) is non empty Relation-like dom (Frege Xs) -defined the carrier of L -valued Function-like V27( dom (Frege Xs)) quasi_total Element of bool [:(dom (Frege Xs)), the carrier of L:]
dom (Frege Xs) is non empty set
[:(dom (Frege Xs)), the carrier of L:] is non empty Relation-like set
bool [:(dom (Frege Xs)), the carrier of L:] is non empty set
rng (/\\ ((Frege Xs),L)) is non empty Element of bool the carrier of L
Xsi is Relation-like Function-like Element of Xs
Xsi . Xsi is Relation-like Y . Xsi -defined the carrier of L -valued Function-like V27(Y . Xsi) quasi_total Element of bool [:(Y . Xsi), the carrier of L:]
Y . Xsi is set
[:(Y . Xsi), the carrier of L:] is Relation-like set
bool [:(Y . Xsi), the carrier of L:] is non empty set
//\ ((Xsi . Xsi),L) is Element of the carrier of L
dom (Xsi . Xsi) is Element of bool (Y . Xsi)
bool (Y . Xsi) is non empty set
{ { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in Xsi . b₁ ) } where b₁ is Element of g : b₁ in dom (Xsi . Xsi) } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
u is set
x is Element of g
Xsi . x is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } is set
x is set
Xsb is Element of the carrier of (BoolePoset X)
uparrow Xsb is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsb) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsb) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow Xsb) is set
Xsa is Element of X
{Xsa} is non empty set
u is set
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in Xsi . b₁ ) } ,L)) where b₁ is Element of g : b₁ in dom (Xsi . Xsi) } is set
x is Element of g
Xsi . x is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } ,L) is Element of the carrier of L
x is set
Xsb is Element of the carrier of (BoolePoset X)
uparrow Xsb is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsb) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsb) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow Xsb) is set
Xsa is Element of X
{Xsa} is non empty set
x is Element of bool the carrier of L
{ ("/\" (b₁,L)) where b₁ is Element of bool the carrier of L : b₁ in { { (G . (uparrow b₂)) where b₃ is Element of the carrier of (BoolePoset X) : ex b₄ being Element of X st
( b₂ = {b₃} & b₃ in Xsi . b₁ ) } where b₂ is Element of g : b₁ in dom (Xsi . Xsi) } } is set
x is Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
x is Element of g
Xsi . x is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . x ) } is set
dom Xsi is set
rng Xsi is set
union (rng Xsi) is set
u is set
x is set
x is set
Xsi . x is set
Xs . x is Relation-like Function-like set
G . x is set
[:(G . x), the carrier of L:] is Relation-like set
bool [:(G . x), the carrier of L:] is non empty set
dom (Xs . x) is set
Xsb is non empty filtered upper Element of bool the carrier of (BoolePoset X)
u is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in u ) } is set
x is set
union { { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in Xsi . b₁ ) } where b₁ is Element of g : b₁ in dom (Xsi . Xsi) } is set
Xsb is set
Xsa is Element of g
Xsi . Xsa is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . Xsa ) } is set
Yab is Element of the carrier of (BoolePoset X)
uparrow Yab is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Yab) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Yab) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow Yab) is set
Yab is Element of X
{Yab} is non empty set
Yab is Element of X
{Yab} is non empty set
Xsb is Element of the carrier of (BoolePoset X)
uparrow Xsb is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsb) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsb) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow Xsb) is set
Xsa is Element of X
{Xsa} is non empty set
Xsa is Element of X
{Xsa} is non empty set
Yab is set
Yab is set
Xsi . Yab is set
c is Element of g
Xsi . c is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi . c ) } is set
Xsb is set
Xs . Xsb is Relation-like Function-like set
G . Xsb is set
[:(G . Xsb), the carrier of L:] is Relation-like set
bool [:(G . Xsb), the carrier of L:] is non empty set
dom (Xs . Xsb) is set
Xsi . Xsb is set
Xsa is Element of the carrier of (BoolePoset X)
x is Element of the carrier of (BoolePoset X)
Yab is non empty filtered upper Element of bool the carrier of (BoolePoset X)
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in u ) } ,L) is Element of the carrier of L
rng (Xsi . Xsi) is Element of bool the carrier of L
"/\" ((rng (Xsi . Xsi)),L) is Element of the carrier of L
"/\" (H₂(Xsi),L) is Element of the carrier of L
"/\" ((union { { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in Xsi . b₁ ) } where b₁ is Element of g : b₁ in dom (Xsi . Xsi) } ),L) is Element of the carrier of L
Xsi is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi ) } ,L) is Element of the carrier of L
{s} is non empty set
"/\" ({s},L) is Element of the carrier of L
g --> Xsi is non empty Relation-like g -defined bool X -valued Function-like constant V27(g) quasi_total Element of bool [:g,(bool X):]
[:g,(bool X):] is non empty Relation-like set
bool [:g,(bool X):] is non empty set
dom (doms Xs) is set
dom (g --> Xsi) is non empty Element of bool g
u is set
Xs . u is Relation-like Function-like set
G . u is set
(g --> the carrier of L) . u is set
[:(G . u),((g --> the carrier of L) . u):] is Relation-like set
bool [:(G . u),((g --> the carrier of L) . u):] is non empty set
dom (Xs . u) is set
(doms Xs) . u is set
(g --> Xsi) . u is set
the Element of g is Element of g
x is Relation-like Function-like Element of Xs
x . the Element of g is set
Xsb is set
Y . x is set
Xsi . x is Relation-like Y . x -defined the carrier of L -valued Function-like V27(Y . x) quasi_total Element of bool [:(Y . x), the carrier of L:]
[:(Y . x), the carrier of L:] is Relation-like set
bool [:(Y . x), the carrier of L:] is non empty set
dom (Xsi . x) is Element of bool (Y . x)
bool (Y . x) is non empty set
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in x . b₁ ) } ,L)) where b₁ is Element of g : b₁ in dom (Xsi . x) } is set
Xsa is Element of g
x . Xsa is set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in x . Xsa ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in x . Xsa ) } ,L) is Element of the carrier of L
dom x is set
//\ ((Xsi . x),L) is Element of the carrier of L
rng (Xsi . x) is Element of bool the carrier of L
"/\" ((rng (Xsi . x)),L) is Element of the carrier of L
Xs is Element of g
Xs . Xs is non empty Relation-like G . Xs -defined the carrier of L -valued Function-like V27(G . Xs) quasi_total Element of bool [:(G . Xs), the carrier of L:]
G . Xs is non empty set
[:(G . Xs), the carrier of L:] is non empty Relation-like set
bool [:(G . Xs), the carrier of L:] is non empty set
rng (Xs . Xs) is non empty Element of bool the carrier of L
s is Element of the carrier of L
Y is Element of the carrier of L
dom (Xs . Xs) is non empty Element of bool (G . Xs)
bool (G . Xs) is non empty set
Xsi is set
(Xs . Xs) . Xsi is set
Xsi is set
(Xs . Xs) . Xsi is set
Xsif is non empty filtered upper Element of bool the carrier of (BoolePoset X)
u is Element of the carrier of (BoolePoset X)
x is Element of the carrier of (BoolePoset X)
x is Element of the carrier of (BoolePoset X)
(Xs . Xs) . x is set
(g --> the carrier of L) . Xs is non empty Element of { the carrier of L}
[:(G . Xs),((g --> the carrier of L) . Xs):] is non empty Relation-like set
bool [:(G . Xs),((g --> the carrier of L) . Xs):] is non empty set
Xsa is non empty Relation-like G . Xs -defined (g --> the carrier of L) . Xs -valued Function-like V27(G . Xs) quasi_total Element of bool [:(G . Xs),((g --> the carrier of L) . Xs):]
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in x ) } is set
Xsa . x is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in x ) } ,L) is Element of the carrier of L
Yab is Element of the carrier of L
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in x ) } is set
Xsc is set
Xsc is Element of the carrier of (BoolePoset X)
uparrow Xsc is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsc) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsc) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow Xsc) is set
d is Element of X
{d} is non empty set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in u ) } is set
Xsc is set
d is Element of the carrier of (BoolePoset X)
uparrow d is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),d) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),d) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow d) is set
r is Element of X
{r} is non empty set
Xsa . u is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in u ) } ,L) is Element of the carrier of L
Xsa . x is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in x ) } ,L) is Element of the carrier of L
\\/ ((/\\ ((Frege Xs),L)),L) is Element of the carrier of L
"\/" ((rng (/\\ ((Frege Xs),L))),L) is Element of the carrier of L
"/\" (g,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
(X,L,G) . (meet g) is set
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in FG } ,L) is Element of the carrier of L
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
[:(X), the carrier of L:] is Relation-like set
bool [:(X), the carrier of L:] is non empty set
G is Relation-like (X) -defined the carrier of L -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of L:]
(X,L,G) is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total infs-preserving meet-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty set
(X,L,G) | (X) is Relation-like (X) -defined the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
RelIncl (Filt (BoolePoset X)) is Relation-like Filt (BoolePoset X) -defined Filt (BoolePoset X) -valued V19() V22() V26() V27( Filt (BoolePoset X)) quasi_total Element of bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):]
[:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty Relation-like set
bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty set
RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) is strict RelStr
BooleLatt X is non empty V161() V168() V175() complete L17()
LattPOSet (BooleLatt X) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (BooleLatt X) is non empty set
K432((BooleLatt X)) is Relation-like the carrier of (BooleLatt X) -defined the carrier of (BooleLatt X) -valued V19() V22() V26() V27( the carrier of (BooleLatt X)) quasi_total Element of bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):]
[: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty Relation-like set
bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty set
RelStr(# the carrier of (BooleLatt X),K432((BooleLatt X)) #) is strict RelStr
the carrier of (LattPOSet (BooleLatt X)) is non empty set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
dom (X,L,G) is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
bool the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
dom ((X,L,G) | (X)) is Element of bool (X)
bool (X) is non empty set
dom G is Element of bool (X)
Lg is set
((X,L,G) | (X)) . Lg is set
(X,L,G) . Lg is set
f is non empty Element of bool (bool the carrier of (BoolePoset X))
F is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in F } is set
[:f, the carrier of L:] is non empty Relation-like set
bool [:f, the carrier of L:] is non empty set
GF is non empty Relation-like f -defined the carrier of L -valued Function-like V27(f) quasi_total Element of bool [:f, the carrier of L:]
g is Element of f
GF . g is Element of the carrier of L
G . g is set
Xsf is Element of the carrier of (BoolePoset X)
uparrow Xsf is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsf) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsf) is non empty upper Element of bool the carrier of (BoolePoset X)
FG is Element of the carrier of L
Xs is Element of the carrier of L
Xs is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } ,L) is Element of the carrier of L
Xsi is Element of X
{Xsi} is non empty set
Xsi is Element of X
{Xsi} is non empty set
Y is Element of the carrier of (BoolePoset X)
Xs is Element of F
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } is set
s is Element of X
{s} is non empty set
s is Element of X
{s} is non empty set
Y is set
Xsi is Element of the carrier of (BoolePoset X)
uparrow Xsi is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsi) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsi) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow Xsi) is set
Xsi is Element of X
{Xsi} is non empty set
{FG} is non empty set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } ,L) is Element of the carrier of L
Y is Element of the carrier of L
G . Lg is set
"\/" ( { ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in F } ,L) is Element of the carrier of L
X is set
(X) is Element of bool (bool the carrier of (BoolePoset X))
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
Filt (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of L is non empty set
[:(X), the carrier of L:] is Relation-like set
bool [:(X), the carrier of L:] is non empty set
G is Relation-like (X) -defined the carrier of L -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of L:]
(X,L,G) is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total infs-preserving meet-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:] is non empty set
Mg is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total CLHomomorphism of InclPoset (Filt (BoolePoset X)),L
Mg | (X) is Relation-like (X) -defined the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
RelIncl (Filt (BoolePoset X)) is Relation-like Filt (BoolePoset X) -defined Filt (BoolePoset X) -valued V19() V22() V26() V27( Filt (BoolePoset X)) quasi_total Element of bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):]
[:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty Relation-like set
bool [:(Filt (BoolePoset X)),(Filt (BoolePoset X)):] is non empty set
RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) is strict RelStr
BooleLatt X is non empty V161() V168() V175() complete L17()
LattPOSet (BooleLatt X) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete RelStr
the carrier of (BooleLatt X) is non empty set
K432((BooleLatt X)) is Relation-like the carrier of (BooleLatt X) -defined the carrier of (BooleLatt X) -valued V19() V22() V26() V27( the carrier of (BooleLatt X)) quasi_total Element of bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):]
[: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty Relation-like set
bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty set
RelStr(# the carrier of (BooleLatt X),K432((BooleLatt X)) #) is strict RelStr
the carrier of (LattPOSet (BooleLatt X)) is non empty set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
GF is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
FG is non empty filtered upper Element of bool the carrier of (BoolePoset X)
{ ("/\" ( { (G . (uparrow b₂)) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,L)) where b₁ is Element of bool X : b₁ in FG } is set
{ ("/\" ( { (uparrow b₂) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,(InclPoset (Filt (BoolePoset X))))) where b₁ is Element of bool X : b₁ in FG } is set
Xs is set
s is Element of bool X
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in s ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in s ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Xs is set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xs ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
bool the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
Xs is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
s is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Y is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Xsi is Element of bool X
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
u is Element of bool X
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in u ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in u ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Top (InclPoset (Filt (BoolePoset X))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" ({},(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Top (InclPoset (Filt (BoolePoset X))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" ({},(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Xsb is set
Xsa is Element of the carrier of (BoolePoset X)
uparrow Xsa is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsa) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsa) is non empty upper Element of bool the carrier of (BoolePoset X)
Yab is Element of X
{Yab} is non empty set
Xsa is set
Yab is Element of the carrier of (BoolePoset X)
uparrow Yab is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Yab) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Yab) is non empty upper Element of bool the carrier of (BoolePoset X)
Yab is Element of X
{Yab} is non empty set
Xsb is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" (Xsb,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
meet Xsb is set
x is Element of FG
Xsi is Element of FG
Yab is Element of the carrier of (BoolePoset X)
Yab is Element of FG
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Yab ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Xsa is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" (Xsa,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
meet Xsa is set
Top (InclPoset (Filt (BoolePoset X))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" ({},(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Xsc is set
d is Element of the carrier of (BoolePoset X)
uparrow d is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),d) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),d) is non empty upper Element of bool the carrier of (BoolePoset X)
r is Element of X
{r} is non empty set
Xsc is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
"/\" (Xsc,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
meet Xsc is set
d is set
r is set
c₃₅ is Element of the carrier of (BoolePoset X)
uparrow c₃₅ is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),c₃₅) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),c₃₅) is non empty upper Element of bool the carrier of (BoolePoset X)
c₃₆ is Element of X
{c₃₆} is non empty set
d is set
r is set
c₃₅ is Element of the carrier of (BoolePoset X)
uparrow c₃₅ is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),c₃₅) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),c₃₅) is non empty upper Element of bool the carrier of (BoolePoset X)
c₃₆ is Element of X
{c₃₆} is non empty set
s is set
Mg .: Xs is Element of bool the carrier of L
bool the carrier of L is non empty set
Y is set
Mg . Y is set
Xsi is Element of bool X
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi ) } is set
"/\" ( { (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi ) } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Xsif is set
u is Element of the carrier of (BoolePoset X)
uparrow u is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),u) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),u) is non empty upper Element of bool the carrier of (BoolePoset X)
x is Element of X
{x} is non empty set
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Xsi ) } is set
x is set
Xsif is Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
Mg .: Xsif is Element of bool the carrier of L
x is set
Mg . x is set
Xsb is Element of the carrier of (BoolePoset X)
uparrow Xsb is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsb) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsb) is non empty upper Element of bool the carrier of (BoolePoset X)
Xsa is Element of X
{Xsa} is non empty set
G . x is set
Xsb is Element of the carrier of (BoolePoset X)
uparrow Xsb is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsb) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsb) is non empty upper Element of bool the carrier of (BoolePoset X)
Xsa is Element of X
{Xsa} is non empty set
x is Element of the carrier of (BoolePoset X)
uparrow x is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),x) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),x) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow x) is set
Xsb is Element of X
{Xsb} is non empty set
Mg . (uparrow x) is set
Xsb is Element of X
{Xsb} is non empty set
"/\" ((Mg .: Xsif),L) is Element of the carrier of L
"/\" (Xsif,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Mg . ("/\" (Xsif,(InclPoset (Filt (BoolePoset X))))) is Element of the carrier of L
Y is Element of bool X
{ (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Y ) } is set
"/\" ( { (G . (uparrow b₁)) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Y ) } ,L) is Element of the carrier of L
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st
( b₁ = {b₂} & b₂ in Y ) } is set
Xsi is set
Xsif is Element of the carrier of (BoolePoset X)
uparrow Xsif is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),Xsif) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),Xsif) is non empty upper Element of bool the carrier of (BoolePoset X)
u is Element of X
{u} is non empty set
Xsi is Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))
Mg .: Xsi is Element of bool the carrier of L
"/\" ((Mg .: Xsi),L) is Element of the carrier of L
"/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
Mg . ("/\" (Xsi,(InclPoset (Filt (BoolePoset X))))) is Element of the carrier of L
u is set
x is set
Mg . x is set
x is Element of the carrier of (BoolePoset X)
uparrow x is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),x) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),x) is non empty upper Element of bool the carrier of (BoolePoset X)
Xsb is Element of X
{Xsb} is non empty set
G . x is set
x is Element of the carrier of (BoolePoset X)
uparrow x is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),x) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),x) is non empty upper Element of bool the carrier of (BoolePoset X)
Xsb is Element of X
{Xsb} is non empty set
x is Element of the carrier of (BoolePoset X)
uparrow x is non empty filtered upper Element of bool the carrier of (BoolePoset X)
K80( the carrier of (BoolePoset X),x) is non empty Element of bool the carrier of (BoolePoset X)
uparrow K80( the carrier of (BoolePoset X),x) is non empty upper Element of bool the carrier of (BoolePoset X)
G . (uparrow x) is set
x is Element of X
{x} is non empty set
Mg . (uparrow x) is set
x is Element of X
{x} is non empty set
"\/" ( { ("/\" ( { (uparrow b₂) where b₂ is Element of the carrier of (BoolePoset X) : ex b₃ being Element of X st
( b₂ = {b₃} & b₃ in b₁ ) } ,(InclPoset (Filt (BoolePoset X))))) where b₁ is Element of bool X : b₁ in FG } ,(InclPoset (Filt (BoolePoset X)))) is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))
g is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
g . GF is Element of the carrier of L
"\/" ((Mg .: Xs),L) is Element of the carrier of L
F is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of L -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L:]
F . GF is Element of the carrier of L
X is set
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
Filt (BoolePoset X) is non empty set
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
(X) is Element of bool (bool the carrier of (BoolePoset X))
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
Mg is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
the carrier of Mg is non empty set
[:(X), the carrier of Mg:] is Relation-like set
bool [:(X), the carrier of Mg:] is non empty set
the carrier of (InclPoset (Filt (BoolePoset X))) is non empty set
f is Relation-like (X) -defined the carrier of Mg -valued Function-like V27((X)) quasi_total Element of bool [:(X), the carrier of Mg:]
(X,Mg,f) is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of Mg -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total infs-preserving meet-preserving filtered-infs-preserving directed-sups-preserving Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of Mg:]
[: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of Mg:] is non empty Relation-like set
bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of Mg:] is non empty set
g is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of Mg -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total CLHomomorphism of InclPoset (Filt (BoolePoset X)),Mg
g | (X) is Relation-like (X) -defined the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of Mg -valued Function-like Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of Mg:]
Mg is non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of Mg -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X)))) quasi_total CLHomomorphism of InclPoset (Filt (BoolePoset X)),Mg
Mg | (X) is Relation-like (X) -defined the carrier of (InclPoset (Filt (BoolePoset X))) -defined the carrier of Mg -valued Function-like Element of bool [: the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of Mg:]
X is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
G is set
Mg is set
card G is cardinal set
card Mg is cardinal set
f is Relation-like Function-like set
dom f is set
rng f is set
f " is Relation-like Function-like set
dom (f ") is set
the carrier of L is non empty set
bool the carrier of L is non empty set
rng (f ") is set
the carrier of X is non empty set
bool the carrier of X is non empty set
Mg is Element of bool the carrier of L
Lg is Element of bool the carrier of X
[:Lg, the carrier of L:] is Relation-like set
bool [:Lg, the carrier of L:] is non empty set
f is Relation-like Lg -defined the carrier of L -valued Function-like V27(Lg) quasi_total Element of bool [:Lg, the carrier of L:]
F is non empty Relation-like the carrier of X -defined the carrier of L -valued Function-like V27( the carrier of X) quasi_total CLHomomorphism of X,L
F | Lg is Relation-like the carrier of X -defined Lg -defined the carrier of X -defined the carrier of L -valued Function-like Element of bool [: the carrier of X, the carrier of L:]
[: the carrier of X, the carrier of L:] is non empty Relation-like set
bool [: the carrier of X, the carrier of L:] is non empty set
[:Mg, the carrier of X:] is Relation-like set
bool [:Mg, the carrier of X:] is non empty set
g is Relation-like Mg -defined the carrier of X -valued Function-like V27(Mg) quasi_total Element of bool [:Mg, the carrier of X:]
G is non empty Relation-like the carrier of L -defined the carrier of X -valued Function-like V27( the carrier of L) quasi_total CLHomomorphism of L,X
G | Mg is Relation-like the carrier of L -defined Mg -defined the carrier of L -defined the carrier of X -valued Function-like Element of bool [: the carrier of L, the carrier of X:]
[: the carrier of L, the carrier of X:] is non empty Relation-like set
bool [: the carrier of L, the carrier of X:] is non empty set
G * F is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
GF is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total CLHomomorphism of X,X
GF | Lg is Relation-like the carrier of X -defined Lg -defined the carrier of X -defined the carrier of X -valued Function-like Element of bool [: the carrier of X, the carrier of X:]
G * f is Relation-like Lg -defined the carrier of X -valued Function-like V27(Lg) quasi_total Element of bool [:Lg, the carrier of X:]
[:Lg, the carrier of X:] is Relation-like set
bool [:Lg, the carrier of X:] is non empty set
g * f is Relation-like Lg -defined the carrier of X -valued Function-like Element of bool [:Lg, the carrier of X:]
id Lg is Relation-like Lg -defined Lg -valued Function-like one-to-one V27(Lg) quasi_total Element of bool [:Lg,Lg:]
[:Lg,Lg:] is Relation-like set
bool [:Lg,Lg:] is non empty set
id X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V27( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X:]
F * G is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
FG is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V27( the carrier of L) quasi_total CLHomomorphism of L,L
FG | Mg is Relation-like the carrier of L -defined Mg -defined the carrier of L -defined the carrier of L -valued Function-like Element of bool [: the carrier of L, the carrier of L:]
F * g is Relation-like Mg -defined the carrier of L -valued Function-like V27(Mg) quasi_total Element of bool [:Mg, the carrier of L:]
[:Mg, the carrier of L:] is Relation-like set
bool [:Mg, the carrier of L:] is non empty set
f * g is Relation-like Mg -defined the carrier of L -valued Function-like Element of bool [:Mg, the carrier of L:]
id Mg is Relation-like Mg -defined Mg -valued Function-like one-to-one V27(Mg) quasi_total Element of bool [:Mg,Mg:]
[:Mg,Mg:] is Relation-like set
bool [:Mg,Mg:] is non empty set
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of L:]
id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of L:]
rng F is non empty Element of bool the carrier of L
F " is Relation-like Function-like set
X is set
card X is cardinal set
BoolePoset X is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete RelStr
Filt (BoolePoset X) is non empty set
the carrier of (BoolePoset X) is non empty set
bool the carrier of (BoolePoset X) is non empty set
{ b₁ where b₁ is non empty filtered upper Element of bool the carrier of (BoolePoset X) : verum } is set
InclPoset (Filt (BoolePoset X)) is non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
(X) is Element of bool (bool the carrier of (BoolePoset X))
bool (bool the carrier of (BoolePoset X)) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of (BoolePoset X) : ex b₂ being Element of X st b₁ = {b₂} } is set
card (X) is cardinal set
L is non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete RelStr
G is set
card G is cardinal set