:: WAYBEL16 semantic presentation

K165() is Element of K32(K161())

K161() is set

K32(K161()) is non empty set

K113() is set

K32(K113()) is non empty set

{} is empty finite V35() set

the empty finite V35() set is empty finite V35() set

1 is non empty set

{{},1} is non empty finite set

K32(K165()) is non empty set

L is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

p is Element of the carrier of L

uparrow p is non empty filtered upper Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

(uparrow p) /\ (uparrow A) is Element of K32( the carrier of L)

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

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

uparrow (p "\/" A) is non empty filtered upper Element of K32( the carrier of L)

L is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

p is Element of the carrier of L

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

K32( 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 K32( the carrier of L)

(downarrow p) /\ (downarrow A) is Element of K32( the carrier of L)

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

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

downarrow (p "/\" A) is non empty directed lower Element of K32( the carrier of L)

L is non empty RelStr

the carrier of L is non empty set

A is Element of the carrier of L

uparrow A is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

the carrier of L \ (uparrow A) is Element of K32( the carrier of L)

p is Element of the carrier of L

uparrow p is Element of K32( the carrier of L)

{p} is non empty finite Element of K32( the carrier of L)

(uparrow p) \ {p} is Element of K32( the carrier of L)

(uparrow p) /\ (uparrow A) is Element of K32( the carrier of L)

x is set

k is Element of the carrier of L

x is set

k is Element of the carrier of L

L is non empty RelStr

the carrier of L is non empty set

A is Element of the carrier of L

downarrow A is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

the carrier of L \ (downarrow A) is Element of K32( the carrier of L)

p is Element of the carrier of L

downarrow p is Element of K32( the carrier of L)

{p} is non empty finite Element of K32( the carrier of L)

(downarrow p) \ {p} is Element of K32( the carrier of L)

(downarrow p) /\ (downarrow A) is Element of K32( the carrier of L)

x is set

k is Element of the carrier of L

x is set

k is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

L ~ is non empty strict reflexive transitive antisymmetric with_infima RelStr

the carrier of (L ~) is non empty set

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

p is Element of K32( the carrier of L)

A is Element of K32( the carrier of L)

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

x is Element of K32( the carrier of (L ~))

k is Element of K32( the carrier of (L ~))

x "/\" k is Element of K32( the carrier of (L ~))

c

{ (b

y is Element of the carrier of L

x is Element of the carrier of L

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

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

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

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

{ (b

c

{ (b

y is Element of the carrier of (L ~)

x is Element of the carrier of (L ~)

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

~ y is Element of the carrier of L

~ x is Element of the carrier of L

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

{ (b

L is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

L ~ is non empty strict reflexive transitive antisymmetric with_suprema RelStr

the carrier of (L ~) is non empty set

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

p is Element of K32( the carrier of L)

A is Element of K32( the carrier of L)

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

x is Element of K32( the carrier of (L ~))

k is Element of K32( the carrier of (L ~))

x "\/" k is Element of K32( the carrier of (L ~))

c

{ (b

y is Element of the carrier of L

x is Element of the carrier of L

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

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

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

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

{ (b

c

{ (b

y is Element of the carrier of (L ~)

x is Element of the carrier of (L ~)

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

~ y is Element of the carrier of L

~ x is Element of the carrier of L

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

{ (b

L is non empty reflexive transitive RelStr

Filt L is set

L ~ is non empty strict reflexive transitive RelStr

Ids (L ~) is non empty set

p is set

the carrier of (L ~) is non empty set

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

{ b

A is non empty directed lower Element of K32( the carrier of (L ~))

the carrier of L is non empty set

K32( the carrier of L) is non empty set

{ b

p is set

the carrier of L is non empty set

K32( the carrier of L) is non empty set

{ b

A is non empty filtered upper Element of K32( the carrier of L)

the carrier of (L ~) is non empty set

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

{ b

L is non empty reflexive transitive RelStr

Ids L is non empty set

L ~ is non empty strict reflexive transitive RelStr

Filt (L ~) is set

p is set

the carrier of (L ~) is non empty set

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

{ b

A is non empty filtered upper Element of K32( the carrier of (L ~))

the carrier of L is non empty set

K32( the carrier of L) is non empty set

{ b

p is set

the carrier of L is non empty set

K32( the carrier of L) is non empty set

{ b

A is non empty directed lower Element of K32( the carrier of L)

the carrier of (L ~) is non empty set

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

{ b

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

the carrier of L is non empty set

p is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of p is non empty set

K33( the carrier of L, the carrier of p) is non empty set

K32(K33( the carrier of L, the carrier of p)) is non empty set

Top p is Element of the carrier of p

the carrier of L --> (Top p) is V7() V10( the carrier of L) V11( the carrier of p) V12() V18( the carrier of L, the carrier of p) Element of K32(K33( the carrier of L, the carrier of p))

A is V7() V10( the carrier of L) V11( the carrier of p) V12() V18( the carrier of L, the carrier of p) Element of K32(K33( the carrier of L, the carrier of p))

x is V7() V10( the carrier of L) V11( the carrier of p) V12() V18( the carrier of L, the carrier of p) Element of K32(K33( the carrier of L, the carrier of p))

K32( the carrier of L) is non empty set

k is Element of K32( the carrier of L)

rng x is Element of K32( the carrier of p)

K32( the carrier of p) is non empty set

{(Top p)} is non empty finite Element of K32( the carrier of p)

x .: k is Element of K32( the carrier of p)

c

y is Element of the carrier of L

x . c

x . y is Element of the carrier of p

"\/" ((x .: k),p) is Element of the carrier of p

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

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

k is Element of K32( the carrier of L)

x .: k is Element of K32( the carrier of p)

K32({(Top p)}) is non empty finite V35() set

"/\" ((x .: k),p) is Element of the carrier of p

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

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

"/\" ((x .: k),p) is Element of the carrier of p

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

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

"/\" ((x .: k),p) is Element of the carrier of p

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

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

"/\" ((x .: k),p) is Element of the carrier of p

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

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

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

L is non empty reflexive transitive antisymmetric upper-bounded RelStr

Filt L is set

the carrier of L is non empty set

p is Element of the carrier of L

Top L is Element of the carrier of L

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

K32( the carrier of L) is non empty set

A is Element of the carrier of L

{ b

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

Filt (BoolePoset L) is non empty set

InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set

K32( the carrier of (InclPoset (Filt (BoolePoset L)))) is non empty set

the carrier of (BoolePoset L) is non empty set

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

A is non empty Element of K32( the carrier of (InclPoset (Filt (BoolePoset L))))

meet A is set

x is set

RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))

K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set

K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set

RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr

the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set

{ b

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

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

x is Element of K32( the carrier of (BoolePoset L))

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

x is Element of K32( the carrier of (BoolePoset L))

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

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

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

x is set

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

Filt (BoolePoset L) is non empty set

InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set

K32( the carrier of (InclPoset (Filt (BoolePoset L)))) is non empty set

A is non empty Element of K32( the carrier of (InclPoset (Filt (BoolePoset L))))

"/\" (A,(InclPoset (Filt (BoolePoset L)))) is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

meet A is set

the carrier of (BoolePoset L) is non empty set

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

{ b

RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))

K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set

K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set

RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr

the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set

x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

k is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

c

y is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

k is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

L is set

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

K32(L) is non empty set

K32(K32(L)) is non empty set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of (BoolePoset L) is non empty set

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

A is set

p is non empty Element of K32( the carrier of (BoolePoset L))

x is set

A /\ x is set

L /\ L is set

A is set

x is set

L is set

{L} is non empty finite set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of (BoolePoset L) is non empty set

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

p is set

p is non empty Element of K32( the carrier of (BoolePoset L))

A is set

x is set

A is set

x is set

A /\ x is set

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

Filt (BoolePoset L) is non empty set

InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr

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

K32(L) is non empty set

K32(K32(L)) is non empty set

the carrier of (BoolePoset L) is non empty set

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

{ b

RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))

K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set

K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set

RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr

the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set

the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set

x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

Filt (BoolePoset L) is non empty set

InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr

{L} is non empty finite set

the carrier of (BoolePoset L) is non empty set

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

{ b

RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))

K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set

K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set

RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr

the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set

the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set

x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

c

y is set

A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

Filt (BoolePoset L) is non empty set

InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr

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

the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set

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

K32(L) is non empty set

K32(K32(L)) is non empty set

the carrier of (BoolePoset L) is non empty set

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

{ b

RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))

K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set

K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set

RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr

the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set

A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

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

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

Filt (BoolePoset L) is non empty set

InclPoset (Filt (BoolePoset L)) is non empty strict reflexive transitive antisymmetric RelStr

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

the carrier of (InclPoset (Filt (BoolePoset L))) is non empty set

{L} is non empty finite set

the carrier of (BoolePoset L) is non empty set

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

{ b

RelIncl (Filt (BoolePoset L)) is V7() V10( Filt (BoolePoset L)) V11( Filt (BoolePoset L)) V17( Filt (BoolePoset L)) V117() V120() V124() Element of K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L))))

K33((Filt (BoolePoset L)),(Filt (BoolePoset L))) is non empty set

K32(K33((Filt (BoolePoset L)),(Filt (BoolePoset L)))) is non empty set

RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is strict RelStr

the carrier of RelStr(# (Filt (BoolePoset L)),(RelIncl (Filt (BoolePoset L))) #) is set

A is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

x is Element of the carrier of (InclPoset (Filt (BoolePoset L)))

k is non empty filtered upper Element of K32( the carrier of (BoolePoset L))

c

y is set

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

L is non empty set

InclPoset L is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset L) is non empty set

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

p is non empty Element of K32( the carrier of (InclPoset L))

union p is set

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

A is set

x is Element of the carrier of (InclPoset L)

L is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

Filt L is non empty set

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

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

Ids (L ~) is non empty set

InclPoset (Ids (L ~)) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete RelStr

L is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

Filt L is non empty set

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

L is non empty RelStr

the carrier of L is non empty set

L is non empty RelStr

the carrier of L is non empty set

p is Element of the carrier of L

uparrow p is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

{p} is non empty finite Element of K32( the carrier of L)

(uparrow p) \ {p} is Element of K32( the carrier of L)

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

L is non empty RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

p is Element of K32( the carrier of L)

A is Element of the carrier of L

x is Element of the carrier of L

p is Element of K32( the carrier of L)

A is Element of K32( the carrier of L)

x is set

k is Element of the carrier of L

k is Element of the carrier of L

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

p is Element of the carrier of L

uparrow p is non empty filtered upper Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

{p} is non empty finite Element of K32( the carrier of L)

(uparrow p) \ {p} is Element of K32( the carrier of L)

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

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

{p} \/ (uparrow A) is non empty Element of K32( the carrier of L)

x is Element of the carrier of L

x is set

k is Element of the carrier of L

x is Element of the carrier of L

x is set

k is Element of the carrier of L

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

{p} \/ (uparrow A) is non empty Element of K32( the carrier of L)

(uparrow p) \ {p} is Element of K32( the carrier of L)

x is Element of the carrier of L

x is Element of the carrier of L

x is Element of the carrier of L

x is Element of the carrier of L

x is Element of the carrier of L

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

L is non empty reflexive transitive antisymmetric upper-bounded RelStr

Top L is Element of the carrier of L

the carrier of L is non empty set

(L) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

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

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

(uparrow (Top L)) \ {(Top L)} is Element of K32( the carrier of L)

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

{(Top L)} \ {(Top L)} is finite Element of K32( the carrier of L)

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

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

L is non empty reflexive transitive antisymmetric with_infima RelStr

(L) is Element of K32( the carrier of L)

the carrier of L is non empty set

K32( the carrier of L) is non empty set

IRR L is Element of K32( the carrier of L)

p is set

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

{A} is non empty finite Element of K32( the carrier of L)

x is Element of the carrier of L

uparrow x is non empty filtered upper Element of K32( the carrier of L)

{A} \/ (uparrow x) is non empty Element of K32( the carrier of L)

k is Element of the carrier of L

c

k "/\" c

L is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

p is Element of the carrier of L

(L) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

IRR L is Element of K32( the carrier of L)

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

p is Element of the carrier of L

uparrow p is non empty filtered upper Element of K32( the carrier of L)

{p} is non empty finite Element of K32( the carrier of L)

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

{p} \/ (uparrow A) is non empty Element of K32( the carrier of L)

x is Element of K32( the carrier of L)

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

k is set

c

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

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

(L) is Element of K32( the carrier of L)

p is Element of K32( the carrier of L)

A is set

x is Element of the carrier of L

uparrow x is non empty filtered upper Element of K32( the carrier of L)

(uparrow x) /\ p is Element of K32( the carrier of L)

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

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

the carrier of L is non empty set

p is Element of the carrier of L

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

the carrier of L \ (uparrow A) is Element of K32( the carrier of L)

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

uparrow p is non empty filtered upper Element of K32( the carrier of L)

{p} is non empty finite Element of K32( the carrier of L)

(uparrow p) \ {p} is Element of K32( the carrier of L)

(uparrow p) /\ (uparrow A) is Element of K32( the carrier of L)

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

L is non empty transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

p is Element of the carrier of L

A is Element of the carrier of L

x is Element of the carrier of L

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

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

k is Element of the carrier of L

L is non empty reflexive transitive antisymmetric distributive with_suprema with_infima RelStr

the carrier of L is non empty set

p is Element of the carrier of L

A is Element of the carrier of L

x is Element of the carrier of L

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

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

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

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

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

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

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

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

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

L ~ is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete RelStr

the carrier of L is non empty set

K32( the carrier of L) is non empty set

p is Element of the carrier of L

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

the carrier of L \ (downarrow p) is Element of K32( the carrier of L)

uparrow p is non empty filtered upper Element of K32( the carrier of L)

{p} is non empty finite Element of K32( the carrier of L)

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

{p} \/ (uparrow A) is non empty Element of K32( the carrier of L)

{ b

x is Element of K32( the carrier of L)

k is Element of the carrier of L

c

k "/\" c

y is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

k "/\" A is Element of the carrier of L

c

k "/\" (c

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

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

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

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

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

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

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

x is Element of the carrier of L

x is Element of the carrier of L

x is Element of the carrier of L

x is Element of the carrier of L

Top L is Element of the carrier of L

(L) is Element of K32( the carrier of L)

(downarrow p) ` is Element of K32( the carrier of L)

the carrier of (L ~) is non empty set

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

c

x is Element of the carrier of L

k is non empty filtered upper Element of K32( the carrier of L)

"/\" (c

y is Element of the carrier of L

D is Element of the carrier of L

{p} "\/" c

{ (p "\/" b

d is Element of the carrier of L

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

d is Element of the carrier of L

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

{(p ~)} is non empty finite Element of K32( the carrier of (L ~))

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

{(p ~)} "/\" y is Element of K32( the carrier of (L ~))

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

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

("/\" (c

(p ~) "/\" (("/\" (c

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

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

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

"/\" (({p} "\/" c

D is non empty directed Element of K32( the carrier of L)

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

D \ (downarrow p) is Element of K32( the carrier of L)

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

d is set

d is Element of the carrier of L

d is Element of the carrier of L

d "/\" A is Element of the carrier of L

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

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

L ~ is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete RelStr

the carrier of L is non empty set

CompactSublatt L is non empty strict reflexive transitive antisymmetric V128(L) join-inheriting with_suprema SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

p is Element of the carrier of L

K32( the carrier of L) is non empty set

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

the carrier of L \ (downarrow p) is Element of K32( the carrier of L)

x is Element of the carrier of L

uparrow p is non empty filtered upper Element of K32( the carrier of L)

{p} is non empty finite Element of K32( the carrier of L)

(uparrow p) \ {p} is Element of K32( the carrier of L)

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

A is non empty filtered upper Open Element of K32( the carrier of L)

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

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

the carrier of (L ~) is non empty set

x is Element of the carrier of L

uparrow x is non empty filtered upper Element of K32( the carrier of L)

the carrier of L \ (uparrow x) is Element of K32( the carrier of L)

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

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

{(p ~)} is non empty finite Element of K32( the carrier of (L ~))

k is non empty directed Element of K32( the carrier of (L ~))

{(p ~)} "/\" k is Element of K32( the carrier of (L ~))

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

c

{ (p "\/" b

y is Element of the carrier of L

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

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

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

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

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

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

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

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

c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

A is Element of the carrier of L

p is Element of the carrier of L

x is Element of the carrier of L

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

K32( the carrier of L) is non empty set

k is Element of the carrier of L

waybelow k is non empty directed lower Element of K32( the carrier of L)

x is Element of the carrier of L

CompactSublatt L is non empty strict reflexive transitive antisymmetric V128(L) join-inheriting with_suprema SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

k is Element of the carrier of L

uparrow k is non empty filtered upper Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

the carrier of L \ (uparrow k) is Element of K32( the carrier of L)

(uparrow k) ` is Element of K32( the carrier of L)

c

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

(L) is Element of K32( the carrier of L)

the carrier of L is non empty set

K32( the carrier of L) is non empty set

A is Element of the carrier of L

p is Element of the carrier of L

x is Element of the carrier of L

k is Element of the carrier of L

p is Element of K32( the carrier of L)

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

(L) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

p is Element of the carrier of L

uparrow p is non empty filtered upper Element of K32( the carrier of L)

(uparrow p) /\ (L) is Element of K32( the carrier of L)

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

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

the carrier of L is non empty set

K32( the carrier of L) is non empty set

p is Element of K32( the carrier of L)

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

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

{A} is non empty finite Element of K32( the carrier of L)

x is Element of the carrier of L

uparrow x is non empty filtered upper Element of K32( the carrier of L)

{A} \/ (uparrow x) is non empty Element of K32( the carrier of L)

k is Element of the carrier of L

k is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

CompactSublatt L is non empty strict reflexive transitive antisymmetric V128(L) join-inheriting with_suprema SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

p is Element of the carrier of L

uparrow p is non empty filtered upper Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

{ b

( b

"/\" ( { b

( b

x is Element of the carrier of L

k is Element of the carrier of L

c

uparrow c

the carrier of L \ (uparrow c

{p} is non empty finite Element of K32( the carrier of L)

x is Element of the carrier of L

uparrow x is non empty filtered upper Element of K32( the carrier of L)

{p} \/ (uparrow x) is non empty Element of K32( the carrier of L)

compactbelow p is non empty Element of K32( the carrier of L)

compactbelow x is non empty Element of K32( the carrier of L)

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

k is set

{ b

c

uparrow c

the carrier of L \ (uparrow c

y is Element of the carrier of L

y is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic RelStr

the carrier of L is non empty set

CompactSublatt L is non empty strict reflexive transitive antisymmetric V128(L) join-inheriting with_suprema SubRelStr of L

the carrier of (CompactSublatt L) is non empty set

p is Element of the carrier of L

A is Element of the carrier of L

uparrow A is non empty filtered upper Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

the carrier of L \ (uparrow A) is Element of K32( the carrier of L)

uparrow p is non empty filtered upper Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

{ b

A is Element of K32( the carrier of L)

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

x is Element of the carrier of L

k is Element of the carrier of L

uparrow k is non empty filtered upper Element of K32( the carrier of L)

the carrier of L \ (uparrow k) is Element of K32( the carrier of L)

k is Element of the carrier of L

uparrow k is non empty filtered upper Element of K32( the carrier of L)

the carrier of L \ (uparrow k) is Element of K32( the carrier of L)