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

bool S is non empty set

cMRn1 is set

iMRn1 is Element of R

iMRn1 /\ S is Element of bool n

union { (b

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

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

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

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

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

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

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

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

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

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

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

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

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

the InternalRel of R \/ { [b

{ [(b

( the InternalRel of R \/ { [b

{(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

[:((2 * n) \ n),{(2 * n)}:] is finite set

((( the InternalRel of R \/ { [b

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

the InternalRel of R \/ { [b

{ [(b

( the InternalRel of R \/ { [b

{(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

[:((2 * n) \ n),{(2 * n)}:] is finite set

((( the InternalRel of R \/ { [b

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