:: MYCIELSK semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
COMPLEX is set
bool NAT is non empty non trivial non finite set
{} is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real set
the empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real set is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of NAT
0 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of NAT
card {} is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real 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
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative 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
n is symmetric RelStr
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
n is symmetric RelStr
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
card n is epsilon-transitive epsilon-connected ordinal cardinal set
R is V89() a_partition of n
card R is epsilon-transitive epsilon-connected ordinal cardinal set
S is set
choose S is Element of S
the Element of S is Element of S
S is Relation-like Function-like set
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
{ (b₁ /\ S) where b₁ is Element of R : not b₁ 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 { (b₁ /\ S) where b₁ is Element of R : not b₁ 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
{ (b₁ /\ S) where b₁ is Element of R : not b₁ misses S } is set
iMRn is set
iMRn /\ S is Element of bool n
iMRn is Relation-like Function-like set
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
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
S is Element of bool n
(n,R,S) is finite V89() a_partition of S
{ (b₁ /\ S) where b₁ is Element of R : not b₁ misses S } is set
card (n,R,S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn is non empty finite set
{ H₁(b₁) where b₁ is Element of iMRn : S₁[b₁] } is set
card iMRn is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
n is set
bool n is non empty set
R is finite V89() a_partition of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
S is Element of bool n
(n,R,S) is finite V89() a_partition of S
{ (b₁ /\ S) where b₁ is Element of R : not b₁ misses S } is set
card (n,R,S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
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
x is Relation-like R -defined N -valued Function-like V21(R) quasi_total finite Element of bool [:R,N:]
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
{ (b₁ /\ S) where b₁ is Element of R : not b₁ misses S } is set
subrelstr S is strict V76(n) SubRelStr of n
the carrier of (subrelstr S) 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 (subrelstr S) is non empty set
y is Element of bool the carrier of (subrelstr S)
xp1 is Element of the carrier of (subrelstr S)
yp1 is Element of the carrier of (subrelstr S)
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
the empty trivial finite {} -element with_finite_clique# with_finite_stability# RelStr is empty trivial finite {} -element with_finite_clique# with_finite_stability# RelStr
n is empty trivial finite {} -element with_finite_clique# with_finite_stability# RelStr
the carrier of n is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real set
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
{ H₁(b₁) where b₁ is Element of S : S₁[b₁] } 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 (subrelstr R) is set
( the carrier of n,iMRn,R) is V89() a_partition of R
{ (b₁ /\ R) where b₁ is Element of iMRn : not b₁ misses R } is set
cMRn1 is V89() a_partition of R
bool the carrier of (subrelstr R) 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
card R is epsilon-transitive epsilon-connected ordinal cardinal set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn is finite V89() StableSet-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn is finite V89() StableSet-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn is finite V89() StableSet-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn is finite V89() StableSet-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is empty trivial finite {} -element with_finite_clique# with_finite_stability# () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real set
R is finite V32() V89() StableSet-wise a_partition of the carrier of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is non empty () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is non empty set
R is non empty finite V89() StableSet-wise a_partition of the carrier of n
card R is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
the empty trivial finite {} -element with_finite_clique# with_finite_stability# () RelStr is empty trivial finite {} -element with_finite_clique# with_finite_stability# () RelStr
n is empty trivial finite {} -element with_finite_clique# with_finite_stability# () RelStr
the carrier of n is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real set
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
{ H₁(b₁) where b₁ is Element of S : S₁[b₁] } 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 (subrelstr R) is set
( the carrier of n,iMRn,R) is V89() a_partition of R
{ (b₁ /\ R) where b₁ is Element of iMRn : not b₁ misses R } is set
cMRn1 is V89() a_partition of R
bool the carrier of (subrelstr R) 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
card R is epsilon-transitive epsilon-connected ordinal cardinal set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn is finite V89() Clique-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn is finite V89() Clique-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn is finite V89() Clique-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn is finite V89() Clique-wise a_partition of the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite V89() Clique-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite V89() Clique-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is empty trivial finite {} -element with_finite_clique# with_finite_stability# () () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real set
R is finite V32() V89() Clique-wise StableSet-wise a_partition of the carrier of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is non empty () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is non empty set
R is non empty finite V89() Clique-wise a_partition of the carrier of n
card R is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
n is finite with_finite_clique# with_finite_stability# () () RelStr
clique# n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is finite set
card the carrier of n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
bool the carrier of n is non empty finite V32() set
R is finite connected Element of bool the carrier of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is finite with_finite_clique# with_finite_stability# () () RelStr
stability# n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is finite set
card the carrier of n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
bool the carrier of n is non empty finite V32() set
R is finite stable Element of bool the carrier of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is finite with_finite_clique# with_finite_stability# () () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is finite set
card the carrier of n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
R is finite V32() V89() StableSet-wise a_partition of the carrier of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is finite with_finite_clique# with_finite_stability# () () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of n is finite set
card the carrier of n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
R is finite V32() V89() Clique-wise a_partition of the carrier of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is with_finite_clique# () RelStr
clique# n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
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
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
S is finite V89() StableSet-wise a_partition of the carrier of n
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card (card S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card (card R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
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
cMRn1 is Relation-like R -defined S -valued Function-like quasi_total finite Element of bool [:R,S:]
iMRn1 is set
N is set
cMRn1 . iMRn1 is set
cMRn1 . N is set
n is with_finite_stability# () RelStr
stability# n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
S is finite V89() Clique-wise a_partition of the carrier of n
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card (card S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card (card R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
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
cMRn1 is Relation-like R -defined S -valued Function-like quasi_total finite Element of bool [:R,S:]
iMRn1 is set
N is set
cMRn1 . iMRn1 is set
cMRn1 . N is set
n is RelStr
the carrier of n is set
ComplRelStr n is strict irreflexive RelStr
the carrier of (ComplRelStr n) 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 (ComplRelStr n)
cMRn1 is Element of the carrier of (ComplRelStr 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
the InternalRel of (ComplRelStr n) is Relation-like the carrier of (ComplRelStr n) -defined the carrier of (ComplRelStr n) -valued Element of bool [: the carrier of (ComplRelStr n), the carrier of (ComplRelStr n):]
[: the carrier of (ComplRelStr n), the carrier of (ComplRelStr n):] is set
bool [: the carrier of (ComplRelStr n), the carrier of (ComplRelStr n):] 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
ComplRelStr n is strict irreflexive RelStr
the carrier of (ComplRelStr n) 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 (ComplRelStr n)
cMRn1 is Element of the carrier of (ComplRelStr 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
the InternalRel of (ComplRelStr n) is Relation-like the carrier of (ComplRelStr n) -defined the carrier of (ComplRelStr n) -valued Element of bool [: the carrier of (ComplRelStr n), the carrier of (ComplRelStr n):]
[: the carrier of (ComplRelStr n), the carrier of (ComplRelStr n):] is set
bool [: the carrier of (ComplRelStr n), the carrier of (ComplRelStr n):] 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 finite with_finite_clique# with_finite_stability# () () RelStr
ComplRelStr n is strict irreflexive RelStr
the carrier of n is finite set
the carrier of (ComplRelStr n) is set
n is symmetric RelStr
the carrier of n is set
bool the carrier of n is non empty set
ComplRelStr n is strict symmetric irreflexive RelStr
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) is non empty set
R is connected Element of bool the carrier of n
S is Element of the carrier of (ComplRelStr n)
iMRn is Element of the carrier of (ComplRelStr n)
cMRn1 is Element of the carrier of n
iMRn1 is Element of the carrier of n
n is symmetric RelStr
ComplRelStr n is strict symmetric irreflexive RelStr
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) 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 (ComplRelStr n)
S is Element of the carrier of n
iMRn is Element of the carrier of n
cMRn1 is Element of the carrier of (ComplRelStr n)
iMRn1 is Element of the carrier of (ComplRelStr n)
n is RelStr
the carrier of n is set
bool the carrier of n is non empty set
ComplRelStr n is strict irreflexive RelStr
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) is non empty set
R is stable Element of bool the carrier of n
iMRn is Element of the carrier of (ComplRelStr n)
cMRn1 is Element of the carrier of (ComplRelStr n)
iMRn1 is Element of the carrier of n
N is Element of the carrier of n
n is RelStr
ComplRelStr n is strict irreflexive RelStr
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) 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 (ComplRelStr n)
S is Element of the carrier of n
iMRn is Element of the carrier of n
cMRn1 is Element of the carrier of (ComplRelStr n)
iMRn1 is Element of the carrier of (ComplRelStr n)
n is with_finite_clique# RelStr
ComplRelStr n is strict irreflexive RelStr
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
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) is non empty set
iMRn is finite stable Element of bool the carrier of (ComplRelStr n)
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
{} (ComplRelStr n) is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element strongly_connected V63() ext-real non positive non negative real connected stable Element of bool the carrier of (ComplRelStr n)
card ({} (ComplRelStr n)) is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real Element of omega
iMRn is finite stable Element of bool the carrier of (ComplRelStr n)
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
cMRn1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
iMRn1 is finite stable Element of bool the carrier of (ComplRelStr n)
card iMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn1 is finite stable Element of bool the carrier of (ComplRelStr n)
card iMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
N is finite stable Element of bool the carrier of (ComplRelStr n)
card N is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite stable Element of bool the carrier of (ComplRelStr n)
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is symmetric with_finite_stability# RelStr
ComplRelStr n is strict symmetric irreflexive RelStr
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
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) is non empty set
iMRn is finite connected Element of bool the carrier of (ComplRelStr n)
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
{} (ComplRelStr n) is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element strongly_connected V63() ext-real non positive non negative real connected stable Element of bool the carrier of (ComplRelStr n)
card ({} (ComplRelStr n)) is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V32() cardinal {} -element V63() ext-real non positive non negative real Element of omega
iMRn is finite connected Element of bool the carrier of (ComplRelStr n)
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
cMRn1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
iMRn1 is finite connected Element of bool the carrier of (ComplRelStr n)
card iMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn1 is finite connected Element of bool the carrier of (ComplRelStr n)
card iMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
N is finite connected Element of bool the carrier of (ComplRelStr n)
card N is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite connected Element of bool the carrier of (ComplRelStr n)
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is symmetric with_finite_clique# RelStr
clique# n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
ComplRelStr n is strict symmetric irreflexive with_finite_stability# RelStr
stability# (ComplRelStr n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) is non empty set
S is finite stable Element of bool the carrier of (ComplRelStr n)
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
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
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
iMRn is finite connected Element of bool the carrier of n
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is symmetric with_finite_stability# RelStr
stability# n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
ComplRelStr n is strict symmetric irreflexive with_finite_clique# RelStr
clique# (ComplRelStr n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of (ComplRelStr n) is set
bool the carrier of (ComplRelStr n) is non empty set
iMRn is finite connected Element of bool the carrier of (ComplRelStr n)
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
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
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite stable Element of bool the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is RelStr
the carrier of n is set
ComplRelStr n is strict irreflexive RelStr
the carrier of (ComplRelStr n) 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 (ComplRelStr n) is non empty set
n is symmetric RelStr
ComplRelStr n is strict symmetric irreflexive RelStr
the carrier of (ComplRelStr n) is set
the carrier of n is set
R is V89() Clique-wise a_partition of the carrier of (ComplRelStr n)
iMRn is set
bool the carrier of (ComplRelStr n) is non empty set
bool the carrier of n is non empty set
n is symmetric RelStr
the carrier of n is set
ComplRelStr n is strict symmetric irreflexive RelStr
the carrier of (ComplRelStr n) 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 (ComplRelStr n) is non empty set
n is RelStr
ComplRelStr n is strict irreflexive RelStr
the carrier of (ComplRelStr n) is set
the carrier of n is set
R is V89() StableSet-wise a_partition of the carrier of (ComplRelStr n)
iMRn is set
bool the carrier of (ComplRelStr n) is non empty set
bool the carrier of n is non empty set
n is () RelStr
ComplRelStr n is strict irreflexive RelStr
the carrier of n is set
R is V89() StableSet-wise a_partition of the carrier of n
the carrier of (ComplRelStr n) is set
n is symmetric () RelStr
ComplRelStr n is strict symmetric irreflexive RelStr
the carrier of n is set
R is V89() Clique-wise a_partition of the carrier of n
the carrier of (ComplRelStr n) is set
n is symmetric () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
ComplRelStr n is strict symmetric irreflexive () RelStr
((ComplRelStr n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of (ComplRelStr n) is set
iMRn is finite V89() Clique-wise a_partition of the carrier of (ComplRelStr n)
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
the carrier of n is set
cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite V89() StableSet-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is symmetric () RelStr
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
ComplRelStr n is strict symmetric irreflexive () RelStr
((ComplRelStr n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of (ComplRelStr n) is set
iMRn is finite V89() StableSet-wise a_partition of the carrier of (ComplRelStr n)
card iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
the carrier of n is set
cMRn1 is finite V89() Clique-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
cMRn1 is finite V89() Clique-wise a_partition of the carrier of n
card cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
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
{ b₁ where b₁ is Element of the carrier of n : ( b₁ < R or R < b₁ ) } 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
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite V89() StableSet-wise a_partition of the carrier of n
card R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
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 {cMRn1} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
(card R) - (card {cMRn1}) is V63() ext-real real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative 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
x is Relation-like Function-like set
dom x is set
N is non empty set
y is non empty finite set
{ H₁(b₁) where b₁ is Element of y : S₂[b₁] } 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 { H₁(b₁) where b₁ is Element of y : S₂[b₁] } 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 y is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
card {cMRn1} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
(card R) - (card {cMRn1}) is V63() ext-real real set
(card y) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(card R) - 1 is V63() ext-real real set
((card R) - 1) + 1 is V63() ext-real real set
e is Relation-like Function-like 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
n2 is Relation-like y -defined e -valued Function-like quasi_total finite Element of bool [:y,e:]
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
card e is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[:n,n:] is finite set
bool [:n,n:] is non empty finite V32() set
R is Relation-like n -defined n -valued finite Element of bool [:n,n:]
RelStr(# n,R #) is strict RelStr
the carrier of RelStr(# n,R #) is set
n is strict ( 0 )
n is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
R is strict (n)
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is strict (n)
[:n,n:] is finite set
bool [:n,n:] is non empty finite V32() set
R is Relation-like n -defined n -valued finite Element of bool [:n,n:]
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 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[:n,n:] is finite set
id n is Relation-like 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 is Relation-like n -defined n -valued finite Element of bool [:n,n:]
R \ (id n) is Relation-like n -defined n -valued finite Element of bool [:n,n:]
RelStr(# n,(R \ (id n)) #) is strict RelStr
S is finite strict with_finite_clique# with_finite_stability# () () (n)
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
R is finite strict with_finite_clique# with_finite_stability# () () (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
S is finite strict with_finite_clique# with_finite_stability# () () (n)
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 epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
id n is Relation-like 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 epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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 epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (n)
[#] (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 epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (n)
clique# (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
card n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card (card n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
[#] (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)
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card the carrier of (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
S is finite connected Element of bool the carrier of (n)
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(n) is non empty finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (n)
stability# (n) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
[#] (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
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (n)
((n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
clique# (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
the carrier of (n) is finite set
card the carrier of (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card (card n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(n) is non empty finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (n)
((n)) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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)
card cMRn1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
cMRn1 is non empty finite V32() V89() Clique-wise a_partition of the carrier of (n)
card cMRn1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
cMRn1 is non empty finite V32() V89() a_partition of the carrier of (n)
card cMRn1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (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
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
yp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
x + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
[(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
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
yp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
yp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
the carrier of R is finite set
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
the carrier of (n,R) is non empty finite set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
N is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
x + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
N is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
N + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
[(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
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
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)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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
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
S is set
iMRn is set
[S,iMRn] is non empty set
{S,iMRn} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,iMRn},{S}} is non empty finite V32() set
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
n - n is V63() ext-real real set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
x + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
[(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
n - n is V63() ext-real real 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
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n - n is V63() ext-real real 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
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n - n is V63() ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (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
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
iMRn + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[S,(iMRn + n)] is non empty set
{S,(iMRn + n)} is non empty finite V32() set
{{S,(iMRn + n)},{S}} is non empty finite V32() set
S + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[(S + n),iMRn] is non empty set
{(S + n),iMRn} is non empty finite V32() set
{(S + n)} is non empty trivial finite V32() 1 -element set
{{(S + n),iMRn},{(S + n)}} is non empty finite V32() set
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real 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
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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
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
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
iMRn + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[S,(iMRn + n)] is non empty set
{S,(iMRn + n)} is non empty finite V32() set
{S} is non empty trivial finite V32() 1 -element set
{{S,(iMRn + n)},{S}} is non empty finite V32() set
[S,iMRn] is non empty set
{S,iMRn} is non empty finite V32() set
{{S,iMRn},{S}} is non empty finite V32() set
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
n - n is V63() ext-real real set
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
xp1 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[y,(xp1 + n)] is non empty set
{y,(xp1 + n)} is non empty finite V32() set
{y} is non empty trivial finite V32() 1 -element set
{{y,(xp1 + n)},{y}} is non empty finite V32() set
[y,xp1] is non empty set
{y,xp1} is non empty finite V32() set
{{y,xp1},{y}} is non empty finite V32() set
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
[(y + n),xp1] is non empty set
{(y + n),xp1} is non empty finite V32() set
{(y + n)} is non empty trivial finite V32() 1 -element set
{{(y + n),xp1},{(y + n)}} is non empty finite V32() set
[y,xp1] is non empty set
{y,xp1} is non empty finite V32() set
{y} is non empty trivial finite V32() 1 -element set
{{y,xp1},{y}} is non empty finite V32() set
n - n is V63() ext-real real set
y is set
xp1 is set
[y,xp1] is non empty set
{y,xp1} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,xp1},{y}} is non empty finite V32() set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n - n is V63() ext-real real set
y is set
xp1 is set
[y,xp1] is non empty set
{y,xp1} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,xp1},{y}} is non empty finite V32() set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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
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
iMRn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
S + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[(S + n),iMRn] is non empty set
{(S + n),iMRn} is non empty finite V32() set
{(S + n)} is non empty trivial finite V32() 1 -element set
{{(S + n),iMRn},{(S + n)}} 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
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
n - n is V63() ext-real real set
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
xp1 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[y,(xp1 + n)] is non empty set
{y,(xp1 + n)} is non empty finite V32() set
{y} is non empty trivial finite V32() 1 -element set
{{y,(xp1 + n)},{y}} is non empty finite V32() set
[y,xp1] is non empty set
{y,xp1} is non empty finite V32() set
{{y,xp1},{y}} is non empty finite V32() set
n - n is V63() ext-real real set
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
y + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
[(y + n),xp1] is non empty set
{(y + n),xp1} is non empty finite V32() set
{(y + n)} is non empty trivial finite V32() 1 -element set
{{(y + n),xp1},{(y + n)}} is non empty finite V32() set
[y,xp1] is non empty set
{y,xp1} is non empty finite V32() set
{y} is non empty trivial finite V32() 1 -element set
{{y,xp1},{y}} is non empty finite V32() set
y is set
xp1 is set
[y,xp1] is non empty set
{y,xp1} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,xp1},{y}} is non empty finite V32() set
y is set
xp1 is set
[y,xp1] is non empty set
{y,xp1} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,xp1},{y}} is non empty finite V32() set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n - n is V63() ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
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 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[S,(2 * n)] is non empty set
{S,(2 * n)} is non empty finite V32() set
{S} is non empty trivial finite V32() 1 -element set
{{S,(2 * n)},{S}} is non empty finite V32() set
[(2 * n),S] is non empty set
{(2 * n),S} is non empty finite V32() set
{(2 * n)} is non empty trivial finite V32() 1 -element set
{{(2 * n),S},{(2 * n)}} 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
{ [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
{ [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is set
( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } is 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 \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):] is set
[:((2 * n) \ n),{(2 * n)}:] is finite set
((( the InternalRel of R \/ { [b₁,(b₂ + n)] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ { [(b₁ + n),b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : [b₁,b₂] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict with_finite_clique# with_finite_stability# () () (n)
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
the carrier of (n,R) is non empty finite set
bool the carrier of (n,R) is non empty finite V32() set
S is finite Element of bool the carrier of (n,R)
subrelstr S is finite strict V76((n,R)) with_finite_clique# with_finite_stability# () () SubRelStr of (n,R)
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
the carrier of (subrelstr S) is finite set
the InternalRel of (subrelstr S) is Relation-like the carrier of (subrelstr S) -defined the carrier of (subrelstr S) -valued finite Element of bool [: the carrier of (subrelstr S), the carrier of (subrelstr S):]
[: the carrier of (subrelstr S), the carrier of (subrelstr S):] is finite set
bool [: the carrier of (subrelstr S), the carrier of (subrelstr S):] is non empty finite V32() set
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), 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
xx is set
e is set
e is set
[e,e] is non empty set
{e,e} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,e},{e}} is non empty finite V32() set
n2 is Element of the carrier of (n,R)
se is Element of the carrier of (n,R)
mp1 is Element of the carrier of (subrelstr S)
m is Element of the carrier of (subrelstr S)
xx is set
e is set
e is set
[e,e] is non empty set
{e,e} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,e},{e}} is non empty finite V32() set
mp1 is Element of the carrier of (subrelstr S)
m is Element of the carrier of (subrelstr S)
n2 is Element of the carrier of (n,R)
se is Element of the carrier of (n,R)
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict irreflexive with_finite_clique# with_finite_stability# () () (n)
clique# R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
clique# (n,R) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real 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
the carrier of (n,R) is non empty finite set
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), 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
bool the carrier of R is non empty finite V32() set
y is finite connected Element of bool the carrier of R
card y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
bool the carrier of (n,R) is non empty finite V32() set
xp1 is finite Element of bool the carrier of (n,R)
subrelstr xp1 is finite strict V76((n,R)) with_finite_clique# with_finite_stability# () () SubRelStr of (n,R)
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
yp1 is finite connected Element of bool the carrier of (n,R)
card yp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
yp1 /\ xp1 is finite Element of bool the carrier of (n,R)
xx is set
e is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n2 is set
se is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{e,se} is non empty finite V32() set
yp1 \ {e,se} is finite Element of bool the carrier of (n,R)
card (yp1 \ {e,se}) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card {e,se} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
(card yp1) - (card {e,se}) is V63() ext-real real set
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(1 + 2) - 2 is V63() ext-real real set
(card yp1) - 2 is V63() ext-real real set
mn is set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
e is Element of the carrier of (n,R)
mp1 is Element of the carrier of (n,R)
[e,se] is non empty set
{e} is non empty trivial finite V32() 1 -element set
{{e,se},{e}} is non empty finite V32() set
[se,e] is non empty set
{se,e} is non empty finite V32() set
{se} is non empty trivial finite V32() 1 -element set
{{se,e},{se}} is non empty finite V32() set
e is Element of the carrier of (n,R)
f is Element of the carrier of (n,R)
[e,f] is non empty set
{e,f} is non empty finite V32() set
{e} is non empty trivial finite V32() 1 -element set
{{e,f},{e}} is non empty finite V32() set
[f,e] is non empty set
{f,e} is non empty finite V32() set
{f} is non empty trivial finite V32() 1 -element set
{{f,e},{f}} is non empty finite V32() set
mp1 is Element of the carrier of (n,R)
[se,f] is non empty set
{se,f} is non empty finite V32() set
{se} is non empty trivial finite V32() 1 -element set
{{se,f},{se}} is non empty finite V32() set
[f,se] is non empty set
{f,se} is non empty finite V32() set
{{f,se},{f}} is non empty finite V32() set
mp1 is Element of the carrier of (n,R)
f is Element of the carrier of (n,R)
[se,f] is non empty set
{se,f} is non empty finite V32() set
{se} is non empty trivial finite V32() 1 -element set
{{se,f},{se}} is non empty finite V32() set
[f,se] is non empty set
{f,se} is non empty finite V32() set
{f} is non empty trivial finite V32() 1 -element set
{{f,se},{f}} is non empty finite V32() set
e is Element of the carrier of (n,R)
[e,f] is non empty set
{e,f} is non empty finite V32() set
{e} is non empty trivial finite V32() 1 -element set
{{e,f},{e}} is non empty finite V32() set
[f,e] is non empty set
{f,e} is non empty finite V32() set
{{f,e},{f}} is non empty finite V32() set
{e} is non empty trivial finite V32() 1 -element set
yp1 \ {e} is finite Element of bool the carrier of (n,R)
card (yp1 \ {e}) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
card {e} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
(card yp1) - (card {e}) is V63() ext-real real set
(card yp1) - 1 is V63() ext-real real set
n2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + n2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
e is Element of the carrier of (n,R)
se is Element of the carrier of (n,R)
[e,n2] is non empty set
{e,n2} is non empty finite V32() set
{{e,n2},{e}} is non empty finite V32() set
[n2,e] is non empty set
{n2,e} is non empty finite V32() set
{n2} is non empty trivial finite V32() 1 -element set
{{n2,e},{n2}} is non empty finite V32() set
[n2,n2] is non empty set
{n2,n2} is non empty finite V32() set
{{n2,n2},{n2}} is non empty finite V32() set
(yp1 \ {e}) \/ {n2} is non empty finite set
m is set
mn is Element of the carrier of R
m is finite Element of bool the carrier of R
f is Element of the carrier of R
sf is Element of the carrier of (n,R)
wp1 is Element of the carrier of (n,R)
sf is Element of the carrier of (n,R)
[sf,e] is non empty set
{sf,e} is non empty finite set
{sf} is non empty trivial finite 1 -element set
{{sf,e},{sf}} is non empty finite V32() set
[e,sf] is non empty set
{e,sf} is non empty finite set
{{e,sf},{e}} is non empty finite V32() set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[f,n2] is non empty set
{f,n2} is non empty finite V32() set
{f} is non empty trivial finite V32() 1 -element set
{{f,n2},{f}} is non empty finite V32() set
[n2,f] is non empty set
{n2,f} is non empty finite V32() set
{{n2,f},{n2}} is non empty finite V32() set
wp1 is Element of the carrier of (n,R)
[wp1,e] is non empty set
{wp1,e} is non empty finite set
{wp1} is non empty trivial finite 1 -element set
{{wp1,e},{wp1}} is non empty finite V32() set
[e,wp1] is non empty set
{e,wp1} is non empty finite set
{{e,wp1},{e}} is non empty finite V32() set
mnp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[mnp1,n2] is non empty set
{mnp1,n2} is non empty finite V32() set
{mnp1} is non empty trivial finite V32() 1 -element set
{{mnp1,n2},{mnp1}} is non empty finite V32() set
[n2,mnp1] is non empty set
{n2,mnp1} is non empty finite V32() set
{{n2,mnp1},{n2}} is non empty finite V32() set
mn is finite connected Element of bool the carrier of R
card mn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
((card yp1) - 1) + 1 is V63() ext-real real set
(2 + 1) - 1 is V63() ext-real real set
n2 is set
se is set
mp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
m is Element of the carrier of (n,R)
e is Element of the carrier of (n,R)
[mp1,e] is non empty set
{mp1,e} is non empty finite V32() set
{mp1} is non empty trivial finite V32() 1 -element set
{{mp1,e},{mp1}} is non empty finite V32() set
[e,mp1] is non empty set
{e,mp1} is non empty finite V32() set
{{e,mp1},{e}} is non empty finite V32() set
n is () RelStr
the carrier of n is set
bool the carrier of n is non empty set
(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is Element of bool the carrier of n
subrelstr R is strict V76(n) () SubRelStr of n
((subrelstr R)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
S is finite V89() StableSet-wise a_partition of the carrier of n
card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
( the carrier of n,S,R) is finite V89() a_partition of R
{ (b₁ /\ R) where b₁ is Element of S : not b₁ misses R } is set
the carrier of (subrelstr R) is set
card ( the carrier of n,S,R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is finite strict irreflexive with_finite_clique# with_finite_stability# () () (n)
(n,R) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * n) + 1)
2 * n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
((n,R)) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
1 + (R) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real 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
the carrier of (n,R) is non empty finite set
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), 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
xp1 is finite V32() V89() StableSet-wise a_partition of the carrier of R
card xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in a₁ } is set
yp1 is set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in yp1 } is set
yp1 is Relation-like Function-like set
dom yp1 is set
{ (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } is set
card { (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } is epsilon-transitive epsilon-connected ordinal cardinal set
e is set
yp1 . e is set
e \/ (yp1 . e) is set
e is set
yp1 . e is set
e \/ (yp1 . e) is set
e is Relation-like Function-like set
dom e is set
rng e is set
e is set
n2 is set
e . n2 is set
yp1 . n2 is set
n2 \/ (yp1 . n2) is set
[:xp1, { (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } :] is set
bool [:xp1, { (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } :] is non empty set
e is Relation-like xp1 -defined { (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } -valued Function-like quasi_total finite Element of bool [:xp1, { (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } :]
rng e is finite set
n2 is set
se is finite Element of xp1
yp1 . se is set
se \/ (yp1 . se) is set
e . se is set
n2 is set
dom e is finite set
se is set
e . n2 is set
e . se is set
dom e is finite V32() Element of bool xp1
bool xp1 is non empty finite V32() set
yp1 . n2 is set
n2 \/ (yp1 . n2) is set
yp1 . se is set
se \/ (yp1 . se) is set
mp1 is set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in se } is set
m is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
0 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mp1 is set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in n2 } is set
m is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
0 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{(2 * n)} is non empty trivial finite V32() 1 -element set
{{(2 * n)}} is non empty trivial finite V32() 1 -element set
{ (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } \/ {{(2 * n)}} is non empty set
union ( { (b₁ \/ (yp1 . b₁)) where b₁ is finite Element of xp1 : b₁ in xp1 } \/ {{(2 * n)}}) is set
e is set
n2 is set
se is finite Element of xp1
yp1 . se is set
se \/ (yp1 . se) is set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in se } is set
mp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mp1 + 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
mp1 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
bool the carrier of (n,R) is non empty finite V32() set
e is set
n2 is set
e is set
n2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
union xp1 is finite set
se is set
yp1 . se is set
se \/ (yp1 . se) is set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
se is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + se is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
union xp1 is finite set
m is set
yp1 . m is set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in m } is set
m \/ (yp1 . m) is set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
e is finite Element of bool the carrier of (n,R)
n2 is finite Element of xp1
yp1 . n2 is set
n2 \/ (yp1 . n2) is set
n2 is finite Element of bool the carrier of (n,R)
se is set
mp1 is finite Element of xp1
yp1 . mp1 is set
mp1 \/ (yp1 . mp1) is set
m is finite Element of xp1
yp1 . m is set
m \/ (yp1 . m) is set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in m } is set
mn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
mn + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in mp1 } is set
mn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
mn + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in mp1 } is set
mn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
mn + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in m } is set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
f + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mp1 is finite Element of xp1
yp1 . mp1 is set
mp1 \/ (yp1 . mp1) is set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in mp1 } is set
m is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mp1 is finite Element of xp1
yp1 . mp1 is set
mp1 \/ (yp1 . mp1) is set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in mp1 } is set
m is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n2 is set
e is non empty finite V32() V89() a_partition of the carrier of (n,R)
se is finite Element of xp1
yp1 . se is set
se \/ (yp1 . se) is set
bool the carrier of R is non empty finite V32() set
mp1 is finite Element of bool the carrier of R
yp1 . mp1 is set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in mp1 } is set
m is set
mn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
mn + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
m is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
mn is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
mn + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
m is Element of the carrier of (n,R)
mn is Element of the carrier of (n,R)
[m,mn] is non empty set
{m,mn} is non empty finite set
{m} is non empty trivial finite 1 -element set
{{m,mn},{m}} is non empty finite V32() set
[mn,m] is non empty set
{mn,m} is non empty finite set
{mn} is non empty trivial finite 1 -element set
{{mn,m},{mn}} is non empty finite V32() set
f is Element of the carrier of R
f is Element of the carrier of R
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
f + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[f,f] is non empty set
{f,f} is non empty finite V32() set
{f} is non empty trivial finite V32() 1 -element set
{{f,f},{f}} is non empty finite V32() set
[f,f] is non empty set
{f,f} is non empty finite V32() set
{f} is non empty trivial finite V32() 1 -element set
{{f,f},{f}} is non empty finite V32() set
mnp1 is Element of the carrier of R
sf is Element of the carrier of R
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
f + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[f,f] is non empty set
{f,f} is non empty finite V32() set
{f} is non empty trivial finite V32() 1 -element set
{{f,f},{f}} is non empty finite V32() set
[f,f] is non empty set
{f,f} is non empty finite V32() set
{f} is non empty trivial finite V32() 1 -element set
{{f,f},{f}} is non empty finite V32() set
mnp1 is Element of the carrier of R
sf is Element of the carrier of R
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
f + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
f + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n2 is non empty finite V32() V89() StableSet-wise a_partition of the carrier of (n,R)
card n2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
se is finite Element of xp1
yp1 . se is set
se \/ (yp1 . se) is set
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
{ (b₁ + n) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT : b₁ in se } is set
mp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
mp1 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
xp1 is non empty finite V32() V89() StableSet-wise a_partition of the carrier of (n,R)
card xp1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
n + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
bool the carrier of (n,R) is non empty finite V32() set
yp1 is finite Element of bool the carrier of (n,R)
subrelstr yp1 is finite strict V76((n,R)) with_finite_clique# with_finite_stability# () () SubRelStr of (n,R)
( the carrier of (n,R),xp1,yp1) is finite V32() V89() a_partition of yp1
{ (b₁ /\ yp1) where b₁ is Element of xp1 : not b₁ misses yp1 } is set
xx is finite V32() V89() StableSet-wise a_partition of the carrier of R
card xx is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of omega
union xp1 is finite set
e is set
e is finite Element of bool the carrier of (n,R)
e /\ yp1 is finite Element of bool the carrier of (n,R)
mp1 is Element of the carrier of R
(R,mp1) is finite Element of bool the carrier of R
bool the carrier of R is non empty finite V32() set
m is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
m + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
0 + n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
f is set
f is finite Element of bool the carrier of (n,R)
f /\ yp1 is finite Element of bool the carrier of (n,R)
wp1 is set
wp1 is Element of the carrier of R
w is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[m,w] is non empty set
{m,w} is non empty finite V32() set
{m} is non empty trivial finite V32() 1 -element set
{{m,w},{m}} is non empty finite V32() set
[w,m] is non empty set
{w,m} is non empty finite V32() set
{w} is non empty trivial finite V32() 1 -element set
{{w,m},{w}} is non empty finite V32() set
[(m + n),w] is non empty set
{(m + n),w} is non empty finite V32() set
{(m + n)} is non empty trivial finite V32() 1 -element set
{{(m + n),w},{(m + n)}} is non empty finite V32() set
[w,(m + n)] is non empty set
{w,(m + n)} is non empty finite V32() set
{{w,(m + n)},{w}} is non empty finite V32() set
wp2 is Element of the carrier of (n,R)
mnp1 is Element of the carrier of (n,R)
[(m + n),(2 * n)] is non empty set
{(m + n),(2 * n)} is non empty finite V32() set
{{(m + n),(2 * n)},{(m + n)}} is non empty finite V32() set
n2 is Element of the carrier of (n,R)
xp1 is non empty finite V32() V89() StableSet-wise a_partition of the carrier of (n,R)
card xp1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of omega
n is Relation-like Function-like set
dom n is set
n . 0 is set
(2) is non empty finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () (2)
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real Element of NAT
R is Relation-like Function-like set
dom R is set
R . 0 is set
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
3 * (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ 0)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
3 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(3 * 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(2 + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ 0)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n . S is set
2 |^ S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ S)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R . S is set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n . (S + 1) is set
2 |^ (S + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ (S + 1)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (S + 1))) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R . (S + 1) is set
iMRn is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ S)) -' 1)
(((3 * (2 |^ S)) -' 1),iMRn) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ S)) -' 1)) + 1)
2 * ((3 * (2 |^ S)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ S)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
1 * (2 |^ S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
1 - 1 is V63() ext-real real set
(3 * (2 |^ S)) - 1 is V63() ext-real real set
2 * (2 |^ S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (S + 1))) - 1 is V63() ext-real real set
2 * ((3 * (2 |^ S)) - 1) is V63() ext-real real set
(2 * ((3 * (2 |^ S)) - 1)) + 1 is V63() ext-real real set
3 * (2 * (2 |^ S)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 * (2 |^ S))) - 2 is V63() ext-real real set
((3 * (2 * (2 |^ S))) - 2) + 1 is V63() ext-real real set
(3 * (2 |^ (S + 1))) - 2 is V63() ext-real real set
((3 * (2 |^ (S + 1))) - 2) + 1 is V63() ext-real real set
S is set
n . S is set
R . S is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
2 |^ n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
S is set
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
iMRn is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ R)) -' 1)
(((3 * (2 |^ R)) -' 1),iMRn) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ R)) -' 1)) + 1)
2 * ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ R)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R is Relation-like Function-like set
dom R is set
R . 0 is set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R . S is set
2 |^ S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ S)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
R . (S + 1) is set
2 |^ (S + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ (S + 1)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (S + 1))) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
2 |^ S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
3 * (2 |^ S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ S)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
iMRn is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ S)) -' 1)
(((3 * (2 |^ S)) -' 1),iMRn) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ S)) -' 1)) + 1)
2 * ((3 * (2 |^ S)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ S)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
1 * (2 |^ S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
1 - 1 is V63() ext-real real set
(3 * (2 |^ S)) - 1 is V63() ext-real real set
2 * (2 |^ S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (S + 1))) - 1 is V63() ext-real real set
2 * ((3 * (2 |^ S)) - 1) is V63() ext-real real set
(2 * ((3 * (2 |^ S)) - 1)) + 1 is V63() ext-real real set
3 * (2 * (2 |^ S)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 * (2 |^ S))) - 2 is V63() ext-real real set
((3 * (2 * (2 |^ S))) - 2) + 1 is V63() ext-real real set
(3 * (2 |^ (S + 1))) - 2 is V63() ext-real real set
((3 * (2 |^ (S + 1))) - 2) + 1 is V63() ext-real real set
R . n is set
S is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
iMRn is Relation-like Function-like set
iMRn . n is set
dom iMRn is set
iMRn . 0 is set
cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
2 |^ cMRn1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ cMRn1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ cMRn1)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
iMRn . cMRn1 is set
cMRn1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
iMRn . (cMRn1 + 1) is set
iMRn1 is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ cMRn1)) -' 1)
(((3 * (2 |^ cMRn1)) -' 1),iMRn1) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ cMRn1)) -' 1)) + 1)
2 * ((3 * (2 |^ cMRn1)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ cMRn1)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
R . cMRn1 is set
R . (cMRn1 + 1) is set
N is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ cMRn1)) -' 1)
(((3 * (2 |^ cMRn1)) -' 1),N) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ cMRn1)) -' 1)) + 1)
R is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
iMRn is Relation-like Function-like set
iMRn . n is set
dom iMRn is set
iMRn . 0 is set
S is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
cMRn1 is Relation-like Function-like set
cMRn1 . n is set
dom cMRn1 is set
cMRn1 . 0 is set
(0) is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ 0)) -' 1)
n is Relation-like Function-like set
n . 0 is set
dom n is set
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
((R + 1)) is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ (R + 1))) -' 1)
2 |^ (R + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ (R + 1)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (R + 1))) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
(R) is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ R)) -' 1)
(((3 * (2 |^ R)) -' 1),(R)) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ R)) -' 1)) + 1)
2 * ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ R)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
S is Relation-like Function-like set
S . R is set
dom S is set
S . 0 is set
iMRn is Relation-like Function-like set
iMRn . (R + 1) is set
dom iMRn is set
iMRn . 0 is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
2 |^ n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(R) is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ R)) -' 1)
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
((R + 1)) is finite strict with_finite_clique# with_finite_stability# () () ((3 * (2 |^ (R + 1))) -' 1)
2 |^ (R + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ (R + 1)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (R + 1))) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
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
the carrier of ((R + 1)) is finite set
the InternalRel of ((R + 1)) is Relation-like the carrier of ((R + 1)) -defined the carrier of ((R + 1)) -valued finite Element of bool [: the carrier of ((R + 1)), the carrier of ((R + 1)):]
[: the carrier of ((R + 1)), the carrier of ((R + 1)):] is finite set
bool [: the carrier of ((R + 1)), the carrier of ((R + 1)):] is non empty finite V32() set
N is set
[N,N] is non empty set
{N,N} is non empty finite set
{N} is non empty trivial finite 1 -element set
{{N,N},{N}} is non empty finite V32() set
(((3 * (2 |^ R)) -' 1),(R)) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ R)) -' 1)) + 1)
2 * ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ R)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[y,y] is non empty set
{y,y} is non empty finite V32() set
{y} is non empty trivial finite V32() 1 -element set
{{y,y},{y}} is non empty finite V32() set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
2 |^ n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(R) is finite strict irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ R)) -' 1)
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
((R + 1)) is finite strict irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ (R + 1))) -' 1)
2 |^ (R + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ (R + 1)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (R + 1))) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
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
the carrier of ((R + 1)) is finite set
the InternalRel of ((R + 1)) is Relation-like the carrier of ((R + 1)) -defined the carrier of ((R + 1)) -valued finite Element of bool [: the carrier of ((R + 1)), the carrier of ((R + 1)):]
[: the carrier of ((R + 1)), the carrier of ((R + 1)):] is finite set
bool [: the carrier of ((R + 1)), the carrier of ((R + 1)):] is non empty finite V32() set
(((3 * (2 |^ R)) -' 1),(R)) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ R)) -' 1)) + 1)
2 * ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ R)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real 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
[y,x] is non empty set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V32() set
xp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
yp1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[xp1,yp1] is non empty set
{xp1,yp1} is non empty finite V32() set
{xp1} is non empty trivial finite V32() 1 -element set
{{xp1,yp1},{xp1}} is non empty finite V32() set
[yp1,xp1] is non empty set
{yp1,xp1} is non empty finite V32() set
{yp1} is non empty trivial finite V32() 1 -element set
{{yp1,xp1},{yp1}} is non empty finite V32() set
xx is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((3 * (2 |^ R)) -' 1) + xx is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((3 * (2 |^ R)) -' 1) + ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
xx + ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[x,xx] is non empty set
{x,xx} is non empty finite set
{{x,xx},{x}} is non empty finite V32() set
[xx,x] is non empty set
{xx,x} is non empty finite set
{xx} is non empty trivial finite V32() 1 -element set
{{xx,x},{xx}} is non empty finite V32() set
xx is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((3 * (2 |^ R)) -' 1) + xx is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((3 * (2 |^ R)) -' 1) + ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
xx + ((3 * (2 |^ R)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
[xx,y] is non empty set
{xx,y} is non empty finite set
{xx} is non empty trivial finite V32() 1 -element set
{{xx,y},{xx}} is non empty finite V32() set
[y,xx] is non empty set
{y,xx} is non empty finite set
{{y,xx},{y}} is non empty finite V32() set
clique# (0) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
clique# (2) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
((0)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((2)) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
2 |^ n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
clique# (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
((n + 1)) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ (n + 1))) -' 1)
2 |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ (n + 1)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ (n + 1))) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
clique# ((n + 1)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(((n + 1))) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(((3 * (2 |^ n)) -' 1),(n)) is non empty finite strict with_finite_clique# with_finite_stability# () () ((2 * ((3 * (2 |^ n)) -' 1)) + 1)
2 * ((3 * (2 |^ n)) -' 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(2 * ((3 * (2 |^ n)) -' 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
1 + ((n)) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
2 |^ n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
clique# (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(R) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ R)) -' 1)
2 |^ R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ R) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ R)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
((R)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
R + 2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
2 |^ n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
clique# (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () ((3 * (2 |^ n)) -' 1)
2 |^ n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of REAL
3 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(3 * (2 |^ n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real positive non negative real set
clique# (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
((n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
ComplRelStr (n) is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () RelStr
S is finite strict symmetric irreflexive with_finite_clique# with_finite_stability# () () RelStr
stability# S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set
(S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V63() ext-real non negative real set