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