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
{ b1 where b1 is Element of K32(L) : Y c= b1 } is set
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
{ b1 where b1 is Element of the carrier of Y : b1 is_way_below f . v } is set
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
{ b1 where b1 is Element of the carrier of L : b1 is_way_below v } is set
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
{ b1 where b1 is Element of the carrier of Y : b1 is_way_below v } is set
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
{ b1 where b1 is Element of the carrier of L : Y . b1 <= b1 } is set
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 "/\" b1) where b1 is Element of the carrier of L : b1 in Y } is set
"\/" ( { (f "/\" b1) where b1 is Element of the carrier of L : b1 in Y } ,L) is Element of the carrier of L
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 "/\" b1) where b1 is Element of the carrier of L : b1 in f } is set
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 "/\" b1) where b1 is Element of the carrier of L : b1 in f } ,L) 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 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
v is Element of the carrier of (BoolePoset Y)
f . v 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
v9 is Element of K32( the carrier of L)
"\/" (v9,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
L ~ is non empty strict 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)
Y is Element of 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
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean RelStr
L ~ is non empty strict 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)
Y is Element of 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
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean RelStr
L ~ is non empty strict 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)
Y is Element of 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
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean RelStr
L ~ is non empty strict 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)
Y is Element of 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
L is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean RelStr
L ~ is non empty strict 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)
Y is Element of 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
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)
L ~ is non empty strict reflexive transitive antisymmetric RelStr
Y is Element of 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