:: WAYBEL15 semantic presentation

K133() is Element of K32(K129())

K129() is set

K32(K129()) is non empty set

K128() is set

K32(K128()) is non empty set

{} is empty Function-like functional finite V48() set

1 is non empty set

{{},1} is non empty finite set

K32(K133()) is non empty set

K33(1,1) is non empty set

K32(K33(1,1)) is non empty set

K33(K33(1,1),1) is non empty set

K32(K33(K33(1,1),1)) is non empty set

L is RelStr

Y is full SubRelStr of L

f is full SubRelStr of Y

the carrier of f is set

the carrier of Y is set

the InternalRel of Y is V7() V10( the carrier of Y) V11( the carrier of Y) Element of K32(K33( the carrier of Y, the carrier of Y))

K33( the carrier of Y, the carrier of Y) is set

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

the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) Element of K32(K33( the carrier of L, the carrier of L))

the carrier of L is set

K33( the carrier of L, the carrier of L) is set

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

the InternalRel of L |_2 the carrier of Y is V7() set

the InternalRel of f is V7() V10( the carrier of f) V11( the carrier of f) Element of K32(K33( the carrier of f, the carrier of f))

K33( the carrier of f, the carrier of f) is set

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

( the InternalRel of L |_2 the carrier of Y) |_2 the carrier of f is V7() set

the InternalRel of L |_2 the carrier of f is V7() set

z is SubRelStr of L

L is set

Y is non empty set

K33(L,Y) is set

K32(K33(L,Y)) is non empty set

f is non empty set

K33(Y,f) is non empty set

K32(K33(Y,f)) is non empty set

z is V7() V10(L) V11(Y) Function-like V27(L) quasi_total Element of K32(K33(L,Y))

v is non empty V7() V10(Y) V11(f) Function-like V27(Y) quasi_total Element of K32(K33(Y,f))

v * z is V7() V10(L) V11(f) Function-like V27(L) quasi_total Element of K32(K33(L,f))

K33(L,f) is set

K32(K33(L,f)) is non empty set

L is set

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

the carrier of (BoolePoset L) is non empty set

K32(L) is non empty set

Y is Element of the carrier of (BoolePoset L)

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

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

{ b

f is set

z is Element of K32(L)

v is Element of the carrier of (BoolePoset L)

f is set

z is Element of the carrier of (BoolePoset L)

L is non empty antisymmetric upper-bounded RelStr

the carrier of L is non empty set

Top L is Element of the carrier of L

Y is Element of the carrier of L

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

Y is non empty reflexive transitive antisymmetric RelStr

the carrier of Y is non empty set

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

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

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

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

f is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

z is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

[f,z] is Connection of L,Y

{f,z} is non empty functional finite set

{f} is non empty functional finite set

{{f,z},{f}} is non empty finite V48() set

Image z is non empty strict reflexive transitive antisymmetric full SubRelStr of L

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

K32( the carrier of L) is non empty set

subrelstr (rng z) is strict reflexive transitive antisymmetric full SubRelStr of L

the carrier of (Image z) is non empty set

the carrier of (Image z) |` z is V7() V10( the carrier of Y) V11( the carrier of L) Function-like Element of K32(K33( the carrier of Y, the carrier of L))

v is Element of the carrier of Y

z9 is Element of the carrier of Y

corestr z is non empty V7() V10( the carrier of Y) V11( the carrier of (Image z)) Function-like V27( the carrier of Y) quasi_total onto Element of K32(K33( the carrier of Y, the carrier of (Image z)))

K33( the carrier of Y, the carrier of (Image z)) is non empty set

K32(K33( the carrier of Y, the carrier of (Image z))) is non empty set

(corestr z) . v is Element of the carrier of (Image z)

(corestr z) . z9 is Element of the carrier of (Image z)

v9 is Element of the carrier of Y

z . v9 is Element of the carrier of L

{v9} is non empty finite Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

f " {v9} is Element of K32( the carrier of L)

f * z is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

K33( the carrier of Y, the carrier of Y) is non empty set

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

id Y is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like one-to-one V27( the carrier of Y) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of Y, the carrier of Y))

id the carrier of Y is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like one-to-one V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

dom z is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

z . v is Element of the carrier of L

z . z9 is Element of the carrier of L

f . (z . v) is Element of the carrier of Y

f . (z . z9) is Element of the carrier of Y

(f * z) . v is Element of the carrier of Y

(f * z) . z9 is Element of the carrier of Y

(id Y) . v is Element of the carrier of Y

rng (corestr z) is Element of K32( the carrier of (Image z))

K32( the carrier of (Image z)) is non empty set

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

Y is non empty reflexive transitive antisymmetric RelStr

the carrier of Y is non empty set

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

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

f is non empty reflexive transitive antisymmetric RelStr

the carrier of f is non empty set

K33( the carrier of Y, the carrier of f) is non empty set

K32(K33( the carrier of Y, the carrier of f)) is non empty set

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

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

K33( the carrier of f, the carrier of Y) is non empty set

K32(K33( the carrier of f, the carrier of Y)) is non empty set

z is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

v is non empty V7() V10( the carrier of Y) V11( the carrier of f) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of f))

v * z is non empty V7() V10( the carrier of L) V11( the carrier of f) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of f))

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

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

z9 is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

[z,z9] is Connection of L,Y

{z,z9} is non empty functional finite set

{z} is non empty functional finite set

{{z,z9},{z}} is non empty finite V48() set

v9 is non empty V7() V10( the carrier of f) V11( the carrier of Y) Function-like V27( the carrier of f) quasi_total Element of K32(K33( the carrier of f, the carrier of Y))

[v,v9] is Connection of Y,f

{v,v9} is non empty functional finite set

{v} is non empty functional finite set

{{v,v9},{v}} is non empty finite V48() set

z9 * v9 is non empty V7() V10( the carrier of f) V11( the carrier of L) Function-like V27( the carrier of f) quasi_total Element of K32(K33( the carrier of f, the carrier of L))

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

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

[(v * z),(z9 * v9)] is Connection of L,f

{(v * z),(z9 * v9)} is non empty functional finite set

{(v * z)} is non empty functional finite set

{{(v * z),(z9 * v9)},{(v * z)}} is non empty finite V48() set

f is Element of the carrier of f

dom v9 is Element of K32( the carrier of f)

K32( the carrier of f) is non empty set

f1 is Element of the carrier of L

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

K32( the carrier of L) is non empty set

(v * z) . f1 is Element of the carrier of f

(z9 * v9) . f is Element of the carrier of L

z . f1 is Element of the carrier of Y

v . (z . f1) is Element of the carrier of f

v9 . f is Element of the carrier of Y

z9 . (v9 . f) is Element of the carrier of L

z9 . (z . f1) is Element of the carrier of L

z9 * z is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of L))

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

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

(z9 * z) . f1 is Element of the carrier of L

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of L, the carrier of L))

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of L))

(id L) . f1 is Element of the carrier of L

v9 . f is Element of the carrier of Y

z9 . (v9 . f) is Element of the carrier of L

z . f1 is Element of the carrier of Y

v . (v9 . f) is Element of the carrier of f

v . (z . f1) is Element of the carrier of f

v * v9 is non empty V7() V10( the carrier of f) V11( the carrier of f) Function-like V27( the carrier of f) quasi_total Element of K32(K33( the carrier of f, the carrier of f))

K33( the carrier of f, the carrier of f) is non empty set

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

(v * v9) . f is Element of the carrier of f

id f is non empty V7() V10( the carrier of f) V11( the carrier of f) Function-like one-to-one V27( the carrier of f) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of f, the carrier of f))

id the carrier of f is non empty V7() V10( the carrier of f) V11( the carrier of f) Function-like one-to-one V27( the carrier of f) quasi_total Element of K32(K33( the carrier of f, the carrier of f))

(id f) . f is Element of the carrier of f

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

Y is non empty reflexive transitive antisymmetric RelStr

the carrier of Y is non empty set

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

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

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

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

f is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

f " is V7() Function-like set

z is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

[f,z] is Connection of L,Y

{f,z} is non empty functional finite set

{f} is non empty functional finite set

{{f,z},{f}} is non empty finite V48() set

[z,f] is Connection of Y,L

{z,f} is non empty functional finite set

{z} is non empty functional finite set

{{z,f},{z}} is non empty finite V48() set

z9 is Element of the carrier of L

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

K32( the carrier of L) is non empty set

z * f is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of L))

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

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

id (dom f) is V7() V10( dom f) V11( dom f) Function-like one-to-one V27( dom f) quasi_total Element of K32(K33((dom f),(dom f)))

K33((dom f),(dom f)) is set

K32(K33((dom f),(dom f))) is non empty set

id L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of L, the carrier of L))

id the carrier of L is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like one-to-one V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of L))

v is Element of the carrier of Y

f . z9 is Element of the carrier of Y

z . v is Element of the carrier of L

z . (f . z9) is Element of the carrier of L

(z * f) . z9 is Element of the carrier of L

dom z is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

f * z is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

K33( the carrier of Y, the carrier of Y) is non empty set

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

rng f is Element of K32( the carrier of Y)

id (rng f) is V7() V10( rng f) V11( rng f) Function-like one-to-one V27( rng f) quasi_total Element of K32(K33((rng f),(rng f)))

K33((rng f),(rng f)) is set

K32(K33((rng f),(rng f))) is non empty set

id Y is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like one-to-one V27( the carrier of Y) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of Y, the carrier of Y))

id the carrier of Y is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like one-to-one V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

f . (z . v) is Element of the carrier of Y

(f * z) . v is Element of the carrier of Y

z9 is Element of the carrier of Y

v is Element of the carrier of L

z . z9 is Element of the carrier of L

f . v is Element of the carrier of Y

f . (z . z9) is Element of the carrier of Y

(f * z) . z9 is Element of the carrier of Y

z . (f . v) is Element of the carrier of L

(z * f) . v is Element of the carrier of L

L is set

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

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

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

the carrier of (BoolePoset L) is non empty set

Y is Element of the carrier of (CompactSublatt (BoolePoset L))

f is Element of the carrier of (CompactSublatt (BoolePoset L))

z is Element of the carrier of (BoolePoset L)

v is Element of the carrier of (BoolePoset L)

z /\ v is set

z "/\" v is Element of the carrier of (BoolePoset L)

v9 is Element of the carrier of (CompactSublatt (BoolePoset L))

f is Element of the carrier of (BoolePoset L)

z9 is Element of the carrier of (CompactSublatt (BoolePoset L))

{Y,f} is non empty finite Element of K32( the carrier of (CompactSublatt (BoolePoset L)))

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

L is set

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

L is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of L is non empty set

Y is non empty reflexive transitive antisymmetric up-complete RelStr

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

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

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

f " is V7() Function-like set

v is Element of the carrier of L

waybelow v is lower Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

f .: (waybelow v) is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

f . v is Element of the carrier of Y

waybelow (f . v) is lower Element of K32( the carrier of Y)

z9 is set

{ b

v9 is Element of the carrier of Y

z is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

z . v9 is Element of the carrier of L

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

dom z is Element of K32( the carrier of Y)

rng f is Element of K32( the carrier of Y)

f . (z . v9) is Element of the carrier of Y

z9 is set

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

v9 is set

f . v9 is set

{ b

f is Element of the carrier of L

f . f is Element of the carrier of Y

L is non empty reflexive transitive antisymmetric RelStr

Y is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

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

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

f " is V7() Function-like set

z is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

v is Element of the carrier of Y

z . v is Element of the carrier of L

waybelow (z . v) is lower Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

rng f is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

f . (z . v) is Element of the carrier of Y

"\/" ((waybelow (z . v)),L) is Element of the carrier of L

f . ("\/" ((waybelow (z . v)),L)) is Element of the carrier of Y

f .: (waybelow (z . v)) is Element of K32( the carrier of Y)

"\/" ((f .: (waybelow (z . v))),Y) is Element of the carrier of Y

waybelow (f . (z . v)) is lower Element of K32( the carrier of Y)

"\/" ((waybelow (f . (z . v))),Y) is Element of the carrier of Y

waybelow v is lower Element of K32( the carrier of Y)

"\/" ((waybelow v),Y) is Element of the carrier of Y

v is Element of the carrier of Y

waybelow v is lower Element of K32( the carrier of Y)

K32((waybelow v)) is non empty set

z9 is finite Element of K32((waybelow v))

v9 is set

z .: z9 is finite Element of K32( the carrier of L)

dom z is Element of K32( the carrier of Y)

f is set

z . f is set

{ b

f1 is Element of the carrier of Y

z . f1 is Element of the carrier of L

z . v is Element of the carrier of L

waybelow (z . v) is lower Element of K32( the carrier of L)

K32((waybelow (z . v))) is non empty set

v9 is finite Element of K32((waybelow (z . v)))

f is Element of the carrier of L

f . (z . v) is Element of the carrier of Y

f . f is Element of the carrier of Y

f1 is Element of the carrier of Y

f .: v9 is finite Element of K32( the carrier of Y)

f " z9 is Element of K32( the carrier of L)

f .: (f " z9) is Element of K32( the carrier of Y)

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

Y is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

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

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

f " is V7() Function-like set

z is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

v is Element of the carrier of Y

CompactSublatt Y is strict reflexive transitive antisymmetric full join-inheriting SubRelStr of Y

the carrier of (CompactSublatt Y) is set

z9 is Element of the carrier of Y

{v,z9} is non empty finite Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

z . v is Element of the carrier of L

CompactSublatt L is strict reflexive transitive antisymmetric full join-inheriting SubRelStr of L

the carrier of (CompactSublatt L) is set

z . z9 is Element of the carrier of L

dom z is Element of K32( the carrier of Y)

z .: {v,z9} is non empty finite Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

{(z . v),(z . z9)} is non empty finite Element of K32( the carrier of L)

"/\" ({(z . v),(z . z9)},L) is Element of the carrier of L

"/\" ({v,z9},Y) is Element of the carrier of Y

z . ("/\" ({v,z9},Y)) is Element of the carrier of L

"/\" ((z .: {v,z9}),L) is Element of the carrier of L

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

the carrier of L is non empty set

Ids L is non empty set

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

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

the carrier of Y is non empty set

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

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

SupMap L is non empty V7() V10( the carrier of (InclPoset (Ids L))) V11( the carrier of L) Function-like V27( the carrier of (InclPoset (Ids L))) quasi_total Element of K32(K33( the carrier of (InclPoset (Ids L)), the carrier of L))

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

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

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

f is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

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

K32( the carrier of L) is non empty set

z is set

v is Element of the carrier of L

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

dom f is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

f . (downarrow v) is set

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

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

Y is non empty reflexive transitive antisymmetric RelStr

the carrier of Y is non empty set

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

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

f is non empty reflexive transitive antisymmetric RelStr

the carrier of f is non empty set

K33( the carrier of Y, the carrier of f) is non empty set

K32(K33( the carrier of Y, the carrier of f)) is non empty set

z is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

v is non empty V7() V10( the carrier of Y) V11( the carrier of f) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of f))

v * z is non empty V7() V10( the carrier of L) V11( the carrier of f) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of f))

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

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

K32( the carrier of L) is non empty set

z9 is Element of K32( the carrier of L)

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

z .: z9 is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

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

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

v .: (z .: z9) is Element of K32( the carrier of f)

K32( the carrier of f) is non empty set

"\/" ((v .: (z .: z9)),f) is Element of the carrier of f

"\/" ((z .: z9),Y) is Element of the carrier of Y

v . ("\/" ((z .: z9),Y)) is Element of the carrier of f

(v * z) .: z9 is Element of K32( the carrier of f)

z . ("\/" (z9,L)) is Element of the carrier of Y

"\/" (((v * z) .: z9),f) is Element of the carrier of f

v . (z . ("\/" (z9,L))) is Element of the carrier of f

(v * z) . ("\/" (z9,L)) is Element of the carrier of f

L is non empty RelStr

the carrier of L is non empty set

Y is non empty RelStr

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

Image f is non empty strict full SubRelStr of Y

rng f is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

subrelstr (rng f) is strict full SubRelStr of Y

the carrier of (Image f) is non empty set

K32( the carrier of (Image f)) is non empty set

inclusion f is non empty V7() V10( the carrier of (Image f)) V11( the carrier of Y) Function-like one-to-one V27( the carrier of (Image f)) quasi_total monotone Element of K32(K33( the carrier of (Image f), the carrier of Y))

K33( the carrier of (Image f), the carrier of Y) is non empty set

K32(K33( the carrier of (Image f), the carrier of Y)) is non empty set

id (Image f) is non empty V7() V10( the carrier of (Image f)) V11( the carrier of (Image f)) Function-like one-to-one V27( the carrier of (Image f)) quasi_total idempotent monotone isomorphic projection Element of K32(K33( the carrier of (Image f), the carrier of (Image f)))

K33( the carrier of (Image f), the carrier of (Image f)) is non empty set

K32(K33( the carrier of (Image f), the carrier of (Image f))) is non empty set

id the carrier of (Image f) is non empty V7() V10( the carrier of (Image f)) V11( the carrier of (Image f)) Function-like one-to-one V27( the carrier of (Image f)) quasi_total Element of K32(K33( the carrier of (Image f), the carrier of (Image f)))

z is Element of K32( the carrier of (Image f))

(inclusion f) .: z is Element of K32( the carrier of Y)

L is set

BoolePoset L is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic RelStr

the carrier of (BoolePoset L) is non empty set

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

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

Y is non empty V7() V10( the carrier of (BoolePoset L)) V11( the carrier of (BoolePoset L)) Function-like V27( the carrier of (BoolePoset L)) quasi_total Element of K32(K33( the carrier of (BoolePoset L), the carrier of (BoolePoset L)))

Image Y is non empty strict reflexive transitive antisymmetric full SubRelStr of BoolePoset L

rng Y is Element of K32( the carrier of (BoolePoset L))

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

subrelstr (rng Y) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset L

inclusion Y is non empty V7() V10( the carrier of (Image Y)) V11( the carrier of (BoolePoset L)) Function-like one-to-one V27( the carrier of (Image Y)) quasi_total monotone Element of K32(K33( the carrier of (Image Y), the carrier of (BoolePoset L)))

the carrier of (Image Y) is non empty set

K33( the carrier of (Image Y), the carrier of (BoolePoset L)) is non empty set

K32(K33( the carrier of (Image Y), the carrier of (BoolePoset L))) is non empty set

id (Image Y) is non empty V7() V10( the carrier of (Image Y)) V11( the carrier of (Image Y)) Function-like one-to-one V27( the carrier of (Image Y)) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of (Image Y), the carrier of (Image Y)))

K33( the carrier of (Image Y), the carrier of (Image Y)) is non empty set

K32(K33( the carrier of (Image Y), the carrier of (Image Y))) is non empty set

id the carrier of (Image Y) is non empty V7() V10( the carrier of (Image Y)) V11( the carrier of (Image Y)) Function-like one-to-one V27( the carrier of (Image Y)) quasi_total Element of K32(K33( the carrier of (Image Y), the carrier of (Image Y)))

K32( the carrier of (Image Y)) is non empty set

f is non empty directed lower Element of K32( the carrier of (Image Y))

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

dom Y is Element of K32( the carrier of (BoolePoset L))

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

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

Y .: f is Element of K32( the carrier of (BoolePoset L))

"\/" ((Y .: f),(BoolePoset L)) is Element of the carrier of (BoolePoset L)

(inclusion Y) .: f is non empty Element of K32( the carrier of (BoolePoset L))

"\/" (((inclusion Y) .: f),(BoolePoset L)) is Element of the carrier of (BoolePoset L)

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

(inclusion Y) . ("\/" (f,(Image Y))) is Element of the carrier of (BoolePoset L)

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

the carrier of L is non empty set

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

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

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

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

z is non empty V7() V10( the carrier of L) V11( the carrier of Y) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of Y))

[f,z] is Connection of Y,L

{f,z} is non empty functional finite set

{f} is non empty functional finite set

{{f,z},{f}} is non empty finite V48() set

z * f is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

K33( the carrier of Y, the carrier of Y) is non empty set

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

v is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like V27( the carrier of Y) quasi_total idempotent monotone projection kernel Element of K32(K33( the carrier of Y, the carrier of Y))

z9 is non empty set

BoolePoset z9 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic RelStr

the carrier of (BoolePoset z9) is non empty set

K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)) is non empty set

K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9))) is non empty set

v9 is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total idempotent monotone projection closure Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

Image v9 is non empty strict reflexive transitive antisymmetric with_infima full meet-inheriting infs-inheriting filtered-infs-inheriting SubRelStr of BoolePoset z9

rng v9 is Element of K32( the carrier of (BoolePoset z9))

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

subrelstr (rng v9) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset z9

the carrier of (Image v9) is non empty set

K33( the carrier of Y, the carrier of (Image v9)) is non empty set

K32(K33( the carrier of Y, the carrier of (Image v9))) is non empty set

f is non empty V7() V10( the carrier of Y) V11( the carrier of (Image v9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (Image v9)))

K33( the carrier of (Image v9), the carrier of Y) is non empty set

K32(K33( the carrier of (Image v9), the carrier of Y)) is non empty set

f " is V7() Function-like set

corestr v9 is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (Image v9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total onto monotone Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (Image v9)))

K33( the carrier of (BoolePoset z9), the carrier of (Image v9)) is non empty set

K32(K33( the carrier of (BoolePoset z9), the carrier of (Image v9))) is non empty set

the carrier of (Image v9) |` v9 is V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

f1 is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of Y) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of Y))

inclusion v9 is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (BoolePoset z9)) Function-like one-to-one V27( the carrier of (Image v9)) quasi_total monotone Element of K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9)))

K33( the carrier of (Image v9), the carrier of (BoolePoset z9)) is non empty set

K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9))) is non empty set

id (Image v9) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (Image v9)) Function-like one-to-one V27( the carrier of (Image v9)) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of (Image v9), the carrier of (Image v9)))

K33( the carrier of (Image v9), the carrier of (Image v9)) is non empty set

K32(K33( the carrier of (Image v9), the carrier of (Image v9))) is non empty set

id the carrier of (Image v9) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (Image v9)) Function-like one-to-one V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (Image v9)))

(inclusion v9) * f is non empty V7() V10( the carrier of Y) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (BoolePoset z9)))

K33( the carrier of Y, the carrier of (BoolePoset z9)) is non empty set

K32(K33( the carrier of Y, the carrier of (BoolePoset z9))) is non empty set

((inclusion v9) * f) * v is non empty V7() V10( the carrier of Y) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (BoolePoset z9)))

(((inclusion v9) * f) * v) * f1 is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * v) * f1) * (corestr v9) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

f1 * f is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

dom f is Element of K32( the carrier of Y)

K32( the carrier of Y) is non empty set

id (dom f) is V7() V10( dom f) V11( dom f) Function-like one-to-one V27( dom f) quasi_total Element of K32(K33((dom f),(dom f)))

K33((dom f),(dom f)) is set

K32(K33((dom f),(dom f))) is non empty set

id Y is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like one-to-one V27( the carrier of Y) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of K32(K33( the carrier of Y, the carrier of Y))

id the carrier of Y is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like one-to-one V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

rng f1 is Element of K32( the carrier of Y)

f * f1 is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of L) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of L))

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

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

(f * f1) * (corestr v9) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of L) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of L))

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

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

rng ((f * f1) * (corestr v9)) is Element of K32( the carrier of L)

K32( the carrier of L) is non empty set

((inclusion v9) * f) * z is non empty V7() V10( the carrier of L) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of (BoolePoset z9)))

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

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

dom (((inclusion v9) * f) * z) is Element of K32( the carrier of L)

f * z is non empty V7() V10( the carrier of L) V11( the carrier of (Image v9)) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of (Image v9)))

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

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

dom (f * z) is Element of K32( the carrier of L)

p is set

(f * z) . p is set

(inclusion v9) . ((f * z) . p) is set

(inclusion v9) * (f * z) is non empty V7() V10( the carrier of L) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of (BoolePoset z9)))

((inclusion v9) * (f * z)) . p is set

(((inclusion v9) * f) * z) . p is set

f1 * (corestr v9) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of Y) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of Y))

K33( the carrier of (BoolePoset z9), the carrier of Y) is non empty set

K32(K33( the carrier of (BoolePoset z9), the carrier of Y)) is non empty set

v * (f1 * (corestr v9)) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of Y) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of Y))

f * (v * (f1 * (corestr v9))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (Image v9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (Image v9)))

f1 * (id (Image v9)) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of Y) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of Y))

(((inclusion v9) * f) * v) * (f1 * (id (Image v9))) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * v) * (f1 * (id (Image v9)))) * (f * (v * (f1 * (corestr v9)))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * v) * f1) * (f * (v * (f1 * (corestr v9)))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * v) * f1) * f is non empty V7() V10( the carrier of Y) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * v) * f1) * f) * (v * (f1 * (corestr v9))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((inclusion v9) * f) * v) * (id Y) is non empty V7() V10( the carrier of Y) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * v) * (id Y)) * (v * (f1 * (corestr v9))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((inclusion v9) * f) * v) * (v * (f1 * (corestr v9))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((inclusion v9) * f) * v) * v is non empty V7() V10( the carrier of Y) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * v) * v) * (f1 * (corestr v9)) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

v * v is non empty V7() V10( the carrier of Y) V11( the carrier of Y) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of Y))

((inclusion v9) * f) * (v * v) is non empty V7() V10( the carrier of Y) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (BoolePoset z9)))

(((inclusion v9) * f) * (v * v)) * (f1 * (corestr v9)) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((inclusion v9) * f) * v) * (f1 * (corestr v9)) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

p is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

p * p is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * v) * f1) * (corestr v9)) * ((((inclusion v9) * f) * v) * (f1 * (corestr v9))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

((inclusion v9) * f) * (v * (f1 * (corestr v9))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * v) * f1) * (corestr v9)) * (((inclusion v9) * f) * (v * (f1 * (corestr v9)))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(inclusion v9) * (f * (v * (f1 * (corestr v9)))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * v) * f1) * (corestr v9)) * ((inclusion v9) * (f * (v * (f1 * (corestr v9))))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * v) * f1) * (corestr v9)) * (inclusion v9) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9)))

((((((inclusion v9) * f) * v) * f1) * (corestr v9)) * (inclusion v9)) * (f * (v * (f1 * (corestr v9)))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(corestr v9) * (inclusion v9) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (Image v9)) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (Image v9)))

((((inclusion v9) * f) * v) * f1) * ((corestr v9) * (inclusion v9)) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * v) * f1) * ((corestr v9) * (inclusion v9))) * (f * (v * (f1 * (corestr v9)))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * v) * f1) * (id (Image v9)) is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * v) * f1) * (id (Image v9))) * (f * (v * (f1 * (corestr v9)))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

p is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total idempotent monotone projection Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

Image p is non empty strict reflexive transitive antisymmetric full SubRelStr of BoolePoset z9

rng p is Element of K32( the carrier of (BoolePoset z9))

subrelstr (rng p) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset z9

(((inclusion v9) * f) * z) * f is non empty V7() V10( the carrier of Y) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * z) * f) * f1 is non empty V7() V10( the carrier of (Image v9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (Image v9)) quasi_total Element of K32(K33( the carrier of (Image v9), the carrier of (BoolePoset z9)))

(((((inclusion v9) * f) * z) * f) * f1) * (corestr v9) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

((((inclusion v9) * f) * z) * f) * (f1 * (corestr v9)) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

f * (f1 * (corestr v9)) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of L) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of L))

(((inclusion v9) * f) * z) * (f * (f1 * (corestr v9))) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

(((inclusion v9) * f) * z) * ((f * f1) * (corestr v9)) is non empty V7() V10( the carrier of (BoolePoset z9)) V11( the carrier of (BoolePoset z9)) Function-like V27( the carrier of (BoolePoset z9)) quasi_total Element of K32(K33( the carrier of (BoolePoset z9), the carrier of (BoolePoset z9)))

rng (((inclusion v9) * f) * z) is Element of K32( the carrier of (BoolePoset z9))

rng (f * z) is Element of K32( the carrier of (Image v9))

K32( the carrier of (Image v9)) is non empty set

subrelstr (rng (f * z)) is strict reflexive transitive antisymmetric full SubRelStr of Image v9

the carrier of (subrelstr (rng (f * z))) is set

[f1,f] is Connection of Image v9,Y

{f1,f} is non empty functional finite set

{f1} is non empty functional finite set

{{f1,f},{f1}} is non empty finite V48() set

[(f * f1),(f * z)] is Connection of Image v9,L

{(f * f1),(f * z)} is non empty functional finite set

{(f * f1)} is non empty functional finite set

{{(f * f1),(f * z)},{(f * f1)}} is non empty finite V48() set

Image (f * z) is non empty strict reflexive transitive antisymmetric full SubRelStr of Image v9

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

the carrier of L is non empty set

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

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

Y is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total idempotent monotone projection kernel Element of K32(K33( the carrier of L, the carrier of L))

Image Y is non empty strict reflexive transitive antisymmetric full SubRelStr of L

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

K32( the carrier of L) is non empty set

subrelstr (rng Y) is strict reflexive transitive antisymmetric full SubRelStr of L

f is Element of K32( the carrier of L)

the carrier of (Image Y) is non empty set

corestr Y is non empty V7() V10( the carrier of L) V11( the carrier of (Image Y)) Function-like V27( the carrier of L) quasi_total onto monotone Element of K32(K33( the carrier of L, the carrier of (Image Y)))

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

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

the carrier of (Image Y) |` Y is V7() V10( the carrier of L) V11( the carrier of L) Function-like Element of K32(K33( the carrier of L, the carrier of L))

(corestr Y) .: f is Element of K32( the carrier of (Image Y))

K32( the carrier of (Image Y)) is non empty set

Y .: f is Element of K32( the carrier of L)

"\/" (((corestr Y) .: f),L) is Element of the carrier of L

"\/" (((corestr Y) .: f),(Image Y)) is Element of the carrier of (Image Y)

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

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

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

(corestr Y) . ("\/" (f,L)) is Element of the carrier of (Image Y)

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

the carrier of L is non empty set

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

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

Y is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total idempotent monotone projection Element of K32(K33( the carrier of L, the carrier of L))

Image Y is non empty strict reflexive transitive antisymmetric full SubRelStr of L

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

K32( the carrier of L) is non empty set

subrelstr (rng Y) is strict reflexive transitive antisymmetric full SubRelStr of L

{ b

f is non empty Element of K32( the carrier of L)

subrelstr f is non empty strict reflexive transitive antisymmetric full SubRelStr of L

the carrier of (subrelstr f) is non empty set

K33( the carrier of (subrelstr f), the carrier of (subrelstr f)) is non empty set

K32(K33( the carrier of (subrelstr f), the carrier of (subrelstr f))) is non empty set

Y | f is V7() V10( the carrier of L) V11( the carrier of L) Function-like Element of K32(K33( the carrier of L, the carrier of L))

z is non empty V7() V10( the carrier of (subrelstr f)) V11( the carrier of (subrelstr f)) Function-like V27( the carrier of (subrelstr f)) quasi_total Element of K32(K33( the carrier of (subrelstr f), the carrier of (subrelstr f)))

K32( the carrier of (subrelstr f)) is non empty set

v is Element of K32( the carrier of (subrelstr f))

z9 is Element of K32( the carrier of L)

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

z .: v is Element of K32( the carrier of (subrelstr f))

Y .: v is Element of K32( the carrier of L)

dom z is Element of K32( the carrier of (subrelstr f))

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

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

"\/" ((z .: v),(subrelstr f)) is Element of the carrier of (subrelstr f)

"\/" ((Y .: v),L) is Element of the carrier of L

Y . ("\/" (v9,L)) is Element of the carrier of L

z . ("\/" (v,(subrelstr f))) is Element of the carrier of (subrelstr f)

the carrier of (subrelstr (rng Y)) is set

rng z is Element of K32( the carrier of (subrelstr f))

subrelstr (rng z) is strict reflexive transitive antisymmetric full SubRelStr of subrelstr f

the carrier of (subrelstr (rng z)) is set

Image z is non empty strict reflexive transitive antisymmetric full SubRelStr of subrelstr f

L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

Y is set

BoolePoset Y is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic RelStr

the carrier of (BoolePoset Y) is non empty set

K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)) is non empty set

K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y))) is non empty set

f is non empty V7() V10( the carrier of (BoolePoset Y)) V11( the carrier of (BoolePoset Y)) Function-like V27( the carrier of (BoolePoset Y)) quasi_total idempotent monotone projection Element of K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)))

Image f is non empty strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

rng f is Element of K32( the carrier of (BoolePoset Y))

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

subrelstr (rng f) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

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

the carrier of L is non empty set

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

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

Y is non empty set

BoolePoset Y is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic RelStr

the carrier of (BoolePoset Y) is non empty set

K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)) is non empty set

K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y))) is non empty set

f is non empty V7() V10( the carrier of (BoolePoset Y)) V11( the carrier of (BoolePoset Y)) Function-like V27( the carrier of (BoolePoset Y)) quasi_total idempotent monotone projection Element of K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)))

Image f is non empty strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

rng f is Element of K32( the carrier of (BoolePoset Y))

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

subrelstr (rng f) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

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

the carrier of L is non empty set

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

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

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

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

Y is non empty set

BoolePoset Y is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic RelStr

the carrier of (BoolePoset Y) is non empty set

K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)) is non empty set

K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y))) is non empty set

f is non empty V7() V10( the carrier of (BoolePoset Y)) V11( the carrier of (BoolePoset Y)) Function-like V27( the carrier of (BoolePoset Y)) quasi_total idempotent monotone projection Element of K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)))

Image f is non empty strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

rng f is Element of K32( the carrier of (BoolePoset Y))

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

subrelstr (rng f) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

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

the carrier of L is non empty set

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

the carrier of Y is non empty set

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

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

f is non empty V7() V10( the carrier of Y) V11( the carrier of L) Function-like V27( the carrier of Y) quasi_total Element of K32(K33( the carrier of Y, the carrier of L))

Y is set

BoolePoset Y is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic RelStr

the carrier of (BoolePoset Y) is non empty set

K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)) is non empty set

K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y))) is non empty set

f is non empty V7() V10( the carrier of (BoolePoset Y)) V11( the carrier of (BoolePoset Y)) Function-like V27( the carrier of (BoolePoset Y)) quasi_total idempotent monotone projection Element of K32(K33( the carrier of (BoolePoset Y), the carrier of (BoolePoset Y)))

Image f is non empty strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

rng f is Element of K32( the carrier of (BoolePoset Y))

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

subrelstr (rng f) is strict reflexive transitive antisymmetric full SubRelStr of BoolePoset Y

L is non empty RelStr

the carrier of L is non empty set

L ~ is non empty strict RelStr

PRIME (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

Y is Element of the carrier of L

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

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

K32( the carrier of L) is non empty set

Y is Element of K32( the carrier of L)

f is Element of the carrier of L

z is Element of the carrier of L

Y is Element of K32( the carrier of L)

f is Element of K32( the carrier of L)

z is set

v is Element of the carrier of L

v is Element of the carrier of L

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

the carrier of L is non empty set

Bottom L is Element of the carrier of L

Y is Element of the carrier of L

f is Element of the carrier of L

z is Element of the carrier of L

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

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

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

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

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

f is Element of the carrier of L

z is Element of the carrier of L

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

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

Top L is Element of the carrier of L

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

the carrier of L is non empty set

Y is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean 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

L ~ is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (L ~) is non empty set

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

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

Bottom L is Element of the carrier of L

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

(PRIME (L ~)) \ {(Bottom L)} is Element of K32( the carrier of (L ~))

Y is set

f is Element of the carrier of (L ~)

~ f is Element of the carrier of L

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

Y is set

f is Element of the carrier of L

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

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

the carrier of L is non empty set

f is Element of the carrier of L

Y is Element of the carrier of L

'not' Y is Element of the carrier of L

Bottom L is Element of the carrier of L

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

Y => is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total Element of K32(K33( the carrier of L, the carrier of L))

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

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

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

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

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

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

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

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

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

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

Top L is Element of the carrier of L

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

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

the carrier of L is non empty set

K32( the carrier of L) is non empty set

Y is Element of K32( the carrier of L)

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

f is Element of the carrier of L

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

{ (f "/\" b

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

z is Element of the carrier of L

z "/\" is non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total monotone Element of K32(K33( the carrier of L, the carrier of L))

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

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

L is non empty antisymmetric with_infima lower-bounded RelStr

the carrier of L is non empty set

Bottom L is Element of the carrier of L

Y is Element of the carrier of L

f is Element of the carrier of L

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean 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)

Y is Element of the carrier of L

f is Element of K32( the carrier of L)

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

z is Element of the carrier of L

{ (Y "/\" b

v is Element of the carrier of L

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

Bottom L is Element of the carrier of L

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

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

L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean 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)

Y is Element of K32( the carrier of L)

f is Element of K32( the carrier of L)

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

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

z is set

v is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean 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)

Y is Element of the carrier of L

f is Element of K32( the carrier of L)

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

Bottom L is Element of the carrier of L

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

f \ {(Bottom L)} is Element of K32( the carrier of L)

z is Element of K32( the carrier of L)

v is Element of the carrier of L

z9 is Element of the carrier of L

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

v is set

z9 is Element of the carrier of L

v is Element of the carrier of L

L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean 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)

Y is Element of K32( the carrier of L)

BoolePoset Y is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic RelStr

the carrier of (BoolePoset Y) is non empty set

f is Element of the carrier of (BoolePoset Y)

z is Element of K32( the carrier of L)

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

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

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

f is non empty V7() V10( the carrier of (BoolePoset Y)) V11( the carrier of L) Function-like V27( the carrier of (BoolePoset Y)) quasi_total Element of K32(K33( the carrier of (BoolePoset Y), the carrier of L))

z is Element of the carrier of (BoolePoset Y)

f . z is Element of the carrier of L

z9 is Element of K32( the carrier of L)

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

v is Element of the carrier of (BoolePoset Y)

f . v is Element of the carrier of L

v9 is Element of K32( the carrier of L)

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

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

z is set

v is Element of K32( the carrier of L)

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

dom f is Element of K32( the carrier of (BoolePoset Y))

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

f . v is set

z9 is Element of K32( the carrier of L)

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

z is Element of the carrier of (BoolePoset Y)

f . z is Element of the carrier of L