:: 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
is non trivial Relation-like non finite V69() V70() V71() set
bool is non empty non trivial non finite set
bool () 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
is non empty non trivial Relation-like non finite V69() V70() V71() set
bool 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

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
is non empty non trivial Relation-like non finite V69() set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite V69() set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like non finite V69() V70() V71() set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like RAT -valued non finite V69() V70() V71() set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like RAT -valued non finite V69() V70() V71() set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like RAT -valued INT -valued non finite V69() V70() V71() set
bool is non empty non trivial non finite set
is non empty non trivial Relation-like RAT -valued INT -valued non finite V69() V70() V71() set
bool is non empty non trivial non finite set

bool 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

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

[:A,A:] is Relation-like set
bool [:A,A:] is non empty set

A is set

[:A,A:] is Relation-like set
bool [:A,A:] is non empty set

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

[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
RelStr(# A,() #) is strict total reflexive transitive 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

bool [:{X},{X}:] is non empty finite V47() set
the carrier of A is set

A is RelStr
A is set
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set

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

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

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

X is set
Y is set
A . X is set
A . Y is set
A is set

A is non empty set
the Element of A is Element of A

1 -tuples_on A is FinSequenceSet of A

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

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

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

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

bool [:A,A:] is non empty finite V47() set

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

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

[:A,A:] is Relation-like set
bool [:A,A:] is non empty set

is non empty trivial finite V47() 1 -element V79() V80() V81() V82() V83() V84() set

bool is non empty finite V47() set
RelStr(# ,() #) 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

[:{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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,X) is Element of bool the carrier of A
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
(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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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

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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses [#] A } is set
(A,([#] A)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X /\ Y } is set
(A,Y) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X \/ Y } is set
(A,Y) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
Y is Element of bool the carrier of A
(A,Y) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
Y is Element of bool the carrier of A
(A,Y) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
Y is Element of bool the carrier of A
(A,Y) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X /\ Y } is set
(A,Y) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X ` } is set
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X ` } is set
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= (A,X) } is set
(A,(A,(A,X))) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses (A,X) } is set
(A,(A,(A,X))) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,X) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X ` } is set
(A,(X `)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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,({} 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses (A,X) } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,(A,X)) is Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses (A,X) } is set
(A,(A,X)) is (A) Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) c= X } is set
(A,X) is (A) Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) misses X } is set
(A,X) is finite (A) Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : Class ( the InternalRel of A,b1) 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
{ b1 where b1 is Element of the carrier of A : not Class ( the InternalRel of A,b1) 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()