:: NECKLA_2 semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

[:2,2:] is non empty finite set
[:[:2,2:],2:] is non empty finite set
bool [:[:2,2:],2:] is non empty finite V41() set
K385() is set

{0,1,2,3} is non empty finite set

N4 is set
C is set
[:N4,C:] is set
bool [:N4,C:] is non empty set
k is Relation-like N4 -defined C -valued Element of bool [:N4,C:]

the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued Element of bool [: the carrier of (), the carrier of ():]
the carrier of () is set
[: the carrier of (), the carrier of ():] is set
bool [: the carrier of (), the carrier of ():] is non empty set
[0,1] is set
{0,1} is non empty finite V41() set
is non empty trivial finite V41() 1 -element set
{{0,1},} is non empty finite V41() set
[1,0] is set
{1,0} is non empty finite V41() set
{1} is non empty trivial finite V41() 1 -element set
{{1,0},{1}} is non empty finite V41() set
[1,2] is set
{1,2} is non empty finite V41() set
{{1,2},{1}} is non empty finite V41() set
[2,1] is set
{2,1} is non empty finite V41() set
{2} is non empty trivial finite V41() 1 -element set
{{2,1},{2}} is non empty finite V41() set
[2,3] is set
{2,3} is non empty finite V41() set
{{2,3},{2}} is non empty finite V41() set
[3,2] is set
{3,2} is non empty finite V41() set
{3} is non empty trivial finite V41() 1 -element set
{{3,2},{3}} is non empty finite V41() set
{[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} is non empty finite set

[(0 + 1),0] is set
{(0 + 1),0} is non empty finite V41() set
{(0 + 1)} is non empty trivial finite V41() 1 -element set
{{(0 + 1),0},{(0 + 1)}} is non empty finite V41() set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } \/ { [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } is set
C is set
k is set
m is set
[k,m] is set
{k,m} is non empty finite set
{k} is non empty trivial finite 1 -element set
{{k,m},{k}} is non empty finite V41() set

[S,(S + 1)] is set
{S,(S + 1)} is non empty finite V41() set
{S} is non empty trivial finite V41() 1 -element set
{{S,(S + 1)},{S}} is non empty finite V41() set

[(S + 1),S] is set
{(S + 1),S} is non empty finite V41() set
{(S + 1)} is non empty trivial finite V41() 1 -element set
{{(S + 1),S},{(S + 1)}} is non empty finite V41() set

[(2 + 1),(1 + 1)] is set
{(2 + 1),(1 + 1)} is non empty finite V41() set
{(2 + 1)} is non empty trivial finite V41() 1 -element set
{{(2 + 1),(1 + 1)},{(2 + 1)}} is non empty finite V41() set
[(1 + 1),(2 + 1)] is set
{(1 + 1),(2 + 1)} is non empty finite V41() set
{(1 + 1)} is non empty trivial finite V41() 1 -element set
{{(1 + 1),(2 + 1)},{(1 + 1)}} is non empty finite V41() set
[(1 + 1),(0 + 1)] is set
{(1 + 1),(0 + 1)} is non empty finite V41() set
{{(1 + 1),(0 + 1)},{(1 + 1)}} is non empty finite V41() set
[(0 + 1),(1 + 1)] is set
{(0 + 1),(1 + 1)} is non empty finite V41() set
{{(0 + 1),(1 + 1)},{(0 + 1)}} is non empty finite V41() set
[0,(0 + 1)] is set
{0,(0 + 1)} is non empty finite V41() set
{{0,(0 + 1)},} is non empty finite V41() set
C is set

C is Element of Rank R

R is set

R is Element of FinSETS
[:{0,1},{0,1}:] is non empty finite set
bool [:{0,1},{0,1}:] is non empty finite V41() set
id {0,1} is non empty Relation-like set

RelStr(# {0,1},C #) is non empty strict RelStr
k is non empty strict RelStr
the carrier of k is non empty set
[: the carrier of (), the carrier of k:] is set
bool [: the carrier of (), the carrier of k:] is non empty set
m is Relation-like the carrier of () -defined the carrier of k -valued Function-like V29( the carrier of (), the carrier of k) Element of bool [: the carrier of (), the carrier of k:]
dom m is set
m . 3 is set
m . 2 is set
m . 1 is set
the InternalRel of k is Relation-like the carrier of k -defined the carrier of k -valued Element of bool [: the carrier of k, the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
bool [: the carrier of k, the carrier of k:] is non empty set
R is RelStr
the carrier of R is set
N4 is RelStr
the carrier of N4 is set
the carrier of R \/ the carrier of N4 is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of N4 is Relation-like the carrier of N4 -defined the carrier of N4 -valued Element of bool [: the carrier of N4, the carrier of N4:]
[: the carrier of N4, the carrier of N4:] is set
bool [: the carrier of N4, the carrier of N4:] is non empty set
the InternalRel of R \/ the InternalRel of N4 is set
[:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is set
bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is non empty set
k is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
k \/ m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
H1 is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
RelStr(# ( the carrier of R \/ the carrier of N4),H1 #) is strict RelStr
the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #) is set
the InternalRel of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #) is Relation-like the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #) -defined the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #) -valued Element of bool [: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #):]
[: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #):] is set
bool [: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #):] is non empty set
C is strict RelStr
the carrier of C is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is set
bool [: the carrier of C, the carrier of C:] is non empty set
k is strict RelStr
the carrier of k is set
the InternalRel of k is Relation-like the carrier of k -defined the carrier of k -valued Element of bool [: the carrier of k, the carrier of k:]
[: the carrier of k, the carrier of k:] is set
bool [: the carrier of k, the carrier of k:] is non empty set
R is RelStr
the carrier of R is set
N4 is RelStr
the carrier of N4 is set
the carrier of R \/ the carrier of N4 is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of N4 is Relation-like the carrier of N4 -defined the carrier of N4 -valued Element of bool [: the carrier of N4, the carrier of N4:]
[: the carrier of N4, the carrier of N4:] is set
bool [: the carrier of N4, the carrier of N4:] is non empty set
the InternalRel of R \/ the InternalRel of N4 is set
[: the carrier of R, the carrier of N4:] is set
( the InternalRel of R \/ the InternalRel of N4) \/ [: the carrier of R, the carrier of N4:] is set
[: the carrier of N4, the carrier of R:] is set
(( the InternalRel of R \/ the InternalRel of N4) \/ [: the carrier of R, the carrier of N4:]) \/ [: the carrier of N4, the carrier of R:] is set
[:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is set
bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is non empty set
S is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
H1 is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
S \/ H1 is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
k is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
(S \/ H1) \/ k is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
((S \/ H1) \/ k) \/ m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]
RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) is strict RelStr
the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) is set
the InternalRel of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) is Relation-like the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) -defined the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) -valued Element of bool [: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #):]
[: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #):] is set
bool [: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #):] is non empty set
C is strict RelStr
the carrier of C is set
the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is set
bool [: the carrier of C, the carrier of C:] is non empty set
k is strict RelStr
the carrier of k is set
the InternalRel of k is Relation-like the carrier of k -defined the carrier of k -valued Element of bool [: the carrier of k, the carrier of k:]
[: the carrier of k, the carrier of k:] is set
bool [: the carrier of k, the carrier of k:] is non empty set
R is set
N4 is set
C is set
k is strict RelStr
the carrier of k is set
the InternalRel of k is Relation-like the carrier of k -defined the carrier of k -valued Element of bool [: the carrier of k, the carrier of k:]
[: the carrier of k, the carrier of k:] is set
bool [: the carrier of k, the carrier of k:] is non empty set
[ the carrier of k, the InternalRel of k] is set
{ the carrier of k, the InternalRel of k} is non empty finite set
{ the carrier of k} is non empty trivial finite 1 -element set
{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set
m is strict RelStr
the carrier of m is set
the InternalRel of m is Relation-like the carrier of m -defined the carrier of m -valued Element of bool [: the carrier of m, the carrier of m:]
[: the carrier of m, the carrier of m:] is set
bool [: the carrier of m, the carrier of m:] is non empty set
[ the carrier of m, the InternalRel of m] is set
{ the carrier of m, the InternalRel of m} is non empty finite set
{ the carrier of m} is non empty trivial finite 1 -element set
{{ the carrier of m, the InternalRel of m},{ the carrier of m}} is non empty finite V41() set
R is set
N4 is set
C is set
k is strict RelStr
the carrier of k is set
the InternalRel of k is Relation-like the carrier of k -defined the carrier of k -valued Element of bool [: the carrier of k, the carrier of k:]
[: the carrier of k, the carrier of k:] is set
bool [: the carrier of k, the carrier of k:] is non empty set
[ the carrier of k, the InternalRel of k] is set
{ the carrier of k, the InternalRel of k} is non empty finite set
{ the carrier of k} is non empty trivial finite 1 -element set
{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set
k is strict RelStr
the carrier of k is set
the InternalRel of k is Relation-like the carrier of k -defined the carrier of k -valued Element of bool [: the carrier of k, the carrier of k:]
[: the carrier of k, the carrier of k:] is set
bool [: the carrier of k, the carrier of k:] is non empty set
[ the carrier of k, the InternalRel of k] is set
{ the carrier of k, the InternalRel of k} is non empty finite set
{ the carrier of k} is non empty trivial finite 1 -element set
{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set
C is strict RelStr
the carrier of C is set
k is strict RelStr
the carrier of k is set
the InternalRel of k is Relation-like the carrier of k -defined the carrier of k -valued Element of bool [: the carrier of k, the carrier of k:]
[: the carrier of k, the carrier of k:] is set
bool [: the carrier of k, the carrier of k:] is non empty set
[ the carrier of k, the InternalRel of k] is set
{ the carrier of k, the InternalRel of k} is non empty finite set
{ the carrier of k} is non empty trivial finite 1 -element set
{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set
N4 is set
C is set
k is strict RelStr
the carrier of k is set
() is set

bool is non empty finite V41() set
RelStr(# {},({} ({},{})) #) is strict RelStr
the carrier of RelStr(# {},({} ({},{})) #) is set
bool () is non empty set
bool () is non empty Element of bool (bool ())
bool (bool ()) is non empty set
R is set
N4 is set
N4 is Element of bool (bool ())
Intersect N4 is Element of bool ()
C is Element of bool ()
m is strict RelStr
the carrier of m is set
S is strict RelStr
the carrier of S is set
(m,S) is strict RelStr
(m,S) is strict RelStr
H1 is strict RelStr
the carrier of H1 is set
f is strict RelStr
the carrier of f is set
(f,H1) is strict RelStr
the carrier of m \/ the carrier of S is set
cS is strict RelStr
the carrier of cS is set
H2 is strict RelStr
the carrier of H2 is set
m is strict RelStr
the carrier of m is set
S is strict RelStr
the carrier of S is set
H1 is strict RelStr
the carrier of H1 is set
(S,H1) is strict RelStr
(S,H1) is strict RelStr
meet N4 is Element of bool ()
k is strict RelStr
the carrier of k is set
m is strict RelStr
the carrier of m is set
(k,m) is strict RelStr
(k,m) is strict RelStr
S is set
S is set
k is strict RelStr
the carrier of k is set
m is set
k is strict RelStr
the carrier of k is set
m is strict RelStr
the carrier of m is set
S is strict RelStr
the carrier of S is set
(m,S) is strict RelStr
(m,S) is strict RelStr
k is Element of bool ()
m is set
k is strict RelStr
the carrier of k is set
m is strict RelStr
the carrier of m is set
S is strict RelStr
the carrier of S is set
(m,S) is strict RelStr
(m,S) is strict RelStr
H1 is Element of bool ()
R is Element of bool ()
N4 is Element of bool ()
() is Element of bool ()
is non empty finite set
bool is non empty finite V41() set

RelStr(# ,R #) is non empty strict RelStr
the carrier of RelStr(# ,R #) is non empty set
R is set
C is strict RelStr
the carrier of C is set
N4 is strict RelStr
{N4} is non empty trivial finite 1 -element set
() \ {N4} is Element of bool ()
S is strict RelStr
the carrier of S is set
H1 is strict RelStr
the carrier of H1 is set
m is Element of bool ()
the carrier of N4 is set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of N4 is Relation-like the carrier of N4 -defined the carrier of N4 -valued Element of bool [: the carrier of N4, the carrier of N4:]
the carrier of N4 is set
[: the carrier of N4, the carrier of N4:] is set
bool [: the carrier of N4, the carrier of N4:] is non empty set
the carrier of N4 is set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of N4 is Relation-like the carrier of N4 -defined the carrier of N4 -valued Element of bool [: the carrier of N4, the carrier of N4:]
[: the carrier of N4, the carrier of N4:] is set
bool [: the carrier of N4, the carrier of N4:] is non empty set
H2 is non empty set
H2 \/ the carrier of H1 is non empty set
(S,H1) is strict RelStr
(S,H1) is strict RelStr
the carrier of (S,H1) is set
S is strict RelStr
the carrier of S is set
C is strict RelStr
the carrier of C is set
R is RelStr
the carrier of R is set
N4 is strict RelStr
the carrier of N4 is set
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in a2 & b3 in a2 & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

N4 is set
{ b1 where b1 is Element of () : b1 is trivial finite RelStr } is set

dom C is set
C . 0 is set
Union C is set
k is set
m is set
C . m is set

C . H1 is set

C . (H1 + 1) is set
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . H1 & b3 in C . H1 & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

H2 is set
cS is Element of ()
cH1 is strict RelStr
the carrier of cH1 is set
cH2 is strict RelStr
the carrier of cH2 is set
(cH1,cH2) is strict RelStr
(cH1,cH2) is strict RelStr
(C . H1) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . H1 & b3 in C . H1 & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

H1 is set
H2 is Element of ()

C . S is set

C . m is set

C . (m + 1) is set
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

(C . m) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

S is set

C . m is set
C . S is set

C . (m + H1) is set

C . (m + (H1 + 1)) is set

C . ((m + H1) + 1) is set

C . (m + 0) is set

k is Element of bool ()
m is strict RelStr
the carrier of m is set
S is strict RelStr
the carrier of S is set
(m,S) is strict RelStr
(m,S) is strict RelStr
H1 is set
C . H1 is set
H2 is set
C . H2 is set

C . (max (f,cS)) is set
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . (max (f,cS)) & b3 in C . (max (f,cS)) & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

C . ((max (f,cS)) + 1) is set
(C . (max (f,cS))) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . (max (f,cS)) & b3 in C . (max (f,cS)) & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

C . f is set
C . cS is set
m is set
m is strict RelStr
the carrier of m is set

C . m is set

C . (m + 1) is set
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

C . (H1 + 1) is set
C . H1 is set
(C . H1) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) )
}
is set

H2 is strict RelStr
the carrier of H2 is set
f is strict RelStr
the carrier of f is set
(H2,f) is strict RelStr
(H2,f) is strict RelStr
H2 is Element of ()
f is strict RelStr
the carrier of f is set
cS is strict RelStr
the carrier of cS is set
(f,cS) is strict RelStr
(f,cS) is strict RelStr
H2 is strict RelStr
the carrier of H2 is set
f is strict RelStr
the carrier of f is set
(H2,f) is strict RelStr
(H2,f) is strict RelStr
m is Element of ()
S is non empty trivial finite 1 -element strict RelStr
m is set
C . m is set
m is strict RelStr
the carrier of m is set
S is strict RelStr
the carrier of S is set
(m,S) is strict RelStr
(m,S) is strict RelStr
R is non empty strict RelStr
the carrier of R is non empty set
k is strict RelStr
the carrier of k is set
C is finite Element of FinSETS

S is non empty strict RelStr
the carrier of S is non empty set

S is non empty strict RelStr
the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
dom the InternalRel of S is set
rng the InternalRel of S is set
[: the carrier of (), the carrier of S:] is set
bool [: the carrier of (), the carrier of S:] is non empty set
H1 is Relation-like the carrier of () -defined the carrier of S -valued Function-like V29( the carrier of (), the carrier of S) Element of bool [: the carrier of (), the carrier of S:]

H1 . 0 is set
H1 . 1 is set
[(H1 . 0),(H1 . 1)] is set
{(H1 . 0),(H1 . 1)} is non empty finite set
{(H1 . 0)} is non empty trivial finite 1 -element set
{{(H1 . 0),(H1 . 1)},{(H1 . 0)}} is non empty finite V41() set
[0,0] is set
{0,0} is non empty finite V41() set
is non empty finite V41() set
H1 is strict RelStr
the carrier of H1 is set
H2 is strict RelStr
the carrier of H2 is set
(H1,H2) is strict RelStr
(H1,H2) is strict RelStr
H1 is strict RelStr
the carrier of H1 is set
H2 is strict RelStr
the carrier of H2 is set
(H1,H2) is strict RelStr
(H1,H2) is strict RelStr
[1,3] is set
{1,3} is non empty finite V41() set
{{1,3},{1}} is non empty finite V41() set
[0,2] is set
{0,2} is non empty finite V41() set
{{0,2},} is non empty finite V41() set
[0,3] is set
{0,3} is non empty finite V41() set
{{0,3},} is non empty finite V41() set
the InternalRel of H1 is Relation-like the carrier of H1 -defined the carrier of H1 -valued Element of bool [: the carrier of H1, the carrier of H1:]
[: the carrier of H1, the carrier of H1:] is set
bool [: the carrier of H1, the carrier of H1:] is non empty set
the InternalRel of H2 is Relation-like the carrier of H2 -defined the carrier of H2 -valued Element of bool [: the carrier of H2, the carrier of H2:]
[: the carrier of H2, the carrier of H2:] is set
bool [: the carrier of H2, the carrier of H2:] is non empty set
[: the carrier of H1, the carrier of H2:] is set
[: the carrier of H2, the carrier of H1:] is set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
dom the InternalRel of S is set
y is set
the InternalRel of H1 \/ the InternalRel of H2 is set
( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set
(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set
rng the InternalRel of S is set
y is set
the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:] is set
( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set
the InternalRel of H1 \/ (( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:]) is set
[: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] is set
the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set
the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) is set
the InternalRel of H1 \/ the InternalRel of H2 is set
( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set
( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set
(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set
rng the InternalRel of H1 is set
[: the carrier of (), the carrier of S:] is set
bool [: the carrier of (), the carrier of S:] is non empty set
y is Relation-like the carrier of () -defined the carrier of S -valued Function-like V29( the carrier of (), the carrier of S) Element of bool [: the carrier of (), the carrier of S:]
y . 1 is set
y . 0 is set
[(y . 1),(y . 0)] is set
{(y . 1),(y . 0)} is non empty finite set
{(y . 1)} is non empty trivial finite 1 -element set
{{(y . 1),(y . 0)},{(y . 1)}} is non empty finite V41() set
y . 3 is set
y . 2 is set
[(y . 3),(y . 2)] is set
{(y . 3),(y . 2)} is non empty finite set
{(y . 3)} is non empty trivial finite 1 -element set
{{(y . 3),(y . 2)},{(y . 3)}} is non empty finite V41() set
[(y . 2),(y . 1)] is set
{(y . 2),(y . 1)} is non empty finite set
{(y . 2)} is non empty trivial finite 1 -element set
{{(y . 2),(y . 1)},{(y . 2)}} is non empty finite V41() set
rng the InternalRel of H2 is set
[(y . 2),(y . 3)] is set
{(y . 2),(y . 3)} is non empty finite set
{{(y . 2),(y . 3)},{(y . 2)}} is non empty finite V41() set
the carrier of H1 \/ the carrier of H2 is set
[(y . 0),(y . 1)] is set
{(y . 0),(y . 1)} is non empty finite set
{(y . 0)} is non empty trivial finite 1 -element set
{{(y . 0),(y . 1)},{(y . 0)}} is non empty finite V41() set
dom the InternalRel of H1 is set
[(y . 1),(y . 2)] is set
{(y . 1),(y . 2)} is non empty finite set
{{(y . 1),(y . 2)},{(y . 1)}} is non empty finite V41() set
dom the InternalRel of H2 is set
[(y . 0),(y . 2)] is set
{(y . 0),(y . 2)} is non empty finite set
{{(y . 0),(y . 2)},{(y . 0)}} is non empty finite V41() set
[(y . 0),(y . 3)] is set
{(y . 0),(y . 3)} is non empty finite set
{{(y . 0),(y . 3)},{(y . 0)}} is non empty finite V41() set
[(y . 1),(y . 3)] is set
{(y . 1),(y . 3)} is non empty finite set
{{(y . 1),(y . 3)},{(y . 1)}} is non empty finite V41() set
dom y is set
rng y is set
cH1 is set
cH2 is set
y . cH2 is set
[: the carrier of (), the carrier of H1:] is set
bool [: the carrier of (), the carrier of H1:] is non empty set
the InternalRel of H1 \/ the InternalRel of H2 is set
( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set
(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set
cH1 is finite set
cH2 is finite set
cH1 \/ cH2 is finite set
cS is finite set
x is set
cH1 /\ cH2 is finite set

x is Element of the carrier of ()
y is Element of the carrier of ()
[x,y] is set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V41() set
y . x is set
y . y is set
[(y . x),(y . y)] is set
{(y . x),(y . y)} is non empty finite set
{(y . x)} is non empty trivial finite 1 -element set
{{(y . x),(y . y)},{(y . x)}} is non empty finite V41() set
[: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] is set
( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set
the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set
the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) is set
[(y . 0),(y . 3)] is set
{(y . 0),(y . 3)} is non empty finite set
{{(y . 0),(y . 3)},{(y . 0)}} is non empty finite V41() set
[(y . 1),(y . 3)] is set
{(y . 1),(y . 3)} is non empty finite set
{{(y . 1),(y . 3)},{(y . 1)}} is non empty finite V41() set
the InternalRel of H1 \/ the InternalRel of H2 is set
( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set
(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set
[(y . 0),(y . 2)] is set
{(y . 0),(y . 2)} is non empty finite set
{{(y . 0),(y . 2)},{(y . 0)}} is non empty finite V41() set
dom y is set
rng y is set
cH1 is set
cH2 is set
y . cH2 is set
[: the carrier of (), the carrier of H2:] is set
bool [: the carrier of (), the carrier of H2:] is non empty set
cH1 is finite set
cH2 is finite set
cH1 \/ cH2 is finite set
cS is finite set
x is set
cH1 /\ cH2 is finite set

x is Element of the carrier of ()
y is Element of the carrier of ()
[x,y] is set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V41() set
y . x is set
y . y is set
[(y . x),(y . y)] is set
{(y . x),(y . y)} is non empty finite set
{(y . x)} is non empty trivial finite 1 -element set
{{(y . x),(y . y)},{(y . x)}} is non empty finite V41() set
[: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] is set
( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set
the InternalRel of H1 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set
the InternalRel of H2 \/ ( the InternalRel of H1 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) is set
f is Relation-like the carrier of () -defined the carrier of S -valued Function-like V29( the carrier of (), the carrier of S) Element of bool [: the carrier of (), the carrier of S:]
f . 0 is set
f . 1 is set
[(f . 0),(f . 1)] is set
{(f . 0),(f . 1)} is non empty finite set
{(f . 0)} is non empty trivial finite 1 -element set
{{(f . 0),(f . 1)},{(f . 0)}} is non empty finite V41() set
f . 3 is set
f . 2 is set
[(f . 3),(f . 2)] is set
{(f . 3),(f . 2)} is non empty finite set
{(f . 3)} is non empty trivial finite 1 -element set
{{(f . 3),(f . 2)},{(f . 3)}} is non empty finite V41() set
[(f . 2),(f . 3)] is set
{(f . 2),(f . 3)} is non empty finite set
{(f . 2)} is non empty trivial finite 1 -element set
{{(f . 2),(f . 3)},{(f . 2)}} is non empty finite V41() set
[(f . 2),(f . 1)] is set
{(f . 2),(f . 1)} is non empty finite set
{{(f . 2),(f . 1)},{(f . 2)}} is non empty finite V41() set
[(f . 1),(f . 2)] is set
{(f . 1),(f . 2)} is non empty finite set
{(f . 1)} is non empty trivial finite 1 -element set
{{(f . 1),(f . 2)},{(f . 1)}} is non empty finite V41() set
[(f . 1),(f . 0)] is set
{(f . 1),(f . 0)} is non empty finite set
{{(f . 1),(f . 0)},{(f . 1)}} is non empty finite V41() set
dom f is set
cH1 is finite set
cH2 is finite set
cH1 \/ cH2 is finite set
the InternalRel of H1 \/ the InternalRel of H2 is set
cS is finite set
y is set
cH1 /\ cH2 is finite set

y is Element of the carrier of ()
x is Element of the carrier of ()
[y,x] is set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V41() set
f . y is set
f . x is set
[(f . y),(f . x)] is set
{(f . y),(f . x)} is non empty finite set
{(f . y)} is non empty trivial finite 1 -element set
{{(f . y),(f . x)},{(f . y)}} is non empty finite V41() set
rng f is set
y is set
x is set
f . x is set
[: the carrier of (), the carrier of H1:] is set
bool [: the carrier of (), the carrier of H1:] is non empty set
dom f is set
cH1 is finite set
cH2 is finite set
cH1 \/ cH2 is finite set
the InternalRel of H1 \/ the InternalRel of H2 is set
cS is finite set
y is set
cH1 /\ cH2 is finite set

y is Element of the carrier of ()
x is Element of the carrier of ()
[y,x] is set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V41() set
f . y is set
f . x is set
[(f . y),(f . x)] is set
{(f . y),(f . x)} is non empty finite set
{(f . y)} is non empty trivial finite 1 -element set
{{(f . y),(f . x)},{(f . y)}} is non empty finite V41() set
rng f is set
y is set
x is set
f . x is set
[: the carrier of (), the carrier of H2:] is set
bool [: the carrier of (), the carrier of H2:] is non empty set

cS is non empty strict RelStr
the carrier of cS is non empty set

cH2 is non empty strict RelStr
the carrier of cH2 is non empty set

m is non empty strict RelStr
the carrier of m is non empty set

m is non empty strict RelStr
the carrier of m is non empty set