:: 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₁() is non empty finite V117() reflexive transitive antisymmetric lower-bounded upper-bounded V124() with_suprema with_infima V194() RelStr
the carrier of F₁() is non empty V43() set
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₁(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is Element of the carrier of F₁()
(F₁(),f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
X is Element of the carrier of F₁()
(F₁(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
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₁(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
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 V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
X is Element of the carrier of F₁()
(F₁(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
{{}} 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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of the carrier of L : ( b₁ < X & not b₁ <= f ) } is set
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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of bool the carrier of L : b₁ is lower } is set
{} 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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of bool the carrier of (subrelstr (L)) : b₁ is lower } is set
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₁) where b₁ is Element of the carrier of L : b₁ in r2 } is set
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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of bool the carrier of (subrelstr (L)) : b₁ is lower } is set
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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of bool the carrier of (subrelstr (L)) : b₁ is lower } is set
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₁ where b₁ is Element of the carrier of L : ( not b₁ = Bottom L & ( for b₂, b₃ being Element of the carrier of L holds
( not b₁ = b₂ "\/" b₃ or b₁ = b₂ or b₁ = b₃ ) ) ) } is set
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₁ where b₁ is Element of bool the carrier of (subrelstr (L)) : b₁ is lower } is set
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):]