:: LATTICE6 semantic presentation

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

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

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

RAT is set
INT is 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

the carrier of () is non empty set

the carrier of L is non empty finite set
bool the carrier of L is finite V39() set

the carrier of () 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

the carrier of () is non empty set
bool the carrier of () is set
D9 is Element of bool the carrier of ()

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

u is Element of the carrier of ()
{u} is non empty trivial finite V42(1) set
v is Element of the carrier of ()

the carrier of () is non empty set
bool the carrier of () is set

rng q is finite set
D9 is Element of bool the carrier of ()
len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

the carrier of () is non empty set
bool the carrier of () is set
D9 is Element of bool the carrier of ()

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

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 ()
q . (X + 1) is set
b is set
Seg (X + 1) is finite V42(X + 1) Element of bool NAT

a2 is Element of the carrier of ()
x9 is Element of the carrier of ()
x9 is Element of the carrier of ()
x is Element of the carrier of ()
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 ()
x9 is Element of the carrier of ()
a2 is Element of the carrier of ()
x9 is Element of the carrier of ()

the carrier of () is non empty set
bool the carrier of () is set

rng q is finite set
D9 is Element of bool the carrier of ()
len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

the carrier of () is non empty set
bool the carrier of () is set
G is Element of bool the carrier of ()

rng D9 is finite set
len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of 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,() #) is non empty strict V157() reflexive transitive antisymmetric RelStr
bool the carrier of () is set
X is finite Element of bool the carrier of L
G is finite Element of bool the carrier of ()

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

the carrier of L is non empty finite set
bool the carrier of L is finite V39() set

the carrier of () 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

the carrier of () is non empty set
bool the carrier of () is set
D9 is Element of bool the carrier of ()

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

u is Element of the carrier of ()
{u} is non empty trivial finite V42(1) set
v is Element of the carrier of ()

the carrier of () is non empty set
bool the carrier of () is set

rng q is finite set
D9 is Element of bool the carrier of ()
len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

the carrier of () is non empty set
bool the carrier of () is set
D9 is Element of bool the carrier of ()

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

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 ()
q . (X + 1) is set
b is set
Seg (X + 1) is finite V42(X + 1) Element of bool NAT

a2 is Element of the carrier of ()
x9 is Element of the carrier of ()
x9 is Element of the carrier of ()
x is Element of the carrier of ()
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 ()
x9 is Element of the carrier of ()
a2 is Element of the carrier of ()
x9 is Element of the carrier of ()

the carrier of () is non empty set
bool the carrier of () is set

rng q is finite set
D9 is Element of bool the carrier of ()
len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

the carrier of () is non empty set
bool the carrier of () is set
G is Element of bool the carrier of ()

rng D9 is finite set
len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of 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,() #) is non empty strict V157() reflexive transitive antisymmetric RelStr
bool the carrier of () is set
X is finite Element of bool the carrier of L
G is finite Element of bool the carrier of ()

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

the carrier of L is non empty finite set
bool the carrier of L is finite V39() set

the carrier of () 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

the carrier of () is non empty set
bool the carrier of () is set
D9 is Element of bool the carrier of ()

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

u is Element of the carrier of ()
{u} is non empty trivial finite V42(1) set
v is Element of the carrier of ()

the carrier of () is non empty set
bool the carrier of () is set

rng q is finite set
D9 is Element of bool the carrier of ()
len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

the carrier of () is non empty set
bool the carrier of () is set
D9 is Element of bool the carrier of ()

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

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 ()
Seg (X + 1) is finite V42(X + 1) Element of bool NAT

a2 is Element of the carrier of ()
% a2 is Element of the carrier of G
the carrier of G is non empty finite set
(% a2) % is Element of the carrier of ()
% 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 ()
((% b) "\/" (% a2)) % is Element of the carrier of ()
x is Element of the carrier of ()
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

the carrier of () is non empty set
bool the carrier of () is set

rng q is finite set
D9 is Element of bool the carrier of ()
len q is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

the carrier of () is non empty set
bool the carrier of () is set
G is Element of bool the carrier of ()

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,() #) is non empty strict V157() reflexive transitive antisymmetric RelStr
bool the carrier of () is set
X is finite Element of bool the carrier of L
G is finite Element of bool the carrier of ()

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

the carrier of () 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 ()
G is Element of the carrier of ()
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,() #) is non empty strict V157() reflexive transitive antisymmetric RelStr

the carrier of L is non empty finite set
bool the carrier of L is finite V39() set

the carrier of () is non empty set
bool the carrier of () 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 ()

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

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 ()
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 ()
% b is Element of the carrier of L
(% b) % is Element of the carrier of ()
% 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 ()
((% u) "/\" (% b)) % is Element of the carrier of ()
x9 is Element of the carrier of ()
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 ()
% x9 is Element of the carrier of L
(% x9) % is Element of the carrier of ()
x is Element of the carrier of ()
(% 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

rng D9 is finite set
G is finite Element of bool the carrier of ()
len D9 is V26() V27() V28() V32() V33() V34() finite V40() V106() ext-real Element of NAT

X is finite Element of bool the carrier of ()

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

D9 is Element of the carrier of ()
q is Element of the carrier of ()
q is Element of the carrier of ()
D9 is Element of the carrier of ()

rng G is finite set
X is finite Element of bool the carrier of ()
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,() #) 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 ()

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 ()
% q is Element of the carrier of L
h is Element of the carrier of L
h % is Element of the carrier of ()
u is Element of the carrier of ()
v is Element of the carrier of L
v % is Element of the carrier of ()
(% q) % is Element of the carrier of ()
h is Element of the carrier of L
(% q) % is Element of the carrier of ()
u is Element of the carrier of ()
h % is Element of the carrier of ()

the carrier of L is non empty set
bool the carrier of L is set
a is Element of bool the carrier of L
{ (b1 %) where b1 is Element of the carrier of L : b1 in a } is set

the carrier of () is non empty set
bool the carrier of () is set
G is set
D9 is Element of the carrier of L
D9 % is Element of the carrier of ()

the carrier of () is non empty set
bool the carrier of () is set
a is Element of bool the carrier of ()
{ (% b1) where b1 is Element of the carrier of () : b1 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 ()
% D9 is Element of the carrier of L

a is set
the carrier of () is non empty set
the InternalRel of () is Relation-like V16( the carrier of ()) V201() V204() V208() Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like set
bool [: the carrier of (), the carrier of ():] 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,() #) 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 ()
q is Element of the carrier of ()
[q,D9] is set
the InternalRel of () -Seg D9 is set
Coim ( the InternalRel of (),D9) is set
{D9} is non empty trivial finite V42(1) set
(Coim ( the InternalRel of (),D9)) \ {D9} is Element of bool (Coim ( the InternalRel of (),D9))
bool (Coim ( the InternalRel of (),D9)) is set
( the InternalRel of () -Seg D9) /\ G is finite Element of bool the carrier of L
the Element of ( the InternalRel of () -Seg D9) /\ G is Element of ( the InternalRel of () -Seg D9) /\ G
[ the Element of ( the InternalRel of () -Seg D9) /\ G,D9] is set

the carrier of () is non empty set
the InternalRel of () is Relation-like V16( the carrier of ()) V201() V204() V208() Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like set
bool [: the carrier of (), the carrier of ():] is set
the InternalRel of () ~ is Relation-like V16( the carrier of ()) V201() V204() V208() Element of bool [: the carrier of (), the carrier of ():]
RelStr(# the carrier of (),( the InternalRel of () ~) #) is non empty strict V157() reflexive transitive antisymmetric RelStr
the carrier of (() ~) is non empty set
the InternalRel of (() ~) is Relation-like V16( the carrier of (() ~)) V201() V204() V208() Element of bool [: the carrier of (() ~), the carrier of (() ~):]
[: the carrier of (() ~), the carrier of (() ~):] is Relation-like set
bool [: the carrier of (() ~), the carrier of (() ~):] 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,() #) 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 ()
q is Element of the carrier of ()
h is Element of the carrier of (() ~)
u is Element of the carrier of (() ~)
v is Element of the carrier of ()
q ~ is Element of the carrier of (() ~)
v ~ is Element of the carrier of (() ~)
u is Element of the carrier of (() ~)
[u,q] is set
the InternalRel of (() ~) -Seg q is set
Coim ( the InternalRel of (() ~),q) is set
{q} is non empty trivial finite V42(1) set
(Coim ( the InternalRel of (() ~),q)) \ {q} is Element of bool (Coim ( the InternalRel of (() ~),q))
bool (Coim ( the InternalRel of (() ~),q)) is set
( the InternalRel of (() ~) -Seg q) /\ G is finite Element of bool the carrier of L
the Element of ( the InternalRel of (() ~) -Seg q) /\ G is Element of ( the InternalRel of (() ~) -Seg q) /\ G
[ the Element of ( the InternalRel of (() ~) -Seg q) /\ G,q] is set

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

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

the carrier of L is non empty set

the carrier of L is non empty set

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

the carrier of L is non empty set
a is Element of the carrier of L
X is Element of the carrier of L

the carrier of () is non empty set
X % is Element of the carrier of ()
% (X %) is Element of the carrier of L
the InternalRel of () is Relation-like V16( the carrier of ()) V201() V204() V208() Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like set
bool [: the carrier of (), the carrier of ():] is set
G is Element of the carrier of ()
% G is Element of the carrier of L
(% G) % is Element of the carrier of ()
D9 is Element of the carrier of L
D9 % is Element of the carrier of ()
[(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

the carrier of L is non empty set
a is Element of the carrier of L
X is Element of the carrier of L

the carrier of (() ~) is non empty set
X % is Element of the carrier of ()
the carrier of () is non empty set
(X %) ~ is Element of the carrier of (() ~)
~ ((X %) ~) is Element of the carrier of ()
% (~ ((X %) ~)) is Element of the carrier of L
the InternalRel of (() ~) is Relation-like V16( the carrier of (() ~)) V201() V204() V208() Element of bool [: the carrier of (() ~), the carrier of (() ~):]
[: the carrier of (() ~), the carrier of (() ~):] is Relation-like set
bool [: the carrier of (() ~), the carrier of (() ~):] is set
G is Element of the carrier of (() ~)
~ G is Element of the carrier of ()
% (~ G) is Element of the carrier of L
(~ G) ~ is Element of the carrier of (() ~)
(% (~ G)) % is Element of the carrier of ()
D9 is Element of the carrier of L
D9 % is Element of the carrier of ()
(D9 %) ~ is Element of the carrier of (() ~)
~ ((D9 %) ~) is Element of the carrier of ()
% (~ ((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

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

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

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

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

the carrier of L is non empty set
a is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } ,L) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } ,L) is Element of the carrier of L

the carrier of L is non empty set

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
{ b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } ,L) is Element of the carrier of L
(L,a) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = 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

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
{ b1 where b1 is Element of the carrier of L : ( Top L [= b1 & not b1 = Top L ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( Top L [= b1 & not b1 = Top L ) } ,L) is Element of the carrier of L

(Top L) % is Element of the carrier of ()
the carrier of () 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 () is Element of the carrier of ()
"/\" ({},()) is Element of the carrier of ()
"/\" ({},L) is Element of the carrier of L

Bottom L is Element of the carrier of L
the carrier of L is non empty set
(L,()) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 [= Bottom L & not b1 = Bottom L ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= Bottom L & not b1 = Bottom L ) } ,L) is Element of the carrier of L

() % is Element of the carrier of ()
the carrier of () 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 () is Element of the carrier of ()
G is Element of the carrier of ()
D9 is Element of the carrier of ()
G "\/" D9 is Element of the carrier of ()

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
"\/" ({},()) is Element of the carrier of ()
"\/" ({},L) is Element of the carrier of L

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
{ b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = 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

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
{ b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = 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

the carrier of L is non empty set
a is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } is set
(L,a) is Element of the carrier of L
"/\" ( { b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = 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

the carrier of L is non empty set
a is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = 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
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = 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

the carrier of L is non empty set

a is Element of the carrier of L
a % is Element of the carrier of ()
the carrier of () is non empty set
{ b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } is set
(L,a) is Element of the carrier of L
"/\" ( { b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } ,L) is Element of the carrier of L
(L,a) % is Element of the carrier of ()
% (a %) is Element of the carrier of L
G is Element of the carrier of ()
D9 is Element of the carrier of ()
G "/\" D9 is Element of the carrier of ()
% G is Element of the carrier of L
(% G) % is Element of the carrier of ()
% D9 is Element of the carrier of L
(% D9) % is Element of the carrier of ()

the carrier of L is non empty set

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 ()
the carrier of () is non empty set
X % is Element of the carrier of ()
(a %) "/\" (X %) is Element of the carrier of ()
a "\/" X is Element of the carrier of L
(a %) "\/" (X %) is Element of the carrier of ()
G is Element of the carrier of L
G % is Element of the carrier of ()
D9 is Element of the carrier of ()
% D9 is Element of the carrier of L
(% D9) % is Element of the carrier of ()
(% 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 ()
q is Element of the carrier of ()
% q is Element of the carrier of L
(% q) % is Element of the carrier of ()
(% 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

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
a % is Element of the carrier of ()
the carrier of () 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 ()
X % is Element of the carrier of ()
G "/\" X is Element of the carrier of L
(G %) "/\" (X %) is Element of the carrier of ()

the carrier of L is non empty set

a is Element of the carrier of L
a % is Element of the carrier of ()
the carrier of () is non empty set
{ b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } is set
(L,a) is Element of the carrier of L
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } ,L) is Element of the carrier of L
(L,a) % is Element of the carrier of ()
% (a %) is Element of the carrier of L
G is Element of the carrier of ()
D9 is Element of the carrier of ()
G "\/" D9 is Element of the carrier of ()
% G is Element of the carrier of L
(% G) % is Element of the carrier of ()
% D9 is Element of the carrier of L
(% D9) % is Element of the carrier of ()

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
a % is Element of the carrier of ()
the carrier of () 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 ()
X % is Element of the carrier of ()
G "\/" X is Element of the carrier of L
(G %) "\/" (X %) is Element of the carrier of ()

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

a % is Element of the carrier of ()
the carrier of () is non empty set

the carrier of L is non empty set

the carrier of L is non empty set
a is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } is set
Bottom L is Element of the carrier of 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
"\/" ({()},L) is Element of the carrier of L
(L,a) is Element of the carrier of L
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= a & not b1 = a ) } ,L) is Element of the carrier of L

the carrier of L is non empty set
a is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = 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
"/\" ( { b1 where b1 is Element of the carrier of L : ( a [= b1 & not b1 = a ) } ,L) is Element of the carrier of L

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

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

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

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

the carrier of L is non empty set
bool the carrier of L is set

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
{ b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= X ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= 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
{ b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= X ) } is set
D9 is set
q is Element of the carrier of L
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= X ) } ,L) is Element of the carrier of L
X is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= X ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= X ) } ,L) is Element of the carrier of L
G is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= G ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= G ) } ,L) is Element of the carrier of L

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
{ b1 where b1 is Element of the carrier of L : ( b1 in a & X [= b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & X [= b1 ) } ,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
{ b1 where b1 is Element of the carrier of L : ( b1 in a & X [= b1 ) } is set
D9 is set
q is Element of the carrier of L
"/\" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & X [= b1 ) } ,L) is Element of the carrier of L
X is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 in a & X [= b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & X [= b1 ) } ,L) is Element of the carrier of L
G is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 in a & G [= b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & G [= b1 ) } ,L) is Element of the carrier of L

the carrier of L is non empty set
bool the carrier of L is set

a is Element of bool the carrier of L
(L,a) is Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () is set
{ (b1 %) where b1 is Element of the carrier of L : b1 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 ()
G is Element of bool (L,a)
"/\" (G,()) is Element of the carrier of ()
D9 is set
D9 is Element of bool the carrier of ()
(L,D9) is Element of bool the carrier of L
{ (% b1) where b1 is Element of the carrier of () : b1 in D9 } is set
q is Element of the carrier of L
q % is Element of the carrier of ()
h is Element of the carrier of ()
% h is Element of the carrier of L
(% h) % is Element of the carrier of ()
q is set
h is Element of the carrier of ()
% h is Element of the carrier of L
u is Element of the carrier of L
u % is Element of the carrier of ()
q is Element of the carrier of L
h is Element of the carrier of ()
% h is Element of the carrier of L
(% h) % is Element of the carrier of ()
"/\" ((L,D9),L) is Element of the carrier of L
bool (L,a) is set
X is Element of the carrier of ()
% 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 ()
{ (b1 %) where b1 is Element of the carrier of L : b1 in D9 } is set
q is Element of the carrier of ()
% q is Element of the carrier of L
(% q) % is Element of the carrier of ()
h is Element of the carrier of L
h % is Element of the carrier of ()
(% X) % is Element of the carrier of ()
q is set
h is Element of the carrier of L
h % is Element of the carrier of ()
q is Element of the carrier of ()
(% X) % is Element of the carrier of ()
h is Element of the carrier of L
h % is Element of the carrier of ()
"/\" ((L,D9),()) is Element of the carrier of ()

the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : b1 is (L) } is set
bool the carrier of L is set
X is set
G is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is (L) } is set
X is set
G is Element of the carrier of L

the carrier of L is non empty set
bool the carrier of L is set
(L) is Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 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
{ b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= D9 ) } is set
{ b1 where b1 is Element of the carrier of L : ( b1 [= D9 & not b1 = D9 ) } is set
u is Element of the carrier of L
u is set
v is Element of the carrier of L
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & b1 [= D9 ) } ,L) is Element of the carrier of L
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= D9 & not b1 = 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
{ b1 where b1 is Element of the carrier of L : ( b1 [= G & not b1 = G ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 [= G & not b1 = G ) } ,L) is Element of the carrier of L

the carrier of L is non empty set
bool the carrier of L is set
(L) is Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 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
{ b1 where b1 is Element of the carrier of L : ( b1 in a & D9 [= b1 ) } is set
{ b1 where b1 is Element of the carrier of L : ( D9 [= b1 & not b1 = D9 ) } is set
u is Element of the carrier of L
u is set
v is Element of the carrier of L
"/\" ( { b1 where b1 is Element of the carrier of L : ( D9 [= b1 & not b1 = D9 ) } ,L) is Element of the carrier of L
"/\" ( { b1 where b1 is Element of the carrier of L : ( b1 in a & D9 [= b1 ) } ,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
{ b1 where b1 is Element of the carrier of L : ( G [= b1 & not b1 = G ) } is set
"/\" ( { b1 where b1 is Element of the carrier of L : ( G [= b1 & not b1 = G ) } ,L) is Element of the carrier of L

(L) is Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is set
{ b1 where b1 is Element of the carrier of L : b1 is (L) } is set

the carrier of (() ~) is non empty set
bool (L) is set
the InternalRel of (() ~) is Relation-like V16( the carrier of (() ~)) V201() V204() V208() Element of bool [: the carrier of (() ~), the carrier of (() ~):]
[: the carrier of (() ~), the carrier of (() ~):] is Relation-like set
bool [: the carrier of (() ~), the carrier of (() ~):] is set
a is Element of the carrier of (() ~)
~ a is Element of the carrier of ()
the carrier of () is non empty set
% (~ a) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( % (~ a) [= b1 & not b1 = % (~ a) ) } is set