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

"/\" ( { ("/\" (b

{ b

Mg is set

f is Element of bool the carrier of X

f is Element of bool the carrier of X

{ ("/\" (b

"/\" ( { ("/\" (b

union { b

"/\" ((union { b

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

"\/" ( { ("\/" (b

{ b

Mg is set

f is Element of bool the carrier of X

f is Element of bool the carrier of X

{ ("\/" (b

"\/" ( { ("\/" (b

union { b

"\/" ((union { b

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

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

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

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

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

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

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

Filt (BoolePoset X) is non empty set

{ b

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

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

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

( b

"\/" ( { ("/\" ( { (uparrow b

( b

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

( b

"/\" ( { (uparrow b

( b

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

( b

"/\" ( { (uparrow b

( b

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

( b

"/\" ( { (uparrow b

( b

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

( b

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

( b

"/\" ( { (uparrow b

( b

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

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

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

( b

"\/" ( { ("/\" ( { (G . (uparrow b

( b

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

( b

"\/" ( { ("/\" ( { (G . (uparrow b

( b

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

( b

"\/" ( { ("/\" ( { (G . (uparrow b

( b

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

Filt (BoolePoset X) is non empty set

{ b

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

( b

{ ("/\" ( { (G . (uparrow b

( b

(X,L,G) . Mg is Element of the carrier of L

"\/" ( { ("/\" ( { (G . (uparrow b

( b

f is set

F is Element of bool X

{ (G . (uparrow b

( b

"/\" ( { (G . (uparrow b

( b

(X,L,G) . f is Element of the carrier of L

"\/" ( { ("/\" ( { (G . (uparrow b

( b

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

Filt (BoolePoset X) is non empty set

{ b

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

( b

Mg is Element of bool X

{ (G . (uparrow b

( b

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

( b

bool X is non empty Element of bool (bool X)

bool (bool X) is non empty set

"/\" ( { (G . (uparrow b

( b

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

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

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

( b

"\/" (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

( b

union g is set

g is set

G is Element of bool X

{ (G . (uparrow b

( b

"/\" ( { (G . (uparrow b

( b

GF is set

{ ("/\" ( { (G . (uparrow b

( b

union { { ("/\" ( { (G . (uparrow b

( b

G is set

GF is Element of Mg

{ ("/\" ( { (G . (uparrow b

( b

FG is Element of bool X

{ (G . (uparrow b

( b

"/\" ( { (G . (uparrow b

( b

bool the carrier of L is non empty set

{ ("\/" (b

( b

(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

( b

FG is set

Xsf is Element of bool X

{ (G . (uparrow b

( b

"/\" ( { (G . (uparrow b

( b

"\/" ((union { { ("/\" ( { (G . (uparrow b

( b

"\/" ( { ("\/" (b

( b

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

( b

Xs is set

s is Element of bool X

{ (G . (uparrow b

( b

"/\" ( { (G . (uparrow b

( b

Xs is Element of bool the carrier of L

(X,L,G) . Xsf is Element of the carrier of L

"\/" ( { ("/\" ( { (G . (uparrow b

( b

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

( b

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

( b

"\/" ( { ("/\" ( { (G . (uparrow b

( b

(X,L,G) . f is Element of the carrier of L

"\/" ( { ("/\" ( { (G . (uparrow b

( b

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

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

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

( b

"/\" ( { (G . (uparrow b

( b

g is non empty Element of bool the carrier of (InclPoset (Filt (BoolePoset X)))

{ ("/\" ( { (G . (uparrow b

( b

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

( b

"/\" ( { (G . (uparrow b

( b

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

( b

(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

( b

"/\" ( { (G . (uparrow b

( b

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

( b

"/\" ( { (G . (uparrow b

( b

Xs . Xs is set

meet g is set

FG is non empty Element of the carrier of (InclPoset (Filt (BoolePoset X)))

{ ("/\" ( { (G . (uparrow b

( b

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

( b

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

( b

"\/" ( { ("/\" ( { (G . (uparrow b

( b

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

( b

(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

( b

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 .