:: 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

union { [:b

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

union { [:b

{ [:b

union { [:b

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

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

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

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

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

c

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

(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

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

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

Seg z is V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() z -element Element of bool NAT

{ b

(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

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

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

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

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

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

2 + c

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

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

field dq9 is set

field c

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