ROUGHS_1

:: ROUGHS_1 semantic presentation

REAL is non empty non trivial non finite V79() V80() V81() V85() set
NAT is non trivial V38() non finite cardinal limit_cardinal V79() V80() V81() V82() V83() V84() V85() Element of bool REAL
bool REAL is non empty non trivial non finite set
NAT is non trivial V38() non finite cardinal limit_cardinal V79() V80() V81() V82() V83() V84() V85() set
bool NAT is non empty non trivial non finite set
[:NAT,REAL:] is non trivial Relation-like non finite V69() V70() V71() set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V79() V85() set
RAT is non empty non trivial non finite V79() V80() V81() V82() V85() set
INT is non empty non trivial non finite V79() V80() V81() V82() V83() V85() set
bool NAT is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [:REAL,REAL:] is non empty non trivial non finite set
2 is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
[:2,2:] is non empty Relation-like RAT -valued INT -valued finite V69() V70() V71() V72() set
[:[:2,2:],2:] is non empty Relation-like RAT -valued INT -valued finite V69() V70() V71() V72() set
bool [:[:2,2:],2:] is non empty finite V47() set
{} is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set
the empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set
1 is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
{{},1} is non empty finite V47() V79() V80() V81() V82() V83() V84() set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite V69() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite V69() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued non finite V69() V70() V71() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued non finite V69() V70() V71() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V69() V70() V71() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V69() V70() V71() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V69() V70() V71() V72() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V69() V70() V71() V72() set
bool [:[:NAT,NAT:],NAT:] is non empty set
3 is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
0 is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered Element of NAT
card {} is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set
union {} is finite set
dom {} is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set
rng {} is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set
id {} is empty Relation-like non-empty empty-yielding {} -defined {} -valued RAT -valued INT -valued reflexive symmetric antisymmetric transitive functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set
<*> REAL is empty Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of REAL
Sum (<*> REAL) is ext-real V62() V66() Element of REAL
Seg 1 is non empty trivial finite 1 -element V79() V80() V81() V82() V83() V84() Element of bool NAT
{1} is non empty trivial finite V47() 1 -element V79() V80() V81() V82() V83() V84() set
Seg 2 is non empty finite 2 -element V79() V80() V81() V82() V83() V84() Element of bool NAT
{1,2} is non empty finite V47() V79() V80() V81() V82() V83() V84() set
A is set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive total Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
RelStr(# A,(id A) #) is strict total reflexive transitive antisymmetric RelStr
A is set
nabla A is Relation-like A -defined A -valued reflexive symmetric transitive total Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive total Element of bool [:A,A:]
X is set
Y is set
[X,Y] is set
{X,Y} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,Y},{X}} is non empty finite V47() set
A is non trivial set
nabla A is Relation-like A -defined A -valued reflexive symmetric transitive total Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
RelStr(# A,(nabla A) #) is strict total reflexive transitive RelStr
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive total Element of bool [:A,A:]
A is total reflexive RelStr
the carrier of A is set
id the carrier of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric antisymmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive total Element of bool [: the carrier of A, the carrier of A:]
X is set
Y is set
[X,Y] is set
{X,Y} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,Y},{X}} is non empty finite V47() set
A is RelStr
the carrier of A is set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
the carrier of A is set
X is set
{X} is non empty trivial finite 1 -element set
X is set
{X} is non empty trivial finite 1 -element set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
[:{X},{X}:] is non empty Relation-like finite set
[X,X] is set
{X,X} is non empty finite set
{{X,X},{X}} is non empty finite V47() set
{[X,X]} is non empty trivial Relation-like finite 1 -element set
id {X} is non empty Relation-like {X} -defined {X} -valued reflexive symmetric antisymmetric transitive total finite Element of bool [:{X},{X}:]
bool [:{X},{X}:] is non empty finite V47() set
the carrier of A is set
A is total reflexive RelStr
A is RelStr
A is set
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive total Element of bool [:A,A:]
X is Relation-like A -defined A -valued reflexive total Element of bool [:A,A:]
field X is set
A is RelStr
the carrier of A is set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
id the carrier of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric antisymmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
A is RelStr
A is RelStr
the non trivial set is non trivial set
nabla the non trivial set is Relation-like the non trivial set -defined the non trivial set -valued reflexive symmetric transitive total Element of bool [: the non trivial set , the non trivial set :]
[: the non trivial set , the non trivial set :] is Relation-like set
bool [: the non trivial set , the non trivial set :] is non empty set
RelStr(# the non trivial set ,(nabla the non trivial set ) #) is non empty non trivial strict total reflexive transitive non discrete () RelStr
A is non empty non discrete () RelStr
the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
id the carrier of A is non empty Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric antisymmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
X is set
Y is set
[X,Y] is set
{X,Y} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,Y},{X}} is non empty finite V47() set
X is Element of the carrier of A
Y is Element of the carrier of A
[X,Y] is Element of [: the carrier of A, the carrier of A:]
{X,Y} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,Y},{X}} is non empty finite V47() set
Z is Element of the carrier of A
y is Element of the carrier of A
[Z,y] is Element of [: the carrier of A, the carrier of A:]
{Z,y} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,y},{Z}} is non empty finite V47() set
A is set
X is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of A
Y is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of A
X ^ Y is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of A
Union (X ^ Y) is set
rng (X ^ Y) is finite set
union (rng (X ^ Y)) is set
Union X is set
rng X is finite set
union (rng X) is set
Union Y is set
rng Y is finite set
union (rng Y) is set
(Union X) \/ (Union Y) is set
rng (X ^ Y) is finite Element of bool A
bool A is non empty set
union (rng (X ^ Y)) is set
rng X is finite Element of bool A
rng Y is finite Element of bool A
(rng X) \/ (rng Y) is finite Element of bool A
union ((rng X) \/ (rng Y)) is set
X is Relation-like Function-like set
A is Relation-like Function-like set
Y is set
Z is set
A . Y is set
A . Z is set
dom A is set
X . Y is set
X . Z is set
A is Relation-like Function-like set
X is set
Y is set
A . X is set
A . Y is set
A is set
<*> A is empty Relation-like non-empty empty-yielding NAT -defined A -valued Function-like functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element disjoint_valued V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of A
A is non empty set
the Element of A is Element of A
1 |-> the Element of A is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like Element of 1 -tuples_on A
1 -tuples_on A is FinSequenceSet of A
A * is non empty functional FinSequence-membered FinSequenceSet of A
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like Element of A * : len b₁ = 1 } is set
K312((Seg 1), the Element of A) is Relation-like Seg 1 -defined { the Element of A} -valued Function-like V29( Seg 1,{ the Element of A}) finite Element of bool [:(Seg 1),{ the Element of A}:]
{ the Element of A} is non empty trivial finite 1 -element set
[:(Seg 1),{ the Element of A}:] is non empty Relation-like finite set
bool [:(Seg 1),{ the Element of A}:] is non empty finite V47() set
Y is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of A
Z is set
y is set
Y . Z is set
Y . y is set
dom Y is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom Y is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom Y is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
A is set
bool A is non empty set
X is Relation-like NAT -defined bool A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool A
Y is ext-real non negative V38() V42() finite cardinal V62() V66() set
X . Y is set
dom X is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom X is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom X is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
A is set
bool A is non empty set
X is Relation-like NAT -defined bool A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool A
Union X is set
rng X is finite set
union (rng X) is set
rng X is finite Element of bool (bool A)
bool (bool A) is non empty set
union (rng X) is set
Y is set
Z is set
A is finite set
[:A,A:] is Relation-like finite set
bool [:A,A:] is non empty finite V47() set
X is Relation-like A -defined A -valued finite Element of bool [:A,A:]
RelStr(# A,X #) is strict RelStr
A is set
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
X is set
Y is set
Z is Relation-like A -defined A -valued reflexive symmetric total Element of bool [:A,A:]
Class (Z,Y) is Element of bool A
bool A is non empty set
Class (Z,X) is Element of bool A
[X,Y] is set
{X,Y} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,Y},{X}} is non empty finite V47() set
[Y,X] is set
{Y,X} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,X},{Y}} is non empty finite V47() set
A is RelStr
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
the carrier of A is set
[: the carrier of A, the carrier of A:] is Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
A is set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive total Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
RelStr(# A,(id A) #) is strict total reflexive transitive antisymmetric discrete () RelStr
{{}} is non empty trivial finite V47() 1 -element V79() V80() V81() V82() V83() V84() set
id {{}} is non empty Relation-like {{}} -defined {{}} -valued RAT -valued INT -valued reflexive symmetric antisymmetric transitive total finite V69() V70() V71() V72() Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is non empty Relation-like RAT -valued INT -valued finite V69() V70() V71() V72() set
bool [:{{}},{{}}:] is non empty finite V47() set
RelStr(# {{}},(id {{}}) #) is non empty finite strict total reflexive transitive antisymmetric discrete () () () RelStr
{0,1} is non empty finite V47() V79() V80() V81() V82() V83() V84() Element of bool REAL
nabla {0,1} is Relation-like {0,1} -defined {0,1} -valued reflexive symmetric transitive total finite V69() V70() V71() V72() Element of bool [:{0,1},{0,1}:]
[:{0,1},{0,1}:] is non empty Relation-like RAT -valued INT -valued finite V69() V70() V71() V72() set
bool [:{0,1},{0,1}:] is non empty finite V47() set
RelStr(# {0,1},(nabla {0,1}) #) is non empty finite strict total reflexive transitive RelStr
Z is non empty RelStr
A is non empty () RelStr
the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
A is non empty () () RelStr
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
the carrier of A is non empty set
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
A is non empty RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
X is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
Y is set
Z is Element of the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is set
Z is Element of the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) \ (A,X) is Element of bool the carrier of A
A is non empty RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
A is non empty RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is Element of the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Y is Element of the carrier of A
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is Element of the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
Y is Element of the carrier of A
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
Y is set
Z is Element of the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is set
Z is Element of the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) is Element of bool the carrier of A
(A,X) \ (A,X) is Element of bool the carrier of A
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) \ (A,X) is Element of bool the carrier of A
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
[Z,Y] is set
{Z,Y} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,Y},{Z}} is non empty finite V47() set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Z},{Y}} is non empty finite V47() set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
A is non empty () RelStr
{} A is empty proper Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered strongly_connected Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is non empty set
(A,({} A)) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= {} A } is set
X is set
Y is Element of the carrier of A
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
A is non empty () RelStr
{} A is empty proper Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered strongly_connected Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is non empty set
(A,({} A)) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses {} A } is set
X is set
Y is Element of the carrier of A
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
A is non empty () RelStr
[#] A is non empty non proper Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is non empty set
(A,([#] A)) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= [#] A } is set
X is set
Class ( the InternalRel of A,X) is Element of bool the carrier of A
A is non empty () RelStr
[#] A is non empty non proper Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is non empty set
(A,([#] A)) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses [#] A } is set
(A,([#] A)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= [#] A } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
Y is Element of bool the carrier of A
X /\ Y is Element of bool the carrier of A
(A,(X /\ Y)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X /\ Y } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Y } is set
(A,X) /\ (A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is Element of bool the carrier of A
X \/ Y is Element of bool the carrier of A
(A,(X \/ Y)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X \/ Y } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Y } is set
(A,X) \/ (A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
Y is Element of bool the carrier of A
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Y } is set
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is Element of bool the carrier of A
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Y } is set
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
Y is Element of bool the carrier of A
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Y } is set
(A,X) \/ (A,Y) is Element of bool the carrier of A
X \/ Y is Element of bool the carrier of A
(A,(X \/ Y)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X \/ Y } is set
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is Element of bool the carrier of A
X /\ Y is Element of bool the carrier of A
(A,(X /\ Y)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X /\ Y } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Y } is set
(A,X) /\ (A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
X ` is Element of bool the carrier of A
the carrier of A \ X is set
(A,(X `)) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X ` } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) ` is Element of bool the carrier of A
the carrier of A \ (A,X) is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
X ` is Element of bool the carrier of A
the carrier of A \ X is set
(A,(X `)) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X ` } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) ` is Element of bool the carrier of A
the carrier of A \ (A,X) is set
(A,(X `)) ` is Element of bool the carrier of A
the carrier of A \ (A,(X `)) is set
((A,(X `)) `) ` is Element of bool the carrier of A
the carrier of A \ ((A,(X `)) `) is set
(X `) ` is Element of bool the carrier of A
the carrier of A \ (X `) is set
(A,((X `) `)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (X `) ` } is set
(A,((X `) `)) ` is Element of bool the carrier of A
the carrier of A \ (A,((X `) `)) is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (A,X) } is set
(A,(A,(A,X))) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses (A,(A,X)) } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
[Z,Y] is set
{Z,Y} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,Y},{Z}} is non empty finite V47() set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Z},{Y}} is non empty finite V47() set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
[Z,Y] is set
{Z,Y} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,Y},{Z}} is non empty finite V47() set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Z},{Y}} is non empty finite V47() set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses (A,X) } is set
(A,(A,(A,X))) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (A,(A,X)) } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
[Z,Y] is set
{Z,Y} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,Y},{Z}} is non empty finite V47() set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Z},{Y}} is non empty finite V47() set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
[Z,Y] is set
{Z,Y} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,Y},{Z}} is non empty finite V47() set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Z},{Y}} is non empty finite V47() set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) \ (A,X) is Element of bool the carrier of A
X ` is Element of bool the carrier of A
the carrier of A \ X is set
(A,(X `)) is Element of bool the carrier of A
(A,(X `)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X ` } is set
(A,(X `)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X ` } is set
(A,(X `)) \ (A,(X `)) is Element of bool the carrier of A
Y is set
(A,X) ` is Element of bool the carrier of A
the carrier of A \ (A,X) is set
(A,X) ` is Element of bool the carrier of A
the carrier of A \ (A,X) is set
Y is set
(A,X) ` is Element of bool the carrier of A
the carrier of A \ (A,X) is set
(A,X) ` is Element of bool the carrier of A
the carrier of A \ (A,X) is set
((A,X) `) ` is Element of bool the carrier of A
the carrier of A \ ((A,X) `) is set
A is non empty () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (A,X) } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses (A,X) } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
y is set
Class ( the InternalRel of A,y) is Element of bool the carrier of A
A is non empty () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses (A,X) } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (A,X) } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Z is set
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
y is set
Class ( the InternalRel of A,y) is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
{} A is empty proper Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered strongly_connected Element of bool the carrier of A
(A,({} A)) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= {} A } is set
A is non empty () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
(A,(A,X)) \ (A,(A,X)) is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses (A,X) } is set
(A,(A,X)) is (A) Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
(A,(A,X)) \ (A,(A,X)) is Element of bool the carrier of A
A is non empty () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
X is Element of bool the carrier of A
(A,X) is (A) Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is set
Z is set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Z},{Y}} is non empty finite V47() set
[Z,Y] is set
{Z,Y} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,Y},{Z}} is non empty finite V47() set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
Class ( the InternalRel of A,Z) is Element of bool the carrier of A
A is non empty non discrete () () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
X is Element of the carrier of A
Y is Element of the carrier of A
[X,Y] is Element of [: the carrier of A, the carrier of A:]
{X,Y} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,Y},{X}} is non empty finite V47() set
{X} is non empty trivial finite 1 -element Element of bool the carrier of A
(A,{X}) is (A) Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses {X} } is set
A is non empty () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
(A,X) is (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) is (A) Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
[(A,X),(A,X)] is Element of [:(bool the carrier of A),(bool the carrier of A):]
[:(bool the carrier of A),(bool the carrier of A):] is non empty Relation-like set
{(A,X),(A,X)} is non empty finite set
{(A,X)} is non empty trivial finite 1 -element set
{{(A,X),(A,X)},{(A,X)}} is non empty finite V47() set
A is non empty finite () RelStr
the carrier of A is non empty finite set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
X is Element of the carrier of A
Class ( the InternalRel of A,X) is finite Element of bool the carrier of A
bool the carrier of A is non empty finite V47() set
card (Class ( the InternalRel of A,X)) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
A is non empty finite () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
X is finite Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
Y is set
Class ( the InternalRel of A,Y) is finite Element of bool the carrier of A
X /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
card (X /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Y)) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
Y is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Y is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Z is Element of the carrier of A
Y . Z is ext-real V62() V66() Element of REAL
Class ( the InternalRel of A,Z) is finite Element of bool the carrier of A
X /\ (Class ( the InternalRel of A,Z)) is finite Element of bool the carrier of A
card (X /\ (Class ( the InternalRel of A,Z))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Z)) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z))) is ext-real non negative V62() V66() set
Y is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Z is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
A is non empty finite () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Y is Element of the carrier of A
(A,X) . Y is ext-real V62() V66() Element of REAL
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
Class ( the InternalRel of A,Y) is finite Element of bool the carrier of A
X /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
card (X /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Y)) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
[.0,1.] is V79() V80() V81() Element of bool REAL
A is non empty finite () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Y is Element of the carrier of A
(A,X) . Y is ext-real V62() V66() Element of REAL
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
Y is Element of the carrier of A
(A,X) . Y is ext-real V62() V66() Element of REAL
Class ( the InternalRel of A,Y) is finite Element of bool the carrier of A
X /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
card (X /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Y)) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) ` is finite Element of bool the carrier of A
the carrier of A \ (A,X) is finite set
Y is Element of the carrier of A
(A,X) . Y is ext-real V62() V66() Element of REAL
Class ( the InternalRel of A,Y) is finite Element of bool the carrier of A
X /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
card (X /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Y)) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,X) is finite Element of bool the carrier of A
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) is finite (A) Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) \ (A,X) is finite Element of bool the carrier of A
Y is Element of the carrier of A
(A,X) . Y is ext-real V62() V66() Element of REAL
(A,X) ` is finite Element of bool the carrier of A
the carrier of A \ (A,X) is finite set
A is non empty discrete () () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
id the carrier of A is non empty Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric antisymmetric transitive total Element of bool [: the carrier of A, the carrier of A:]
(A,X) is (A) Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
Y is set
Class ( the InternalRel of A,Y) is Element of bool the carrier of A
{Y} is non empty trivial finite 1 -element set
Z is set
A is non empty discrete () () () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
A is non empty finite discrete () () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite (A) Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
chi (X, the carrier of A) is Relation-like the carrier of A -defined {{},1} -valued Function-like V29( the carrier of A,{{},1}) finite V69() V70() V71() V72() Element of bool [: the carrier of A,{{},1}:]
[: the carrier of A,{{},1}:] is non empty Relation-like RAT -valued INT -valued finite V69() V70() V71() V72() set
bool [: the carrier of A,{{},1}:] is non empty finite V47() set
{0,1} is non empty finite V47() V79() V80() V81() V82() V83() V84() Element of bool REAL
Y is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
y is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
x is set
Y . x is ext-real V62() V66() set
y . x is ext-real V62() V66() set
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) ` is finite (A) Element of bool the carrier of A
the carrier of A \ (A,X) is finite set
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Y is set
Z is set
[Y,Z] is set
{Y,Z} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Z},{Y}} is non empty finite V47() set
(A,X) . Y is ext-real V62() V66() set
(A,X) . Z is ext-real V62() V66() set
Class ( the InternalRel of A,Y) is finite Element of bool the carrier of A
X /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
card (X /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Y)) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
Class ( the InternalRel of A,Z) is finite Element of bool the carrier of A
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
X ` is finite Element of bool the carrier of A
the carrier of A \ X is finite set
(A,(X `)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Y is Element of the carrier of A
(A,(X `)) . Y is ext-real V62() V66() Element of REAL
(A,X) . Y is ext-real V62() V66() Element of REAL
1 - ((A,X) . Y) is ext-real V62() V66() set
[#] A is non empty non proper finite Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
Class ( the InternalRel of A,Y) is finite Element of bool the carrier of A
([#] A) /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
([#] A) \ X is finite Element of bool the carrier of A
(([#] A) \ X) /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
card ((([#] A) \ X) /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Y)) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card ((([#] A) \ X) /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
X /\ (Class ( the InternalRel of A,Y)) is finite Element of bool the carrier of A
(([#] A) /\ (Class ( the InternalRel of A,Y))) \ (X /\ (Class ( the InternalRel of A,Y))) is finite Element of bool the carrier of A
card ((([#] A) /\ (Class ( the InternalRel of A,Y))) \ (X /\ (Class ( the InternalRel of A,Y)))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card ((([#] A) /\ (Class ( the InternalRel of A,Y))) \ (X /\ (Class ( the InternalRel of A,Y))))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
card (([#] A) /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (X /\ (Class ( the InternalRel of A,Y))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (([#] A) /\ (Class ( the InternalRel of A,Y)))) - (card (X /\ (Class ( the InternalRel of A,Y)))) is ext-real V62() V66() set
((card (([#] A) /\ (Class ( the InternalRel of A,Y)))) - (card (X /\ (Class ( the InternalRel of A,Y))))) / (card (Class ( the InternalRel of A,Y))) is ext-real V62() V66() set
(card (([#] A) /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
(card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
((card (([#] A) /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y)))) - ((card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y)))) is ext-real V62() V66() set
(card (Class ( the InternalRel of A,Y))) / (card (Class ( the InternalRel of A,Y))) is ext-real non negative V62() V66() set
((card (Class ( the InternalRel of A,Y))) / (card (Class ( the InternalRel of A,Y)))) - ((card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y)))) is ext-real V62() V66() set
1 - ((card (X /\ (Class ( the InternalRel of A,Y)))) / (card (Class ( the InternalRel of A,Y)))) is ext-real V62() V66() set
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Y is finite Element of bool the carrier of A
(A,Y) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
(A,Y) . Z is ext-real V62() V66() Element of REAL
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
Class ( the InternalRel of A,Z) is finite Element of bool the carrier of A
X /\ (Class ( the InternalRel of A,Z)) is finite Element of bool the carrier of A
card (X /\ (Class ( the InternalRel of A,Z))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
Y /\ (Class ( the InternalRel of A,Z)) is finite Element of bool the carrier of A
card (Y /\ (Class ( the InternalRel of A,Z))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Class ( the InternalRel of A,Z)) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z))) is ext-real non negative V62() V66() set
(card (Y /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z))) is ext-real non negative V62() V66() set
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
Y is finite Element of bool the carrier of A
X \/ Y is finite Element of bool the carrier of A
(A,(X \/ Y)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,(X \/ Y)) . Z is ext-real V62() V66() Element of REAL
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
Y is finite Element of bool the carrier of A
X /\ Y is finite Element of bool the carrier of A
(A,(X /\ Y)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Z is Element of the carrier of A
(A,(X /\ Y)) . Z is ext-real V62() V66() Element of REAL
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,X) . Z is ext-real V62() V66() Element of REAL
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Y is finite Element of bool the carrier of A
(A,Y) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
X \/ Y is finite Element of bool the carrier of A
(A,(X \/ Y)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
(A,Y) . Z is ext-real V62() V66() Element of REAL
max (((A,X) . Z),((A,Y) . Z)) is ext-real V62() V66() set
(A,(X \/ Y)) . Z is ext-real V62() V66() Element of REAL
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Y is finite Element of bool the carrier of A
X \/ Y is finite Element of bool the carrier of A
(A,(X \/ Y)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,Y) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Z is Element of the carrier of A
(A,(X \/ Y)) . Z is ext-real V62() V66() Element of REAL
(A,X) . Z is ext-real V62() V66() Element of REAL
(A,Y) . Z is ext-real V62() V66() Element of REAL
((A,X) . Z) + ((A,Y) . Z) is ext-real V62() V66() set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
Class ( the InternalRel of A,Z) is finite Element of bool the carrier of A
(X \/ Y) /\ (Class ( the InternalRel of A,Z)) is finite Element of bool the carrier of A
card ((X \/ Y) /\ (Class ( the InternalRel of A,Z))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
X /\ (Class ( the InternalRel of A,Z)) is finite Element of bool the carrier of A
Y /\ (Class ( the InternalRel of A,Z)) is finite Element of bool the carrier of A
(X /\ (Class ( the InternalRel of A,Z))) \/ (Y /\ (Class ( the InternalRel of A,Z))) is finite Element of bool the carrier of A
card ((X /\ (Class ( the InternalRel of A,Z))) \/ (Y /\ (Class ( the InternalRel of A,Z)))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (X /\ (Class ( the InternalRel of A,Z))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
card (Y /\ (Class ( the InternalRel of A,Z))) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(card (X /\ (Class ( the InternalRel of A,Z)))) + (card (Y /\ (Class ( the InternalRel of A,Z)))) is ext-real non negative V38() V42() finite cardinal V62() V66() set
card (Class ( the InternalRel of A,Z)) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
((card (X /\ (Class ( the InternalRel of A,Z)))) + (card (Y /\ (Class ( the InternalRel of A,Z))))) / (card (Class ( the InternalRel of A,Z))) is ext-real non negative V62() V66() set
(card (X /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z))) is ext-real non negative V62() V66() set
(card (Y /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z))) is ext-real non negative V62() V66() set
((card (X /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z)))) + ((card (Y /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z)))) is ext-real non negative V62() V66() set
((A,X) . Z) + ((card (Y /\ (Class ( the InternalRel of A,Z)))) / (card (Class ( the InternalRel of A,Z)))) is ext-real V62() V66() set
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
Y is finite Element of bool the carrier of A
X /\ Y is finite Element of bool the carrier of A
(A,(X /\ Y)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,Y) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
Z is Element of the carrier of A
(A,(X /\ Y)) . Z is ext-real V62() V66() Element of REAL
(A,X) . Z is ext-real V62() V66() Element of REAL
(A,Y) . Z is ext-real V62() V66() Element of REAL
min (((A,X) . Z),((A,Y) . Z)) is ext-real V62() V66() set
A is non empty finite () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is Relation-like NAT -defined bool the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
dom X is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
Y is Element of the carrier of A
len X is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
Z is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
len Z is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
dom Z is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
Z is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
len Z is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
dom Z is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
Seg (len Z) is finite len Z -element V79() V80() V81() V82() V83() V84() Element of bool NAT
y is ext-real non negative V38() V42() finite cardinal V62() V66() set
Z . y is ext-real V62() V66() set
( the carrier of A,X,y) is finite Element of bool the carrier of A
(A,( the carrier of A,X,y)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,( the carrier of A,X,y)) . Y is ext-real V62() V66() Element of REAL
Seg (len X) is finite len X -element V79() V80() V81() V82() V83() V84() Element of bool NAT
Z is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
dom Z is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
y is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
dom y is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
x is ext-real non negative V38() V42() finite cardinal V62() V66() set
Z . x is ext-real V62() V66() set
y . x is ext-real V62() V66() set
X is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
Z . X is ext-real V62() V66() set
( the carrier of A,X,X) is finite Element of bool the carrier of A
(A,( the carrier of A,X,X)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,( the carrier of A,X,X)) . Y is ext-real V62() V66() Element of REAL
y . X is ext-real V62() V66() set
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is Relation-like NAT -defined bool the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
Y is Element of the carrier of A
(A,X,Y) is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
Z is finite Element of bool the carrier of A
<*Z*> is non empty trivial Relation-like NAT -defined bool the carrier of A -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
X ^ <*Z*> is non empty Relation-like NAT -defined bool the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
(A,(X ^ <*Z*>),Y) is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
(A,Z) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,Z) . Y is ext-real V62() V66() Element of REAL
<*((A,Z) . Y)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one finite 1 -element V69() V70() V71() V73() V74() V75() V76() FinSequence-like FinSubsequence-like FinSequence of REAL
(A,X,Y) ^ <*((A,Z) . Y)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
dom X is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom (A,X,Y) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
len X is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
Seg (len X) is finite len X -element V79() V80() V81() V82() V83() V84() Element of bool NAT
len (A,X,Y) is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
Seg (len (A,X,Y)) is finite len (A,X,Y) -element V79() V80() V81() V82() V83() V84() Element of bool NAT
dom (A,(X ^ <*Z*>),Y) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom (X ^ <*Z*>) is non empty finite V79() V80() V81() V82() V83() V84() Element of bool NAT
len <*Z*> is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(len X) + (len <*Z*>) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() set
Seg ((len X) + (len <*Z*>)) is non empty finite (len X) + (len <*Z*>) -element V79() V80() V81() V82() V83() V84() Element of bool NAT
(len X) + 1 is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() set
Seg ((len X) + 1) is non empty finite (len X) + 1 -element V79() V80() V81() V82() V83() V84() Element of bool NAT
X is ext-real non negative V38() V42() finite cardinal V62() V66() set
(A,(X ^ <*Z*>),Y) . X is ext-real V62() V66() set
((A,X,Y) ^ <*((A,Z) . Y)*>) . X is ext-real V62() V66() set
m is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(A,(X ^ <*Z*>),Y) . m is ext-real V62() V66() set
( the carrier of A,(X ^ <*Z*>),m) is finite Element of bool the carrier of A
(A,( the carrier of A,(X ^ <*Z*>),m)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,( the carrier of A,(X ^ <*Z*>),m)) . Y is ext-real V62() V66() Element of REAL
((A,X,Y) ^ <*((A,Z) . Y)*>) . m is ext-real V62() V66() set
(A,X,Y) . m is ext-real V62() V66() set
( the carrier of A,X,m) is finite Element of bool the carrier of A
(A,( the carrier of A,X,m)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,( the carrier of A,X,m)) . Y is ext-real V62() V66() Element of REAL
((A,X,Y) ^ <*((A,Z) . Y)*>) . m is ext-real V62() V66() set
dom ((A,X,Y) ^ <*((A,Z) . Y)*>) is non empty finite V79() V80() V81() V82() V83() V84() Element of bool NAT
len <*((A,Z) . Y)*> is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(len (A,X,Y)) + (len <*((A,Z) . Y)*>) is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() set
Seg ((len (A,X,Y)) + (len <*((A,Z) . Y)*>)) is non empty finite (len (A,X,Y)) + (len <*((A,Z) . Y)*>) -element V79() V80() V81() V82() V83() V84() Element of bool NAT
A is non empty finite () () RelStr
the carrier of A is non empty finite set
{} A is empty proper Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered strongly_connected Element of bool the carrier of A
bool the carrier of A is non empty finite V47() set
(A,({} A)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
X is Element of the carrier of A
(A,({} A)) . X is ext-real V62() V66() Element of REAL
(A,({} A)) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses {} A } is set
(A,({} A)) ` is finite Element of bool the carrier of A
the carrier of A \ (A,({} A)) is finite set
[#] A is non empty non proper finite Element of bool the carrier of A
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is Element of the carrier of A
Y is Relation-like NAT -defined bool the carrier of A -valued Function-like finite disjoint_valued FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
( the carrier of A,Y) is finite Element of bool the carrier of A
rng Y is finite set
union (rng Y) is set
(A,( the carrier of A,Y)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
(A,( the carrier of A,Y)) . X is ext-real V62() V66() Element of REAL
(A,Y,X) is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (A,Y,X) is ext-real V62() V66() Element of REAL
Z is Relation-like NAT -defined bool the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
( the carrier of A,Z) is finite Element of bool the carrier of A
rng Z is finite set
union (rng Z) is set
(A,( the carrier of A,Z)) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,( the carrier of A,Z)) . X is ext-real V62() V66() Element of REAL
(A,Z,X) is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (A,Z,X) is ext-real V62() V66() Element of REAL
y is finite Element of bool the carrier of A
<*y*> is non empty trivial Relation-like NAT -defined bool the carrier of A -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
Z ^ <*y*> is non empty Relation-like NAT -defined bool the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of A
( the carrier of A,(Z ^ <*y*>)) is finite Element of bool the carrier of A
rng (Z ^ <*y*>) is non empty finite set
union (rng (Z ^ <*y*>)) is set
(A,( the carrier of A,(Z ^ <*y*>))) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,( the carrier of A,(Z ^ <*y*>))) . X is ext-real V62() V66() Element of REAL
(A,(Z ^ <*y*>),X) is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (A,(Z ^ <*y*>),X) is ext-real V62() V66() Element of REAL
x is set
rng Z is finite V47() Element of bool (bool the carrier of A)
bool (bool the carrier of A) is non empty finite V47() set
X is set
dom Z is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
m is set
Z . m is set
m is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
( the carrier of A,(Z ^ <*y*>),m) is finite Element of bool the carrier of A
( the carrier of A,Z,m) is finite Element of bool the carrier of A
len Z is ext-real non negative V38() V42() finite cardinal V62() V66() V67() V68() V79() V80() V81() V82() V83() V84() Element of NAT
(len Z) + 1 is non empty ext-real positive non negative V38() V42() finite cardinal V62() V66() set
( the carrier of A,(Z ^ <*y*>),((len Z) + 1)) is finite Element of bool the carrier of A
( the carrier of A,<*y*>) is finite Element of bool the carrier of A
rng <*y*> is non empty trivial finite 1 -element set
union (rng <*y*>) is set
( the carrier of A,Z) \/ ( the carrier of A,<*y*>) is finite Element of bool the carrier of A
( the carrier of A,Z) \/ y is finite Element of bool the carrier of A
(A,y) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,y) . X is ext-real V62() V66() Element of REAL
((A,( the carrier of A,Z)) . X) + ((A,y) . X) is ext-real V62() V66() set
<*((A,y) . X)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one finite 1 -element V69() V70() V71() V73() V74() V75() V76() FinSequence-like FinSubsequence-like FinSequence of REAL
(A,Z,X) ^ <*((A,y) . X)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum ((A,Z,X) ^ <*((A,y) . X)*>) is ext-real V62() V66() Element of REAL
<*> (bool the carrier of A) is empty Relation-like non-empty empty-yielding NAT -defined bool the carrier of A -valued Function-like functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element disjoint_valued V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of bool the carrier of A
( the carrier of A,(<*> (bool the carrier of A))) is finite Element of bool the carrier of A
rng (<*> (bool the carrier of A)) is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered set
union (rng (<*> (bool the carrier of A))) is finite set
(A,( the carrier of A,(<*> (bool the carrier of A)))) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
(A,( the carrier of A,(<*> (bool the carrier of A)))) . X is ext-real V62() V66() Element of REAL
(A,(<*> (bool the carrier of A)),X) is Relation-like NAT -defined REAL -valued Function-like finite V69() V70() V71() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (A,(<*> (bool the carrier of A)),X) is ext-real V62() V66() Element of REAL
dom (A,(<*> (bool the carrier of A)),X) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom (<*> (bool the carrier of A)) is empty Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered Element of bool NAT
{} A is empty proper Relation-like non-empty empty-yielding RAT -valued functional ext-real non positive non negative V38() V42() finite finite-yielding V47() cardinal {} -element V62() V66() V69() V70() V71() V72() V79() V80() V81() V82() V83() V84() V85() FinSequence-like FinSequence-membered strongly_connected Element of bool the carrier of A
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
{ b₁ where b₁ is Element of the carrier of A : (A,X) . b₁ = 1 } is set
Y is set
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
Y is set
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
{ b₁ where b₁ is Element of the carrier of A : not (A,X) . b₁ <= 0 } is set
Y is set
(A,X) ` is finite Element of bool the carrier of A
the carrier of A \ (A,X) is finite set
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
Y is set
(A,X) ` is finite Element of bool the carrier of A
the carrier of A \ (A,X) is finite set
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
A is non empty finite () () RelStr
the carrier of A is non empty finite set
bool the carrier of A is non empty finite V47() set
X is finite Element of bool the carrier of A
(A,X) is finite Element of bool the carrier of A
(A,X) is finite (A) Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric transitive total finite Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like finite set
bool [: the carrier of A, the carrier of A:] is non empty finite V47() set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,X) is finite (A) Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,X) \ (A,X) is finite Element of bool the carrier of A
(A,X) is Relation-like the carrier of A -defined REAL -valued Function-like V29( the carrier of A, REAL ) finite V69() V70() V71() Element of bool [: the carrier of A,REAL:]
[: the carrier of A,REAL:] is non empty non trivial Relation-like non finite V69() V70() V71() set
bool [: the carrier of A,REAL:] is non empty non trivial non finite set
{ b₁ where b₁ is Element of the carrier of A : ( not (A,X) . b₁ <= 0 & not 1 <= (A,X) . b₁ ) } is set
Y is set
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
Y is set
Z is Element of the carrier of A
(A,X) . Z is ext-real V62() V66() Element of REAL
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Z } is set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Z } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
Z is Element of bool the carrier of A
y is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
Y is Element of bool the carrier of A
Z is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Y } is set
(A,Z) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Z } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
Y is Element of bool the carrier of A
Z is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Y } is set
(A,Z) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Z } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
Y is Element of bool the carrier of A
Z is Element of bool the carrier of A
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Z } is set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Z } is set
y is Element of bool the carrier of A
(A,y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= y } is set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Z } is set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Z } is set
y is Element of bool the carrier of A
(A,y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses y } is set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Z } is set
y is Element of bool the carrier of A
(A,y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses y } is set
Z is Element of bool the carrier of A
(A,Z) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Z } is set
y is Element of bool the carrier of A
(A,y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= y } is set
(A,Z) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Z } is set
(A,y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses y } is set
A is non empty () RelStr
the carrier of A is non empty set
bool the carrier of A is non empty set
X is Element of bool the carrier of A
Y is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Y } is set
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Y } is set
(A,X) is Element of bool the carrier of A
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued reflexive symmetric total Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty Relation-like set
bool [: the carrier of A, the carrier of A:] is non empty set
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= X } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : Class ( the InternalRel of A,b₁) c= Y } is set
(A,X) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses X } is set
(A,Y) is Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not Class ( the InternalRel of A,b₁) misses Y } is set