:: LATTICE5 semantic presentation

REAL is V56() V57() V58() V62() V74() V75() V77() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() V63() V72() V74() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
COMPLEX is V56() V62() set
RAT is V56() V57() V58() V59() V62() set
INT is V56() V57() V58() V59() V60() V62() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() V63() V72() V74() cardinal limit_cardinal set
bool NAT is non empty non empty-membered V63() set
bool NAT is non empty non empty-membered V63() set

bool is non empty set

bool is non empty set
K322(NAT) is V89() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
{{},1} is non empty V56() V57() V58() V59() V60() V61() V72() V74() set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is non empty Relation-like V63() set
is non empty Relation-like V63() set
bool is non empty non empty-membered V63() set
K475() is set
K576() is non empty strict LattStr
the carrier of K576() is non empty set
K579() is V56() V57() V58() V59() V60() V61() V74() Element of bool NAT
[:K579(),K579():] is Relation-like set
[:[:K579(),K579():],K579():] is Relation-like set
bool [:[:K579(),K579():],K579():] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real positive V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT

proj1 L is set

proj2 A is set
union () is set

proj2 (doms A) is set
union (proj2 (doms A)) is set
D is set
L . D is set
[D,(L . D)] is V18() set
{D,(L . D)} is non empty set
{D} is non empty trivial 1 -element set
{{D,(L . D)},{D}} is non empty set
S is set
proj1 A is set
FS is set

proj1 (doms A) is set
(doms A) . FS is set
proj1 (A . FS) is set
D is set
S is set
proj1 (doms A) is set
FS is set
(doms A) . FS is set
proj1 A is set

proj1 (A . FS) is set
FS . D is set
[D,(FS . D)] is V18() set
{D,(FS . D)} is non empty set
{D} is non empty trivial 1 -element set
{{D,(FS . D)},{D}} is non empty set
L is non empty set
union L is set
A is non empty set
union A is set
[:(),():] is Relation-like set
{ [:b1,b2:] where b1 is Element of L, b2 is Element of A : ( b1 in L & b2 in A ) } is set
union { [:b1,b2:] where b1 is Element of L, b2 is Element of A : ( b1 in L & b2 in A ) } is set
S is set
FS is set
FS is set
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
FD is set
f is set
z is Element of L
w is Element of A
[:z,w:] is Relation-like set
S is set
FS is set
FS is Element of L
FD is Element of A
[:FS,FD:] is Relation-like set
f is set
w is set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
L is non empty set
union L is set
[:(),():] is Relation-like set
{ [:b1,b1:] where b1 is Element of L : b1 in L } is set
union { [:b1,b1:] where b1 is Element of L : b1 in L } is set
{ [:b1,b2:] where b1, b2 is Element of L : ( b1 in L & b2 in L ) } is set
union { [:b1,b2:] where b1, b2 is Element of L : ( b1 in L & b2 in L ) } is set
S is set
FS is set
FS is Element of L
FD is Element of L
[:FS,FD:] is Relation-like set
[:FD,FD:] is Relation-like set
[:FS,FS:] is Relation-like set
S is set
FS is Element of L
[:FS,FS:] is Relation-like set
L is set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
L is set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
A is set
L is set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
the carrier of (L) is non empty set
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
the carrier of () is non empty set
D is Element of the carrier of ()
% D is Element of the carrier of ()
{ b1 where b1 is Relation-like L -defined L -valued Element of bool [:L,L:] : b1 is Relation-like L -defined L -valued total reflexive symmetric transitive Element of bool [:L,L:] } is set

D is Element of the carrier of ()
S is Element of the carrier of (L)
L is set

the carrier of () is non empty set
A is Element of the carrier of ()
D is Element of the carrier of ()
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set

A "/\" D is Element of the carrier of ()
the L_meet of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty non empty-membered set
the L_meet of () . (S,FS) is set
[S,FS] is V18() set
{S,FS} is non empty set
{S} is non empty trivial 1 -element set
{{S,FS},{S}} is non empty set
the L_meet of () . [S,FS] is set
L is set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
the carrier of (L) is non empty set
A is Element of the carrier of (L)
D is Element of the carrier of (L)
FS is Element of the carrier of ()
FS % is Element of the carrier of ()
the carrier of () is non empty set
FS is Element of the carrier of ()
FS % is Element of the carrier of ()
FS is Element of the carrier of ()
FS is Element of the carrier of ()
FS % is Element of the carrier of ()
the carrier of () is non empty set
FS % is Element of the carrier of ()

the carrier of L is non empty set
K559(L) is Relation-like the carrier of L -defined the carrier of L -valued total reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty non empty-membered set
RelStr(# the carrier of L,K559(L) #) is strict RelStr
the carrier of () is non empty set
A is Element of the carrier of ()
D is Element of the carrier of ()
A "/\" D is Element of the carrier of ()
% A is Element of the carrier of L
% D is Element of the carrier of L
(% A) "/\" (% D) is Element of the carrier of L
S is Element of the carrier of L
FS is Element of the carrier of L
S "/\" FS is Element of the carrier of L
(S "/\" FS) % is Element of the carrier of ()
FS % is Element of the carrier of ()
FD is Element of the carrier of ()
S % is Element of the carrier of ()
f is Element of the carrier of ()
w is Element of the carrier of L
w % is Element of the carrier of ()
L is set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
the carrier of (L) is non empty set
A is Element of the carrier of (L)
D is Element of the carrier of (L)
A "/\" D is Element of the carrier of (L)
A /\ D is set
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
S is Element of the carrier of ()
FS is Element of the carrier of ()
S "/\" FS is Element of the carrier of ()
the L_meet of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty non empty-membered set

the L_meet of () . (FS,FD) is set
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
the L_meet of () . [FS,FD] is set
S /\ FS is set
the carrier of () is non empty set
FS is Element of the carrier of ()
S is Element of the carrier of ()
FS is Element of the carrier of ()
FS % is Element of the carrier of ()
% (FS %) is Element of the carrier of ()
FD is Element of the carrier of ()
FD % is Element of the carrier of ()
% (FD %) is Element of the carrier of ()
FS "/\" FD is Element of the carrier of ()

the carrier of L is non empty set
K559(L) is Relation-like the carrier of L -defined the carrier of L -valued total reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty non empty-membered set
RelStr(# the carrier of L,K559(L) #) is strict RelStr
the carrier of () is non empty set
A is Element of the carrier of ()
D is Element of the carrier of ()
A "\/" D is Element of the carrier of ()
% A is Element of the carrier of L
% D is Element of the carrier of L
(% A) "\/" (% D) is Element of the carrier of L
S is Element of the carrier of L
FS is Element of the carrier of L
S "\/" FS is Element of the carrier of L
(S "\/" FS) % is Element of the carrier of ()
FS % is Element of the carrier of ()
S % is Element of the carrier of ()
FD is Element of the carrier of ()
f is Element of the carrier of ()
w is Element of the carrier of L
w % is Element of the carrier of ()
L is set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
the carrier of (L) is non empty set
[:L,L:] is Relation-like set
bool [:L,L:] is non empty set
A is Element of the carrier of (L)
D is Element of the carrier of (L)
A "\/" D is Element of the carrier of (L)

the carrier of () is non empty set
FD is Element of the carrier of ()
FS is Element of the carrier of ()
f is Element of the carrier of ()
f % is Element of the carrier of ()
% (f %) is Element of the carrier of ()
w is Element of the carrier of ()
w % is Element of the carrier of ()
% (w %) is Element of the carrier of ()
f "\/" w is Element of the carrier of ()
the L_join of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty non empty-membered set
the L_join of () . (f,w) is Element of the carrier of ()
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
the L_join of () . [f,w] is set
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty non empty-membered set
A is Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_<=_than A } is set
S is Element of the carrier of L
FS is Element of the carrier of L
FS is Element of the carrier of L
FD is Element of the carrier of L
f is Element of the carrier of L
FS is Element of the carrier of L
A is set
{ b1 where b1 is Element of the carrier of L : A is_<=_than b1 } is set
S is set
FS is Element of the carrier of L
S is Element of the carrier of L
FS is Element of the carrier of L
FS is Element of the carrier of L
FD is Element of the carrier of L
FS is Element of the carrier of L
L is set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
the carrier of (L) is non empty set
bool the carrier of (L) is non empty non empty-membered set
A is Element of bool the carrier of (L)
A /\ the carrier of (L) is Element of bool the carrier of (L)
[:L,L:] is Relation-like set
bool [:L,L:] is non empty Element of bool (bool [:L,L:])
bool [:L,L:] is non empty set
bool (bool [:L,L:]) is non empty non empty-membered set
S is set
S is Element of bool (bool [:L,L:])

FS is Relation-like L -defined L -valued Element of bool [:L,L:]
FS is set
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
FD is set
FS is Relation-like L -defined L -valued Element of bool [:L,L:]
dom FS is Element of bool L
bool L is non empty set
field FS is set
FD is set
f is set
w is set
[FD,f] is V18() set
{FD,f} is non empty set
{FD} is non empty trivial 1 -element set
{{FD,f},{FD}} is non empty set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
[FD,w] is V18() set
{FD,w} is non empty set
{{FD,w},{FD}} is non empty set
z is set
FD is set
f is set
[FD,f] is V18() set
{FD,f} is non empty set
{FD} is non empty trivial 1 -element set
{{FD,f},{FD}} is non empty set
[f,FD] is V18() set
{f,FD} is non empty set
{f} is non empty trivial 1 -element set
{{f,FD},{f}} is non empty set
w is set

f is Element of the carrier of (L)
w is Element of the carrier of (L)

dq9 is set
q is set
[dq9,q] is V18() set
{dq9,q} is non empty set
{dq9} is non empty trivial 1 -element set
{{dq9,q},{dq9}} is non empty set
w is Element of the carrier of (L)

c11 is Element of the carrier of (L)
c11 is set
dq9 is set

the carrier of L is non empty set

the carrier of A is non empty set
[: the carrier of L, the carrier of A:] is non empty Relation-like set
bool [: the carrier of L, the carrier of A:] is non empty non empty-membered set
the Element of the carrier of A is Element of the carrier of A
the carrier of L --> the Element of the carrier of A is non empty Relation-like the carrier of L -defined the carrier of A -valued Function-like constant total quasi_total Element of bool [: the carrier of L, the carrier of A:]
{ the Element of the carrier of A} is non empty trivial 1 -element set
[: the carrier of L,{ the Element of the carrier of A}:] is non empty Relation-like set
S is Relation-like the carrier of L -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of A:]
FS is Element of the carrier of L
FS is Element of the carrier of L
FS "/\" FS is Element of the carrier of L
S . (FS "/\" FS) is Element of the carrier of A
S . FS is Element of the carrier of A
S . FS is Element of the carrier of A
(S . FS) "/\" (S . FS) is Element of the carrier of A
the Element of the carrier of A "/\" the Element of the carrier of A is Element of the carrier of A
(S . FS) "/\" the Element of the carrier of A is Element of the carrier of A
FS is Element of the carrier of L
FS is Element of the carrier of L
FS "\/" FS is Element of the carrier of L
S . (FS "\/" FS) is Element of the carrier of A
S . FS is Element of the carrier of A
S . FS is Element of the carrier of A
(S . FS) "\/" (S . FS) is Element of the carrier of A
the Element of the carrier of A "\/" the Element of the carrier of A is Element of the carrier of A
(S . FS) "\/" the Element of the carrier of A is Element of the carrier of A

the carrier of L is non empty set
the Element of the carrier of L is Element of the carrier of L
{ the Element of the carrier of L} is non empty trivial 1 -element Element of bool the carrier of L
bool the carrier of L is non empty non empty-membered set
[:{ the Element of the carrier of L},{ the Element of the carrier of L}:] is non empty Relation-like set
bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:] is non empty non empty-membered set
the Relation-like { the Element of the carrier of L} -defined { the Element of the carrier of L} -valued Element of bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:] is Relation-like { the Element of the carrier of L} -defined { the Element of the carrier of L} -valued Element of bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:]
S is Element of the carrier of L
FS is Element of the carrier of L
{S,FS} is non empty Element of bool the carrier of L
"\/" ({S,FS},L) is Element of the carrier of L
the Element of the carrier of L "\/" the Element of the carrier of L is Element of the carrier of L
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty non empty-membered set
S is set
FS is set
FS is set
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
[ the Element of the carrier of L, the Element of the carrier of L] is V18() Element of [: the carrier of L, the carrier of L:]
{ the Element of the carrier of L, the Element of the carrier of L} is non empty set
{ the Element of the carrier of L} is non empty trivial 1 -element set
{{ the Element of the carrier of L, the Element of the carrier of L},{ the Element of the carrier of L}} is non empty set
RelStr(# { the Element of the carrier of L}, the Relation-like { the Element of the carrier of L} -defined { the Element of the carrier of L} -valued Element of bool [:{ the Element of the carrier of L},{ the Element of the carrier of L}:] #) is non empty trivial V125() 1 -element strict RelStr
S is strict SubRelStr of L
FS is Element of the carrier of L
FS is Element of the carrier of L
{FS,FS} is non empty Element of bool the carrier of L
"/\" ({FS,FS},L) is Element of the carrier of L
the Element of the carrier of L "/\" the Element of the carrier of L is Element of the carrier of L

the carrier of L is non empty set

the carrier of A is non empty set
[: the carrier of L, the carrier of A:] is non empty Relation-like set
bool [: the carrier of L, the carrier of A:] is non empty non empty-membered set
D is Relation-like the carrier of L -defined the carrier of A -valued Function-like quasi_total meet-preserving join-preserving Element of bool [: the carrier of L, the carrier of A:]

rng D is Element of bool the carrier of A
bool the carrier of A is non empty non empty-membered set

the carrier of (subrelstr (rng D)) is set
dom D is Element of bool the carrier of L
bool the carrier of L is non empty non empty-membered set
FS is Element of the carrier of A
FS is Element of the carrier of A
{FS,FS} is non empty Element of bool the carrier of A
"\/" ({FS,FS},A) is Element of the carrier of A
FD is set
D . FD is set
f is set
D . f is set
w is Element of the carrier of L
z is Element of the carrier of L
{w,z} is non empty Element of bool the carrier of L
D .: {w,z} is Element of bool the carrier of A
"\/" ((D .: {w,z}),A) is Element of the carrier of A
"\/" ({w,z},L) is Element of the carrier of L
D . ("\/" ({w,z},L)) is Element of the carrier of A
FS is Element of the carrier of A
FS is Element of the carrier of A
{FS,FS} is non empty Element of bool the carrier of A
"/\" ({FS,FS},A) is Element of the carrier of A
FD is set
D . FD is set
f is set
D . f is set
w is Element of the carrier of L
z is Element of the carrier of L
{w,z} is non empty Element of bool the carrier of L
D .: {w,z} is Element of bool the carrier of A
"/\" ((D .: {w,z}),A) is Element of the carrier of A
"/\" ({w,z},L) is Element of the carrier of L
D . ("/\" ({w,z},L)) is Element of the carrier of A
L is non empty set
L is non empty set
A is set
D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

Seg D is V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() D -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set

FS is Relation-like set

dom FS is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT
FS . 1 is set
len FS is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
FD is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS . FD is set
FD + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS . (FD + 1) is set
[(FS . FD),(FS . (FD + 1))] is V18() set
{(FS . FD),(FS . (FD + 1))} is non empty set
{(FS . FD)} is non empty trivial 1 -element set
{{(FS . FD),(FS . (FD + 1))},{(FS . FD)}} is non empty set
Seg (len FS) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len FS -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b1 & b1 <= len FS ) } is set
Seg (len FS) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len FS -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b1 & b1 <= len FS ) } is set
FS . (len FS) is set
L is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
A + D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
A + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
L is non empty set
A is set
D is set

FS is Relation-like set
FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FD is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

len f is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
f . (len f) is set
dom f is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT
rng f is non empty Element of bool L
bool L is non empty non empty-membered set
FD - FS is V37() ext-real V43() set
z is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
w is Element of L

{ } is set
Seg z is V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() z -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b1 & b1 <= z ) } is set

{w} is non empty trivial 1 -element set
[:(Seg z),{w}:] is Relation-like set
bool [:(Seg z),{w}:] is non empty set

dom dq9 is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT

len q is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
len dq9 is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
(len f) + (len dq9) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + (FD - FS) is V37() ext-real V43() set
q . 1 is set
f . 1 is set
q . (len q) is set
q . ((len f) + (len dq9)) is set
dq9 . (len dq9) is set
Q is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
q . Q is set
Q + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
q . (Q + 1) is set
[(q . Q),(q . (Q + 1))] is V18() set
{(q . Q),(q . (Q + 1))} is non empty set
{(q . Q)} is non empty trivial 1 -element set
{{(q . Q),(q . (Q + 1))},{(q . Q)}} is non empty set
Seg (len f) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len f -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
f . (Q + 1) is set
f . Q is set
dq9 . 1 is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
Q - (len f) is V37() ext-real V43() set
(Q - (len f)) + (len f) is V37() ext-real V43() set
0 + (len f) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((len f) + (len dq9)) - (len f) is V37() ext-real V43() set
u is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(Q + 1) - (len f) is V37() ext-real V43() set
dq9 . ((Q + 1) - (len f)) is set
dq9 . (u + 1) is set
Seg (len dq9) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len dq9 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b1 & b1 <= len dq9 ) } is set
dq9 . u is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
f . (Q + 1) is set
f . Q is set
dq9 . 1 is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
Q - (len f) is V37() ext-real V43() set
(Q - (len f)) + (len f) is V37() ext-real V43() set
0 + (len f) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((len f) + (len dq9)) - (len f) is V37() ext-real V43() set
u is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(Q + 1) - (len f) is V37() ext-real V43() set
dq9 . ((Q + 1) - (len f)) is set
dq9 . (u + 1) is set
Seg (len dq9) is non empty V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() len dq9 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : ( 1 <= b1 & b1 <= len dq9 ) } is set
dq9 . u is set
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
L is non empty set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
[:L,L:] is non empty Relation-like set
bool [:L,L:] is non empty non empty-membered set

the carrier of A is set

S is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT : S1[b1] } is set

field D is set
f is set
w is set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set

len z is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
z . 1 is set
z . (len z) is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

2 + c11 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
dq9 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
dq9 + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
q is non empty V56() V57() V58() V59() V60() V61() V72() V74() Element of bool NAT
min q is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(min q) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

len u is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
u . 1 is set
u . (len u) is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(min q) - 1 is V37() ext-real V43() set
((min q) - 1) + 2 is V37() ext-real V43() set
(min q) -' 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real non negative V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((min q) + 1) - 1 is V37() ext-real V43() set
u is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
u + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

b is set
e is set
[b,e] is V18() set
{b,e} is non empty set
{b} is non empty trivial 1 -element set
{{b,e},{b}} is non empty set

FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

w is set
z is set
[w,z] is V18() set
{w,z} is non empty set
{w} is non empty trivial 1 -element set
{{w,z},{w}} is non empty set

field f is set
field FD is set

q is set
Q is set
[q,Q] is V18() set
{q,Q} is non empty set
{q} is non empty trivial 1 -element set
{{q,Q},{q}} is non empty set

field dq9 is set
field c11 is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(FS + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

len u is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(FS + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

len u is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
L is non empty set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
[:L,L:] is non empty Relation-like set
bool [:L,L:] is non empty non empty-membered set

the carrier of A is set
(L,A) is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

(D + 1) + S is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(D + 1) + FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
((D + 1) + FS) + 1 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
D + FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
(D + FS) + 2 is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT

f is set
w is set
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set

(D + 2) + FS is epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V74() V75() V76() cardinal Element of NAT
field FD is set
field FS is set

len z is non empty epsilon-transitive epsilon-connected ordinal natural V37() ext-real V43() V54() V55() V56() V57() V58() V59() V60() V61() V63() V72() V73() V74() V75() V76() cardinal Element of NAT
L is non empty set
[:L,L:] is non empty Relation-like set
A is 1-sorted
the carrier of A is set
[:[:L,L:], the carrier of A:] is Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
S is Element of L
FS is Element of L
D . (S,FS) is set
[S,FS] is V18() set
{S,FS} is non empty set
{S} is non empty trivial 1 -element set
{{S,FS},{S}} is non empty set
D . [S,FS] is set
[S,FS] is V18() Element of [:L,L:]
FS is Element of [:L,L:]
D . FS is Element of the carrier of A
L is non empty set
[:L,L:] is non empty Relation-like set
A is 1-sorted
the carrier of A is set
[:[:L,L:], the carrier of A:] is Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty set
L is non empty set
[:L,L:] is non empty Relation-like set

the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty non empty-membered set
L is non empty set
[:L,L:] is non empty Relation-like set

the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty non empty-membered set
Bottom A is Element of the carrier of A
[:L,L:] --> () is non empty Relation-like [:L,L:] -defined the carrier of A -valued Function-like constant total quasi_total Element of bool [:[:L,L:], the carrier of A:]
{()} is non empty trivial 1 -element set
[:[:L,L:],{()}:] is non empty Relation-like set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
S is Element of L
FS is Element of L
[S,FS] is V18() Element of [:L,L:]
{S,FS} is non empty set
{S} is non empty trivial 1 -element set
{{S,FS},{S}} is non empty set
D . [S,FS] is Element of the carrier of A
S is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
FS is Element of L
FS is Element of L
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
FS is Element of L
FD is Element of L
(L,A,S,FS,FD) is Element of the carrier of A
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
S . [FS,FD] is set
FS is Element of L
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
(L,A,S,FS,FD) is Element of the carrier of A
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
S . [FS,FD] is set
(L,A,S,FS,FS) "\/" (L,A,S,FS,FD) is Element of the carrier of A
FS is Element of L
(L,A,S,FS,FS) is Element of the carrier of A
[FS,FS] is V18() set
{FS,FS} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FS},{FS}} is non empty set
S . [FS,FS] is set
L is non empty set
[:L,L:] is non empty Relation-like set

the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty Relation-like set
bool [:[:L,L:], the carrier of A:] is non empty non empty-membered set

the carrier of () is non empty set
K559(()) is Relation-like the carrier of () -defined the carrier of () -valued total reflexive antisymmetric transitive Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty non empty-membered set
RelStr(# the carrier of (),K559(()) #) is strict RelStr
the carrier of (L) is non empty set
[: the carrier of A, the carrier of (L):] is non empty Relation-like set
bool [: the carrier of A, the carrier of (L):] is non empty non empty-membered set
bool [:L,L:] is non empty non empty-membered set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total (L,A) (L,A) (L,A) Element of bool [:[:L,L:], the carrier of A:]
S is Element of the carrier of A
FS is Relation-like L -defined L -valued Element of bool [:L,L:]
FS is set
FD is set
[FS,FD] is V18() set
{FS,FD} is non empty set
{FS} is non empty trivial 1 -element set
{{FS,FD},{FS}} is non empty set
[FD,FS] is V18() set
{FD,FS} is non empty set
{FD} is non empty trivial 1 -element set
{{FD,FS},{FD}} is non empty set
w is Element of L
f is Element of L
(L,A,D,w,f) is Element of the carrier of A
[w,f] is V18() set
{w,f} is non empty set
{w} is non empty trivial 1 -element set
{{w,f},{w}} is non empty set
D . [w,f] is set
(L,A,D,f,w) is Element of the carrier of A
[f,w] is V18() set
{f,w} is non empty set
{f} is non empty trivial 1 -element set
{{f,w},{f}} is non empty set
D . [f,w] is set
FS is set
[FS,FS] is V18() set