:: LATTICE6 semantic presentation

REAL is set

NAT is non empty non trivial V26() V27() V28() non finite V40() V41() Element of bool REAL

bool REAL is set

NAT is non empty non trivial V26() V27() V28() non finite V40() V41() set

bool NAT is non trivial non finite set

bool NAT is non trivial non finite set

2 is non empty V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

[:2,2:] is Relation-like finite set

[:[:2,2:],2:] is Relation-like finite set

bool [:[:2,2:],2:] is finite V39() set

COMPLEX is set

RAT is set

INT is set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real set

1 is non empty V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

{{},1} is non empty finite V39() set

3 is non empty V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg 1 is non empty trivial finite V42(1) Element of bool NAT

{1} is non empty trivial finite V39() V42(1) set

Seg 2 is non empty finite V42(2) Element of bool NAT

{1,2} is non empty finite V39() set

len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real set

BooleLatt {} is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V145() complemented Boolean complete LattStr

the carrier of (BooleLatt {}) is non empty set

bool {} is finite V39() set

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

the carrier of L is non empty finite set

bool the carrier of L is finite V39() set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

a is finite Element of bool the carrier of L

X is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

X + 1 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

D9 is Element of bool the carrier of (LattPOSet G)

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

q . 1 is set

h is set

dom q is finite Element of bool NAT

u is Element of the carrier of (LattPOSet G)

{u} is non empty trivial finite V42(1) set

v is Element of the carrier of (LattPOSet G)

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

D9 is Element of bool the carrier of (LattPOSet G)

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

D9 is Element of bool the carrier of (LattPOSet G)

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg X is finite V42(X) Element of bool NAT

q | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (q | (Seg X)) is finite set

v is set

len (q | (Seg X)) is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

v is Element of the carrier of (LattPOSet G)

q . (X + 1) is set

b is set

Seg (X + 1) is finite V42(X + 1) Element of bool NAT

dom q is finite Element of bool NAT

a2 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

x is Element of the carrier of (LattPOSet G)

n is set

q . n is set

n is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

dom (q | (Seg X)) is finite Element of bool NAT

(q | (Seg X)) . n is set

n is set

q . n is set

n is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

dom (q | (Seg X)) is finite Element of bool NAT

(q | (Seg X)) . n is set

a2 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

a2 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

D9 is Element of bool the carrier of (LattPOSet G)

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

X is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet X is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet X) is non empty set

bool the carrier of (LattPOSet X) is set

G is Element of bool the carrier of (LattPOSet X)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( 0 ) V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of bool NAT

dom D9 is finite Element of bool NAT

LattRel L is Relation-like V16( the carrier of L) finite V201() V204() V208() Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like finite set

bool [: the carrier of L, the carrier of L:] is finite V39() set

RelStr(# the carrier of L,(LattRel L) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

bool the carrier of (LattPOSet L) is set

X is finite Element of bool the carrier of L

G is finite Element of bool the carrier of (LattPOSet L)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

dom D9 is finite Element of bool NAT

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg (len D9) is finite V42( len D9) Element of bool NAT

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

the carrier of L is non empty finite set

bool the carrier of L is finite V39() set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

a is finite Element of bool the carrier of L

X is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

X + 1 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

D9 is Element of bool the carrier of (LattPOSet G)

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

q . 1 is set

h is set

dom q is finite Element of bool NAT

u is Element of the carrier of (LattPOSet G)

{u} is non empty trivial finite V42(1) set

v is Element of the carrier of (LattPOSet G)

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

D9 is Element of bool the carrier of (LattPOSet G)

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

D9 is Element of bool the carrier of (LattPOSet G)

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg X is finite V42(X) Element of bool NAT

q | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (q | (Seg X)) is finite set

v is set

len (q | (Seg X)) is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

v is Element of the carrier of (LattPOSet G)

q . (X + 1) is set

b is set

Seg (X + 1) is finite V42(X + 1) Element of bool NAT

dom q is finite Element of bool NAT

a2 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

x is Element of the carrier of (LattPOSet G)

n is set

q . n is set

n is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

dom (q | (Seg X)) is finite Element of bool NAT

(q | (Seg X)) . n is set

n is set

q . n is set

n is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

dom (q | (Seg X)) is finite Element of bool NAT

(q | (Seg X)) . n is set

a2 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

a2 is Element of the carrier of (LattPOSet G)

x9 is Element of the carrier of (LattPOSet G)

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

D9 is Element of bool the carrier of (LattPOSet G)

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

X is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet X is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet X) is non empty set

bool the carrier of (LattPOSet X) is set

G is Element of bool the carrier of (LattPOSet X)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( 0 ) V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of bool NAT

dom D9 is finite Element of bool NAT

LattRel L is Relation-like V16( the carrier of L) finite V201() V204() V208() Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like finite set

bool [: the carrier of L, the carrier of L:] is finite V39() set

RelStr(# the carrier of L,(LattRel L) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

bool the carrier of (LattPOSet L) is set

X is finite Element of bool the carrier of L

G is finite Element of bool the carrier of (LattPOSet L)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

dom D9 is finite Element of bool NAT

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg (len D9) is finite V42( len D9) Element of bool NAT

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

the carrier of L is non empty finite set

bool the carrier of L is finite V39() set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

a is finite Element of bool the carrier of L

X is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

X + 1 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

D9 is Element of bool the carrier of (LattPOSet G)

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

q . 1 is set

h is set

dom q is finite Element of bool NAT

u is Element of the carrier of (LattPOSet G)

{u} is non empty trivial finite V42(1) set

v is Element of the carrier of (LattPOSet G)

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

D9 is Element of bool the carrier of (LattPOSet G)

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

D9 is Element of bool the carrier of (LattPOSet G)

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

q . (X + 1) is set

h is set

Seg X is finite V42(X) Element of bool NAT

q | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (q | (Seg X)) is finite set

b is set

len (q | (Seg X)) is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

b is Element of the carrier of (LattPOSet G)

Seg (X + 1) is finite V42(X + 1) Element of bool NAT

dom q is finite Element of bool NAT

a2 is Element of the carrier of (LattPOSet G)

% a2 is Element of the carrier of G

the carrier of G is non empty finite set

(% a2) % is Element of the carrier of (LattPOSet G)

% b is Element of the carrier of G

(% b) "\/" (% a2) is Element of the carrier of G

(% b) "\/" ((% b) "\/" (% a2)) is Element of the carrier of G

(% b) "\/" (% b) is Element of the carrier of G

((% b) "\/" (% b)) "\/" (% a2) is Element of the carrier of G

(% a2) "\/" ((% b) "\/" (% a2)) is Element of the carrier of G

(% a2) "\/" (% a2) is Element of the carrier of G

((% a2) "\/" (% a2)) "\/" (% b) is Element of the carrier of G

(% a2) "\/" (% b) is Element of the carrier of G

(% b) % is Element of the carrier of (LattPOSet G)

((% b) "\/" (% a2)) % is Element of the carrier of (LattPOSet G)

x is Element of the carrier of (LattPOSet G)

n is set

q . n is set

n is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

dom (q | (Seg X)) is finite Element of bool NAT

(dom q) /\ (Seg X) is finite Element of bool NAT

(Seg (X + 1)) /\ (Seg X) is finite Element of bool NAT

(q | (Seg X)) . n is set

G is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet G is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet G) is non empty set

bool the carrier of (LattPOSet G) is set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng q is finite set

D9 is Element of bool the carrier of (LattPOSet G)

len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

X is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet X is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet X) is non empty set

bool the carrier of (LattPOSet X) is set

G is Element of bool the carrier of (LattPOSet X)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg (len D9) is finite V42( len D9) Element of bool NAT

dom D9 is finite Element of bool NAT

LattRel L is Relation-like V16( the carrier of L) finite V201() V204() V208() Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like finite set

bool [: the carrier of L, the carrier of L:] is finite V39() set

RelStr(# the carrier of L,(LattRel L) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

bool the carrier of (LattPOSet L) is set

X is finite Element of bool the carrier of L

G is finite Element of bool the carrier of (LattPOSet L)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

dom D9 is finite Element of bool NAT

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg (len D9) is finite V42( len D9) Element of bool NAT

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

the carrier of L is non empty finite set

bool the carrier of L is finite V39() set

a is finite Element of bool the carrier of L

X is Element of the carrier of (LattPOSet L)

G is Element of the carrier of (LattPOSet L)

LattRel L is Relation-like V16( the carrier of L) finite V201() V204() V208() Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like finite set

bool [: the carrier of L, the carrier of L:] is finite V39() set

RelStr(# the carrier of L,(LattRel L) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() LattStr

the carrier of L is non empty finite set

bool the carrier of L is finite V39() set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

bool the carrier of (LattPOSet L) is set

a is finite Element of bool the carrier of L

X is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

X + 1 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

G is finite Element of bool the carrier of (LattPOSet L)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg X is finite V42(X) Element of bool NAT

D9 | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (D9 | (Seg X)) is finite set

u is set

len (D9 | (Seg X)) is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

u is Element of the carrier of (LattPOSet L)

D9 . (X + 1) is set

v is set

Seg (X + 1) is finite V42(X + 1) Element of bool NAT

dom D9 is finite Element of bool NAT

b is Element of the carrier of (LattPOSet L)

% b is Element of the carrier of L

(% b) % is Element of the carrier of (LattPOSet L)

% u is Element of the carrier of L

(% u) "/\" (% b) is Element of the carrier of L

((% u) "/\" (% b)) "\/" (% u) is Element of the carrier of L

((% u) "/\" (% b)) "\/" (% b) is Element of the carrier of L

(% u) % is Element of the carrier of (LattPOSet L)

((% u) "/\" (% b)) % is Element of the carrier of (LattPOSet L)

x9 is Element of the carrier of (LattPOSet L)

x is set

D9 . x is set

n is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

dom (D9 | (Seg X)) is finite Element of bool NAT

(dom D9) /\ (Seg X) is finite Element of bool NAT

(Seg (X + 1)) /\ (Seg X) is finite Element of bool NAT

(D9 | (Seg X)) . n is set

x9 is Element of the carrier of (LattPOSet L)

% x9 is Element of the carrier of L

(% x9) % is Element of the carrier of (LattPOSet L)

x is Element of the carrier of (LattPOSet L)

(% x9) "/\" ((% u) "/\" (% b)) is Element of the carrier of L

(% x9) "/\" (% u) is Element of the carrier of L

((% x9) "/\" (% u)) "/\" (% b) is Element of the carrier of L

(% x9) "/\" (% b) is Element of the carrier of L

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

G is finite Element of bool the carrier of (LattPOSet L)

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() finite finite-yielding V39() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V106() ext-real Element of NAT

X is finite Element of bool the carrier of (LattPOSet L)

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng G is finite set

len G is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg (len G) is finite V42( len G) Element of bool NAT

dom G is finite Element of bool NAT

D9 is Element of the carrier of (LattPOSet L)

q is Element of the carrier of (LattPOSet L)

q is Element of the carrier of (LattPOSet L)

D9 is Element of the carrier of (LattPOSet L)

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng G is finite set

X is finite Element of bool the carrier of (LattPOSet L)

len G is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

LattRel L is Relation-like V16( the carrier of L) finite V201() V204() V208() Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like finite set

bool [: the carrier of L, the carrier of L:] is finite V39() set

RelStr(# the carrier of L,(LattRel L) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

X is finite Element of bool the carrier of L

G is finite Element of bool the carrier of (LattPOSet L)

D9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D9 is finite set

dom D9 is finite Element of bool NAT

len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

Seg (len D9) is finite V42( len D9) Element of bool NAT

q is Element of the carrier of (LattPOSet L)

% q is Element of the carrier of L

h is Element of the carrier of L

h % is Element of the carrier of (LattPOSet L)

u is Element of the carrier of (LattPOSet L)

v is Element of the carrier of L

v % is Element of the carrier of (LattPOSet L)

(% q) % is Element of the carrier of (LattPOSet L)

h is Element of the carrier of L

(% q) % is Element of the carrier of (LattPOSet L)

u is Element of the carrier of (LattPOSet L)

h % is Element of the carrier of (LattPOSet L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of L is non empty set

bool the carrier of L is set

a is Element of bool the carrier of L

{ (b

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

bool the carrier of (LattPOSet L) is set

G is set

D9 is Element of the carrier of L

D9 % is Element of the carrier of (LattPOSet 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 V157() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

bool the carrier of (LattPOSet L) is set

a is Element of bool the carrier of (LattPOSet L)

{ (% b

the carrier of L is non empty set

bool the carrier of L is set

G is set

D9 is Element of the carrier of (LattPOSet L)

% D9 is Element of the carrier of L

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

a is set

the carrier of (LattPOSet L) is non empty set

the InternalRel of (LattPOSet L) is Relation-like V16( the carrier of (LattPOSet L)) V201() V204() V208() Element of bool [: the carrier of (LattPOSet L), the carrier of (LattPOSet L):]

[: the carrier of (LattPOSet L), the carrier of (LattPOSet L):] is Relation-like set

bool [: the carrier of (LattPOSet L), the carrier of (LattPOSet L):] is set

the carrier of L is non empty finite set

LattRel L is Relation-like V16( the carrier of L) finite V201() V204() V208() Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like finite set

bool [: the carrier of L, the carrier of L:] is finite V39() set

RelStr(# the carrier of L,(LattRel L) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

bool the carrier of L is finite V39() set

G is finite Element of bool the carrier of L

D9 is Element of the carrier of (LattPOSet L)

q is Element of the carrier of (LattPOSet L)

[q,D9] is set

the InternalRel of (LattPOSet L) -Seg D9 is set

Coim ( the InternalRel of (LattPOSet L),D9) is set

{D9} is non empty trivial finite V42(1) set

(Coim ( the InternalRel of (LattPOSet L),D9)) \ {D9} is Element of bool (Coim ( the InternalRel of (LattPOSet L),D9))

bool (Coim ( the InternalRel of (LattPOSet L),D9)) is set

( the InternalRel of (LattPOSet L) -Seg D9) /\ G is finite Element of bool the carrier of L

the Element of ( the InternalRel of (LattPOSet L) -Seg D9) /\ G is Element of ( the InternalRel of (LattPOSet L) -Seg D9) /\ G

[ the Element of ( the InternalRel of (LattPOSet L) -Seg D9) /\ G,D9] is set

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded RelStr

(LattPOSet L) ~ is non empty strict V157() reflexive transitive antisymmetric RelStr

the carrier of (LattPOSet L) is non empty set

the InternalRel of (LattPOSet L) is Relation-like V16( the carrier of (LattPOSet L)) V201() V204() V208() Element of bool [: the carrier of (LattPOSet L), the carrier of (LattPOSet L):]

[: the carrier of (LattPOSet L), the carrier of (LattPOSet L):] is Relation-like set

bool [: the carrier of (LattPOSet L), the carrier of (LattPOSet L):] is set

the InternalRel of (LattPOSet L) ~ is Relation-like V16( the carrier of (LattPOSet L)) V201() V204() V208() Element of bool [: the carrier of (LattPOSet L), the carrier of (LattPOSet L):]

RelStr(# the carrier of (LattPOSet L),( the InternalRel of (LattPOSet L) ~) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

the carrier of ((LattPOSet L) ~) is non empty set

the InternalRel of ((LattPOSet L) ~) is Relation-like V16( the carrier of ((LattPOSet L) ~)) V201() V204() V208() Element of bool [: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):]

[: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):] is Relation-like set

bool [: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):] is set

X is set

the carrier of L is non empty finite set

LattRel L is Relation-like V16( the carrier of L) finite V201() V204() V208() Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like finite set

bool [: the carrier of L, the carrier of L:] is finite V39() set

RelStr(# the carrier of L,(LattRel L) #) is non empty strict V157() reflexive transitive antisymmetric RelStr

bool the carrier of L is finite V39() set

G is finite Element of bool the carrier of L

D9 is Element of the carrier of (LattPOSet L)

q is Element of the carrier of (LattPOSet L)

h is Element of the carrier of ((LattPOSet L) ~)

u is Element of the carrier of ((LattPOSet L) ~)

v is Element of the carrier of (LattPOSet L)

q ~ is Element of the carrier of ((LattPOSet L) ~)

v ~ is Element of the carrier of ((LattPOSet L) ~)

u is Element of the carrier of ((LattPOSet L) ~)

[u,q] is set

the InternalRel of ((LattPOSet L) ~) -Seg q is set

Coim ( the InternalRel of ((LattPOSet L) ~),q) is set

{q} is non empty trivial finite V42(1) set

(Coim ( the InternalRel of ((LattPOSet L) ~),q)) \ {q} is Element of bool (Coim ( the InternalRel of ((LattPOSet L) ~),q))

bool (Coim ( the InternalRel of ((LattPOSet L) ~),q)) is set

( the InternalRel of ((LattPOSet L) ~) -Seg q) /\ G is finite Element of bool the carrier of L

the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg q) /\ G is Element of ( the InternalRel of ((LattPOSet L) ~) -Seg q) /\ G

[ the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg q) /\ G,q] is set

the non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

LattPOSet the non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded RelStr

the non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

LattPOSet the non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded RelStr

(LattPOSet the non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr ) ~ is non empty strict V157() reflexive transitive antisymmetric RelStr

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

L .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric with_suprema with_infima RelStr

(LattPOSet L) ~ is non empty strict V157() reflexive transitive antisymmetric RelStr

LattPOSet (L .:) is non empty strict V157() reflexive transitive antisymmetric with_suprema with_infima RelStr

((LattPOSet L) ~) ~ is non empty strict V157() reflexive transitive antisymmetric RelStr

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded RelStr

(LattPOSet L) ~ is non empty strict V157() reflexive transitive antisymmetric RelStr

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of L is non empty set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of L is non empty set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of L is non empty set

a is Element of the carrier of L

X is Element of the carrier of L

G is Element of the carrier of L

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

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

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

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

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

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

G "\/" a is Element of the carrier of L

(X "\/" a) "\/" (G "\/" a) is Element of the carrier of L

a "\/" G is Element of the carrier of L

a "\/" (a "\/" G) is Element of the carrier of L

X "\/" (a "\/" (a "\/" G)) is Element of the carrier of L

(a "\/" a) "\/" G is Element of the carrier of L

X "\/" ((a "\/" a) "\/" G) is Element of the carrier of L

X "\/" (a "\/" G) is Element of the carrier of L

(X "\/" G) "\/" a is Element of the carrier of L

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

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

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

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

G "/\" a is Element of the carrier of L

(X "/\" a) "/\" (G "/\" a) is Element of the carrier of L

a "/\" (G "/\" a) is Element of the carrier of L

X "/\" (a "/\" (G "/\" a)) is Element of the carrier of L

(a "/\" a) "/\" G is Element of the carrier of L

X "/\" ((a "/\" a) "/\" G) is Element of the carrier of L

a "/\" G is Element of the carrier of L

X "/\" (a "/\" G) is Element of the carrier of L

(X "/\" G) "/\" a is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr

the carrier of L is non empty set

a is Element of the carrier of L

X is Element of the carrier of L

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of (LattPOSet L) is non empty set

X % is Element of the carrier of (LattPOSet L)

% (X %) is Element of the carrier of L

the InternalRel of (LattPOSet L) is Relation-like V16( the carrier of (LattPOSet L)) V201() V204() V208() Element of bool [: the carrier of (LattPOSet L), the carrier of (LattPOSet L):]

[: the carrier of (LattPOSet L), the carrier of (LattPOSet L):] is Relation-like set

bool [: the carrier of (LattPOSet L), the carrier of (LattPOSet L):] is set

G is Element of the carrier of (LattPOSet L)

% G is Element of the carrier of L

(% G) % is Element of the carrier of (LattPOSet L)

D9 is Element of the carrier of L

D9 % is Element of the carrier of (LattPOSet L)

[(D9 %),G] is set

% (D9 %) is Element of the carrier of L

q is Element of the carrier of L

D9 is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr

the carrier of L is non empty set

a is Element of the carrier of L

X is Element of the carrier of L

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric with_suprema with_infima RelStr

(LattPOSet L) ~ is non empty strict V157() reflexive transitive antisymmetric RelStr

the carrier of ((LattPOSet L) ~) is non empty set

X % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

(X %) ~ is Element of the carrier of ((LattPOSet L) ~)

~ ((X %) ~) is Element of the carrier of (LattPOSet L)

% (~ ((X %) ~)) is Element of the carrier of L

the InternalRel of ((LattPOSet L) ~) is Relation-like V16( the carrier of ((LattPOSet L) ~)) V201() V204() V208() Element of bool [: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):]

[: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):] is Relation-like set

bool [: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):] is set

G is Element of the carrier of ((LattPOSet L) ~)

~ G is Element of the carrier of (LattPOSet L)

% (~ G) is Element of the carrier of L

(~ G) ~ is Element of the carrier of ((LattPOSet L) ~)

(% (~ G)) % is Element of the carrier of (LattPOSet L)

D9 is Element of the carrier of L

D9 % is Element of the carrier of (LattPOSet L)

(D9 %) ~ is Element of the carrier of ((LattPOSet L) ~)

~ ((D9 %) ~) is Element of the carrier of (LattPOSet L)

% (~ ((D9 %) ~)) is Element of the carrier of L

[((D9 %) ~),G] is set

q is Element of the carrier of L

D9 is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr

the carrier of L is non empty set

Top L is Element of the carrier of L

a is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded () LattStr

the carrier of L is non empty set

Top L is Element of the carrier of L

a is Element of the carrier of L

X is Element of the carrier of L

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

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

G is Element of the carrier of L

D9 is Element of the carrier of L

X is Element of the carrier of L

G is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

the carrier of L is non empty set

Bottom L is Element of the carrier of L

a is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded () LattStr

the carrier of L is non empty set

Bottom L is Element of the carrier of L

a is Element of the carrier of L

X is Element of the carrier of L

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

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

G is Element of the carrier of L

D9 is Element of the carrier of L

X is Element of the carrier of L

G is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

a is Element of the carrier of L

{ b

"/\" ( { b

{ b

"\/" ( { b

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

a is Element of the carrier of L

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

{ b

"/\" ( { b

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

{ b

"\/" ( { b

G is Element of the carrier of L

D9 is Element of the carrier of L

D9 is Element of the carrier of L

q is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

Top L is Element of the carrier of L

the carrier of L is non empty set

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

{ b

"/\" ( { b

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

(Top L) % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

X is non empty set

the Element of X is Element of X

D9 is Element of the carrier of L

X is Element of the carrier of L

X is Element of the carrier of L

Top (LattPOSet L) is Element of the carrier of (LattPOSet L)

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

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

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

Bottom L is Element of the carrier of L

the carrier of L is non empty set

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

{ b

"\/" ( { b

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

(Bottom L) % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

X is non empty set

the Element of X is Element of X

D9 is Element of the carrier of L

X is Element of the carrier of L

Bottom (LattPOSet L) is Element of the carrier of (LattPOSet L)

G is Element of the carrier of (LattPOSet L)

D9 is Element of the carrier of (LattPOSet L)

G "\/" D9 is Element of the carrier of (LattPOSet L)

X is non empty antisymmetric lower-bounded RelStr

the carrier of X is non empty set

Bottom X is Element of the carrier of X

q is Element of the carrier of X

h is Element of the carrier of X

X is Element of the carrier of L

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

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

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

a is Element of the carrier of L

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

{ b

"/\" ( { b

G is Element of the carrier of L

G is Element of the carrier of L

G is Element of the carrier of L

G is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

a is Element of the carrier of L

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

{ b

"\/" ( { b

G is Element of the carrier of L

G is Element of the carrier of L

G is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () LattStr

the carrier of L is non empty set

a is Element of the carrier of L

{ b

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

"/\" ( { b

G is Element of the carrier of L

G is Element of the carrier of L

D9 is Element of the carrier of L

q is Element of the carrier of L

q is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () LattStr

the carrier of L is non empty set

a is Element of the carrier of L

{ b

G is Element of the carrier of L

D9 is Element of the carrier of L

q is Element of the carrier of L

q is Element of the carrier of L

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

"\/" ( { b

G is Element of the carrier of L

G is Element of the carrier of L

D9 is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

a is Element of the carrier of L

a % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

{ b

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

"/\" ( { b

(L,a) % is Element of the carrier of (LattPOSet L)

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

G is Element of the carrier of (LattPOSet L)

D9 is Element of the carrier of (LattPOSet L)

G "/\" D9 is Element of the carrier of (LattPOSet L)

% G is Element of the carrier of L

(% G) % is Element of the carrier of (LattPOSet L)

% D9 is Element of the carrier of L

(% D9) % is Element of the carrier of (LattPOSet L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of L is non empty set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric with_suprema with_infima RelStr

a is Element of the carrier of L

X is Element of the carrier of L

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

a % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

X % is Element of the carrier of (LattPOSet L)

(a %) "/\" (X %) is Element of the carrier of (LattPOSet L)

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

(a %) "\/" (X %) is Element of the carrier of (LattPOSet L)

G is Element of the carrier of L

G % is Element of the carrier of (LattPOSet L)

D9 is Element of the carrier of (LattPOSet L)

% D9 is Element of the carrier of L

(% D9) % is Element of the carrier of (LattPOSet L)

(% D9) "/\" G is Element of the carrier of L

(% D9) "/\" a is Element of the carrier of L

((% D9) "/\" a) "/\" X is Element of the carrier of L

(% D9) "/\" X is Element of the carrier of L

D9 is Element of the carrier of L

D9 % is Element of the carrier of (LattPOSet L)

q is Element of the carrier of (LattPOSet L)

% q is Element of the carrier of L

(% q) % is Element of the carrier of (LattPOSet L)

(% q) "\/" D9 is Element of the carrier of L

(% q) "\/" a is Element of the carrier of L

((% q) "\/" a) "\/" X is Element of the carrier of L

(% q) "\/" X is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () LattStr

the carrier of L is non empty set

Top L is Element of the carrier of L

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

a is Element of the carrier of L

a % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

X is Element of the carrier of L

G is Element of the carrier of L

G % is Element of the carrier of (LattPOSet L)

X % is Element of the carrier of (LattPOSet L)

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

(G %) "/\" (X %) is Element of the carrier of (LattPOSet L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

a is Element of the carrier of L

a % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

{ b

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

"\/" ( { b

(L,a) % is Element of the carrier of (LattPOSet L)

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

G is Element of the carrier of (LattPOSet L)

D9 is Element of the carrier of (LattPOSet L)

G "\/" D9 is Element of the carrier of (LattPOSet L)

% G is Element of the carrier of L

(% G) % is Element of the carrier of (LattPOSet L)

% D9 is Element of the carrier of L

(% D9) % is Element of the carrier of (LattPOSet L)

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () LattStr

the carrier of L is non empty set

Bottom L is Element of the carrier of L

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

a is Element of the carrier of L

a % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

X is Element of the carrier of L

G is Element of the carrier of L

G % is Element of the carrier of (LattPOSet L)

X % is Element of the carrier of (LattPOSet L)

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

(G %) "\/" (X %) is Element of the carrier of (LattPOSet L)

L is non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () () LattStr

the carrier of L is non empty finite set

a is Element of the carrier of L

Bottom L is Element of the carrier of L

Top L is Element of the carrier of L

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete well_founded RelStr

a % is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of L is non empty set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

a is Element of the carrier of L

{ b

Bottom L is Element of the carrier of L

{(Bottom L)} is non empty trivial finite V42(1) set

G is set

q is Element of the carrier of L

D9 is Element of the carrier of L

q is Element of the carrier of L

G is set

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

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

"\/" ( { b

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

a is Element of the carrier of L

{ b

Top L is Element of the carrier of L

{(Top L)} is non empty trivial finite V42(1) set

G is set

q is Element of the carrier of L

D9 is Element of the carrier of L

q is Element of the carrier of L

G is set

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

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

"/\" ( { b

{{}} is functional non empty trivial finite V39() V42(1) set

[:{{}},{{}}:] is Relation-like finite set

[:[:{{}},{{}}:],{{}}:] is Relation-like finite set

bool [:[:{{}},{{}}:],{{}}:] is finite V39() set

the Relation-like Function-like V20([:{{}},{{}}:],{{}}) finite Element of bool [:[:{{}},{{}}:],{{}}:] is Relation-like Function-like V20([:{{}},{{}}:],{{}}) finite Element of bool [:[:{{}},{{}}:],{{}}:]

LattStr(# {{}}, the Relation-like Function-like V20([:{{}},{{}}:],{{}}) finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like Function-like V20([:{{}},{{}}:],{{}}) finite Element of bool [:[:{{}},{{}}:],{{}}:] #) is non empty strict LattStr

X is non empty LattStr

the carrier of X is non empty set

G is Element of the carrier of X

D9 is Element of the carrier of X

G "/\" D9 is Element of the carrier of X

(G "/\" D9) "\/" D9 is Element of the carrier of X

q is Element of the carrier of X

h is Element of the carrier of X

q "/\" h is Element of the carrier of X

h "/\" q is Element of the carrier of X

G is Element of the carrier of X

D9 is Element of the carrier of X

q is Element of the carrier of X

D9 "/\" q is Element of the carrier of X

G "/\" (D9 "/\" q) is Element of the carrier of X

G "/\" D9 is Element of the carrier of X

(G "/\" D9) "/\" q is Element of the carrier of X

h is Element of the carrier of X

u is Element of the carrier of X

h "\/" u is Element of the carrier of X

h "/\" (h "\/" u) is Element of the carrier of X

G is Element of the carrier of X

D9 is Element of the carrier of X

G "\/" D9 is Element of the carrier of X

D9 "\/" G is Element of the carrier of X

q is Element of the carrier of X

h is Element of the carrier of X

u is Element of the carrier of X

h "\/" u is Element of the carrier of X

q "\/" (h "\/" u) is Element of the carrier of X

q "\/" h is Element of the carrier of X

(q "\/" h) "\/" u is Element of the carrier of X

G is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the non empty trivial finite 1 -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () () LattStr is non empty trivial finite 1 -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () () LattStr

the carrier of the non empty trivial finite 1 -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () () LattStr is non empty trivial finite V42(1) set

a is set

{a} is non empty trivial finite V42(1) set

G is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of G is non empty set

bool the carrier of G is set

D9 is Element of the carrier of G

q is set

q is Element of the carrier of G

X is Element of the carrier of the non empty trivial finite 1 -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () () LattStr

"\/" ({},G) is Element of the carrier of G

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

bool the carrier of L is set

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

bool the carrier of L is set

a is Element of bool the carrier of L

X is Element of the carrier of L

{ b

"\/" ( { b

bool a is set

D9 is Element of bool a

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

q is set

h is Element of the carrier of L

q is Element of the carrier of L

h is Element of the carrier of L

bool a is set

X is Element of the carrier of L

{ b

D9 is set

q is Element of the carrier of L

"\/" ( { b

X is Element of the carrier of L

{ b

"\/" ( { b

G is Element of the carrier of L

{ b

"\/" ( { b

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

bool the carrier of L is set

a is Element of bool the carrier of L

X is Element of the carrier of L

{ b

"/\" ( { b

bool a is set

D9 is Element of bool a

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

q is set

h is Element of the carrier of L

q is Element of the carrier of L

h is Element of the carrier of L

bool a is set

X is Element of the carrier of L

{ b

D9 is set

q is Element of the carrier of L

"/\" ( { b

X is Element of the carrier of L

{ b

"/\" ( { b

G is Element of the carrier of L

{ b

"/\" ( { b

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

bool the carrier of L is set

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

a is Element of bool the carrier of L

(L,a) is Element of bool the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

bool the carrier of (LattPOSet L) is set

{ (b

bool a is set

X is Element of the carrier of L

bool (L,a) is set

X % is Element of the carrier of (LattPOSet L)

G is Element of bool (L,a)

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

D9 is set

D9 is Element of bool the carrier of (LattPOSet L)

(L,D9) is Element of bool the carrier of L

{ (% b

q is Element of the carrier of L

q % is Element of the carrier of (LattPOSet L)

h is Element of the carrier of (LattPOSet L)

% h is Element of the carrier of L

(% h) % is Element of the carrier of (LattPOSet L)

q is set

h is Element of the carrier of (LattPOSet L)

% h is Element of the carrier of L

u is Element of the carrier of L

u % is Element of the carrier of (LattPOSet L)

q is Element of the carrier of L

h is Element of the carrier of (LattPOSet L)

% h is Element of the carrier of L

(% h) % is Element of the carrier of (LattPOSet L)

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

bool (L,a) is set

X is Element of the carrier of (LattPOSet L)

% X is Element of the carrier of L

G is Element of bool a

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

D9 is set

D9 is Element of bool the carrier of L

(L,D9) is Element of bool the carrier of (LattPOSet L)

{ (b

q is Element of the carrier of (LattPOSet L)

% q is Element of the carrier of L

(% q) % is Element of the carrier of (LattPOSet L)

h is Element of the carrier of L

h % is Element of the carrier of (LattPOSet L)

(% X) % is Element of the carrier of (LattPOSet L)

q is set

h is Element of the carrier of L

h % is Element of the carrier of (LattPOSet L)

q is Element of the carrier of (LattPOSet L)

(% X) % is Element of the carrier of (LattPOSet L)

h is Element of the carrier of L

h % is Element of the carrier of (LattPOSet L)

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

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

{ b

bool the carrier of L is set

X is set

G is Element of the carrier of L

{ b

X is set

G is Element of the carrier of L

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

bool the carrier of L is set

(L) is Element of bool the carrier of L

{ b

a is Element of bool the carrier of L

X is set

G is Element of the carrier of L

D9 is Element of the carrier of L

{ b

{ b

u is Element of the carrier of L

u is set

v is Element of the carrier of L

"\/" ( { b

"\/" ( { b

u is Element of the carrier of L

v is Element of the carrier of L

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

{ b

"\/" ( { b

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete LattStr

the carrier of L is non empty set

bool the carrier of L is set

(L) is Element of bool the carrier of L

{ b

a is Element of bool the carrier of L

X is set

G is Element of the carrier of L

D9 is Element of the carrier of L

{ b

{ b

u is Element of the carrier of L

u is set

v is Element of the carrier of L

"/\" ( { b

"/\" ( { b

u is Element of the carrier of L

v is Element of the carrier of L

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

{ b

"/\" ( { b

L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V145() complete () LattStr

(L) is Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is set

{ b

LattPOSet L is non empty strict V157() reflexive transitive antisymmetric lower-bounded upper-bounded V193() V194() with_suprema with_infima complete RelStr

(LattPOSet L) ~ is non empty strict V157() reflexive transitive antisymmetric RelStr

the carrier of ((LattPOSet L) ~) is non empty set

bool (L) is set

the InternalRel of ((LattPOSet L) ~) is Relation-like V16( the carrier of ((LattPOSet L) ~)) V201() V204() V208() Element of bool [: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):]

[: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):] is Relation-like set

bool [: the carrier of ((LattPOSet L) ~), the carrier of ((LattPOSet L) ~):] is set

a is Element of the carrier of ((LattPOSet L) ~)

~ a is Element of the carrier of (LattPOSet L)

the carrier of (LattPOSet L) is non empty set

% (~ a) is Element of the carrier of L

{ b