:: MYCIELSK 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

n is V63() ext-real real set
R is V63() ext-real real set
S is V63() ext-real real set
R -' S is V63() ext-real non negative real set
n * (R -' S) is V63() ext-real real set
n * R is V63() ext-real real set
n * S is V63() ext-real real set
(n * R) -' (n * S) is V63() ext-real non negative real set
R - S is V63() ext-real real set
n * (R - S) is V63() ext-real real set
(n * R) - (n * S) is V63() ext-real real set
R - S is V63() ext-real real set
n * (R - S) is V63() ext-real real set
(n * R) - (n * S) is V63() ext-real real set
n * 0 is V63() ext-real real set
R - S is V63() ext-real real set

R \ S is finite Element of bool R
bool R is non empty finite V32() set
iMRn1 is set
n is set
R is set
S is set
iMRn is set
cMRn1 is set
n \/ R is set
(n \/ R) \/ S is set
((n \/ R) \/ S) \/ iMRn is set
(((n \/ R) \/ S) \/ iMRn) \/ cMRn1 is set
iMRn1 is set
n is set
R is set
n \/ R is set
S is set
(n \/ R) \/ S is set
iMRn is set
((n \/ R) \/ S) \/ iMRn is set
cMRn1 is set
(((n \/ R) \/ S) \/ iMRn) \/ cMRn1 is set

the carrier of n is set
the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is non empty set
R is set
S is set
[R,S] is non empty set
{R,S} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,S},{R}} is non empty finite V32() set
[S,R] is non empty set
{S,R} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,R},{S}} is non empty finite V32() set

the carrier of n is set
R is Element of the carrier of n
S is Element of the carrier of n
the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is non empty set
[R,S] is non empty set
{R,S} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,S},{R}} is non empty finite V32() set
[S,R] is non empty set
{S,R} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,R},{S}} is non empty finite V32() set
n is set

R is V89() a_partition of n

S is set
choose S is Element of S
the Element of S is Element of S

dom S is set
iMRn is set
cMRn1 is set
S . iMRn is set
S . cMRn1 is set
choose iMRn is Element of iMRn
the Element of iMRn is Element of iMRn
choose cMRn1 is Element of cMRn1
the Element of cMRn1 is Element of cMRn1
rng S is set
iMRn is set
cMRn1 is set
S . cMRn1 is set
choose cMRn1 is Element of cMRn1
the Element of cMRn1 is Element of cMRn1
n is set
bool n is non empty set
R is V89() a_partition of n
S is Element of bool n
{ (b1 /\ S) where b1 is Element of R : not b1 misses S } is set
bool S is non empty set
cMRn1 is set
iMRn1 is Element of R
iMRn1 /\ S is Element of bool n
union { (b1 /\ S) where b1 is Element of R : not b1 misses S } is set
cMRn1 is set
iMRn1 is set
cMRn1 is set
union R is set
iMRn1 is set
iMRn1 /\ S is Element of bool n
cMRn1 is Element of bool S
iMRn1 is Element of R
iMRn1 /\ S is Element of bool n
N is set
x is non empty set
xp1 is Element of bool S
yp1 is Element of R
yp1 /\ S is Element of bool n
y is non empty V89() a_partition of x
n is set
{n} is non empty trivial finite 1 -element set
n is set
bool n is non empty set
R is finite V89() a_partition of n
S is Element of bool n
(n,R,S) is V89() a_partition of S
{ (b1 /\ S) where b1 is Element of R : not b1 misses S } is set
iMRn is set
iMRn /\ S is Element of bool n

dom iMRn is set
rng iMRn is set
cMRn1 is set
iMRn1 is Element of R
iMRn1 /\ S is Element of bool n
N is set
x is non empty set
iMRn . iMRn1 is set
n is set
bool n is non empty set
R is finite V89() a_partition of n

S is Element of bool n
(n,R,S) is finite V89() a_partition of S
{ (b1 /\ S) where b1 is Element of R : not b1 misses S } is set

iMRn is non empty finite set
{ H1(b1) where b1 is Element of iMRn : S1[b1] } is set

n is set
bool n is non empty set
R is finite V89() a_partition of n

S is Element of bool n
(n,R,S) is finite V89() a_partition of S
{ (b1 /\ S) where b1 is Element of R : not b1 misses S } is set

iMRn is set
the Element of R is Element of R
cMRn1 is non empty finite set
the Element of R /\ S is Element of bool n
N is non empty finite set
x is set
x /\ S is Element of bool n
[:R,N:] is finite set
bool [:R,N:] is non empty finite V32() set

y is set
xp1 is set
x . y is set
x . xp1 is set
y /\ S is Element of bool n
xp1 /\ S is Element of bool n
yp1 is set
rng x is finite set
y is set
xp1 is set
x . xp1 is set
xp1 /\ S is Element of bool n
y is set
xp1 is Element of R
xp1 /\ S is Element of bool n
x . xp1 is set
iMRn1 is set
N is Element of R
N /\ S is Element of bool n
[:(n,R,S),cMRn1:] is finite set
bool [:(n,R,S),cMRn1:] is non empty finite V32() set
iMRn1 is Relation-like (n,R,S) -defined cMRn1 -valued Function-like V21((n,R,S)) quasi_total finite Element of bool [:(n,R,S),cMRn1:]
N is set
dom iMRn1 is finite set
x is set
iMRn1 . N is set
iMRn1 . x is set
dom iMRn1 is finite Element of bool (n,R,S)
bool (n,R,S) is non empty finite V32() set
(iMRn1 . N) /\ S is Element of bool n
rng iMRn1 is finite set
N is set
dom iMRn1 is finite Element of bool (n,R,S)
bool (n,R,S) is non empty finite V32() set
x is set
iMRn1 . x is set
N /\ S is Element of bool n
y is set
n is RelStr
the carrier of n is set
bool the carrier of n is non empty set
R is V89() StableSet-wise a_partition of the carrier of n
S is Element of bool the carrier of n
( the carrier of n,R,S) is V89() a_partition of S
{ (b1 /\ S) where b1 is Element of R : not b1 misses S } is set
subrelstr S is strict V76(n) SubRelStr of n
the carrier of () is set
cMRn1 is set
iMRn1 is Element of R
iMRn1 /\ S is Element of bool the carrier of n
N is set
bool the carrier of () is non empty set
y is Element of bool the carrier of ()
xp1 is Element of the carrier of ()
yp1 is Element of the carrier of ()
x is non empty RelStr
the carrier of x is non empty set
e is Element of bool the carrier of n
xx is Element of the carrier of n
e is Element of the carrier of n

R is finite V32() V89() StableSet-wise a_partition of the carrier of n
n is RelStr
the carrier of n is set
S is V89() a_partition of the carrier of n
bool the carrier of n is non empty set
iMRn is set
iMRn is V89() StableSet-wise a_partition of the carrier of n
SmallestPartition the carrier of n is V89() a_partition of the carrier of n
S is non empty finite set
{ H1(b1) where b1 is Element of S : S1[b1] } is set
cMRn1 is set
bool the carrier of n is non empty set
iMRn1 is Element of the carrier of n
{iMRn1} is non empty trivial finite 1 -element set
cMRn1 is V89() StableSet-wise a_partition of the carrier of n
n is () RelStr
the carrier of n is set
n is () RelStr
the carrier of n is set
bool the carrier of n is non empty set
R is Element of bool the carrier of n
subrelstr R is strict V76(n) SubRelStr of n
iMRn is V89() StableSet-wise a_partition of the carrier of n
the carrier of () is set
( the carrier of n,iMRn,R) is V89() a_partition of R
{ (b1 /\ R) where b1 is Element of iMRn : not b1 misses R } is set
cMRn1 is V89() a_partition of R
bool the carrier of () is non empty set
iMRn1 is set
N is Element of iMRn
N /\ R is Element of bool the carrier of n
x is set
n is () RelStr
the carrier of n is set
R is V89() StableSet-wise a_partition of the carrier of n

iMRn is finite V89() StableSet-wise a_partition of the carrier of n

iMRn is finite V89() StableSet-wise a_partition of the carrier of n

iMRn is finite V89() StableSet-wise a_partition of the carrier of n

iMRn is finite V89() StableSet-wise a_partition of the carrier of n

cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n

cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n

R is finite V32() V89() StableSet-wise a_partition of the carrier of n

n is non empty () RelStr

the carrier of n is non empty set
R is non empty finite V89() StableSet-wise a_partition of the carrier of n

R is finite V32() V89() StableSet-wise a_partition of the carrier of n
S is finite V32() V89() Clique-wise StableSet-wise a_partition of the carrier of n
n is RelStr
the carrier of n is set
S is V89() a_partition of the carrier of n
bool the carrier of n is non empty set
iMRn is set
iMRn is V89() Clique-wise a_partition of the carrier of n
SmallestPartition the carrier of n is V89() a_partition of the carrier of n
S is non empty finite set
{ H1(b1) where b1 is Element of S : S1[b1] } is set
cMRn1 is set
bool the carrier of n is non empty set
iMRn1 is Element of the carrier of n
{iMRn1} is non empty trivial finite 1 -element set
cMRn1 is V89() Clique-wise a_partition of the carrier of n
n is () RelStr
the carrier of n is set
n is () RelStr
the carrier of n is set
bool the carrier of n is non empty set
R is Element of bool the carrier of n
subrelstr R is strict V76(n) SubRelStr of n
iMRn is V89() Clique-wise a_partition of the carrier of n
the carrier of () is set
( the carrier of n,iMRn,R) is V89() a_partition of R
{ (b1 /\ R) where b1 is Element of iMRn : not b1 misses R } is set
cMRn1 is V89() a_partition of R
bool the carrier of () is non empty set
iMRn1 is set
N is Element of iMRn
N /\ R is Element of bool the carrier of n
x is set
n is () RelStr
the carrier of n is set
R is V89() Clique-wise a_partition of the carrier of n

iMRn is finite V89() Clique-wise a_partition of the carrier of n

iMRn is finite V89() Clique-wise a_partition of the carrier of n

iMRn is finite V89() Clique-wise a_partition of the carrier of n

iMRn is finite V89() Clique-wise a_partition of the carrier of n

cMRn1 is finite V89() Clique-wise a_partition of the carrier of n

cMRn1 is finite V89() Clique-wise a_partition of the carrier of n

R is finite V32() V89() Clique-wise StableSet-wise a_partition of the carrier of n

n is non empty () RelStr

the carrier of n is non empty set
R is non empty finite V89() Clique-wise a_partition of the carrier of n

the carrier of n is finite set

bool the carrier of n is non empty finite V32() set
R is finite connected Element of bool the carrier of n

the carrier of n is finite set

bool the carrier of n is non empty finite V32() set
R is finite stable Element of bool the carrier of n

the carrier of n is finite set

R is finite V32() V89() StableSet-wise a_partition of the carrier of n

the carrier of n is finite set

R is finite V32() V89() Clique-wise a_partition of the carrier of n

the carrier of n is set
bool the carrier of n is non empty set
R is finite connected Element of bool the carrier of n

S is finite V89() StableSet-wise a_partition of the carrier of n

cMRn1 is set
iMRn1 is Element of the carrier of n
union S is set
N is set
[:R,S:] is finite set
bool [:R,S:] is non empty finite V32() set

iMRn1 is set
N is set
cMRn1 . iMRn1 is set
cMRn1 . N is set

the carrier of n is set
bool the carrier of n is non empty set
R is finite stable Element of bool the carrier of n

S is finite V89() Clique-wise a_partition of the carrier of n

cMRn1 is set
iMRn1 is Element of the carrier of n
union S is set
N is set
[:R,S:] is finite set
bool [:R,S:] is non empty finite V32() set

iMRn1 is set
N is set
cMRn1 . iMRn1 is set
cMRn1 . N is set
n is RelStr
the carrier of n is set

the carrier of () is set
R is Element of the carrier of n
S is Element of the carrier of n
iMRn is Element of the carrier of ()
cMRn1 is Element of the carrier of ()
the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is non empty set
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 (), the carrier of ():] is set
bool [: the carrier of (), the carrier of ():] is non empty set
the InternalRel of n ` is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] \ the InternalRel of n is set
id the carrier of n is Relation-like set
( the InternalRel of n `) \ (id the carrier of n) is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[R,S] is non empty set
{R,S} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,S},{R}} is non empty finite V32() set
n is RelStr
the carrier of n is set

the carrier of () is set
R is Element of the carrier of n
S is Element of the carrier of n
iMRn is Element of the carrier of ()
cMRn1 is Element of the carrier of ()
the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is non empty set
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 (), the carrier of ():] is set
bool [: the carrier of (), the carrier of ():] is non empty set
the InternalRel of n ` is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] \ the InternalRel of n is set
id the carrier of n is Relation-like set
( the InternalRel of n `) \ (id the carrier of n) is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[R,S] is non empty set
{R,S} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,S},{R}} is non empty finite V32() set

the carrier of n is finite set
the carrier of () is set

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

the carrier of () is set
bool the carrier of () is non empty set
R is connected Element of bool the carrier of n
S is Element of the carrier of ()
iMRn is Element of the carrier of ()
cMRn1 is Element of the carrier of n
iMRn1 is Element of the carrier of n

the carrier of () is set
bool the carrier of () is non empty set
the carrier of n is set
bool the carrier of n is non empty set
R is connected Element of bool the carrier of ()
S is Element of the carrier of n
iMRn is Element of the carrier of n
cMRn1 is Element of the carrier of ()
iMRn1 is Element of the carrier of ()
n is RelStr
the carrier of n is set
bool the carrier of n is non empty set

the carrier of () is set
bool the carrier of () is non empty set
R is stable Element of bool the carrier of n
iMRn is Element of the carrier of ()
cMRn1 is Element of the carrier of ()
iMRn1 is Element of the carrier of n
N is Element of the carrier of n
n is RelStr

the carrier of () is set
bool the carrier of () is non empty set
the carrier of n is set
bool the carrier of n is non empty set
R is stable Element of bool the carrier of ()
S is Element of the carrier of n
iMRn is Element of the carrier of n
cMRn1 is Element of the carrier of ()
iMRn1 is Element of the carrier of ()

the carrier of n is set
bool the carrier of n is non empty set
S is finite connected Element of bool the carrier of n

the carrier of () is set
bool the carrier of () is non empty set
iMRn is finite stable Element of bool the carrier of ()

iMRn is finite stable Element of bool the carrier of ()

iMRn1 is finite stable Element of bool the carrier of ()

iMRn1 is finite stable Element of bool the carrier of ()

N is finite stable Element of bool the carrier of ()

cMRn1 is finite stable Element of bool the carrier of ()

the carrier of n is set
bool the carrier of n is non empty set
S is finite stable Element of bool the carrier of n

the carrier of () is set
bool the carrier of () is non empty set
iMRn is finite connected Element of bool the carrier of ()

iMRn is finite connected Element of bool the carrier of ()

iMRn1 is finite connected Element of bool the carrier of ()

iMRn1 is finite connected Element of bool the carrier of ()

N is finite connected Element of bool the carrier of ()

cMRn1 is finite connected Element of bool the carrier of ()

the carrier of () is set
bool the carrier of () is non empty set
S is finite stable Element of bool the carrier of ()

the carrier of n is set
bool the carrier of n is non empty set
iMRn is finite connected Element of bool the carrier of n

iMRn is finite connected Element of bool the carrier of n

the carrier of () is set
bool the carrier of () is non empty set
iMRn is finite connected Element of bool the carrier of ()

the carrier of n is set
bool the carrier of n is non empty set
cMRn1 is finite stable Element of bool the carrier of n

cMRn1 is finite stable Element of bool the carrier of n

n is RelStr
the carrier of n is set

the carrier of () is set
R is V89() StableSet-wise a_partition of the carrier of n
S is set
bool the carrier of n is non empty set
bool the carrier of () is non empty set

the carrier of () is set
the carrier of n is set
R is V89() Clique-wise a_partition of the carrier of ()
iMRn is set
bool the carrier of () is non empty set
bool the carrier of n is non empty set

the carrier of n is set

the carrier of () is set
R is V89() Clique-wise a_partition of the carrier of n
iMRn is set
bool the carrier of n is non empty set
bool the carrier of () is non empty set
n is RelStr

the carrier of () is set
the carrier of n is set
R is V89() StableSet-wise a_partition of the carrier of ()
iMRn is set
bool the carrier of () is non empty set
bool the carrier of n is non empty set
n is () RelStr

the carrier of n is set
R is V89() StableSet-wise a_partition of the carrier of n
the carrier of () is set
n is symmetric () RelStr

the carrier of n is set
R is V89() Clique-wise a_partition of the carrier of n
the carrier of () is set
n is symmetric () RelStr

the carrier of () is set
iMRn is finite V89() Clique-wise a_partition of the carrier of ()

the carrier of n is set
cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n

cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n

n is symmetric () RelStr

the carrier of () is set
iMRn is finite V89() StableSet-wise a_partition of the carrier of ()

the carrier of n is set
cMRn1 is finite V89() Clique-wise a_partition of the carrier of n

cMRn1 is finite V89() Clique-wise a_partition of the carrier of n

n is RelStr
the carrier of n is set
bool the carrier of n is non empty set
R is Element of the carrier of n
{ b1 where b1 is Element of the carrier of n : ( b1 < R or R < b1 ) } is set
the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is non empty set
iMRn1 is set
N is Element of the carrier of n
[N,R] is non empty set
{N,R} is non empty finite set
{N} is non empty trivial finite 1 -element set
{{N,R},{N}} is non empty finite V32() set
[R,N] is non empty set
{R,N} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,N},{R}} is non empty finite V32() set
iMRn1 is Element of bool the carrier of n
N is Element of the carrier of n
x is Element of the carrier of n
S is Element of bool the carrier of n
iMRn is Element of bool the carrier of n
cMRn1 is set
iMRn1 is Element of the carrier of n
cMRn1 is set
iMRn1 is Element of the carrier of n
n is () RelStr
the carrier of n is set

R is finite V89() StableSet-wise a_partition of the carrier of n

S is set
union R is set
bool the carrier of n is non empty set
cMRn1 is Element of bool the carrier of n
{cMRn1} is non empty trivial finite 1 -element set
R \ {cMRn1} is finite Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty set
N is set
x is Element of the carrier of n
(n,x) is Element of bool the carrier of n
y is Element of R

(card R) - (card {cMRn1}) is V63() ext-real real set

(card R) - 1 is V63() ext-real real set
((card R) - 1) + 1 is V63() ext-real real set
xp1 is set
{xp1} is non empty trivial finite 1 -element set
x is set
y is Element of the carrier of n
(n,y) is Element of bool the carrier of n
xp1 is Element of R
yp1 is Element of the carrier of n
xx is Element of the carrier of n
(n,yp1) is Element of bool the carrier of n

dom x is set
N is non empty set
y is non empty finite set
{ H1(b1) where b1 is Element of y : S2[b1] } is set
yp1 is set
{yp1} is non empty trivial finite 1 -element set
x " {yp1} is set
yp1 \/ (x " {yp1}) is set
xx is set
e is Element of y
{e} is non empty trivial finite 1 -element set
x " {e} is set
e \/ (x " {e}) is set
union { H1(b1) where b1 is Element of y : S2[b1] } is set
xx is set
e is set
xx is set
e is set
e is Element of the carrier of n
x . e is set
{(x . e)} is non empty trivial finite 1 -element set
x " {(x . e)} is set
(x . e) \/ (x " {(x . e)}) is set
{e} is non empty trivial finite 1 -element set
x " {e} is set
e \/ (x " {e}) is set
xx is Element of bool the carrier of n
e is Element of y
{e} is non empty trivial finite 1 -element set
x " {e} is set
e \/ (x " {e}) is set
e is Element of bool the carrier of n
n2 is Element of y
{n2} is non empty trivial finite 1 -element set
x " {n2} is set
n2 \/ (x " {n2}) is set
se is set
e is set
xx is V89() a_partition of the carrier of n
n2 is Element of y
{n2} is non empty trivial finite 1 -element set
x " {n2} is set
n2 \/ (x " {n2}) is set
e is Element of bool the carrier of n
se is Element of the carrier of n
mp1 is Element of the carrier of n
x . mp1 is set
(n,mp1) is Element of bool the carrier of n
x . se is set
(n,se) is Element of bool the carrier of n

(card R) - (card {cMRn1}) is V63() ext-real real set

(card R) - 1 is V63() ext-real real set
((card R) - 1) + 1 is V63() ext-real real set

dom e is set
rng e is set
e is V89() StableSet-wise a_partition of the carrier of n
n2 is set
se is set
e . se is set
{se} is non empty trivial finite 1 -element set
x " {se} is set
se \/ (x " {se}) is set
[:y,e:] is set
bool [:y,e:] is non empty set

se is set
dom n2 is finite set
mp1 is set
n2 . se is set
n2 . mp1 is set
dom n2 is finite Element of bool y
bool y is non empty finite V32() set
{se} is non empty trivial finite 1 -element set
x " {se} is set
se \/ (x " {se}) is set
{mp1} is non empty trivial finite 1 -element set
x " {mp1} is set
mp1 \/ (x " {mp1}) is set
m is set
mn is Element of bool the carrier of n
m is set
mn is Element of bool the carrier of n
rng n2 is finite set
se is set
mp1 is Element of y
{mp1} is non empty trivial finite 1 -element set
x " {mp1} is set
mp1 \/ (x " {mp1}) is set
n2 . mp1 is Element of e

[:n,n:] is finite set
bool [:n,n:] is non empty finite V32() set

RelStr(# n,R #) is strict RelStr
the carrier of RelStr(# n,R #) is set
n is strict ( 0 )

R is strict (n)

R is strict (n)
[:n,n:] is finite set
bool [:n,n:] is non empty finite V32() set

RelStr(# n,R #) is strict RelStr
iMRn is finite strict with_finite_clique# with_finite_stability# () () (n)
cMRn1 is set
the carrier of iMRn is finite set
[cMRn1,cMRn1] is non empty set
{cMRn1,cMRn1} is non empty finite set
{cMRn1} is non empty trivial finite 1 -element set
{{cMRn1,cMRn1},{cMRn1}} is non empty finite V32() set
the InternalRel of iMRn is Relation-like the carrier of iMRn -defined the carrier of iMRn -valued finite Element of bool [: the carrier of iMRn, the carrier of iMRn:]
[: the carrier of iMRn, the carrier of iMRn:] is finite set
bool [: the carrier of iMRn, the carrier of iMRn:] is non empty finite V32() set

[:n,n:] is finite set

[:n,n:] \ (id n) is Relation-like n -defined n -valued finite Element of bool [:n,n:]
bool [:n,n:] is non empty finite V32() set

R \ (id n) is Relation-like n -defined n -valued finite Element of bool [:n,n:]
RelStr(# n,(R \ (id n)) #) is strict RelStr

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued finite Element of bool [: the carrier of S, the carrier of S:]
the carrier of S is finite set
[: the carrier of S, the carrier of S:] is finite set
bool [: the carrier of S, the carrier of S:] is non empty finite V32() set

the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued finite Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is finite set
[: the carrier of R, the carrier of R:] is finite set
bool [: the carrier of R, the carrier of R:] is non empty finite V32() set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued finite Element of bool [: the carrier of S, the carrier of S:]
the carrier of S is finite set
[: the carrier of S, the carrier of S:] is finite set
bool [: the carrier of S, the carrier of S:] is non empty finite V32() set

(n) is finite strict with_finite_clique# with_finite_stability# () () (n)
the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite Element of bool [: the carrier of (n), the carrier of (n):]
the carrier of (n) is finite set
[: the carrier of (n), the carrier of (n):] is finite set
bool [: the carrier of (n), the carrier of (n):] is non empty finite V32() set
R is set
S is set
[R,S] is non empty set
{R,S} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,S},{R}} is non empty finite V32() set
[:n,n:] is finite set

[:n,n:] \ (id n) is Relation-like n -defined n -valued finite Element of bool [:n,n:]
bool [:n,n:] is non empty finite V32() set

(n) is finite strict with_finite_clique# with_finite_stability# () () (n)
the carrier of (n) is finite set
the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite Element of bool [: the carrier of (n), the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is finite set
bool [: the carrier of (n), the carrier of (n):] is non empty finite V32() set
cMRn1 is set
[cMRn1,cMRn1] is non empty set
{cMRn1,cMRn1} is non empty finite set
{cMRn1} is non empty trivial finite 1 -element set
{{cMRn1,cMRn1},{cMRn1}} is non empty finite V32() set
cMRn1 is set
iMRn1 is set
[cMRn1,iMRn1] is non empty set
{cMRn1,iMRn1} is non empty finite set
{cMRn1} is non empty trivial finite 1 -element set
{{cMRn1,iMRn1},{cMRn1}} is non empty finite V32() set
[iMRn1,cMRn1] is non empty set
{iMRn1,cMRn1} is non empty finite set
{iMRn1} is non empty trivial finite 1 -element set
{{iMRn1,cMRn1},{iMRn1}} is non empty finite V32() set

[#] (n) is non proper finite Element of bool the carrier of (n)
the carrier of (n) is finite set
bool the carrier of (n) is non empty finite V32() set
the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite Element of bool [: the carrier of (n), the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is finite set
bool [: the carrier of (n), the carrier of (n):] is non empty finite V32() set
iMRn is set
cMRn1 is set
[iMRn,cMRn1] is non empty set
{iMRn,cMRn1} is non empty finite set
{iMRn} is non empty trivial finite 1 -element set
{{iMRn,cMRn1},{iMRn}} is non empty finite V32() set
[cMRn1,iMRn] is non empty set
{cMRn1,iMRn} is non empty finite set
{cMRn1} is non empty trivial finite 1 -element set
{{cMRn1,iMRn},{cMRn1}} is non empty finite V32() set

[#] (n) is non proper non proper finite connected Element of bool the carrier of (n)
the carrier of (n) is finite set
bool the carrier of (n) is non empty finite V32() set
S is finite connected Element of bool the carrier of (n)

S is finite connected Element of bool the carrier of (n)

(n) is non empty finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (n)

[#] (n) is non empty non proper non proper finite connected Element of bool the carrier of (n)
the carrier of (n) is non empty finite set
bool the carrier of (n) is non empty finite V32() set

the carrier of (n) is finite set

(n) is non empty finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (n)

the carrier of (n) is non empty finite set
{ the carrier of (n)} is non empty trivial finite V32() 1 -element set
cMRn1 is set
iMRn is non empty finite V32() V89() a_partition of the carrier of (n)
[#] (n) is non empty non proper non proper finite connected Element of bool the carrier of (n)
bool the carrier of (n) is non empty finite V32() set
cMRn1 is non empty finite V32() V89() a_partition of the carrier of (n)

cMRn1 is non empty finite V32() V89() Clique-wise a_partition of the carrier of (n)

cMRn1 is non empty finite V32() V89() a_partition of the carrier of (n)

the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued finite Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is finite set
[: the carrier of R, the carrier of R:] is finite set
bool [: the carrier of R, the carrier of R:] is non empty finite V32() set
{ [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
{ [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
( the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ { [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
{(2 * n)} is non empty trivial finite V32() 1 -element set
(2 * n) \ n is finite Element of bool (2 * n)
bool (2 * n) is non empty finite V32() set
[:{(2 * n)},((2 * n) \ n):] is finite set
(( the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ { [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ { [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set

[:((2 * n) + 1),((2 * n) + 1):] is non empty finite set
N is set
x is set
y is set
[x,y] is non empty set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V32() set

[x,(y + n)] is non empty set
{x,(y + n)} is non empty finite V32() set
{x} is non empty trivial finite V32() 1 -element set
{{x,(y + n)},{x}} is non empty finite V32() set
[x,y] is non empty set
{x,y} is non empty finite V32() set
{{x,y},{x}} is non empty finite V32() set

[(x + n),y] is non empty set
{(x + n),y} is non empty finite V32() set
{(x + n)} is non empty trivial finite V32() 1 -element set
{{(x + n),y},{(x + n)}} is non empty finite V32() set
[x,y] is non empty set
{x,y} is non empty finite V32() set
{x} is non empty trivial finite V32() 1 -element set
{{x,y},{x}} is non empty finite V32() set
x is set
y is set
[x,y] is non empty set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V32() set

x is set
y is set
[x,y] is non empty set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V32() set

bool [:((2 * n) + 1),((2 * n) + 1):] is non empty finite V32() set
N is Relation-like (2 * n) + 1 -defined (2 * n) + 1 -valued finite Element of bool [:((2 * n) + 1),((2 * n) + 1):]
RelStr(# ((2 * n) + 1),N #) is non empty strict RelStr
the InternalRel of RelStr(# ((2 * n) + 1),N #) is Relation-like the carrier of RelStr(# ((2 * n) + 1),N #) -defined the carrier of RelStr(# ((2 * n) + 1),N #) -valued Element of bool [: the carrier of RelStr(# ((2 * n) + 1),N #), the carrier of RelStr(# ((2 * n) + 1),N #):]
the carrier of RelStr(# ((2 * n) + 1),N #) is non empty set
[: the carrier of RelStr(# ((2 * n) + 1),N #), the carrier of RelStr(# ((2 * n) + 1),N #):] is non empty set
bool [: the carrier of RelStr(# ((2 * n) + 1),N #), the carrier of RelStr(# ((2 * n) + 1),N #):] is non empty set
S is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued finite Element of bool [: the carrier of S, the carrier of S:]
the carrier of S is non empty finite set
[: the carrier of S, the carrier of S:] is non empty finite set
bool [: the carrier of S, the carrier of S:] is non empty finite V32() set
iMRn is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
the InternalRel of iMRn is Relation-like the carrier of iMRn -defined the carrier of iMRn -valued finite Element of bool [: the carrier of iMRn, the carrier of iMRn:]
the carrier of iMRn is non empty finite set
[: the carrier of iMRn, the carrier of iMRn:] is non empty finite set
bool [: the carrier of iMRn, the carrier of iMRn:] is non empty finite V32() set

the carrier of R is finite set
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)

the carrier of (n,R) is non empty finite set

(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)

the InternalRel of (n,R) is Relation-like the carrier of (n,R) -defined the carrier of (n,R) -valued finite Element of bool [: the carrier of (n,R), the carrier of (n,R):]
the carrier of (n,R) is non empty finite set
[: the carrier of (n,R), the carrier of (n,R):] is non empty finite set
bool [: the carrier of (n,R), the carrier of (n,R):] is non empty finite V32() set

[S,iMRn] is non empty set
{S,iMRn} is non empty finite V32() set
{S} is non empty trivial finite V32() 1 -element set
{{S,iMRn},{S}} is non empty finite V32() set
the carrier of R is finite set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued finite Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is finite set
bool [: the carrier of R, the carrier of R:] is non empty finite V32() set
{ [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
{ [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
( the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ { [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } is set
{(2 * n)} is non empty trivial finite V32() 1 -element set
(2 * n) \ n is finite Element of bool (2 * n)
bool (2 * n) is non empty finite V32() set
[:{(2 * n)},((2 * n) \ n):] is finite set
(( the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ { [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ { [(b1 + n),b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b1,b2] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set

[N,(x + n)] is non empty set
{N,(x + n)} is non empty finite V32() set
{N} is non empty trivial finite V32() 1 -element set
{{N,(x + n)},{N}} is non empty finite V32() set
[N,x] is non empty set
{N,x} is non empty finite V32() set
{{N,x},{N}} is non empty finite V32() set

[(N + n),x] is non empty set
{(N + n),x} is non empty finite V32() set
{(N + n)} is non empty trivial finite V32() 1 -element set
{{(N + n),x},{(N + n)}} is non empty finite V32() set
[N,x] is non empty set
{N,x} is non empty finite V32() set
{N} is non empty trivial finite V32() 1 -element set
{{N,x},{N}} is non empty finite V32() set

the carrier of R is finite set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued finite Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is finite set
bool [: the carrier of R, the carrier of R:] is non empty finite V32() set
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)

the InternalRel of (n,R) is Relation-like the carrier of (n,R) -defined the carrier of (n,R) -valued finite Element of bool [: the carrier of (n,R), the carrier of (n,R):]
the carrier of (n,R) is non empty finite set
[: the carrier of (n,R), the carrier of (n,R):] is non empty finite set
bool [: the carrier of (n,R), the carrier of (n,R):] is non empty finite V32() set
{ [b1,(b2 + n)] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Ele