:: LATTICE5 semantic presentation

REAL is V56() V57() V58() V62() V74() V75() V77() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() V63() V72() V74() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
COMPLEX is V56() V62() set
RAT is V56() V57() V58() V59() V62() set
INT is V56() V57() V58() V59() V60() V62() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() V63() V72() V74() cardinal limit_cardinal set
bool NAT is non empty non empty-membered V63() set
bool NAT is non empty non empty-membered V63() set
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like set
bool [:COMPLEX,REAL:] is non empty set
K322(NAT) is V89() set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V37() ext-real V43() V56() V57() V58() V59() V60() V61() V62() V63() V74() V75() V76() V77() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V91() set
the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V37() ext-real V43() V56() V57() V58() V59() V60() V61() V62() V63() V74() V75() V76() V77() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V91() set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V37() ext-real V43() V56() V57() V58() V59() V60() V61() V62() V63() V74() V75() V76() V77() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V91() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
{{},1} is non empty V56() V57() V58() V59() V60() V61() V72() V74() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty Relation-like V63() set
[:[:NAT,NAT:],NAT:] is non empty Relation-like V63() set
bool [:[:NAT,NAT:],NAT:] is non empty non empty-membered V63() set
K475() is set
K576() is non empty strict LattStr
the carrier of K576() is non empty set
K579() is V56() V57() V58() V59() V60() V61() V74() Element of bool NAT
[:K579(),K579():] is Relation-like set
[:[:K579(),K579():],K579():] is Relation-like set
bool [:[:K579(),K579():],K579():] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V62() V63() V74() V75() V76() V77() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V91() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
L is Relation-like Function-like set
proj1 L is set
A is Relation-like Function-like Function-yielding V91() set
proj2 A is set
union (proj2 A) is set
doms A is Relation-like Function-like set
proj2 (doms A) is set
union (proj2 (doms A)) is set
D is set
L . D is set
[D,(L . D)] is V18() set
{D,(L . D)} is non empty set
{D} is non empty trivial 1 -element set
{{D,(L . D)},{D}} is non empty set
S is set
proj1 A is set
FS is set
A . FS is Relation-like Function-like set
proj1 (doms A) is set
(doms A) . FS is set
proj1 (A . FS) is set
D is set
S is set
proj1 (doms A) is set
FS is set
(doms A) . FS is set
proj1 A is set
A . FS is Relation-like Function-like set
FS is Relation-like Function-like set
proj1 (A . FS) is set
FS . D is set
[D,(FS . D)] is V18() set
{D,(FS . D)} is non empty set
{D} is non empty trivial 1 -element set
{{D,(FS . D)},{D}} is non empty set
L is non empty set
union L is set
A is non empty set
union A is set
[:(union L),(union A):] is Relation-like set
{ [:b₁,b₂:] where b₁ is Element of L, b₂ is Element of A : ( b₁ in L & b₂ in A ) } is set
union { [:b₁,b₂:] where b₁ is Element of L, b₂ is Element of A : ( b₁ in L & b₂ in A ) } is set
S is set
FS is set
FS is set
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
FD is set
f is set
z is Element of L
w is Element of A
[:z,w:] is Relation-like set
S is set
FS is set
FS is Element of L
FD is Element of A
[:FS,FD:] is Relation-like set
f is set
w is set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
L is non empty set
union L is set
[:(union L),(union L):] is Relation-like set
{ [:b₁,b₁:] where b₁ is Element of L : b₁ in L } is set
union { [:b₁,b₁:] where b₁ is Element of L : b₁ in L } is set
{ [:b₁,b₂:] where b₁, b₂ is Element of L : ( b₁ in L & b₂ in L ) } is set
union { [:b₁,b₂:] where b₁, b₂ is Element of L : ( b₁ in L & b₂ in L ) } is set
S is set
FS is set
FS is Element of L
FD is Element of L
[:FS,FD:] is Relation-like set
[:FD,FD:] is Relation-like set
[:FS,FS:] is Relation-like set
S is set
FS is Element of L
[:FS,FS:] is Relation-like set
L is set
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
L is set
(L) is reflexive transitive antisymmetric RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
A is set
L is set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
the carrier of (L) is non empty set
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
the carrier of (LattPOSet (EqRelLatt L)) is non empty set
D is Element of the carrier of (LattPOSet (EqRelLatt L))
% D is Element of the carrier of (EqRelLatt L)
{ b₁ where b₁ is Relation-like L -defined L -valued Element of bool [:L,L:] : b₁ is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:] } is set
S is Relation-like L -defined L -valued Element of bool [:L,L:]
D is Element of the carrier of (EqRelLatt L)
S is Element of the carrier of (L)
L is set
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (EqRelLatt L) is non empty set
A is Element of the carrier of (EqRelLatt L)
D is Element of the carrier of (EqRelLatt L)
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
S is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
S /\ FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
A "/\" D is Element of the carrier of (EqRelLatt L)
the L_meet of (EqRelLatt L) is Relation-like [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] -defined the carrier of (EqRelLatt L) -valued Function-like quasi_total Element of bool [:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
[:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):] is non empty non empty-membered set
the L_meet of (EqRelLatt L) . (S,FS) is set
[S,FS] is V18() set
{S,FS} is non empty set
{S} is non empty trivial 1 -element set
{{S,FS},{S}} is non empty set
the L_meet of (EqRelLatt L) . [S,FS] is set
L is set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
the carrier of (L) is non empty set
A is Element of the carrier of (L)
D is Element of the carrier of (L)
FS is Element of the carrier of (EqRelLatt L)
FS % is Element of the carrier of (LattPOSet (EqRelLatt L))
the carrier of (LattPOSet (EqRelLatt L)) is non empty set
FS is Element of the carrier of (EqRelLatt L)
FS % is Element of the carrier of (LattPOSet (EqRelLatt L))
FS is Element of the carrier of (EqRelLatt L)
FS is Element of the carrier of (EqRelLatt L)
FS % is Element of the carrier of (LattPOSet (EqRelLatt L))
the carrier of (LattPOSet (EqRelLatt L)) is non empty set
FS % is Element of the carrier of (LattPOSet (EqRelLatt L))
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet L is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
K559(L) is Relation-like the carrier of L -defined the carrier of L -valued total 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 Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty non empty-membered set
RelStr(# the carrier of L,K559(L) #) is strict RelStr
the carrier of (LattPOSet L) is non empty set
A is Element of the carrier of (LattPOSet L)
D is Element of the carrier of (LattPOSet L)
A "/\" D is Element of the carrier of (LattPOSet L)
% A is Element of the carrier of L
% D is Element of the carrier of L
(% A) "/\" (% D) is Element of the carrier of L
S is Element of the carrier of L
FS is Element of the carrier of L
S "/\" FS is Element of the carrier of L
(S "/\" FS) % is Element of the carrier of (LattPOSet L)
FS % is Element of the carrier of (LattPOSet L)
FD is Element of the carrier of (LattPOSet L)
S % is Element of the carrier of (LattPOSet L)
f is Element of the carrier of (LattPOSet L)
w is Element of the carrier of L
w % is Element of the carrier of (LattPOSet L)
L is set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
the carrier of (L) is non empty set
A is Element of the carrier of (L)
D is Element of the carrier of (L)
A "/\" D is Element of the carrier of (L)
A /\ D is set
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
S is Element of the carrier of (EqRelLatt L)
FS is Element of the carrier of (EqRelLatt L)
S "/\" FS is Element of the carrier of (EqRelLatt L)
the L_meet of (EqRelLatt L) is Relation-like [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] -defined the carrier of (EqRelLatt L) -valued Function-like quasi_total Element of bool [:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):]
[:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):] is non empty non empty-membered set
FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
FD is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
the L_meet of (EqRelLatt L) . (FS,FD) is set
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
the L_meet of (EqRelLatt L) . [FS,FD] is set
S /\ FS is set
the carrier of (LattPOSet (EqRelLatt L)) is non empty set
FS is Element of the carrier of (LattPOSet (EqRelLatt L))
S is Element of the carrier of (LattPOSet (EqRelLatt L))
FS is Element of the carrier of (EqRelLatt L)
FS % is Element of the carrier of (LattPOSet (EqRelLatt L))
% (FS %) is Element of the carrier of (EqRelLatt L)
FD is Element of the carrier of (EqRelLatt L)
FD % is Element of the carrier of (LattPOSet (EqRelLatt L))
% (FD %) is Element of the carrier of (EqRelLatt L)
FS "/\" FD is Element of the carrier of (EqRelLatt L)
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet L is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
K559(L) is Relation-like the carrier of L -defined the carrier of L -valued total 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 Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty non empty-membered set
RelStr(# the carrier of L,K559(L) #) is strict RelStr
the carrier of (LattPOSet L) is non empty set
A is Element of the carrier of (LattPOSet L)
D is Element of the carrier of (LattPOSet L)
A "\/" D is Element of the carrier of (LattPOSet L)
% A is Element of the carrier of L
% D is Element of the carrier of L
(% A) "\/" (% D) is Element of the carrier of L
S is Element of the carrier of L
FS is Element of the carrier of L
S "\/" FS is Element of the carrier of L
(S "\/" FS) % is Element of the carrier of (LattPOSet L)
FS % is Element of the carrier of (LattPOSet L)
S % is Element of the carrier of (LattPOSet L)
FD is Element of the carrier of (LattPOSet L)
f is Element of the carrier of (LattPOSet L)
w is Element of the carrier of L
w % is Element of the carrier of (LattPOSet L)
L is set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
the carrier of (L) is non empty set
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
A is Element of the carrier of (L)
D is Element of the carrier of (L)
A "\/" D is Element of the carrier of (L)
S is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
S "\/" FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
the carrier of (LattPOSet (EqRelLatt L)) is non empty set
FD is Element of the carrier of (LattPOSet (EqRelLatt L))
FS is Element of the carrier of (LattPOSet (EqRelLatt L))
f is Element of the carrier of (EqRelLatt L)
f % is Element of the carrier of (LattPOSet (EqRelLatt L))
% (f %) is Element of the carrier of (EqRelLatt L)
w is Element of the carrier of (EqRelLatt L)
w % is Element of the carrier of (LattPOSet (EqRelLatt L))
% (w %) is Element of the carrier of (EqRelLatt L)
f "\/" w is Element of the carrier of (EqRelLatt L)
the L_join of (EqRelLatt L) is Relation-like [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] -defined the carrier of (EqRelLatt L) -valued Function-like quasi_total Element of bool [:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):]
[:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [:[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):], the carrier of (EqRelLatt L):] is non empty non empty-membered set
the L_join of (EqRelLatt L) . (f,w) is Element of the carrier of (EqRelLatt L)
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
the L_join of (EqRelLatt L) . [f,w] is set
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty non empty-membered set
A is Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is_<=_than A } is set
S is Element of the carrier of L
FS is Element of the carrier of L
FS is Element of the carrier of L
FD is Element of the carrier of L
f is Element of the carrier of L
FS is Element of the carrier of L
A is set
{ b₁ where b₁ is Element of the carrier of L : A is_<=_than b₁ } is set
S is set
FS is Element of the carrier of L
S is Element of the carrier of L
FS is Element of the carrier of L
FS is Element of the carrier of L
FD is Element of the carrier of L
FS is Element of the carrier of L
L is set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
the carrier of (L) is non empty set
bool the carrier of (L) is non empty non empty-membered set
A is Element of bool the carrier of (L)
A /\ the carrier of (L) is Element of bool the carrier of (L)
[:L,L:] is Relation-like set
bool [:L,L:] is non empty Element of bool (bool [:L,L:])
bool [:L,L:] is non empty set
bool (bool [:L,L:]) is non empty non empty-membered set
S is set
S is Element of bool (bool [:L,L:])
Intersect S is Relation-like L -defined L -valued Element of bool [:L,L:]
FS is Relation-like L -defined L -valued Element of bool [:L,L:]
FS is set
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
FD is set
FS is Relation-like L -defined L -valued Element of bool [:L,L:]
dom FS is Element of bool L
bool L is non empty set
field FS is set
FD is set
f is set
w is set
[FD,f] is V18() set
{FD,f} is non empty set
{FD} is non empty trivial 1 -element set
{{FD,f},{FD}} is non empty set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
[FD,w] is V18() set
{FD,w} is non empty set
{{FD,w},{FD}} is non empty set
z is set
FD is set
f is set
[FD,f] is V18() set
{FD,f} is non empty set
{FD} is non empty trivial 1 -element set
{{FD,f},{FD}} is non empty set
[f,FD] is V18() set
{f,FD} is non empty set
{f} is non empty trivial 1 -element set
{{f,FD},{f}} is non empty set
w is set
FD is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
f is Element of the carrier of (L)
w is Element of the carrier of (L)
c₁₁ is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
z is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
dq9 is set
q is set
[dq9,q] is V18() set
{dq9,q} is non empty set
{dq9} is non empty trivial 1 -element set
{{dq9,q},{dq9}} is non empty set
w is Element of the carrier of (L)
z is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
c₁₁ is Element of the carrier of (L)
c₁₁ is set
dq9 is set
L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
A is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of A is non empty set
[: the carrier of L, the carrier of A:] is non empty Relation-like set
bool [: the carrier of L, the carrier of A:] is non empty non empty-membered set
the Element of the carrier of A is Element of the carrier of A
the carrier of L --> the Element of the carrier of A is non empty Relation-like the carrier of L -defined the carrier of A -valued Function-like constant total quasi_total Element of bool [: the carrier of L, the carrier of A:]
{ the Element of the carrier of A} is non empty trivial 1 -element set
[: the carrier of L,{ the Element of the carrier of A}:] is non empty Relation-like set
S is Relation-like the carrier of L -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of A:]
FS is Element of the carrier of L
FS is Element of the carrier of L
FS "/\" FS is Element of the carrier of L
S . (FS "/\" FS) is Element of the carrier of A
S . FS is Element of the carrier of A
S . FS is Element of the carrier of A
(S . FS) "/\" (S . FS) is Element of the carrier of A
the Element of the carrier of A "/\" the Element of the carrier of A is Element of the carrier of A
(S . FS) "/\" the Element of the carrier of A is Element of the carrier of A
FS is Element of the carrier of L
FS is Element of the carrier of L
FS "\/" FS is Element of the carrier of L
S . (FS "\/" FS) is Element of the carrier of A
S . FS is Element of the carrier of A
S . FS is Element of the carrier of A
(S . FS) "\/" (S . FS) is Element of the carrier of A
the Element of the carrier of A "\/" the Element of the carrier of A is Element of the carrier of A
(S . FS) "\/" the Element of the carrier of A is Element of the carrier of A
L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
the Element of the carrier of L is Element of the carrier of L
{ the Element of the carrier of L} is non empty trivial 1 -element Element of bool the carrier of L
bool the carrier of L is non empty non empty-membered set
[:{ the Element of the carrier of L},{ the Element of the carrier of L}:] is non empty Relation-like set
bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:] is non empty non empty-membered set
the Relation-like { the Element of the carrier of L} -defined { the Element of the carrier of L} -valued Element of bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:] is Relation-like { the Element of the carrier of L} -defined { the Element of the carrier of L} -valued Element of bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:]
S is Element of the carrier of L
FS is Element of the carrier of L
{S,FS} is non empty Element of bool the carrier of L
"\/" ({S,FS},L) is Element of the carrier of L
the Element of the carrier of L "\/" the Element of the carrier of L is Element of the carrier of L
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty non empty-membered set
S is set
FS is set
FS is set
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
[ the Element of the carrier of L, the Element of the carrier of L] is V18() Element of [: the carrier of L, the carrier of L:]
{ the Element of the carrier of L, the Element of the carrier of L} is non empty set
{ the Element of the carrier of L} is non empty trivial 1 -element set
{{ the Element of the carrier of L, the Element of the carrier of L},{ the Element of the carrier of L}} is non empty set
RelStr(# { the Element of the carrier of L}, the Relation-like { the Element of the carrier of L} -defined { the Element of the carrier of L} -valued Element of bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:] #) is non empty trivial V125() 1 -element strict RelStr
S is strict SubRelStr of L
FS is Element of the carrier of L
FS is Element of the carrier of L
{FS,FS} is non empty Element of bool the carrier of L
"/\" ({FS,FS},L) is Element of the carrier of L
the Element of the carrier of L "/\" the Element of the carrier of L is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L is non empty set
A is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of A is non empty set
[: the carrier of L, the carrier of A:] is non empty Relation-like set
bool [: the carrier of L, the carrier of A:] is non empty non empty-membered set
D is Relation-like the carrier of L -defined the carrier of A -valued Function-like quasi_total meet-preserving join-preserving Element of bool [: the carrier of L, the carrier of A:]
Image D is strict reflexive transitive antisymmetric V184(A) SubRelStr of A
rng D is Element of bool the carrier of A
bool the carrier of A is non empty non empty-membered set
subrelstr (rng D) is strict reflexive transitive antisymmetric V184(A) SubRelStr of A
the carrier of (subrelstr (rng D)) is set
dom D is Element of bool the carrier of L
bool the carrier of L is non empty non empty-membered set
FS is Element of the carrier of A
FS is Element of the carrier of A
{FS,FS} is non empty Element of bool the carrier of A
"\/" ({FS,FS},A) is Element of the carrier of A
FD is set
D . FD is set
f is set
D . f is set
w is Element of the carrier of L
z is Element of the carrier of L
{w,z} is non empty Element of bool the carrier of L
D .: {w,z} is Element of bool the carrier of A
"\/" ((D .: {w,z}),A) is Element of the carrier of A
"\/" ({w,z},L) is Element of the carrier of L
D . ("\/" ({w,z},L)) is Element of the carrier of A
FS is Element of the carrier of A
FS is Element of the carrier of A
{FS,FS} is non empty Element of bool the carrier of A
"/\" ({FS,FS},A) is Element of the carrier of A
FD is set
D . FD is set
f is set
D . f is set
w is Element of the carrier of L
z is Element of the carrier of L
{w,z} is non empty Element of bool the carrier of L
D .: {w,z} is Element of bool the carrier of A
"/\" ((D .: {w,z}),A) is Element of the carrier of A
"/\" ({w,z},L) is Element of the carrier of L
D . ("/\" ({w,z},L)) is Element of the carrier of A
L is non empty set
L is non empty set
A is set
D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D |-> A is Relation-like NAT -defined Function-like V63() D -element FinSequence-like FinSubsequence-like set
Seg D is V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() D -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> A is Relation-like Seg D -defined Seg D -defined {A} -valued Function-like constant total total quasi_total V63() FinSequence-like FinSubsequence-like Element of bool [:(Seg D),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
S is Relation-like set
FS is Relation-like set
FS is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
dom FS is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT
FS . 1 is set
len FS is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
FD is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS . FD is set
FD + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS . (FD + 1) is set
[(FS . FD),(FS . (FD + 1))] is V18() set
{(FS . FD),(FS . (FD + 1))} is non empty set
{(FS . FD)} is non empty trivial 1 -element set
{{(FS . FD),(FS . (FD + 1))},{(FS . FD)}} is non empty set
Seg (len FS) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len FS -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len FS ) } is set
Seg (len FS) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len FS -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len FS ) } is set
FS . (len FS) is set
L is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
A + D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
A + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
L is non empty set
A is set
D is set
S is Relation-like set
FS is Relation-like set
FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FD is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
f is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
len f is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
f . (len f) is set
dom f is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT
rng f is non empty Element of bool L
bool L is non empty non empty-membered set
FD - FS is V37() ext-real V43() set
z is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
w is Element of L
z |-> w is Relation-like NAT -defined L -valued Function-like V63() z -element FinSequence-like FinSubsequence-like Element of z -tuples_on L
z -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
L * is non empty functional FinSequence-membered FinSequenceSet of L
{ b₁ where b₁ is Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like Element of L * : len b₁ = z } is set
Seg z is V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() z -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= z ) } is set
(Seg z) --> w is Relation-like Seg z -defined Seg z -defined L -valued {w} -valued Function-like constant total total quasi_total V63() FinSequence-like FinSubsequence-like Element of bool [:(Seg z),{w}:]
{w} is non empty trivial 1 -element set
[:(Seg z),{w}:] is Relation-like set
bool [:(Seg z),{w}:] is non empty set
c₁₁ is Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
dq9 is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
dom dq9 is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT
f ^ dq9 is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
q is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
len q is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
len dq9 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
(len f) + (len dq9) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + (FD - FS) is V37() ext-real V43() set
q . 1 is set
f . 1 is set
q . (len q) is set
q . ((len f) + (len dq9)) is set
dq9 . (len dq9) is set
Q is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
q . Q is set
Q + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
q . (Q + 1) is set
[(q . Q),(q . (Q + 1))] is V18() set
{(q . Q),(q . (Q + 1))} is non empty set
{(q . Q)} is non empty trivial 1 -element set
{{(q . Q),(q . (Q + 1))},{(q . Q)}} is non empty set
Seg (len f) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len f -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
f . (Q + 1) is set
f . Q is set
dq9 . 1 is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
Q - (len f) is V37() ext-real V43() set
(Q - (len f)) + (len f) is V37() ext-real V43() set
0 + (len f) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((len f) + (len dq9)) - (len f) is V37() ext-real V43() set
u is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(Q + 1) - (len f) is V37() ext-real V43() set
dq9 . ((Q + 1) - (len f)) is set
dq9 . (u + 1) is set
Seg (len dq9) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len dq9 -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len dq9 ) } is set
dq9 . u is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
f . (Q + 1) is set
f . Q is set
dq9 . 1 is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
Q - (len f) is V37() ext-real V43() set
(Q - (len f)) + (len f) is V37() ext-real V43() set
0 + (len f) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((len f) + (len dq9)) - (len f) is V37() ext-real V43() set
u is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(Q + 1) - (len f) is V37() ext-real V43() set
dq9 . ((Q + 1) - (len f)) is set
dq9 . (u + 1) is set
Seg (len dq9) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len dq9 -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len dq9 ) } is set
dq9 . u is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
L is non empty set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V183() RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
[:L,L:] is non empty Relation-like set
bool [:L,L:] is non empty non empty-membered set
A is meet-inheriting join-inheriting SubRelStr of (L)
the carrier of A is set
id L is non empty Relation-like L -defined L -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:L,L:]
D is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
S is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : S₁[b₁] } is set
FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
FD is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
field D is set
f is set
w is set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
FS "\/" FD is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
z is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
len z is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
z . 1 is set
z . (len z) is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
c₁₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V63() cardinal set
2 + c₁₁ is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
dq9 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
dq9 + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
q is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT
min q is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(min q) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
len u is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
u . 1 is set
u . (len u) is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(min q) - 1 is V37() ext-real V43() set
((min q) - 1) + 2 is V37() ext-real V43() set
(min q) -' 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real non negative V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((min q) + 1) - 1 is V37() ext-real V43() set
u is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
v is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
a is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
b is set
e is set
[b,e] is V18() set
{b,e} is non empty set
{b} is non empty trivial 1 -element set
{{b,e},{b}} is non empty set
v "\/" a is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FD is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
f is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
w is set
z is set
[w,z] is V18() set
{w,z} is non empty set
{w} is non empty trivial 1 -element set
{{w,z},{w}} is non empty set
FD "\/" f is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
field f is set
field FD is set
c₁₁ is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
dq9 is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
q is set
Q is set
[q,Q] is V18() set
{q,Q} is non empty set
{q} is non empty trivial 1 -element set
{{q,Q},{q}} is non empty set
c₁₁ "\/" dq9 is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
field dq9 is set
field c₁₁ is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(FS + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
len u is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(FS + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
len u is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
L is non empty set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V183() RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
[:L,L:] is non empty Relation-like set
bool [:L,L:] is non empty non empty-membered set
id L is non empty Relation-like L -defined L -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:L,L:]
A is meet-inheriting join-inheriting SubRelStr of (L)
the carrier of A is set
(L,A) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V63() cardinal set
(D + 1) + S is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(D + 1) + FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((D + 1) + FS) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D + FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(D + FS) + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
FS is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
FD is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
f is set
w is set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
FS "\/" FD is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:]
(D + 2) + FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
field FD is set
field FS is set
z is non empty Relation-like NAT -defined L -valued Function-like V63() FinSequence-like FinSubsequence-like FinSequence of L
len z is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
L is non empty set
[:L,L:] is non empty Relation-like set
A is 1-sorted
the carrier of A is set
[:[:L,L:], the carrier of A:] is Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
S is Element of L
FS is Element of L
D . (S,FS) is set
[S,FS] is V18() set
{S,FS} is non empty set
{S} is non empty trivial 1 -element set
{{S,FS},{S}} is non empty set
D . [S,FS] is set
[S,FS] is V18() Element of [:L,L:]
FS is Element of [:L,L:]
D . FS is Element of the carrier of A
L is non empty set
[:L,L:] is non empty Relation-like set
A is 1-sorted
the carrier of A is set
[:[:L,L:], the carrier of A:] is Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty set
L is non empty set
[:L,L:] is non empty Relation-like set
A is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty non empty-membered set
L is non empty set
[:L,L:] is non empty Relation-like set
A is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty non empty-membered set
Bottom A is Element of the carrier of A
[:L,L:] --> (Bottom A) is non empty Relation-like [:L,L:] -defined the carrier of A -valued Function-like constant total quasi_total Element of bool [:[:L,L:], the carrier of A:]
{(Bottom A)} is non empty trivial 1 -element set
[:[:L,L:],{(Bottom A)}:] is non empty Relation-like set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
S is Element of L
FS is Element of L
[S,FS] is V18() Element of [:L,L:]
{S,FS} is non empty set
{S} is non empty trivial 1 -element set
{{S,FS},{S}} is non empty set
D . [S,FS] is Element of the carrier of A
S is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
FS is Element of L
FS is Element of L
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
FS is Element of L
FD is Element of L
(L,A,S,FS,FD) is Element of the carrier of A
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
S . [FS,FD] is set
FS is Element of L
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
(L,A,S,FS,FD) is Element of the carrier of A
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
S . [FS,FD] is set
(L,A,S,FS,FS) "\/" (L,A,S,FS,FD) is Element of the carrier of A
FS is Element of L
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
L is non empty set
[:L,L:] is non empty Relation-like set
A is non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty non empty-membered set
(L) is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V183() RelStr
EqRelLatt L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattPOSet (EqRelLatt L) is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of (EqRelLatt L) is non empty set
K559((EqRelLatt L)) is Relation-like the carrier of (EqRelLatt L) -defined the carrier of (EqRelLatt L) -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):]
[: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty Relation-like set
bool [: the carrier of (EqRelLatt L), the carrier of (EqRelLatt L):] is non empty non empty-membered set
RelStr(# the carrier of (EqRelLatt L),K559((EqRelLatt L)) #) is strict RelStr
the carrier of (L) is non empty set
[: the carrier of A, the carrier of (L):] is non empty Relation-like set
bool [: the carrier of A, the carrier of (L):] is non empty non empty-membered set
bool [:L,L:] is non empty non empty-membered set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total (L,A) (L,A) (L,A) Element of bool [:[:L,L:], the carrier of A:]
S is Element of the carrier of A
FS is Relation-like L -defined L -valued Element of bool [:L,L:]
FS is set
FD is set
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
[FD,FS] is V18() set
{FD,FS} is non empty set
{FD} is non empty trivial 1 -element set
{{FD,FS},{FD}} is non empty set
w is Element of L
f is Element of L
(L,A,D,w,f) is Element of the carrier of A
[w,f] is V18() set
{w,f} is non empty set
{w} is non empty trivial 1 -element set
{{w,f},{w}} is non empty set
D . [w,f] is set
(L,A,D,f,w) is Element of the carrier of A
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
D . [f,w] is set
FS is set
[FS,FS] is V18() set