:: WAYBEL_7 semantic presentation

K291() is Element of bool K287()

K287() is set

bool K287() is non empty set

omega is set

bool omega is non empty set

bool K291() is non empty set

{} is empty Relation-like non-empty empty-yielding finite finite-yielding V35() set

the empty Relation-like non-empty empty-yielding finite finite-yielding V35() set is empty Relation-like non-empty empty-yielding finite finite-yielding V35() set

1 is non empty set

union {} is finite set

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr

a is set

x is set

"\/" (a,L) is Element of the carrier of L

the carrier of L is non empty set

"\/" (x,L) is Element of the carrier of L

"/\" (x,L) is Element of the carrier of L

"/\" (a,L) is Element of the carrier of L

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

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

bool L is non empty set

bool (bool L) is non empty set

InclPoset (bool L) is non empty strict reflexive transitive antisymmetric non void RelStr

RelIncl (bool L) is Relation-like V20( bool L) V75() V78() V82() Element of bool [:(bool L),(bool L):]

[:(bool L),(bool L):] is non empty Relation-like set

bool [:(bool L),(bool L):] is non empty set

RelStr(# (bool L),(RelIncl (bool L)) #) is strict RelStr

L is non empty antisymmetric lower-bounded upper-bounded bounded RelStr

Top L is Element of the carrier of L

the carrier of L is non empty set

"/\" ({},L) is Element of the carrier of L

Bottom L is Element of the carrier of L

"\/" ({},L) is Element of the carrier of L

a is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

P is Element of the carrier of L

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

L is non empty set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

Top (BoolePoset L) is Element of the carrier of (BoolePoset L)

the carrier of (BoolePoset L) is non empty set

"/\" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)

Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)

"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)

L is non empty reflexive transitive antisymmetric lower-bounded non void RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

"\/" ({},L) is Element of the carrier of L

a is non empty filtered upper Element of bool the carrier of L

x is set

y is Element of the carrier of L

{{}} is non empty finite V35() set

BoolePoset {{}} is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

L is non empty non trivial reflexive transitive antisymmetric upper-bounded non void RelStr

the carrier of L is non empty non trivial set

bool 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

uparrow (Top L) is non empty filtered upper Element of bool the carrier of L

{(Top L)} is non empty finite Element of bool the carrier of L

uparrow {(Top L)} is non empty upper Element of bool the carrier of L

a is non empty filtered upper Element of bool the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

a is Element of the carrier of (BoolePoset L)

'not' a is Element of the carrier of (BoolePoset L)

Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)

"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)

a => (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)

a => is Relation-like Function-like V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):]

[: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty Relation-like set

bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty set

(a =>) . (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)

L \ a is Element of bool L

bool L is non empty set

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

bool (bool L) is non empty set

x is Element of the carrier of (BoolePoset L)

a "/\" x is Element of the carrier of (BoolePoset L)

a /\ x is set

a "\/" x is Element of the carrier of (BoolePoset L)

a \/ x is set

Top (BoolePoset L) is Element of the carrier of (BoolePoset L)

"/\" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

bool the carrier of (BoolePoset L) is non empty set

a is Element of bool the carrier of (BoolePoset L)

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

bool L is non empty set

bool (bool L) is non empty set

x is set

y is set

P is Element of the carrier of (BoolePoset L)

p is Element of the carrier of (BoolePoset L)

x is Element of the carrier of (BoolePoset L)

y is Element of the carrier of (BoolePoset L)

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

bool the carrier of (BoolePoset L) is non empty set

a is Element of bool the carrier of (BoolePoset L)

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

bool L is non empty set

bool (bool L) is non empty set

x is set

y is set

P is Element of the carrier of (BoolePoset L)

p is Element of the carrier of (BoolePoset L)

x is Element of the carrier of (BoolePoset L)

y is Element of the carrier of (BoolePoset L)

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

bool the carrier of (BoolePoset L) is non empty set

a is lower Element of bool the carrier of (BoolePoset L)

x is set

y is set

P is Element of the carrier of (BoolePoset L)

p is Element of the carrier of (BoolePoset L)

P "\/" p is Element of the carrier of (BoolePoset L)

x \/ y is set

x is Element of the carrier of (BoolePoset L)

y is Element of the carrier of (BoolePoset L)

x \/ y is set

x "\/" y is Element of the carrier of (BoolePoset L)

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

bool the carrier of (BoolePoset L) is non empty set

a is upper Element of bool the carrier of (BoolePoset L)

x is set

y is set

P is Element of the carrier of (BoolePoset L)

p is Element of the carrier of (BoolePoset L)

P "/\" p is Element of the carrier of (BoolePoset L)

x /\ y is set

x is Element of the carrier of (BoolePoset L)

y is Element of the carrier of (BoolePoset L)

x /\ y is set

x "/\" y is Element of the carrier of (BoolePoset L)

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

bool the carrier of (BoolePoset L) is non empty set

bool L is non empty set

bool (bool L) is non empty set

a is non empty lower Element of bool the carrier of (BoolePoset L)

x is finite Element of bool (bool L)

bool a is non empty set

P is finite Element of bool a

y is Element of bool the carrier of (BoolePoset L)

"\/" (y,(BoolePoset L)) is Element of the carrier of (BoolePoset L)

Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)

"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)

union x is Element of bool L

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

x is finite Element of bool a

y is finite Element of bool (bool L)

P is finite Element of bool (bool L)

union P is Element of bool L

"\/" (x,(BoolePoset L)) is Element of the carrier of (BoolePoset L)

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

bool the carrier of (BoolePoset L) is non empty set

bool L is non empty set

bool (bool L) is non empty set

a is non empty upper Element of bool the carrier of (BoolePoset L)

Top (BoolePoset L) is Element of the carrier of (BoolePoset L)

"/\" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)

x is finite Element of bool (bool L)

bool a is non empty set

P is finite Element of bool a

y is Element of bool the carrier of (BoolePoset L)

"/\" (y,(BoolePoset L)) is Element of the carrier of (BoolePoset L)

meet y is set

Intersect x is Element of bool L

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

x is finite Element of bool a

y is finite Element of bool (bool L)

"/\" (x,(BoolePoset L)) is Element of the carrier of (BoolePoset L)

P is finite Element of bool (bool L)

meet P is Element of bool L

Intersect P is Element of bool L

L is non empty reflexive transitive antisymmetric non void with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is non empty reflexive transitive antisymmetric non void with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty directed lower Element of bool the carrier of L

x is non empty finite Element of bool the carrier of L

"/\" (x,L) is Element of the carrier of L

y is set

P is set

"/\" (P,L) is Element of the carrier of L

{y} is non empty finite set

P \/ {y} is non empty set

"/\" ((P \/ {y}),L) is Element of the carrier of L

p is Element of the carrier of L

{p} is non empty finite Element of bool the carrier of L

P \/ {p} is non empty set

"/\" ((P \/ {p}),L) is Element of the carrier of L

p is Element of the carrier of L

{p} is non empty finite Element of bool the carrier of L

"/\" ({p},L) is Element of the carrier of L

ax is finite Element of bool the carrier of L

"/\" (ax,L) is Element of the carrier of L

("/\" (ax,L)) "/\" ("/\" ({p},L)) is Element of the carrier of L

ay is Element of the carrier of L

ay is Element of the carrier of L

Y is Element of the carrier of L

ay is Element of the carrier of L

{ay} is non empty finite Element of bool the carrier of L

"/\" ({},L) is Element of the carrier of L

y is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

x "/\" y is Element of the carrier of L

{x,y} is non empty finite Element of bool the carrier of L

"/\" ({x,y},L) is Element of the carrier of L

P is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

a is Element of the carrier of L

x is Element of the carrier of L

a "/\" x is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is non empty Relation-like Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

a is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of a is non empty set

the InternalRel of a is non empty Relation-like Element of bool [: the carrier of a, the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty Relation-like set

bool [: the carrier of a, the carrier of a:] is non empty set

RelStr(# the carrier of a, the InternalRel of a #) is strict RelStr

bool the carrier of L is non empty set

bool the carrier of a is non empty set

x is set

y is non empty directed lower (L) Element of bool the carrier of L

P is Element of bool the carrier of a

p is non empty directed lower Element of bool the carrier of a

ax is Element of the carrier of a

ay is Element of the carrier of a

ax "/\" ay is Element of the carrier of a

{ax,ay} is non empty finite Element of bool the carrier of a

"/\" ({ax,ay},a) is Element of the carrier of a

Y is Element of the carrier of L

F is Element of the carrier of L

{Y,F} is non empty finite Element of bool the carrier of L

Y "/\" F is Element of the carrier of L

"/\" ({Y,F},L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is non empty reflexive transitive antisymmetric non void with_suprema RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty filtered upper Element of bool the carrier of L

x is non empty finite Element of bool the carrier of L

"\/" (x,L) is Element of the carrier of L

y is set

P is set

"\/" (P,L) is Element of the carrier of L

{y} is non empty finite set

P \/ {y} is non empty set

"\/" ((P \/ {y}),L) is Element of the carrier of L

p is Element of the carrier of L

{p} is non empty finite Element of bool the carrier of L

P \/ {p} is non empty set

"\/" ((P \/ {p}),L) is Element of the carrier of L

p is Element of the carrier of L

{p} is non empty finite Element of bool the carrier of L

"\/" ({p},L) is Element of the carrier of L

ax is finite Element of bool the carrier of L

"\/" (ax,L) is Element of the carrier of L

("\/" (ax,L)) "\/" ("\/" ({p},L)) is Element of the carrier of L

ay is Element of the carrier of L

ay is Element of the carrier of L

Y is Element of the carrier of L

ay is Element of the carrier of L

{ay} is non empty finite Element of bool the carrier of L

"\/" ({},L) is Element of the carrier of L

y is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

x "\/" y is Element of the carrier of L

{x,y} is non empty finite Element of bool the carrier of L

"\/" ({x,y},L) is Element of the carrier of L

P is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

a is Element of the carrier of L

x is Element of the carrier of L

a "\/" x is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

the InternalRel of L is non empty Relation-like Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

a is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of a is non empty set

the InternalRel of a is non empty Relation-like Element of bool [: the carrier of a, the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty Relation-like set

bool [: the carrier of a, the carrier of a:] is non empty set

RelStr(# the carrier of a, the InternalRel of a #) is strict RelStr

bool the carrier of L is non empty set

bool the carrier of a is non empty set

x is set

y is non empty filtered upper (L) Element of bool the carrier of L

P is Element of bool the carrier of a

p is non empty filtered upper Element of bool the carrier of a

ax is Element of the carrier of a

ay is Element of the carrier of a

ax "\/" ay is Element of the carrier of a

{ax,ay} is non empty finite Element of bool the carrier of a

"\/" ({ax,ay},a) is Element of the carrier of a

Y is Element of the carrier of L

F is Element of the carrier of L

{Y,F} is non empty finite Element of bool the carrier of L

Y "\/" F is Element of the carrier of L

"\/" ({Y,F},L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L ~ is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of (L ~) is non empty set

bool the carrier of (L ~) is non empty set

a is set

x is non empty directed lower (L) Element of bool the carrier of L

y is non empty filtered upper Element of bool the carrier of (L ~)

P is Element of the carrier of (L ~)

p is Element of the carrier of (L ~)

P "\/" p is Element of the carrier of (L ~)

~ P is Element of the carrier of L

~ p is Element of the carrier of L

(~ P) "/\" (~ p) is Element of the carrier of L

x is non empty filtered upper (L ~ ) Element of bool the carrier of (L ~)

y is non empty directed lower Element of bool the carrier of L

P is Element of the carrier of L

p is Element of the carrier of L

P "/\" p is Element of the carrier of L

P ~ is Element of the carrier of (L ~)

p ~ is Element of the carrier of (L ~)

(P ~) "\/" (p ~) is Element of the carrier of (L ~)

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L ~ is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of (L ~) is non empty set

bool the carrier of (L ~) is non empty set

a is set

(L ~) ~ is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the InternalRel of L is non empty Relation-like Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr

the carrier of ((L ~) ~) is non empty set

bool the carrier of ((L ~) ~) is non empty set

L is non empty reflexive transitive antisymmetric non void with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty directed lower Element of bool the carrier of L

a ` is Element of bool the carrier of L

the carrier of L \ a is set

y is Element of the carrier of L

P is Element of the carrier of L

y "/\" P is Element of the carrier of L

y is Element of the carrier of L

P is Element of the carrier of L

y is Element of the carrier of L

P is Element of the carrier of L

y "/\" P is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

Ids L is non empty set

{ b

InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

PRIME (InclPoset (Ids L)) is Element of bool the carrier of (InclPoset (Ids L))

the carrier of (InclPoset (Ids L)) is non empty set

bool the carrier of (InclPoset (Ids L)) is non empty set

a is non empty directed lower Element of bool the carrier of L

RelIncl (Ids L) is Relation-like V20( Ids L) V75() V78() V82() Element of bool [:(Ids L),(Ids L):]

[:(Ids L),(Ids L):] is non empty Relation-like set

bool [:(Ids L),(Ids L):] is non empty set

RelStr(# (Ids L),(RelIncl (Ids L)) #) is strict RelStr

y is Element of the carrier of (InclPoset (Ids L))

P is Element of the carrier of (InclPoset (Ids L))

p is Element of the carrier of (InclPoset (Ids L))

P "/\" p is Element of the carrier of (InclPoset (Ids L))

Y is non empty directed lower Element of bool the carrier of L

F is non empty directed lower Element of bool the carrier of L

P "/\" p is Element of the carrier of (InclPoset (Ids L))

ax is non empty directed lower Element of bool the carrier of L

ay is non empty directed lower Element of bool the carrier of L

ax /\ ay is Element of bool the carrier of L

Y is set

F is set

f is Element of the carrier of L

FF is Element of the carrier of L

f "/\" FF is Element of the carrier of L

P is Element of the carrier of L

p is Element of the carrier of L

P "/\" p is Element of the carrier of L

downarrow P is non empty directed lower Element of bool the carrier of L

{P} is non empty finite Element of bool the carrier of L

downarrow {P} is non empty lower Element of bool the carrier of L

downarrow p is non empty directed lower Element of bool the carrier of L

{p} is non empty finite Element of bool the carrier of L

downarrow {p} is non empty lower Element of bool the carrier of L

ax is non empty directed lower Element of bool the carrier of L

ay is non empty directed lower Element of bool the carrier of L

Y is Element of the carrier of (InclPoset (Ids L))

F is Element of the carrier of (InclPoset (Ids L))

Y /\ F is set

Y "/\" F is Element of the carrier of (InclPoset (Ids L))

f is set

FF is Element of the carrier of L

y is Element of the carrier of (InclPoset (Ids L))

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty filtered upper Element of bool the carrier of L

x is Element of the carrier of L

'not' x is Element of the carrier of L

Bottom L is Element of the carrier of L

"\/" ({},L) is Element of the carrier of L

x => (Bottom L) is Element of the carrier of L

x => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

(x =>) . (Bottom L) is Element of the carrier of L

x "\/" ('not' x) is Element of the carrier of L

Top L is Element of the carrier of L

"/\" ({},L) is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

x "\/" y is Element of the carrier of L

'not' x is Element of the carrier of L

x => (Bottom L) is Element of the carrier of L

x => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

(x =>) . (Bottom L) is Element of the carrier of L

'not' y is Element of the carrier of L

y => (Bottom L) is Element of the carrier of L

y => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

(y =>) . (Bottom L) is Element of the carrier of L

('not' x) "/\" ('not' y) is Element of the carrier of L

'not' (x "\/" y) is Element of the carrier of L

(x "\/" y) => (Bottom L) is Element of the carrier of L

(x "\/" y) => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

((x "\/" y) =>) . (Bottom L) is Element of the carrier of L

('not' (x "\/" y)) "/\" (x "\/" y) is Element of the carrier of L

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty set

bool the carrier of (BoolePoset L) is non empty set

bool L is non empty set

x is non empty filtered upper Element of bool the carrier of (BoolePoset L)

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

bool (bool L) is non empty set

InclPoset (bool L) is non empty strict reflexive transitive antisymmetric non void RelStr

RelIncl (bool L) is Relation-like V20( bool L) V75() V78() V82() Element of bool [:(bool L),(bool L):]

[:(bool L),(bool L):] is non empty Relation-like set

bool [:(bool L),(bool L):] is non empty set

RelStr(# (bool L),(RelIncl (bool L)) #) is strict RelStr

y is Element of bool L

P is Element of the carrier of (BoolePoset L)

'not' P is Element of the carrier of (BoolePoset L)

Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)

"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)

P => (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)

P => is Relation-like Function-like V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):]

[: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty Relation-like set

bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty set

(P =>) . (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)

L \ y is Element of bool L

y is Element of the carrier of (BoolePoset L)

'not' y is Element of the carrier of (BoolePoset L)

y => (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)

y => is Relation-like Function-like V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):]

(y =>) . (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)

L \ y is Element of bool L

L is non empty reflexive transitive antisymmetric non void RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is non empty reflexive transitive antisymmetric non void RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty filtered upper Element of bool the carrier of L

L is non empty reflexive transitive antisymmetric non void with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty filtered upper Element of bool the carrier of L

x is non empty finite Element of bool the carrier of L

a \/ x is non empty Element of bool the carrier of L

fininfs (a \/ x) is non empty filtered Element of bool the carrier of L

bool (a \/ x) is non empty set

{ ("/\" (b

uparrow (fininfs (a \/ x)) is non empty filtered upper Element of bool the carrier of L

"/\" (x,L) is Element of the carrier of L

y is Element of the carrier of L

the Element of a is Element of a

ax is Element of the carrier of L

ay is finite Element of bool (a \/ x)

"/\" (ay,L) is Element of the carrier of L

ay \ x is finite Element of bool (a \/ x)

Y is set

bool a is non empty set

Y is finite Element of bool a

F is finite Element of bool the carrier of L

F \/ x is non empty finite Element of bool the carrier of L

p is Element of the carrier of L

p "/\" ("/\" (x,L)) is Element of the carrier of L

"/\" (F,L) is Element of the carrier of L

("/\" (F,L)) "/\" ("/\" (x,L)) is Element of the carrier of L

FF is finite Element of bool the carrier of L

ay \/ x is non empty finite set

"/\" (FF,L) is Element of the carrier of L

f is finite Element of bool the carrier of L

"/\" (f,L) is Element of the carrier of L

"/\" ((F \/ x),L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty filtered upper Element of bool the carrier of L

x is non empty filtered upper Element of bool the carrier of L

y is set

P is Element of the carrier of L

'not' P is Element of the carrier of L

Bottom L is Element of the carrier of L

"\/" ({},L) is Element of the carrier of L

P => (Bottom L) is Element of the carrier of L

P => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

(P =>) . (Bottom L) is Element of the carrier of L

P "\/" ('not' P) is Element of the carrier of L

Top L is Element of the carrier of L

"/\" ({},L) is Element of the carrier of L

P "/\" ('not' P) is Element of the carrier of L

ax is set

ay is Element of the carrier of L

x is Element of the carrier of L

'not' x is Element of the carrier of L

Bottom L is Element of the carrier of L

"\/" ({},L) is Element of the carrier of L

x => (Bottom L) is Element of the carrier of L

x => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

(x =>) . (Bottom L) is Element of the carrier of L

{x} is non empty finite Element of bool the carrier of L

a \/ {x} is non empty Element of bool the carrier of L

fininfs (a \/ {x}) is non empty filtered Element of bool the carrier of L

bool (a \/ {x}) is non empty set

{ ("/\" (b

uparrow (fininfs (a \/ {x})) is non empty filtered upper Element of bool the carrier of L

"/\" ({x},L) is Element of the carrier of L

P is Element of the carrier of L

P "/\" ("/\" ({x},L)) is Element of the carrier of L

Top L is Element of the carrier of L

"/\" ({},L) is Element of the carrier of L

P "/\" (Top L) is Element of the carrier of L

x "\/" ('not' x) is Element of the carrier of L

P "/\" (x "\/" ('not' x)) is Element of the carrier of L

P "/\" x is Element of the carrier of L

P "/\" ('not' x) is Element of the carrier of L

(P "/\" x) "\/" (P "/\" ('not' x)) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty directed lower Element of bool the carrier of L

x is non empty finite Element of bool the carrier of L

a \/ x is non empty Element of bool the carrier of L

finsups (a \/ x) is non empty directed Element of bool the carrier of L

bool (a \/ x) is non empty set

{ ("\/" (b

downarrow (finsups (a \/ x)) is non empty directed lower Element of bool the carrier of L

"\/" (x,L) is Element of the carrier of L

y is Element of the carrier of L

the Element of a is Element of a

ax is Element of the carrier of L

ay is finite Element of bool (a \/ x)

"\/" (ay,L) is Element of the carrier of L

ay \ x is finite Element of bool (a \/ x)

Y is set

bool a is non empty set

Y is finite Element of bool a

F is finite Element of bool the carrier of L

F \/ x is non empty finite Element of bool the carrier of L

p is Element of the carrier of L

p "\/" ("\/" (x,L)) is Element of the carrier of L

"\/" (F,L) is Element of the carrier of L

("\/" (F,L)) "\/" ("\/" (x,L)) is Element of the carrier of L

FF is finite Element of bool the carrier of L

ay \/ x is non empty finite set

f is finite Element of bool the carrier of L

"\/" (f,L) is Element of the carrier of L

"\/" (FF,L) is Element of the carrier of L

"\/" ((F \/ x),L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty directed lower Element of bool the carrier of L

x is non empty filtered upper Element of bool the carrier of L

{ b

P is set

p is non empty directed lower Element of bool the carrier of L

P is set

bool the carrier of L is non empty Element of bool (bool the carrier of L)

bool (bool the carrier of L) is non empty set

p is set

ax is non empty directed lower Element of bool the carrier of L

ax is Element of bool the carrier of L

p is Element of bool (bool the carrier of L)

ay is non empty directed lower Element of bool the carrier of L

union p is Element of bool the carrier of L

the Element of P is Element of P

ax is lower Element of bool the carrier of L

Y is Element of bool the carrier of L

F is Element of bool the carrier of L

Y \/ F is Element of bool the carrier of L

ay is Element of bool the carrier of L

Y is non empty directed lower Element of bool the carrier of L

Y is set

ay is non empty directed lower Element of bool the carrier of L

F is set

union P is set

P is set

p is non empty directed lower Element of bool the carrier of L

ax is Element of the carrier of L

ay is Element of the carrier of L

ax "/\" ay is Element of the carrier of L

{ay} is non empty finite Element of bool the carrier of L

p \/ {ay} is non empty Element of bool the carrier of L

finsups (p \/ {ay}) is non empty directed Element of bool the carrier of L

bool (p \/ {ay}) is non empty set

{ ("\/" (b

downarrow (finsups (p \/ {ay})) is non empty directed lower Element of bool the carrier of L

F is set

{ax} is non empty finite Element of bool the carrier of L

p \/ {ax} is non empty Element of bool the carrier of L

finsups (p \/ {ax}) is non empty directed Element of bool the carrier of L

bool (p \/ {ax}) is non empty set

{ ("\/" (b

downarrow (finsups (p \/ {ax})) is non empty directed lower Element of bool the carrier of L

FF is set

G is Element of the carrier of L

"\/" ({ax},L) is Element of the carrier of L

g is Element of the carrier of L

g "\/" ("\/" ({ax},L)) is Element of the carrier of L

gg is Element of the carrier of L

"\/" ({ay},L) is Element of the carrier of L

GG is Element of the carrier of L

GG "\/" ("\/" ({ay},L)) is Element of the carrier of L

g "\/" GG is Element of the carrier of L

GG "\/" g is Element of the carrier of L

(GG "\/" g) "\/" ax is Element of the carrier of L

g "\/" ax is Element of the carrier of L

GG "\/" (g "\/" ax) is Element of the carrier of L

(g "\/" GG) "\/" ax is Element of the carrier of L

(g "\/" GG) "\/" ay is Element of the carrier of L

GG "\/" ay is Element of the carrier of L

g "\/" (GG "\/" ay) is Element of the carrier of L

((g "\/" GG) "\/" ax) "/\" ((g "\/" GG) "\/" ay) is Element of the carrier of L

(g "\/" GG) "\/" (ax "/\" ay) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty directed lower Element of bool the carrier of L

x is Element of the carrier of L

y is set

uparrow x is non empty filtered upper Element of bool the carrier of L

{x} is non empty finite Element of bool the carrier of L

uparrow {x} is non empty upper Element of bool the carrier of L

P is Element of the carrier of L

y is non empty directed lower Element of bool the carrier of L

L is non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is non empty directed lower Element of bool the carrier of L

x is non empty filtered upper Element of bool the carrier of L

L ~ is non empty strict reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr

the carrier of (L ~) is non empty set

bool the carrier of (L ~) is non empty set

y is non empty directed lower Element of bool the carrier of (L ~)

P is non empty filtered upper Element of bool the carrier of (L ~)

p is non empty directed lower Element of bool the carrier of (L ~)

ax is non empty filtered upper Element of bool the carrier of L

L is non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima RelStr

the carrier of L is non empty non trivial set

bool the carrier of L is non empty set

a is non empty proper filtered upper Element of bool the carrier of L

Bottom L is Element of the carrier of L

"\/" ({},L) is Element of the carrier of L

downarrow (Bottom L) is non empty directed lower Element of bool the carrier of L

{(Bottom L)} is non empty finite Element of bool the carrier of L

downarrow {(Bottom L)} is non empty lower Element of bool the carrier of L

y is set

x is non empty directed lower Element of bool the carrier of L

y is non empty filtered upper Element of bool the carrier of L

L is non empty set

BoolePoset L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset L) is non empty non trivial set

bool the carrier of (BoolePoset L) is non empty set

the non empty proper filtered upper Element of bool the carrier of (BoolePoset L) is non empty proper filtered upper Element of bool the carrier of (BoolePoset L)

x is non empty filtered upper Element of bool the carrier of (BoolePoset L)

L is non empty TopSpace-like TopStruct

the carrier of L is non empty set

BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset the carrier of L) is non empty non trivial set

bool the carrier of (BoolePoset the carrier of L) is non empty set

x is non empty proper filtered upper ( BoolePoset the carrier of L) Element of bool the carrier of (BoolePoset the carrier of L)

y is set

bool the carrier of L is non empty set

P is Element of bool the carrier of L

the carrier of L \ P is Element of bool the carrier of L

bool the carrier of L is non empty set

P is Element of bool the carrier of L

Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)

"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)

p is set

ax is Element of the carrier of (BoolePoset the carrier of L)

ay is Element of the carrier of (BoolePoset the carrier of L)

ax "/\" ay is Element of the carrier of (BoolePoset the carrier of L)

P /\ p is Element of bool the carrier of L

L is non empty TopSpace-like TopStruct

the topology of L is non empty Element of bool (bool the carrier of L)

the carrier of L is non empty set

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr

the carrier of (InclPoset the topology of L) is non empty non trivial set

BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset the carrier of L) is non empty non trivial set

bool the carrier of (BoolePoset the carrier of L) is non empty set

y is Element of the carrier of (InclPoset the topology of L)

P is Element of the carrier of (InclPoset the topology of L)

bool the carrier of L is non empty Element of bool (bool the carrier of L)

InclPoset (bool the carrier of L) is non empty strict reflexive transitive antisymmetric non void RelStr

RelIncl (bool the carrier of L) is Relation-like V20( bool the carrier of L) V75() V78() V82() Element of bool [:(bool the carrier of L),(bool the carrier of L):]

[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set

bool [:(bool the carrier of L),(bool the carrier of L):] is non empty set

RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) is strict RelStr

RelIncl the topology of L is Relation-like V20( the topology of L) V75() V78() V82() Element of bool [: the topology of L, the topology of L:]

[: the topology of L, the topology of L:] is non empty Relation-like set

bool [: the topology of L, the topology of L:] is non empty set

RelStr(# the topology of L,(RelIncl the topology of L) #) is strict RelStr

ax is non empty proper filtered upper Element of bool the carrier of (BoolePoset the carrier of L)

{ b

( b

Y is set

F is Element of bool the carrier of L

f is set

Y is Element of bool (bool the carrier of L)

F is Element of bool (bool the carrier of L)

union F is Element of bool the carrier of L

f is set

FF is Element of bool the carrier of L

G is set

f is Element of bool the carrier of L

FF is Element of bool the carrier of L

G is set

bool F is non empty set

f is finite Element of bool F

union f is set

FF is set

G is Element of bool the carrier of L

gg is set

FF is Relation-like Function-like set

dom FF is set

rng FF is set

G is Element of the carrier of (BoolePoset the carrier of L)

p is Element of the carrier of (BoolePoset the carrier of L)

p "/\" G is Element of the carrier of (BoolePoset the carrier of L)

the Element of p "/\" G is Element of p "/\" G

Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)

"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)

p /\ G is set

g is set

FF . g is set

GG is Element of the carrier of (BoolePoset the carrier of L)

L is non empty TopSpace-like TopStruct

the topology of L is non empty Element of bool (bool the carrier of L)

the carrier of L is non empty set

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr

the carrier of (InclPoset the topology of L) is non empty non trivial set

BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset the carrier of L) is non empty non trivial set

bool the carrier of (BoolePoset the carrier of L) is non empty set

a is Element of the carrier of (InclPoset the topology of L)

x is Element of the carrier of (InclPoset the topology of L)

y is non empty proper filtered upper ( BoolePoset the carrier of L) Element of bool the carrier of (BoolePoset the carrier of L)

P is Element of the carrier of L

L is non empty TopSpace-like TopStruct

the topology of L is non empty Element of bool (bool the carrier of L)

the carrier of L is non empty set

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr

the carrier of (InclPoset the topology of L) is non empty non trivial set

BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

the carrier of (BoolePoset the carrier of L) is non empty non trivial set

bool the carrier of (BoolePoset the carrier of L) is non empty set

x is Element of the carrier of (InclPoset the topology of L)

y is Element of the carrier of (InclPoset the topology of L)

RelIncl the topology of L is Relation-like V20( the topology of L) V75() V78() V82() Element of bool [: the topology of L, the topology of L:]

[: the topology of L, the topology of L:] is non empty Relation-like set

bool [: the topology of L, the topology of L:] is non empty set

RelStr(# the topology of L,(RelIncl the topology of L) #) is strict RelStr

P is Element of bool the carrier of L

ax is Element of bool (bool the carrier of L)

union ax is Element of bool the carrier of L

bool ax is non empty set

{ (x \ b

the Element of ax is Element of ax

bool the carrier of L is non empty Element of bool (bool the carrier of L)

InclPoset (bool the carrier of L) is non empty strict reflexive transitive antisymmetric non void RelStr

RelIncl (bool the carrier of L) is Relation-like V20( bool the carrier of L) V75() V78() V82() Element of bool [:(bool the carrier of L),(bool the carrier of L):]

[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set

bool [:(bool the carrier of L),(bool the carrier of L):] is non empty set

RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) is strict RelStr

F is set

p is Element of bool the carrier of L

f is Element of bool the carrier of L

x \ f is Element of bool x

bool x is non empty set

F is Element of bool the carrier of (BoolePoset the carrier of L)

fininfs F is non empty filtered Element of bool the carrier of (BoolePoset the carrier of L)

bool F is non empty set

{ ("/\" (b

uparrow (fininfs F) is non empty filtered upper Element of bool the carrier of (BoolePoset the carrier of L)

Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)

"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)

FF is Element of the carrier of (BoolePoset the carrier of L)

G is finite Element of bool F

"/\" (G,(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)

g is set

GG is Element of bool the carrier of L

x \ GG is Element of bool x

bool x is non empty set

g is Relation-like Function-like set

dom g is set

rng g is set

Top (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)

"/\" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)

gg is Element of bool the carrier of (BoolePoset the carrier of L)

meet gg is set

GG is finite Element of bool ax

union GG is set

a is set

z is set

g . z is set

x \ (g . z) is Element of bool x

bool x is non empty set

FF is non empty filtered upper Element of bool the carrier of (BoolePoset the carrier of L)

G is Element of bool the carrier of L

x \ G is Element of bool x

bool x is non empty set

p is Element of bool the carrier of L

gg is Element of the carrier of L

g is set

GG is Element of bool the carrier of L

x \ GG is Element of bool x

GG /\ (x \ GG) is Element of bool x

L is non empty TopSpace-like TopStruct

the carrier of L is non empty set

bool the carrier of L is non empty set

bool (bool the carrier of L) is non empty set

the topology of L is non empty Element of bool (bool the carrier of L)

InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr

the carrier of (InclPoset the topology of L) is non empty non trivial set

a is open quasi_prebasis Element of bool (bool the carrier of L)

bool a is non empty set

FinMeetCl a is Element of bool (bool the carrier of L)

x is open quasi_basis Element of bool (bool the carrier of L)

BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr

p is Element of the carrier of (InclPoset the topology of L)

ax is Element of the carrier of (InclPoset the topology of L)

ay is Element of bool a

union ay is set

Y is Element of bool (bool the carrier of L)

F is Element of bool the carrier of L

bool ay is non empty set

bool the carrier of L is non empty Element of bool (bool the carrier of L)

InclPoset (bool the carrier of L) is non empty strict reflexive transitive antisymmetric non void RelStr

RelIncl (bool the carrier of L) is Relation-like V20( bool the carrier of L) V75() V78() V82() Element of bool [:(bool the carrier of L),(bool the carrier of L):]

[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set

bool [:(bool the carrier of L),(bool the carrier of L):] is non empty set

RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) is strict RelStr

RelIncl the topology of L is Relation-like V20( the topology of L) V75() V78() V82() Element of bool [: the topology of L, the topology of L:]

[: the topology of L, the topology of L:] is non empty Relation-like set

bool [: the topology of L, the topology of L:] is non empty set

RelStr(# the topology of L,(RelIncl the topology of L) #) is strict RelStr

UniCl x is Element of bool (bool the carrier of L)

bool p is non empty set

the carrier of (BoolePoset the carrier of L) is non empty non trivial set

bool the carrier of (BoolePoset the carrier of L) is non empty set

F is non empty proper filtered upper ( BoolePoset the carrier of L) Element of bool the carrier of (BoolePoset the carrier of L)

f is set

Y is Element of bool the carrier of L

FF is Element of the carrier of L

G is Element of bool the carrier of L

gg is Element of bool (bool the carrier of L)

union gg is Element of bool the carrier of L

g is set

GG is Element of bool the carrier of L

a is Element of bool (bool the carrier of L)

Intersect a is Element of bool the carrier of L

bool F is non empty set

z is set

r is set

f is Relation-like Function-like set

dom f is set

rng f is set

FF is Element of bool a

union FF is set

G is set

f . G is set

bool FF is non empty set

G is finite Element of bool FF

union G is set

the Element of G is Element of G

g is Relation-like Function-like set

dom g is set

rng g is set

GG is set

a is set

g . a is set

z is Element of bool the carrier of L

r is set

f . r is set

the carrier of L \ z is Element of bool the carrier of L

p \ z is Element of bool p

ay is Element of bool the carrier of L

z ` is Element of bool the carrier of L

the carrier of L \ z is set

ay /\ (z `) is Element of bool the carrier of L

p /\ ( the carrier of L \ z) is Element of bool the carrier of L

Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)

"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)

a is set

GG is finite Element of bool (bool the carrier of L)

Intersect GG is Element of bool the carrier of L

z is set

g . z is set

p \ z is Element of bool p

z is set

g . the Element of G is set

p \ the Element of G is Element of bool p

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is Element of the carrier of L

x is Element of the carrier of L

y is non empty directed lower (L) Element of bool the carrier of L

"\/" (y,L) is Element of the carrier of L

y is non empty directed lower Element of bool the carrier of L

"\/" (y,L) is Element of the carrier of L

P is non empty directed lower Element of bool the carrier of L

"\/" (P,L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

a is Element of the carrier of L

downarrow a is non empty directed lower Element of bool the carrier of L

bool the carrier of L is non empty set

{a} is non empty finite Element of bool the carrier of L

downarrow {a} is non empty lower Element of bool the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

x "/\" y is Element of the carrier of L

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of L is non empty set

a is Element of the carrier of L

downarrow a is non empty directed lower Element of bool the carrier of L

bool the carrier of L is non empty set

{a} is non empty finite Element of bool the carrier of L

downarrow {a} is non empty lower Element of bool the carrier of L

"\/" ((downarrow a),L) is Element of the carrier of L

L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is Element of the carrier of L

x is non empty directed lower (L) Element of bool the carrier of L

"\/" (x,L) is Element of the carrier of L

y is non empty finite Element of bool the carrier of L

"/\" (y,L) is Element of the carrier of L

waybelow a is non empty directed lower Element of bool the carrier of L

{ b

P is Element of the carrier of L

L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr

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

bool the carrier of L is non empty set

a is Element of the carrier of L

downarrow a is non empty directed lower Element of bool the carrier of L

{a} is non empty finite Element of bool the carrier of L

downarrow {a} is non empty lower Element of bool the carrier of L

(downarrow a) ` is Element of bool the carrier of L

the carrier of L \ (downarrow a) is set

fininfs ((downarrow a) `) is non empty filtered Element of bool the carrier of L

bool ((downarrow a) `) is non empty set

{ ("/\" (b

uparrow (fininfs ((downarrow a) `)) is non empty filtered upper Element of bool the carrier of L

waybelow a is non empty directed lower Element of bool the carrier of L

{ b

x is set

y is Element of the carrier of L

P is Element of the carrier of L

p is finite Element of bool ((downarrow a) `)

"/\" (p,L) is Element of the carrier of L

ax is finite Element of bool the carrier of L

ay is Element of the carrier of L

(downarrow a) /\ ((downarrow a) `) is Element of bool the carrier of L

ax is finite Element of bool the carrier of L

ax is finite Element of bool the carrier of L

L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr

Top L is Element of the carrier of L

the carrier of L is non empty set

"/\" ({},L) is Element of the carrier of L

bool the carrier of L is non empty set

downarrow (Top L) is non empty directed lower Element of bool the carrier of L

{(Top L)} is non empty finite Element of bool the carrier of L

downarrow {(Top L)} is non empty lower Element of bool the carrier of L

(downarrow (Top L)) ` is Element of bool the carrier of L

the carrier of L \ (downarrow (Top L)) is set

fininfs ((downarrow (Top L)) `) is non empty filtered Element of bool the carrier of L

bool ((downarrow (Top L)) `) is non empty set

{ ("/\" (b

uparrow (fininfs ((downarrow (Top L)) `)) is non empty filtered upper Element of bool the carrier of L

waybelow (Top L) is non empty directed lower Element of bool the carrier of L

{ b

a is Element of the carrier of L

a is non empty finite Element of bool the carrier of L

"/\" (a,L) is Element of the carrier of L

the Element of a is Element of a

y is Element of the carrier of L

P is Element of the carrier of L

a is Element of the carrier of L

L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

a is Element of the carrier of L

downarrow a is non empty directed lower Element of bool the carrier of L

{a} is non empty finite Element of bool the carrier of L

downarrow {a} is non empty lower Element of bool the carrier of L

(downarrow a) ` is Element of bool the carrier of L

the carrier of L \ (downarrow a) is set

fininfs ((downarrow a) `) is non empty filtered Element of bool the carrier of L

bool ((downarrow a) `) is non empty set

{ ("/\" (b

uparrow (fininfs ((downarrow a) `)) is non empty filtered upper Element of bool the carrier of L

waybelow a is non empty directed lower Element of bool the carrier of L

{ b

x is non empty finite Element of bool the carrier of L

"/\" (x,L) is Element of the carrier of L

y is set

P is Element of the carrier of L

L is non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

a is Element of the carrier of L

downarrow a is non empty directed lower Element of bool the carrier of L

bool the carrier of L is non empty set

{a} is non empty finite Element of bool the carrier of L

downarrow {a} is non empty lower Element of bool the carrier of L

(downarrow a) ` is Element of bool the carrier of L

the carrier of L \ (downarrow a) is set

fininfs ((downarrow a) `) is non empty filtered Element of bool the carrier of L

bool ((downarrow a) `) is non empty set

{ ("/\" (b

uparrow (fininfs ((downarrow a) `)) is non empty filtered upper Element of bool the carrier of L

waybelow a is non empty directed lower Element of bool the carrier of L

{ b

"\/" ((downarrow a),L) is Element of the carrier of L

(uparrow (fininfs ((downarrow a) `))) ` is Element of bool the carrier of L

the carrier of L \ (uparrow (fininfs ((downarrow a) `))) is set

((downarrow a) `) ` is Element of bool the carrier of L

the carrier of L \ ((downarrow a) `) is set

P is non empty directed lower Element of bool the carrier of L

p is non empty directed lower (L) Element of bool the carrier of L

"\/" ((waybelow a),L) is Element of the carrier of L

"\/" (p,L) is Element of the carrier of L

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

x is Element of the carrier of L

a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]

a -above x is Element of bool the carrier of L

bool the carrier of L is non empty set

y is Element of the carrier of L

P is Element of the carrier of L

[x,y] is Element of the carrier of [:L,L:]

[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema RelStr

the carrier of [:L,L:] is non empty set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V35() set

[x,P] is Element of the carrier of [:L,L:]

{x,P} is non empty finite set

{{x,P},{x}} is non empty finite V35() set

L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]

x is Element of the carrier of L

a -above x is upper Element of bool the carrier of L

bool the carrier of L is non empty set

y is Element of the carrier of L

P is Element of the carrier of L

[x,y] is Element of the carrier of [:L,L:]

[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of [:L,L:] is non empty set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V35() set

[x,P] is Element of the carrier of [:L,L:]

{x,P} is non empty finite set

{{x,P},{x}} is non empty finite V35() set

y "/\" P is Element of the carrier of L

[x,(y "/\" P)] is Element of the carrier of [:L,L:]

{x,(y "/\" P)} is non empty finite set

{{x,(y "/\" P)},{x}} is non empty finite V35() set

x is Element of the carrier of L

y is Element of the carrier of L

[x,y] is Element of the carrier of [:L,L:]

[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of [:L,L:] is non empty set

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V35() set

P is Element of the carrier of L

[x,P] is Element of the carrier of [:L,L:]

{x,P} is non empty finite set

{{x,P},{x}} is non empty finite V35() set

y "/\" P is Element of the carrier of L

[x,(y "/\" P)] is Element of the carrier of [:L,L:]

{x,(y "/\" P)} is non empty finite set

{{x,(y "/\" P)},{x}} is non empty finite V35() set

a -above x is upper Element of bool the carrier of L

y "/\" P is Element of the carrier of L

[x,(y "/\" P)] is Element of the carrier of [:L,L:]

{x,(y "/\" P)} is non empty finite set

{{x,(y "/\" P)},{x}} is non empty finite V35() set

L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]

x is Element of the carrier of L

P is Element of the carrier of L

[x,P] is Element of the carrier of [:L,L:]

[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

the carrier of [:L,L:] is non empty set

{x,P} is non empty finite set

{x} is non empty finite set

{{x,P},{x}} is non empty finite V35() set

y is Element of the carrier of L

p is Element of the carrier of L

[y,p] is Element of the carrier of [:L,L:]

{y,p} is non empty finite set

{y} is non empty finite set

{{y,p},{y}} is non empty finite V35() set

x "/\" y is Element of the carrier of L

[(x "/\" y),p] is Element of the carrier of [:L,L:]

{(x "/\" y),p} is non empty finite set

{(x "/\" y)} is non empty finite set

{{(x "/\" y),p},{(x "/\" y)}} is non empty finite V35() set

[(x "/\" y),P] is Element of the carrier of [:L,L:]

{(x "/\" y),P} is non empty finite set

{{(x "/\" y),P},{(x "/\" y)}} is non empty finite V35() set

P "/\" p is Element of the carrier of L

[(x "/\" y),(P "/\" p)] is Element of the carrier of [:L,L:]

{(x "/\" y),(P "/\" p)} is non empty finite set

{{(x "/\" y),(P "/\" p)},{(x "/\" y)}} is non empty finite V35() set

x is Element of the carrier of L

x "/\" x is Element of the carrier of L

y is Element of the carrier of L

[x,y] is Element of the carrier of [:L,L:]

{x,y} is non empty finite set

{x} is non empty finite set

{{x,y},{x}} is non empty finite V35() set

P is Element of the carrier of L

[x,P] is Element of the carrier of [:L,L:]

{x,P} is non empty finite set

{{x,P},{x}} is non empty finite V35() set

y "/\" P is Element of the carrier of L

[x,(y "/\" P)] is Element of the carrier of [:L,L:]

{x,(y "/\" P)} is non empty finite set

{{x,(y "/\" P)},{x}} is non empty finite V35() set

L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

bool [: the carrier of L, the carrier of L:] is non empty set

[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr

a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]

the carrier of [:L,L:] is non empty set

bool the carrier of [:L,L:] is non empty set

x is Element of bool the carrier of [:L,L:]

subrelstr x is strict reflexive transitive antisymmetric full SubRelStr of [:L,L:]

the carrier of (subrelstr x) is set

y is reflexive transitive antisymmetric full SubRelStr of [:L,L:]

the carrier of y is set

P is Element of the carrier of [:L,L:]

p is Element of the carrier of [:L,L:]

{P,p} is non empty finite Element of bool the carrier of [:L,L:]

"/\" ({P,p},[:L,L:]) is Element of the carrier of [:L,L:]

P `1 is Element of the carrier of L

P `2 is Element of the carrier of L

[(P `1),(P `2)] is Element of the carrier of [:L,L:]

{(P `1),(P `2)} is non empty finite set

{(P `1)} is non empty finite set

{{(P `1),(P `2)},{(P `1)}} is non empty finite V35() set

p `1 is Element of the carrier of L

p `2 is Element of the carrier of L

[(p `1),(p `2)] is Element of the carrier of [:L,L:]

{(p `1),(p `2)} is non empty finite set

{(p `1)} is non empty finite set

{{(p `1),(p `2)},{(p `1)}} is non empty finite V35() set

proj1 {P,p} is Element of bool the carrier of L

bool the carrier of L is non empty set

"/\" ((proj1 {P,p}),L) is Element of the carrier of L

proj2 {P,p} is Element of bool the carrier of L

"/\" ((proj2 {P,p}),L) is Element of the carrier of L

[("/\" ((proj1 {P,p}),L)),("/\" ((proj2 {P,p}),L))] is Element of the carrier of [:L,L:]

{("/\" ((proj1 {P,p}),L)),("/\" ((proj2 {P,p}),L))} is non empty finite set

{("/\" ((proj1 {P,p}),L))} is non empty finite set

{{("/\" ((proj1 {P,p}),L)),("/\" ((proj2 {P,p}),L))},{("/\" ((proj1 {P,p}),L))}} is non empty finite V35() set

{(P `1),(p `1)} is non empty finite Element of bool the carrier of L

"/\" ({(P `1),(p `1)},L) is Element of the carrier of L

[("/\" ({(P `1),(p `1)},L)),("/\" ((proj2 {P,p}),L))] is Element of the carrier of [:L,L:]

{("/\" ({(P `1),(p `1)},L)),("/\" ((proj2 {P,p}),L))} is non empty finite set

{("/\" ({(P `1),(p `1)},L))} is non empty finite set

{{("/\" ({(P `1),(p `1)},L)),("/\" ((proj2 {P,p}),L))},{("/\" ({(P `1),(p `1)},L))}} is non empty finite V35() set

{(P `2),(p `2)} is non empty finite Element of bool the carrier of L

"/\" ({(P `2),(p `2)