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

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

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

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

(A,X) is Element of bool the carrier of A

{ b

(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

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

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

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

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

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

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

(A,X) is Element of bool the carrier of A

{ b

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

(A,X) is Element of bool the carrier of A

{ b

(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

(A,X) is Element of bool the carrier of A

(A,X) is Element of bool the carrier of A

{ b

(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

(A,X) is Element of bool the carrier of A

{ b

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

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

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

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

(A,([#] A)) is Element of bool the carrier of A

{ b

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

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

(A,Y) is Element of bool the carrier of A

{ b

(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

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

(A,Y) is Element of bool the carrier of A

{ b

(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

Y is Element of bool the carrier of A

(A,Y) is Element of bool the carrier of A

{ b

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

Y is Element of bool the carrier of A

(A,Y) is Element of bool the carrier of A

{ b

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

Y is Element of bool the carrier of A

(A,Y) is Element of bool the carrier of A

{ b

(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

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

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

(A,Y) is Element of bool the carrier of A

{ b

(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

(A,X) is Element of bool the carrier of A

{ b

(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

(A,X) is Element of bool the carrier of A

{ b

(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

(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

(A,(A,X)) is Element of bool the carrier of A

{ b

(A,(A,(A,X))) is Element of bool the carrier of A

{ b

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

(A,(A,X)) is Element of bool the carrier of A

{ b

(A,(A,(A,X))) is Element of bool the carrier of A

{ b

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

(A,X) is Element of bool the carrier of A

{ b

(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

(A,(X `)) is Element of bool the carrier of A

{ b

(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

(A,(A,X)) is Element of bool the carrier of A

{ b

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

(A,(A,X)) is Element of bool the carrier of A

{ b

(A,(A,X)) is Element of bool the carrier of A

{ b

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

(A,(A,X)) is Element of bool the carrier of A

{ b

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

(A,(A,X)) is Element of bool the carrier of A

{ b

(A,(A,X)) is Element of bool the carrier of A

{ b

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

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

(A,(A,X)) is Element of bool the carrier of A

{ b

(A,(A,X)) is Element of bool the carrier of A

{ b

(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

(A,(A,X)) is Element of bool the carrier of A

{ b

(A,(A,X)) is (A) Element of bool the carrier of A

{ b

(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

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

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

(A,X) is (A) Element of bool the carrier of A

{ b

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

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

(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

(A,X) is finite (A) Element of bool the carrier of A

{ b

(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

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