:: 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₁ %) where b₁ is Element of the carrier of L : b₁ in a } is set
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₁) where b₁ is Element of the carrier of (LattPOSet L) : b₁ in a } is set
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₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } ,L) is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } ,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
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₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } ,L) is Element of the carrier of L
(L,a) is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } ,L) is Element of the carrier of L
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₁ where b₁ is Element of the carrier of L : ( Top L [= b₁ & not b₁ = Top L ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( Top L [= b₁ & not b₁ = Top L ) } ,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
(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₁ where b₁ is Element of the carrier of L : ( b₁ [= Bottom L & not b₁ = Bottom L ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= Bottom L & not b₁ = Bottom L ) } ,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
(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₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } ,L) 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
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₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } ,L) 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
{ b₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } is set
(L,a) is Element of the carrier of L
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } ,L) is Element of the carrier of L
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₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } is set
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₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } ,L) is Element of the carrier of L
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₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } is set
(L,a) is Element of the carrier of L
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } ,L) is Element of the carrier of L
(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₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } is set
(L,a) is Element of the carrier of L
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } ,L) is Element of the carrier of L
(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₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } is set
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₁ where b₁ is Element of the carrier of L : ( b₁ [= a & not b₁ = a ) } ,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
{ b₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } is set
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₁ where b₁ is Element of the carrier of L : ( a [= b₁ & not b₁ = a ) } ,L) is Element of the carrier of L
{{}} 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₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= X ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= X ) } ,L) is Element of the carrier of L
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₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= X ) } is set
D9 is set
q is Element of the carrier of L
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= X ) } ,L) is Element of the carrier of L
X is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= X ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= X ) } ,L) is Element of the carrier of L
G is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= G ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= G ) } ,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
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₁ where b₁ is Element of the carrier of L : ( b₁ in a & X [= b₁ ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & X [= b₁ ) } ,L) is Element of the carrier of L
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₁ where b₁ is Element of the carrier of L : ( b₁ in a & X [= b₁ ) } is set
D9 is set
q is Element of the carrier of L
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & X [= b₁ ) } ,L) is Element of the carrier of L
X is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ( b₁ in a & X [= b₁ ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & X [= b₁ ) } ,L) is Element of the carrier of L
G is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : ( b₁ in a & G [= b₁ ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & G [= b₁ ) } ,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
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₁ %) where b₁ is Element of the carrier of L : b₁ in a } is set
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₁) where b₁ is Element of the carrier of (LattPOSet L) : b₁ in D9 } is set
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₁ %) where b₁ is Element of the carrier of L : b₁ in D9 } is set
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₁ where b₁ is Element of the carrier of L : b₁ is (L) } is set
bool the carrier of L is set
X is set
G is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is (L) } is set
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₁ where b₁ is Element of the carrier of L : b₁ is (L) } is set
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₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= D9 ) } is set
{ b₁ where b₁ is Element of the carrier of L : ( b₁ [= D9 & not b₁ = D9 ) } is set
u is Element of the carrier of L
u is set
v is Element of the carrier of L
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & b₁ [= D9 ) } ,L) is Element of the carrier of L
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= D9 & not b₁ = D9 ) } ,L) is Element of the carrier of L
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₁ where b₁ is Element of the carrier of L : ( b₁ [= G & not b₁ = G ) } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= G & not b₁ = G ) } ,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
bool the carrier of L is set
(L) is Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is (L) } is set
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₁ where b₁ is Element of the carrier of L : ( b₁ in a & D9 [= b₁ ) } is set
{ b₁ where b₁ is Element of the carrier of L : ( D9 [= b₁ & not b₁ = D9 ) } is set
u is Element of the carrier of L
u is set
v is Element of the carrier of L
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( D9 [= b₁ & not b₁ = D9 ) } ,L) is Element of the carrier of L
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ in a & D9 [= b₁ ) } ,L) is Element of the carrier of L
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₁ where b₁ is Element of the carrier of L : ( G [= b₁ & not b₁ = G ) } is set
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( G [= b₁ & not b₁ = G ) } ,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
(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₁ where b₁ is Element of the carrier of L : b₁ is (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
(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₁ where b₁ is Element of the carrier of L : ( % (~ a) [= b₁ & not b₁ = % (~ a) ) } is set
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) ~)
[((G %) ~),a] is set
(% (~ a)) % is Element of the carrier of (LattPOSet L)
((% (~ a)) %) ~ is Element of the carrier of ((LattPOSet L) ~)
D9 is Element of the carrier of L
D9 is Element of the carrier of 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) ~)
[((G %) ~),a] is set
{(% (~ a))} is non empty trivial finite V42(1) set
G is set
"/\" ({(% (~ a))},L) is Element of the carrier of L
("/\" ({(% (~ a))},L)) % is Element of the carrier of (LattPOSet L)
{ b₁ where b₁ is Element of bool (L) : ex b₂ being Element of the carrier of (LattPOSet L) st
( % b₂ in { b₁ where b₃ is Element of the carrier of L : ( % (~ a) [= b₁ & not b₁ = % (~ a) ) } & % b₂ = "/\" (b₁,L) ) } is set
union { b₁ where b₁ is Element of bool (L) : ex b₂ being Element of the carrier of (LattPOSet L) st
( % b₂ in { b₁ where b₃ is Element of the carrier of L : ( % (~ a) [= b₁ & not b₁ = % (~ a) ) } & % b₂ = "/\" (b₁,L) ) } is set
(L,(% (~ a))) is Element of the carrier of L
"/\" ( { b₁ where b₁ is Element of the carrier of L : ( % (~ a) [= b₁ & not b₁ = % (~ a) ) } ,L) is Element of the carrier of 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)
(h %) ~ is Element of the carrier of ((LattPOSet L) ~)
u is Element of bool (L)
"/\" (u,L) is Element of the carrier of L
("/\" (u,L)) % is Element of the carrier of (LattPOSet L)
v is set
% (h %) is Element of the carrier of L
v is Element of the carrier of L
q is set
h is set
u is Element of bool (L)
v is Element of the carrier of (LattPOSet L)
% v is Element of the carrier of L
"/\" (u,L) is Element of the carrier of L
"/\" ((union { b₁ where b₁ is Element of bool (L) : ex b₂ being Element of the carrier of (LattPOSet L) st
( % b₂ in { b₁ where b₃ is Element of the carrier of L : ( % (~ a) [= b₁ & not b₁ = % (~ a) ) } & % b₂ = "/\" (b₁,L) ) } ),L) is Element of the carrier of L
("/\" ((union { b₁ where b₁ is Element of bool (L) : ex b₂ being Element of the carrier of (LattPOSet L) st
( % b₂ in { b₁ where b₃ is Element of the carrier of L : ( % (~ a) [= b₁ & not b₁ = % (~ a) ) } & % b₂ = "/\" (b₁,L) ) } ),L)) % is Element of the carrier of (LattPOSet L)
q is Element of the carrier of L
h is set
"/\" (h,L) is Element of the carrier of L
u is Element of bool (L)
v is Element of the carrier of (LattPOSet L)
% v is Element of the carrier of L
"/\" (u,L) is Element of the carrier of L
u is Element of the carrier of (LattPOSet L)
% u is Element of the carrier of L
a is Element of the carrier of L
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
a % is Element of the carrier of (LattPOSet L)
X is Element of the carrier of ((LattPOSet L) ~)
G is Element of bool (L)
"/\" (G,L) is Element of the carrier of L
("/\" (G,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
(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₁ where b₁ is Element of the carrier of L : b₁ is (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
(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₁ where b₁ is Element of the carrier of L : b₁ is (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
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 L
{ b₁ where b₁ is Element of the carrier of L : ( b₁ [= % a & not b₁ = % a ) } is set
G is Element of the carrier of L
G % is Element of the carrier of (LattPOSet L)
[(G %),a] is set
(% a) % is Element of the carrier of (LattPOSet L)
D9 is Element of the carrier of L
D9 is Element of the carrier of 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 L
[(G %),a] is set
{(% a)} is non empty trivial finite V42(1) set
G is set
"\/" ({(% a)},L) is Element of the carrier of L
{ b₁ where b₁ is Element of bool (L) : ex b₂ being Element of the carrier of (LattPOSet L) st
( % b₂ in { b₁ where b₃ is Element of the carrier of L : ( b₁ [= % a & not b₁ = % a ) } & % b₂ = "\/" (b₁,L) ) } is set
union { b₁ where b₁ is Element of bool (L) : ex b₂ being Element of the carrier of (LattPOSet L) st
( % b₂ in { b₁ where b₃ is Element of the carrier of L : ( b₁ [= % a & not b₁ = % a ) } & % b₂ = "\/" (b₁,L) ) } is set
(L,(% a)) is Element of the carrier of L
"\/" ( { b₁ where b₁ is Element of the carrier of L : ( b₁ [= % a & not b₁ = % a ) } ,L) is Element of the carrier of 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)
% (h %) is Element of the carrier of L
u is Element of bool (L)
"\/" (u,L) is Element of the carrier of L
v is set
v is Element of the carrier of L
q is set
h is set
u is Element of bool (L)
v is Element of the carrier of (LattPOSet L)
% v is Element of the carrier of L
"\/" (u,L) is Element of the carrier of L
q is Element of the carrier of L
h is set
"\/" (h,L) is Element of the carrier of L
u is Element of bool (L)
v is Element of the carrier of (LattPOSet L)
% v is Element of the carrier of L
"\/" (u,L) is Element of the carrier of L
u is Element of the carrier of (LattPOSet L)
% u is Element of the carrier of L
"\/" ((union { b₁ where b₁ is Element of bool (L) : ex b₂ being Element of the carrier of (LattPOSet L) st
( % b₂ in { b₁ where b₃ is Element of the carrier of L : ( b₁ [= % a & not b₁ = % a ) } & % b₂ = "\/" (b₁,L) ) } ),L) is Element of the carrier of L
a is Element of the carrier of L
a % is Element of the carrier of (LattPOSet 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 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₁ where b₁ is Element of the carrier of L : b₁ is (L) } is set