FINSET

:: FINSET_1 semantic presentation

begin

definition

let IT be ( ( ) ( ) set ) ;

attr IT is finite means :: FINSET_1:def 1
ex p being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st
( rng p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = IT : ( ( ) ( ) set ) & dom p : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) in omega : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) set ) );

end;

notation

let IT be ( ( ) ( ) set ) ;
antonym infinite IT for finite ;

end;

registration

cluster non empty finite for ( ( ) ( ) set ) ;

end;

registration

cluster empty -> finite for ( ( ) ( ) set ) ;

end;

scheme :: FINSET_1:sch 1
OLambdaC{ F₁() -> ( ( ) ( ) set ) , P₁[ ( ( ) ( ) set ) ], F₂( ( ( ) ( ) set ) ) -> ( ( ) ( ) set ) , F₃( ( ( ) ( ) set ) ) -> ( ( ) ( ) set ) } :

ex f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st
( dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = F₁( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & ( for x being ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) st x : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) in F₁( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
( ( P₁[x : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ] implies f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( ) set ) = F₂( ( ( ) ( ) set ) ,x : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( ) set ) ) & ( P₁[x : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ] implies f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) : ( ( ) ( ) set ) = F₃( ( ( ) ( ) set ) ,x : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Ordinal) ) : ( ( ) ( ) set ) ) ) ) )

proof end;

registration

let x be ( ( ) ( ) set ) ;

cluster {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let x, y be ( ( ) ( ) set ) ;

cluster {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let x, y, z be ( ( ) ( ) set ) ;

cluster {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ,z : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let x1, x2, x3, x4 be ( ( ) ( ) set ) ;

cluster {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let x1, x2, x3, x4, x5 be ( ( ) ( ) set ) ;

cluster {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let x1, x2, x3, x4, x5, x6 be ( ( ) ( ) set ) ;

cluster {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let x1, x2, x3, x4, x5, x6, x7 be ( ( ) ( ) set ) ;

cluster {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let x1, x2, x3, x4, x5, x6, x7, x8 be ( ( ) ( ) set ) ;

cluster {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) ,x8 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -> finite ;

end;

registration

let B be ( ( finite ) ( finite ) set ) ;

cluster -> finite for ( ( ) ( ) Element of bool B : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

let X, Y be ( ( finite ) ( finite ) set ) ;

cluster X : ( ( finite ) ( finite ) set ) \/ Y : ( ( finite ) ( finite ) set ) : ( ( ) ( ) set ) -> finite ;

end;

theorem :: FINSET_1:1

for A, B being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= B : ( ( ) ( ) set ) & B : ( ( ) ( ) set ) is finite holds
A : ( ( ) ( ) set ) is finite ;

theorem :: FINSET_1:2

for A, B being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) is finite & B : ( ( ) ( ) set ) is finite holds
A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) is finite ;

registration

let A be ( ( ) ( ) set ) ;
let B be ( ( finite ) ( finite ) set ) ;

cluster A : ( ( ) ( ) set ) /\ B : ( ( finite ) ( finite ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

let A be ( ( finite ) ( finite ) set ) ;
let B be ( ( ) ( ) set ) ;

cluster A : ( ( finite ) ( finite ) set ) /\ B : ( ( ) ( ) set ) : ( ( ) ( finite ) set ) -> finite ;

cluster A : ( ( finite ) ( finite ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> finite ;

end;

theorem :: FINSET_1:3

for A, B being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) is finite holds
A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) is finite ;

theorem :: FINSET_1:4

for A, B being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) is finite holds
A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is finite ;

registration

let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
let A be ( ( finite ) ( finite ) set ) ;

cluster f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: A : ( ( finite ) ( finite ) set ) : ( ( ) ( ) set ) -> finite ;

end;

theorem :: FINSET_1:5

for A being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st A : ( ( ) ( ) set ) is finite holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: A : ( ( ) ( ) set ) : ( ( ) ( ) set ) is finite ;

theorem :: FINSET_1:6

for A being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) is finite holds
for X being ( ( ) ( ) Subset-Family of ) st X : ( ( ) ( ) Subset-Family of ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) holds
ex x being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X : ( ( ) ( ) Subset-Family of ) & ( for B being ( ( ) ( ) set ) st B : ( ( ) ( ) set ) in X : ( ( ) ( ) Subset-Family of ) & x : ( ( ) ( ) set ) c= B : ( ( ) ( ) set ) holds
B : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) ) ) ;

scheme :: FINSET_1:sch 2
Finite{ F₁() -> ( ( ) ( ) set ) , P₁[ ( ( ) ( ) set ) ] } :

P₁[F₁( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ]

provided

F₁( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is finite and
P₁[ {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ] and
for x, B being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in F₁( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & B : ( ( ) ( ) set ) c= F₁( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & P₁[B : ( ( ) ( ) set ) ] holds
P₁[B : ( ( ) ( ) set ) \/ {x : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ]

proof end;

registration

let A, B be ( ( finite ) ( finite ) set ) ;

cluster [:A : ( ( finite ) ( finite ) set ) ,B : ( ( finite ) ( finite ) set ) :] : ( ( ) ( Relation-like ) set ) -> finite ;

end;

registration

let A, B, C be ( ( finite ) ( finite ) set ) ;

cluster [:A : ( ( finite ) ( finite ) set ) ,B : ( ( finite ) ( finite ) set ) ,C : ( ( finite ) ( finite ) set ) :] : ( ( ) ( ) set ) -> finite ;

end;

registration

let A, B, C, D be ( ( finite ) ( finite ) set ) ;

cluster [:A : ( ( finite ) ( finite ) set ) ,B : ( ( finite ) ( finite ) set ) ,C : ( ( finite ) ( finite ) set ) ,D : ( ( finite ) ( finite ) set ) :] : ( ( ) ( ) set ) -> finite ;

end;

registration

let A be ( ( finite ) ( finite ) set ) ;

cluster bool A : ( ( finite ) ( finite ) set ) : ( ( ) ( non empty ) set ) -> finite ;

end;

theorem :: FINSET_1:7

for A being ( ( ) ( ) set ) holds
( ( A : ( ( ) ( ) set ) is finite & ( for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) is finite ) ) iff union A : ( ( ) ( ) set ) : ( ( ) ( ) set ) is finite ) ;

theorem :: FINSET_1:8

for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) is finite holds
rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) is finite ;

theorem :: FINSET_1:9

for Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st Y : ( ( ) ( ) set ) c= rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) " Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) is finite holds
Y : ( ( ) ( ) set ) is finite ;

registration

let X, Y be ( ( finite ) ( finite ) set ) ;

cluster X : ( ( finite ) ( finite ) set ) \+\ Y : ( ( finite ) ( finite ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

let X be ( ( non empty ) ( non empty ) set ) ;

cluster non empty finite for ( ( ) ( ) Element of bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

begin

theorem :: FINSET_1:10

for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) is finite iff f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is finite ) ;

theorem :: FINSET_1:11

for F being ( ( ) ( ) set ) st F : ( ( ) ( ) set ) is finite & F : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) & F : ( ( ) ( ) set ) is c=-linear holds
ex m being ( ( ) ( ) set ) st
( m : ( ( ) ( ) set ) in F : ( ( ) ( ) set ) & ( for C being ( ( ) ( ) set ) st C : ( ( ) ( ) set ) in F : ( ( ) ( ) set ) holds
m : ( ( ) ( ) set ) c= C : ( ( ) ( ) set ) ) ) ;

theorem :: FINSET_1:12

definition

let R be ( ( Relation-like ) ( Relation-like ) Relation) ;

attr R is finite-yielding means :: FINSET_1:def 2
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in rng R : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) is finite ;

end;

theorem :: FINSET_1:13

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) is finite & X : ( ( ) ( ) set ) c= [:Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
ex A, B being ( ( ) ( ) set ) st
( A : ( ( ) ( ) set ) is finite & A : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & B : ( ( ) ( ) set ) is finite & B : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= [:A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) ;

theorem :: FINSET_1:14

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) is finite & X : ( ( ) ( ) set ) c= [:Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
ex A being ( ( ) ( ) set ) st
( A : ( ( ) ( ) set ) is finite & A : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= [:A : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) ;

registration

cluster non empty Relation-like Function-like finite for ( ( ) ( ) set ) ;

end;

registration

let R be ( ( Relation-like finite ) ( Relation-like finite ) Relation) ;

cluster proj1 R : ( ( Relation-like finite ) ( Relation-like finite ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
let g be ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) Function) ;

cluster g : ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) set ) * f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) -> Relation-like finite ;

end;

registration

let A be ( ( finite ) ( finite ) set ) ;
let B be ( ( ) ( ) set ) ;

cluster Function-like V18(A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) ) -> Function-like V18(A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) ) finite for ( ( ) ( ) Element of bool [:A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

let x, y be ( ( ) ( ) set ) ;

cluster x : ( ( ) ( ) set ) .--> y : ( ( ) ( ) set ) : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) -defined Function-like one-to-one ) set ) -> finite ;

end;

registration

let R be ( ( Relation-like finite ) ( Relation-like finite ) Relation) ;

cluster proj2 R : ( ( Relation-like finite ) ( Relation-like finite ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

let f be ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) Function) ;
let x be ( ( ) ( ) set ) ;

cluster f : ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) set ) " x : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

let f, g be ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) Function) ;

cluster f : ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) set ) +* g : ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like finite ;

end;

definition

let F be ( ( ) ( ) set ) ;

attr F is centered means :: FINSET_1:def 3
( F : ( ( non empty ) ( non empty ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) & ( for G being ( ( ) ( ) set ) st G : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) & G : ( ( ) ( ) set ) c= F : ( ( non empty ) ( non empty ) set ) & G : ( ( ) ( ) set ) is finite holds
meet G : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ) );

end;

definition

let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

redefine attr f is finite-yielding means :: FINSET_1:def 4
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) holds
f : ( ( non empty ) ( non empty ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) is finite ;

end;

definition

let I be ( ( ) ( ) set ) ;
let IT be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) Function) ;

:: original: finite-yielding
redefine attr IT is finite-yielding means :: FINSET_1:def 5
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( non empty ) ( non empty ) set ) holds
IT : ( ( non empty ) ( non empty ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) is finite ;

end;

theorem :: FINSET_1:15

for B, A being ( ( ) ( ) set ) st B : ( ( ) ( ) set ) is infinite holds
not B : ( ( ) ( ) set ) in [:A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ;

registration

let I be ( ( ) ( ) set ) ;
let f be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) Function) ;

cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like f : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) set ) -compatible finite for ( ( ) ( ) set ) ;

end;

registration

let X, Y be ( ( ) ( ) set ) ;

cluster Relation-like X : ( ( ) ( ) set ) -defined Y : ( ( ) ( ) set ) -valued Function-like finite for ( ( ) ( ) set ) ;

end;

registration

let X, Y be ( ( non empty ) ( non empty ) set ) ;

cluster non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined Y : ( ( non empty ) ( non empty ) set ) -valued Function-like finite for ( ( ) ( ) set ) ;

end;

registration

let A be ( ( ) ( ) set ) ;
let F be ( ( Relation-like finite ) ( Relation-like finite ) Relation) ;

cluster A : ( ( ) ( ) set ) |` F : ( ( Relation-like finite ) ( Relation-like finite ) set ) : ( ( Relation-like ) ( Relation-like ) set ) -> Relation-like finite ;

end;

registration

let A be ( ( ) ( ) set ) ;
let F be ( ( Relation-like finite ) ( Relation-like finite ) Relation) ;

cluster F : ( ( Relation-like finite ) ( Relation-like finite ) set ) | A : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) -> Relation-like finite ;

end;

registration

let A be ( ( finite ) ( finite ) set ) ;
let F be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

cluster F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) | A : ( ( finite ) ( finite ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) -> Relation-like finite ;

end;

registration

let R be ( ( Relation-like finite ) ( Relation-like finite ) Relation) ;

cluster field R : ( ( Relation-like finite ) ( Relation-like finite ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

cluster trivial -> finite for ( ( ) ( ) set ) ;

end;

registration

cluster infinite -> non trivial for ( ( ) ( ) set ) ;

end;

registration

let X be ( ( non trivial ) ( non trivial ) set ) ;

cluster non trivial finite for ( ( ) ( ) Element of bool X : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

let x, y, a, b be ( ( ) ( ) set ) ;

cluster (x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ) --> (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> finite ;

end;

definition

let A be ( ( ) ( ) set ) ;

attr A is finite-membered means :: FINSET_1:def 6
for B being ( ( ) ( ) set ) st B : ( ( ) ( ) set ) in A : ( ( non trivial ) ( non trivial ) set ) holds
B : ( ( ) ( ) set ) is finite ;

end;

registration

cluster empty -> finite-membered for ( ( ) ( ) set ) ;

end;

registration

let A be ( ( finite-membered ) ( finite-membered ) set ) ;

cluster -> finite for ( ( ) ( ) Element of A : ( ( non trivial ) ( non trivial ) set ) ) ;

end;

registration

cluster non empty finite finite-membered for ( ( ) ( ) set ) ;

end;

registration

let X be ( ( finite ) ( finite ) set ) ;

cluster {X : ( ( finite ) ( finite ) set ) } : ( ( ) ( non empty finite ) set ) -> finite-membered ;

cluster bool X : ( ( finite ) ( finite ) set ) : ( ( ) ( non empty finite ) set ) -> finite-membered ;

let Y be ( ( finite ) ( finite ) set ) ;

cluster {X : ( ( finite ) ( finite ) set ) ,Y : ( ( finite ) ( finite ) set ) } : ( ( ) ( non empty finite ) set ) -> finite-membered ;

end;

registration

let X be ( ( finite-membered ) ( finite-membered ) set ) ;

cluster -> finite-membered for ( ( ) ( ) Element of bool X : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) set ) ) ;

let Y be ( ( finite-membered ) ( finite-membered ) set ) ;

cluster X : ( ( finite-membered ) ( finite-membered ) set ) \/ Y : ( ( finite-membered ) ( finite-membered ) set ) : ( ( ) ( ) set ) -> finite-membered ;

end;

registration

let X be ( ( finite finite-membered ) ( finite finite-membered ) set ) ;

cluster union X : ( ( finite finite-membered ) ( finite finite-membered ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

cluster non empty Relation-like Function-like finite-yielding for ( ( ) ( ) set ) ;

cluster empty Relation-like -> Relation-like finite-yielding for ( ( ) ( ) set ) ;

end;

registration

let F be ( ( Relation-like Function-like finite-yielding ) ( Relation-like Function-like finite-yielding ) Function) ;
let x be ( ( ) ( ) set ) ;

cluster F : ( ( Relation-like Function-like finite-yielding ) ( Relation-like Function-like finite-yielding ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> finite ;

end;

registration

let F be ( ( Relation-like finite-yielding ) ( Relation-like finite-yielding ) Relation) ;

cluster proj2 F : ( ( Relation-like finite-yielding ) ( Relation-like finite-yielding ) set ) : ( ( ) ( ) set ) -> finite-membered ;

end;