:: LATTICE7 semantic presentation

REAL is V32() V33() V34() V38() set

NAT is V32() V33() V34() V35() V36() V37() V38() Element of bool REAL

bool REAL is non empty set

NAT is V32() V33() V34() V35() V36() V37() V38() set

bool NAT is non empty set

bool NAT is non empty set

{} is empty V32() V33() V34() V35() V36() V37() V38() set

1 is non empty V23() V24() ext-real positive non negative V32() V33() V34() V35() V36() V37() Element of NAT

2 is non empty V23() V24() ext-real positive non negative V32() V33() V34() V35() V36() V37() Element of NAT

L is 1-sorted

the carrier of L is set

bool the carrier of L is non empty set

X is Element of bool the carrier of L

f is Element of bool the carrier of L

b is set

b is Element of the carrier of L

Z1 is Element of the carrier of L

L is non empty V117() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

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

L is non empty V117() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

X is Element of the carrier of L

f is Element of the carrier of L

bool the carrier of L is non empty set

{X,f} is non empty Element of bool the carrier of L

b is non empty strongly_connected Element of bool the carrier of L

Z1 is Element of the carrier of L

L is non empty V117() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

X is Element of the carrier of L

f is Element of the carrier of L

{X,f} is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

b is Element of the carrier of L

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

Bottom L is Element of the carrier of L

X is Element of the carrier of L

{(Bottom L),X} is non empty V43() Element of bool the carrier of L

bool the carrier of L is non empty set

card {(Bottom L),X} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is non empty V43() strongly_connected (L, Bottom L,X)

card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

card the carrier of L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() ext-real set

b is non empty V43() strongly_connected (L, Bottom L,X)

card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() ext-real set

b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z is non empty V43() strongly_connected (L, Bottom L,X)

card Z is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

r2 is non empty V43() strongly_connected (L, Bottom L,X)

card r2 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is non empty V43() strongly_connected (L, Bottom L,X)

card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is non empty V43() strongly_connected (L, Bottom L,X)

card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z1 is non empty V43() strongly_connected (L, Bottom L,X)

card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z1 is non empty V43() strongly_connected (L, Bottom L,X)

card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z is non empty V43() strongly_connected (L, Bottom L,X)

card Z is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

X is Element of the carrier of L

f is Element of the carrier of L

(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Bottom L is Element of the carrier of L

b is non empty V43() strongly_connected (L, Bottom L,X)

card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is non empty V43() strongly_connected (L, Bottom L,X)

card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is non empty V43() strongly_connected (L, Bottom L,X)

card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

{f} is non empty V43() Element of bool the carrier of L

bool the carrier of L is non empty set

b \/ {f} is non empty V43() Element of bool the carrier of L

card (b \/ {f}) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(card b) + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]

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

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

Z is set

r2 is set

[Z,r2] is set

{Z,r2} is non empty set

{Z} is non empty set

{{Z,r2},{Z}} is non empty set

[r2,Z] is set

{r2,Z} is non empty set

{r2} is non empty set

{{r2,Z},{r2}} is non empty set

y is Element of the carrier of L

a is Element of the carrier of L

y is Element of the carrier of L

y is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

Z is Element of the carrier of L

(L,X) + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

X is V43() strongly_connected Element of bool the carrier of L

f is Element of the carrier of L

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

X is V43() strongly_connected Element of bool the carrier of L

f is Element of the carrier of L

b is Element of the carrier of L

(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

X is V43() strongly_connected Element of bool the carrier of L

f is Element of the carrier of L

b is Element of the carrier of L

(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

Bottom L is Element of the carrier of L

X is Element of the carrier of L

(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

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

bool the carrier of L is non empty set

f is non empty V43() strongly_connected (L, Bottom L, Bottom L)

b is set

Z1 is Element of f

b is set

(L,(Bottom L)) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

card {(Bottom L)} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is non empty V43() strongly_connected (L, Bottom L, Bottom L)

card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

{(Bottom L),X} is non empty V43() Element of bool the carrier of L

bool the carrier of L is non empty set

f is Element of the carrier of L

card {(Bottom L),X} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

X is Element of the carrier of L

(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Bottom L is Element of the carrier of L

{(Bottom L),X} is non empty V43() Element of bool the carrier of L

bool the carrier of L is non empty set

card {(Bottom L),X} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

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

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

f is Element of the carrier of L

f is Element of the carrier of L

card {(Bottom L),(Bottom L)} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,(Bottom L)) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

F

the carrier of F

L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

X is Element of the carrier of F

(F

f is Element of the carrier of F

(F

X is Element of the carrier of F

(F

L is Element of the carrier of F

X is Element of the carrier of F

X is Element of the carrier of F

(F

0 is empty V23() V24() ext-real non positive non negative V32() V33() V34() V35() V36() V37() V38() Element of NAT

X is Element of the carrier of F

(F

X is Element of the carrier of F

(F

{{}} is non empty set

[:{{}},{{}}:] is non empty set

bool [:{{}},{{}}:] is non empty set

the V7() V10({{}}) V11({{}}) V28({{}}) reflexive antisymmetric transitive Element of bool [:{{}},{{}}:] is V7() V10({{}}) V11({{}}) V28({{}}) reflexive antisymmetric transitive Element of bool [:{{}},{{}}:]

RelStr(# {{}}, the V7() V10({{}}) V11({{}}) V28({{}}) reflexive antisymmetric transitive Element of bool [:{{}},{{}}:] #) is non empty trivial finite 1 -element strict V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() distributive complemented with_suprema with_infima V194() RelStr

f is non empty V117() reflexive transitive antisymmetric with_suprema with_infima RelStr

L is non empty V117() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

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

card the carrier of L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() ext-real set

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Bottom L is Element of the carrier of L

Z1 is non empty V43() strongly_connected (L, Bottom L,b)

card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is set

Bottom L is Element of the carrier of L

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z1 is non empty V43() strongly_connected (L, Bottom L,b)

card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() ext-real set

Z1 is Element of the carrier of L

b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z1 is Element of the carrier of L

(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

X is non empty V43() strongly_connected Element of bool the carrier of L

card the carrier of L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() ext-real set

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Bottom L is Element of the carrier of L

Z1 is non empty V43() strongly_connected (L, Bottom L,b)

card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is set

Bottom L is Element of the carrier of L

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z1 is non empty V43() strongly_connected (L, Bottom L,b)

card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() ext-real set

Z1 is Element of the carrier of L

b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

b is Element of the carrier of L

(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

Z1 is Element of the carrier of L

(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is Element of the carrier of L

b is Element of the carrier of L

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

Bottom L is Element of the carrier of L

X is Element of the carrier of L

(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is non empty V43() strongly_connected (L, Bottom L,X)

card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is non empty V43() strongly_connected (L, Bottom L,X)

card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

f is non empty V43() strongly_connected (L, Bottom L,X)

card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

{X} is non empty V43() Element of bool the carrier of L

bool the carrier of L is non empty set

f \ {X} is V43() Element of bool the carrier of L

the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]

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

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

Z1 is set

Z is set

[Z1,Z] is set

{Z1,Z} is non empty set

{Z1} is non empty set

{{Z1,Z},{Z1}} is non empty set

[Z,Z1] is set

{Z,Z1} is non empty set

{Z} is non empty set

{{Z,Z1},{Z}} is non empty set

r2 is Element of the carrier of L

y is Element of the carrier of L

Z1 is non empty V43() strongly_connected Element of bool the carrier of L

(L,Z1) is Element of the carrier of L

Z is Element of the carrier of L

r2 is Element of the carrier of L

{r2} is non empty V43() Element of bool the carrier of L

f \/ {r2} is non empty V43() Element of bool the carrier of L

a is Element of the carrier of L

(f \ {X}) \/ {X} is non empty V43() Element of bool the carrier of L

a is set

A is set

[a,A] is set

{a,A} is non empty set

{a} is non empty set

{{a,A},{a}} is non empty set

[A,a] is set

{A,a} is non empty set

{A} is non empty set

{{A,a},{A}} is non empty set

y is Element of the carrier of L

a is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

a is Element of the carrier of L

y is Element of the carrier of L

y is Element of the carrier of L

a is Element of the carrier of L

a is Element of the carrier of L

card (f \/ {r2}) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

(card f) + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

L is non empty V117() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

bool the carrier of L is non empty set

X is set

f is Element of the carrier of L

L is non empty V117() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

(L) is Element of bool the carrier of L

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

X is Element of the carrier of L

f is Element of the carrier of L

b is Element of the carrier of L

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

Z1 is Element of the carrier of L

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() distributive with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

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

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

X is Element of the carrier of L

f is Element of the carrier of L

b is Element of the carrier of L

{ b

Z1 is set

Z is set

r2 is Element of the carrier of L

Z is Element of the carrier of L

r2 is Element of the carrier of L

y is Element of the carrier of L

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

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

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

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() distributive with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

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

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

X is Element of the carrier of L

downarrow X is V43() Element of bool the carrier of L

{X} is non empty V43() Element of bool the carrier of L

downarrow {X} is V43() Element of bool the carrier of L

(downarrow X) /\ (L) is V43() Element of bool the carrier of L

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

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

{(Bottom L)} /\ (L) is V43() Element of bool the carrier of L

the Element of {(Bottom L)} /\ (L) is Element of {(Bottom L)} /\ (L)

f is Element of the carrier of L

b is Element of the carrier of L

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

downarrow f is V43() Element of bool the carrier of L

{f} is non empty V43() Element of bool the carrier of L

downarrow {f} is V43() Element of bool the carrier of L

(downarrow f) /\ (L) is V43() Element of bool the carrier of L

downarrow b is V43() Element of bool the carrier of L

{b} is non empty V43() Element of bool the carrier of L

downarrow {b} is V43() Element of bool the carrier of L

(downarrow b) /\ (L) is V43() Element of bool the carrier of L

((downarrow f) /\ (L)) \/ ((downarrow b) /\ (L)) is V43() Element of bool the carrier of L

Z1 is Element of the carrier of L

Z1 "/\" X is Element of the carrier of L

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

Z1 "/\" b is Element of the carrier of L

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

Z1 is Element of the carrier of L

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

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

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

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

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

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() distributive with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

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

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

X is Element of the carrier of L

downarrow X is V43() Element of bool the carrier of L

{X} is non empty V43() Element of bool the carrier of L

downarrow {X} is V43() Element of bool the carrier of L

(downarrow X) /\ (L) is V43() Element of bool the carrier of L

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

f is Element of the carrier of L

downarrow f is V43() Element of bool the carrier of L

{f} is non empty V43() Element of bool the carrier of L

downarrow {f} is V43() Element of bool the carrier of L

(downarrow f) /\ (L) is V43() Element of bool the carrier of L

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

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

L is RelStr

the carrier of L is set

bool the carrier of L is non empty set

{ b

{} L is empty V32() V33() V34() V35() V36() V37() V38() strongly_connected lower upper Element of bool the carrier of L

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() distributive with_suprema with_infima V194() RelStr

the carrier of L is non empty V43() set

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

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

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

((subrelstr (L))) is non empty set

the carrier of (subrelstr (L)) is set

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

{ b

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

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

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

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

f is V7() V10( the carrier of L) Function-like V28( the carrier of L) set

rng f is set

b is set

dom f is V43() Element of bool the carrier of L

Z1 is set

f . Z1 is set

Z is Element of the carrier of L

downarrow Z is V43() Element of bool the carrier of L

{Z} is non empty V43() Element of bool the carrier of L

downarrow {Z} is V43() Element of bool the carrier of L

(downarrow Z) /\ (L) is V43() Element of bool the carrier of L

r2 is Element of bool the carrier of (subrelstr (L))

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

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

A is Element of the carrier of L

y is Element of the carrier of L

dom f is V43() Element of bool the carrier of L

b is V7() V10( the carrier of L) V11( the carrier of (InclPoset ((subrelstr (L))))) Function-like V29( the carrier of L, the carrier of (InclPoset ((subrelstr (L))))) Element of bool [: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):]

Z1 is Element of the carrier of L

Z is Element of the carrier of L

b . Z1 is Element of the carrier of (InclPoset ((subrelstr (L))))

b . Z is Element of the carrier of (InclPoset ((subrelstr (L))))

downarrow Z1 is V43() Element of bool the carrier of L

{Z1} is non empty V43() Element of bool the carrier of L

downarrow {Z1} is V43() Element of bool the carrier of L

(downarrow Z1) /\ (L) is V43() Element of bool the carrier of L

downarrow Z is V43() Element of bool the carrier of L

{Z} is non empty V43() Element of bool the carrier of L

downarrow {Z} is V43() Element of bool the carrier of L

(downarrow Z) /\ (L) is V43() Element of bool the carrier of L

r2 is Element of the carrier of L

downarrow Z1 is V43() Element of bool the carrier of L

{Z1} is non empty V43() Element of bool the carrier of L

downarrow {Z1} is V43() Element of bool the carrier of L

(downarrow Z1) /\ (L) is V43() Element of bool the carrier of L

downarrow Z is V43() Element of bool the carrier of L

{Z} is non empty V43() Element of bool the carrier of L

downarrow {Z} is V43() Element of bool the carrier of L

(downarrow Z) /\ (L) is V43() Element of bool the carrier of L

r2 is V43() Element of bool the carrier of L

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

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

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

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

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

rng b is Element of bool the carrier of (InclPoset ((subrelstr (L))))

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

Z1 is set

Z is Element of bool the carrier of (subrelstr (L))

dom b is V43() Element of bool the carrier of L

r2 is V43() Element of bool the carrier of L

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

y is Element of the carrier of L

b . y is set

downarrow ("\/" (r2,L)) is V43() Element of bool the carrier of L

{("\/" (r2,L))} is non empty V43() Element of bool the carrier of L

downarrow {("\/" (r2,L))} is V43() Element of bool the carrier of L

(downarrow ("\/" (r2,L))) /\ (L) is V43() Element of bool the carrier of L

a is Element of the carrier of L

A is Element of the carrier of L

y is Element of the carrier of L

{A} is non empty V43() Element of bool the carrier of L

{A} "/\" r2 is V43() Element of bool the carrier of L

a is Element of the carrier of L

{ (A "/\" b

x is Element of the carrier of L

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

{A,x} is non empty V43() Element of bool the carrier of L

r9 is Element of the carrier of (subrelstr (L))

x9 is Element of the carrier of (subrelstr (L))

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

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

a is Element of the carrier of L

y is Element of the carrier of L

y is Element of the carrier of L

bool (L) is non empty set

b . y is Element of the carrier of (InclPoset ((subrelstr (L))))

y is set

b . y is set

Z1 is Element of the carrier of L

b . Z1 is Element of the carrier of (InclPoset ((subrelstr (L))))

Z is Element of the carrier of L

b . Z is Element of the carrier of (InclPoset ((subrelstr (L))))

downarrow Z is V43() Element of bool the carrier of L

{Z} is non empty V43() Element of bool the carrier of L

downarrow {Z} is V43() Element of bool the carrier of L

(downarrow Z) /\ (L) is V43() Element of bool the carrier of L

downarrow Z1 is V43() Element of bool the carrier of L

{Z1} is non empty V43() Element of bool the carrier of L

downarrow {Z1} is V43() Element of bool the carrier of L

(downarrow Z1) /\ (L) is V43() Element of bool the carrier of L

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

r2 is V43() Element of bool the carrier of L

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

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

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() distributive with_suprema with_infima V194() RelStr

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

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

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

((subrelstr (L))) is non empty set

the carrier of (subrelstr (L)) is set

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

{ b

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

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

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

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

X is V7() V10( the carrier of L) V11( the carrier of (InclPoset ((subrelstr (L))))) Function-like V29( the carrier of L, the carrier of (InclPoset ((subrelstr (L))))) Element of bool [: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):]

the set is set

bool the set is non empty set

X is non empty set

f is set

b is set

f /\ b is set

f \/ b is set

{{}} is non empty set

L is non empty set

X is set

f is set

X /\ f is set

X \/ f is set

L is non empty RelStr

the carrier of L is non empty set

X is non empty RelStr

the carrier of X is non empty set

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

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

f is V7() V10( the carrier of L) V11( the carrier of X) Function-like V29( the carrier of L, the carrier of X) Element of bool [: the carrier of L, the carrier of X:]

b is Element of the carrier of L

Z1 is Element of the carrier of L

{b,Z1} is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

L is non empty RelStr

the carrier of L is non empty set

X is non empty RelStr

the carrier of X is non empty set

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

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

f is V7() V10( the carrier of L) V11( the carrier of X) Function-like V29( the carrier of L, the carrier of X) Element of bool [: the carrier of L, the carrier of X:]

b is Element of the carrier of L

Z1 is Element of the carrier of L

{b,Z1} is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

L is non empty ()

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

the carrier of (InclPoset L) is non empty set

X is Element of the carrier of (InclPoset L)

f is Element of the carrier of (InclPoset L)

b is Element of the carrier of (InclPoset L)

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

X "/\" (f "\/" b) is Element of the carrier of (InclPoset L)

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

X "/\" b is Element of the carrier of (InclPoset L)

(X "/\" f) "\/" (X "/\" b) is Element of the carrier of (InclPoset L)

X /\ b is set

f \/ b is set

X /\ f is set

Z is Element of the carrier of (InclPoset L)

Z1 is Element of the carrier of (InclPoset L)

X /\ Z1 is set

X "/\" Z1 is Element of the carrier of (InclPoset L)

X /\ (f \/ b) is set

(X /\ f) \/ (X /\ b) is set

r2 is Element of the carrier of (InclPoset L)

Z \/ r2 is set

X is set

f is set

X /\ f is set

b is set

Z1 is set

b \/ Z1 is set

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

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

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

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

((subrelstr (L))) is non empty set

the carrier of (subrelstr (L)) is set

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

{ b

f is set

b is set

f /\ b is set

f \/ b is set

Z1 is Element of bool the carrier of (subrelstr (L))

Z is Element of bool the carrier of (subrelstr (L))

Z \/ Z1 is Element of bool the carrier of (subrelstr (L))

Z1 is Element of bool the carrier of (subrelstr (L))

Z is Element of bool the carrier of (subrelstr (L))

Z /\ Z1 is Element of bool the carrier of (subrelstr (L))

L is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr

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

the carrier of L is non empty V43() set

bool the carrier of L is non empty set

Bottom L is Element of the carrier of L

{ b

( not b

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

((subrelstr (L))) is non empty set

the carrier of (subrelstr (L)) is set

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

{ b

X is set

InclPoset X is strict V117() reflexive transitive antisymmetric RelStr

X is non empty ()

InclPoset X is non empty strict V117() reflexive transitive antisymmetric distributive with_suprema with_infima RelStr

the carrier of L is non empty V43() set

the carrier of (InclPoset X) is non empty set

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

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

f is V7() V10( the carrier of L) V11( the carrier of (InclPoset X)) Function-like V29( the carrier of L, the carrier of (InclPoset X)) Element of bool [: the carrier of L, the carrier of (InclPoset X):]