:: FINSET_1 semantic presentation

begin

definition
let IT be set ;
attrIT is finite  means :Def1: :: FINSET_1:def 1
 ex p being Function st
( rng p = IT & dom p in omega );
end;

:: deftheorem Def1 defines finite FINSET_1:def_1_:_
 for IT being set holds
( IT is finite iff ex p being Function st
( rng p = IT & dom p in omega ) );

notation
let IT be set ;
antonym  infinite IT for  finite ;
end;

        Lm1:  for x being set holds {x} is finite
proof
let x be set ; ::_thesis: {x} is finite
set p = {{}} --> x;
A1: dom ({{}} --> x) = {{}} by FUNCOP_1:13;
take  {{}} --> x ; :: according to FINSET_1:def_1 ::_thesis: ( rng ({{}} --> x) = {x} & dom ({{}} --> x) in omega )
 for y being set holds
( y in {x} iff ex x being set st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) )
proof
let y be set ; ::_thesis: ( y in {x} iff ex x being set st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) )
thus  ( y in {x} implies ex x being set st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) ) ::_thesis: ( ex x being set st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x ) implies y in {x} )
proof
assume  y in {x} ; ::_thesis: ex x being set st
( x in dom ({{}} --> x) & y = ({{}} --> x) . x )
then A2: y = x by TARSKI:def_1;
take  {} ; ::_thesis: ( {} in dom ({{}} --> x) & y = ({{}} --> x) . {} )
thus  {} in dom ({{}} --> x) by A1, TARSKI:def_1; ::_thesis: y = ({{}} --> x) . {}
 {} in {{}} by TARSKI:def_1;
hence  y = ({{}} --> x) . {} by A2, FUNCOP_1:7; ::_thesis: verum
end;
assume  ex z being set st
( z in dom ({{}} --> x) & y = ({{}} --> x) . z ) ; ::_thesis: y in {x}
then  y = x by FUNCOP_1:7;
hence  y in {x} by TARSKI:def_1; ::_thesis: verum
end;
hence  rng ({{}} --> x) = {x} by FUNCT_1:def_3; ::_thesis: dom ({{}} --> x) in omega
thus  dom ({{}} --> x) in omega by A1, ORDINAL3:15; ::_thesis: verum
end;

registration
cluster non empty finite for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is finite )
proof
 { the set } is finite by Lm1;
hence  ex b1 being set st
( not b1 is empty & b1 is finite ) ; ::_thesis: verum
end;
end;

registration
cluster empty  ->  finite for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is finite
proof
let A be set ; ::_thesis: ( A is empty implies A is finite )
assume A1: A is empty ; ::_thesis: A is finite
take  {} ; :: according to FINSET_1:def_1 ::_thesis: ( rng {} = A & dom {} in omega )
thus  rng {} = A by A1; ::_thesis: dom {} in omega
thus  dom {} in omega by ORDINAL1:def_11; ::_thesis: verum
end;
end;

scheme :: FINSET_1:sch 1
OLambdaC{ F1() ->  set , P1[ set ], F2( set ) ->  set , F3( set ) ->  set } :
 ex f being Function st
( dom f = F1() & ( for x being Ordinal st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )
proof
consider f being Function such that
A1: ( dom f = F1() & ( for x being set st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) from PARTFUN1:sch_1();
take  f ; ::_thesis: ( dom f = F1() & ( for x being Ordinal st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )
thus  ( dom f = F1() & ( for x being Ordinal st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) by A1; ::_thesis: verum
end;

Lm2:  for A, B being set st A is finite & B is finite holds
A \/ B is finite
proof
let A, B be set ; ::_thesis: ( A is finite & B is finite implies A \/ B is finite )
given p being Function such that A1: rng p = A and
A2: dom p in omega ; :: according to FINSET_1:def_1 ::_thesis: ( not B is finite or A \/ B is finite )
given q being Function such that A3: rng q = B and
A4: dom q in omega ; :: according to FINSET_1:def_1 ::_thesis: A \/ B is finite
reconsider domp = dom p, domq = dom q as Ordinal by A2, A4;
deffunc H1( Ordinal) ->  set = p . $1;
deffunc H2( Ordinal) ->  set = q . ($1 -^ domp);
defpred S1[ set ] means $1 in domp;
consider f being Function such that
A5: dom f = domp +^ domq and
A6: for x being Ordinal st x in domp +^ domq holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) from FINSET_1:sch_1();
take  f ; :: according to FINSET_1:def_1 ::_thesis: ( rng f = A \/ B & dom f in omega )
reconsider domp = domp, domq = domq as natural Ordinal by A2, A4;
thus  rng f = A \/ B ::_thesis: dom f in omega
proof
thus  rng f c= A \/ B :: according to XBOOLE_0:def_10 ::_thesis: A \/ B c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in A \/ B )
assume  y in rng f ; ::_thesis: y in A \/ B
then consider x being set  such that
A7: x in dom f and
A8: y = f . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A5, A7;
percases ( x in domp or not x in domp ) ;
supposeA9: x in domp ; ::_thesis: y in A \/ B
then A10: y = p . x by A5, A6, A7, A8;
 p . x in rng p by A9, FUNCT_1:def_3;
hence  y in A \/ B by A1, A10, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA11: not x in domp ; ::_thesis: y in A \/ B
then A12: domp c= x by ORDINAL1:16;
A13: y = q . (x -^ domp) by A5, A6, A7, A8, A11;
 domp +^ (x -^ domp) = x by A12, ORDINAL3:def_5;
then  x -^ domp in dom q by A5, A7, ORDINAL3:22;
then  y in B by A3, A13, FUNCT_1:def_3;
hence  y in A \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \/ B or x in rng f )
assume A14: x in A \/ B ; ::_thesis: x in rng f
percases ( x in rng p or x in rng q ) by A1, A3, A14, XBOOLE_0:def_3;
suppose x in rng p ; ::_thesis: x in rng f
then consider y being set  such that
A15: y in dom p and
A16: x = p . y by FUNCT_1:def_3;
A17: dom p c= dom f by A5, ORDINAL3:24;
then  x = f . y by A5, A6, A15, A16;
hence  x in rng f by A15, A17, FUNCT_1:def_3; ::_thesis: verum
end;
suppose x in rng q ; ::_thesis: x in rng f
then consider y being set  such that
A18: y in domq and
A19: x = q . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A18;
set z = domp +^ y;
 domp c= domp +^ y by ORDINAL3:24;
then A20: not domp +^ y in domp by ORDINAL1:5;
A21: domp +^ y in dom f by A5, A18, ORDINAL3:17;
x = q . ((domp +^ y) -^ domp) by A19, ORDINAL3:52
.= f . (domp +^ y) by A5, A6, A20, A21 ;
hence  x in rng f by A21, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
 domp +^ domq is natural ;
hence  dom f in omega by A5, ORDINAL1:def_12; ::_thesis: verum
end;

registration
let x be set ;
cluster{x} ->  finite ;
coherence
 {x} is finite by Lm1;
end;

registration
let x, y be set ;
cluster{x,y} ->  finite ;
coherence
 {x,y} is finite
proof
 {x,y} = {x} \/ {y} by ENUMSET1:1;
hence  {x,y} is finite by Lm2; ::_thesis: verum
end;
end;

registration
let x, y, z be set ;
cluster{x,y,z} ->  finite ;
coherence
 {x,y,z} is finite
proof
 {x,y,z} = {x} \/ {y,z} by ENUMSET1:2;
hence  {x,y,z} is finite by Lm2; ::_thesis: verum
end;
end;

registration
let x1, x2, x3, x4 be set ;
cluster{x1,x2,x3,x4} ->  finite ;
coherence
 {x1,x2,x3,x4} is finite
proof
 {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by ENUMSET1:4;
hence  {x1,x2,x3,x4} is finite by Lm2; ::_thesis: verum
end;
end;

registration
let x1, x2, x3, x4, x5 be set ;
cluster{x1,x2,x3,x4,x5} ->  finite ;
coherence
 {x1,x2,x3,x4,x5} is finite
proof
 {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} by ENUMSET1:7;
hence  {x1,x2,x3,x4,x5} is finite by Lm2; ::_thesis: verum
end;
end;

registration
let x1, x2, x3, x4, x5, x6 be set ;
cluster{x1,x2,x3,x4,x5,x6} ->  finite ;
coherence
 {x1,x2,x3,x4,x5,x6} is finite
proof
 {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} by ENUMSET1:11;
hence  {x1,x2,x3,x4,x5,x6} is finite by Lm2; ::_thesis: verum
end;
end;

registration
let x1, x2, x3, x4, x5, x6, x7 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7} ->  finite ;
coherence
 {x1,x2,x3,x4,x5,x6,x7} is finite
proof
 {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} by ENUMSET1:16;
hence  {x1,x2,x3,x4,x5,x6,x7} is finite by Lm2; ::_thesis: verum
end;
end;

registration
let x1, x2, x3, x4, x5, x6, x7, x8 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8} ->  finite ;
coherence
 {x1,x2,x3,x4,x5,x6,x7,x8} is finite
proof
 {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} by ENUMSET1:22;
hence  {x1,x2,x3,x4,x5,x6,x7,x8} is finite by Lm2; ::_thesis: verum
end;
end;

registration
let B be finite set ;
cluster  ->  finite for Element of bool B;
coherence
 for b1 being Subset of B holds b1 is finite
proof
let A be Subset of B; ::_thesis: A is finite
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: A is finite
hence  A is finite ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: A is finite
then consider x1 being set  such that
A1: x1 in A by XBOOLE_0:def_1;
consider p being Function such that
A2: rng p = B and
A3: dom p in omega by Def1;
deffunc H1( set ) ->  set = p . B;
deffunc H2( set ) ->  set = x1;
defpred S1[ set ] means p . B in A;
consider q being Function such that
A4: dom q = dom p and
A5: for x being set st x in dom p holds
( ( S1[x] implies q . x = H1(x) ) & ( not S1[x] implies q . x = H2(x) ) ) from PARTFUN1:sch_1();
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_A_implies_ex_x_being_set_st_
(_x_in_dom_q_&_y_=_q_._x_)_)_&_(_ex_x_being_set_st_
(_x_in_dom_q_&_y_=_q_._x_)_implies_y_in_A_)_)
let y be set ; ::_thesis: ( ( y in A implies ex x being set st
( x in dom q & y = q . x ) ) & ( ex x being set st
( x in dom q & y = q . x ) implies b1 in A ) )
thus  ( y in A implies ex x being set st
( x in dom q & y = q . x ) ) ::_thesis: ( ex x being set st
( x in dom q & y = q . x ) implies b1 in A )
proof
assume A6: y in A ; ::_thesis: ex x being set st
( x in dom q & y = q . x )
then consider x being set  such that
A7: x in dom p and
A8: p . x = y by A2, FUNCT_1:def_3;
take  x ; ::_thesis: ( x in dom q & y = q . x )
thus  x in dom q by A4, A7; ::_thesis: y = q . x
thus  y = q . x by A5, A6, A7, A8; ::_thesis: verum
end;
given x being set  such that A9: x in dom q and
A10: y = q . x ; ::_thesis: b1 in A
percases ( p . x in A or not p . x in A ) ;
suppose p . x in A ; ::_thesis: b1 in A
hence  y in A by A4, A5, A9, A10; ::_thesis: verum
end;
suppose not p . x in A ; ::_thesis: b1 in A
hence  y in A by A1, A4, A5, A9, A10; ::_thesis: verum
end;
end;
end;
then  rng q = A by FUNCT_1:def_3;
hence  A is finite by A3, A4, Def1; ::_thesis: verum
end;
end;
end;
end;

registration
let X, Y be finite set ;
clusterX \/ Y ->  finite ;
coherence
 X \/ Y is finite by Lm2;
end;

theorem :: FINSET_1:1
for A, B being set st A c= B & B is finite holds
A is finite ;

theorem :: FINSET_1:2
for A, B being set st A is finite & B is finite holds
A \/ B is finite ;

registration
let A be set ;
let B be finite set ;
clusterA /\ B ->  finite ;
coherence
 A /\ B is finite
proof
 A /\ B c= B by XBOOLE_1:17;
hence  A /\ B is finite ; ::_thesis: verum
end;
end;

registration
let A be finite set ;
let B be set ;
clusterA /\ B ->  finite ;
coherence
 A /\ B is finite ;
clusterA \ B ->  finite ;
coherence
 A \ B is finite ;
end;

theorem :: FINSET_1:3
for A, B being set st A is finite holds
A /\ B is finite ;

theorem :: FINSET_1:4
for A, B being set st A is finite holds
A \ B is finite ;

registration
let f be Function;
let A be finite set ;
clusterf .: A ->  finite ;
coherence
 f .: A is finite
proof
set B = (dom f) /\ A;
consider p being Function such that
A1: rng p = (dom f) /\ A and
A2: dom p in omega by Def1;
take  f * p ; :: according to FINSET_1:def_1 ::_thesis: ( rng (f * p) = f .: A & dom (f * p) in omega )
 rng (f * p) = f .: ((dom f) /\ A) by A1, RELAT_1:127;
hence  rng (f * p) = f .: A by RELAT_1:112; ::_thesis: dom (f * p) in omega
thus  dom (f * p) in omega by A1, A2, RELAT_1:27, XBOOLE_1:17; ::_thesis: verum
end;
end;

theorem :: FINSET_1:5
for A being set
for f being Function st A is finite holds
f .: A is finite ;

theorem Th6: :: FINSET_1:6
for A being set st A is finite holds
for X being Subset-Family of A st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
proof
let A be set ; ::_thesis: ( A is finite implies for X being Subset-Family of A st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume A1: A is finite ; ::_thesis: for X being Subset-Family of A st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
let X be Subset-Family of A; ::_thesis: ( X <> {} implies ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume A2: X <> {} ; ::_thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
consider p being Function such that
A3: rng p = A and
A4: dom p in omega by A1, Def1;
defpred S1[ set ] means p .: $1 in X;
consider G being set  such that
A5: for x being set holds
( x in G iff ( x in bool (dom p) & S1[x] ) ) from XBOOLE_0:sch_1();
 G c= bool (dom p)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in bool (dom p) )
assume  x in G ; ::_thesis: x in bool (dom p)
hence  x in bool (dom p) by A5; ::_thesis: verum
end;
then reconsider GX = G as Subset-Family of (dom p) ;
set x = the Element of X;
 the Element of X is Subset of A by A2, TARSKI:def_3;
then A6: p .: (p " the Element of X) = the Element of X by A3, FUNCT_1:77;
 p " the Element of X c= dom p by RELAT_1:132;
then A7: GX <> {} by A2, A5, A6;
defpred S2[ set ] means ( $1 in omega implies for X being Subset-Family of $1 st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) );
A8: S2[ {} ]
proof
assume  {} in omega ; ::_thesis: for X being Subset-Family of {} st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
let X be Subset-Family of {}; ::_thesis: ( X <> {} implies ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume  X <> {} ; ::_thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
then A9: X = {{}} by ZFMISC_1:1, ZFMISC_1:33;
take  {} ; ::_thesis: ( {} in X & ( for B being set st B in X & {} c= B holds
B = {} ) )
thus  ( {} in X & ( for B being set st B in X & {} c= B holds
B = {} ) ) by A9, TARSKI:def_1; ::_thesis: verum
end;
A10: for O being Ordinal st S2[O] holds
S2[ succ O]
proof
let O be Ordinal; ::_thesis: ( S2[O] implies S2[ succ O] )
assume A11: ( O in omega implies for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ) ; ::_thesis: S2[ succ O]
thus  ( succ O in omega implies for X being Subset-Family of (succ O) st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ) ::_thesis: verum
proof
assume  succ O in omega ; ::_thesis: for X being Subset-Family of (succ O) st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
then A12: succ O c= omega by ORDINAL1:def_2;
let X be Subset-Family of (succ O); ::_thesis: ( X <> {} implies ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume A13: X <> {} ; ::_thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
defpred S3[ set ] means  ex A being set st
( A in X & $1 = A \ {O} );
consider X1 being set  such that
A14: for x being set holds
( x in X1 iff ( x in bool O & S3[x] ) ) from XBOOLE_0:sch_1();
 X1 c= bool O
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in bool O )
assume  x in X1 ; ::_thesis: x in bool O
hence  x in bool O by A14; ::_thesis: verum
end;
then reconsider X2 = X1 as Subset-Family of O ;
set y = the Element of X;
A15: succ O = O \/ {O} by ORDINAL1:def_1;
 the Element of X is Subset of (succ O) by A13, TARSKI:def_3;
then  the Element of X \ {O} c= (O \/ {O}) \ {O} by A15, XBOOLE_1:33;
then A16: the Element of X \ {O} c= O \ {O} by XBOOLE_1:40;
A17: O in succ O by ORDINAL1:6;
A18: not O in O ;
then  the Element of X \ {O} c= O by A16, ZFMISC_1:57;
then  X2 <> {} by A13, A14;
then consider Z being set  such that
A19: Z in X2 and
A20: for B being set st B in X2 & Z c= B holds
B = Z by A11, A12, A17;
consider X1 being set  such that
A21: X1 in X and
A22: Z = X1 \ {O} by A14, A19;
A23: O in {O} by TARSKI:def_1;
then A24: not O in Z by A22, XBOOLE_0:def_5;
A25: now__::_thesis:_(_Z_\/_{O}_in_X_implies_ex_A_being_set_ex_x_being_set_st_
(_x_in_X_&_(_for_B_being_set_st_B_in_X_&_x_c=_B_holds_
B_=_x_)_)_)
assume A26: Z \/ {O} in X ; ::_thesis: ex A being set ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
take A = Z \/ {O}; ::_thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
 for B being set st B in X & A c= B holds
B = A
proof
let B be set ; ::_thesis: ( B in X & A c= B implies B = A )
assume A27: B in X ; ::_thesis: ( not A c= B or B = A )
assume A28: A c= B ; ::_thesis: B = A
A29: now__::_thesis:_(_O_in_B_implies_B_=_A_)
assume A30: O in B ; ::_thesis: B = A
set Y = B \ {O};
 {O} c= B by A30, ZFMISC_1:31;
then A31: B = (B \ {O}) \/ {O} by XBOOLE_1:45;
 A \ {O} c= B \ {O} by A28, XBOOLE_1:33;
then A32: Z \ {O} c= B \ {O} by XBOOLE_1:40;
 not O in Z by A22, A23, XBOOLE_0:def_5;
then A33: Z c= B \ {O} by A32, ZFMISC_1:57;
 B \ {O} c= (O \/ {O}) \ {O} by A15, A27, XBOOLE_1:33;
then  B \ {O} c= O \ {O} by XBOOLE_1:40;
then  B \ {O} c= O by A18, ZFMISC_1:57;
then  B \ {O} in X2 by A14, A27;
hence  B = A by A20, A31, A33; ::_thesis: verum
end;
now__::_thesis:_O_in_B
assume A34: not O in B ; ::_thesis: contradiction
 O in {O} by TARSKI:def_1;
then  O in A by XBOOLE_0:def_3;
hence  contradiction by A28, A34; ::_thesis: verum
end;
hence  B = A by A29; ::_thesis: verum
end;
hence  ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A26; ::_thesis: verum
end;
now__::_thesis:_(_not_Z_\/_{O}_in_X_implies_ex_A,_x_being_set_st_
(_x_in_X_&_(_for_B_being_set_st_B_in_X_&_x_c=_B_holds_
B_=_x_)_)_)
assume A35: not Z \/ {O} in X ; ::_thesis: ex A, x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
take A = Z; ::_thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
now__::_thesis:_not_O_in_X1
assume  O in X1 ; ::_thesis: contradiction
then X1 = X1 \/ {O} by ZFMISC_1:40
.= Z \/ {O} by A22, XBOOLE_1:39 ;
hence  contradiction by A21, A35; ::_thesis: verum
end;
then A36: A in X by A21, A22, ZFMISC_1:57;
 for B being set st B in X & A c= B holds
B = A
proof
let B be set ; ::_thesis: ( B in X & A c= B implies B = A )
assume A37: B in X ; ::_thesis: ( not A c= B or B = A )
then  B \ {O} c= (O \/ {O}) \ {O} by A15, XBOOLE_1:33;
then  B \ {O} c= O \ {O} by XBOOLE_1:40;
then  B \ {O} c= O by A18, ZFMISC_1:57;
then A38: B \ {O} in X2 by A14, A37;
assume A39: A c= B ; ::_thesis: B = A
then  A \ {O} c= B \ {O} by XBOOLE_1:33;
then A40: A c= B \ {O} by A24, ZFMISC_1:57;
A41: now__::_thesis:_not_O_in_B
assume A42: O in B ; ::_thesis: contradiction
A \/ {O} = (B \ {O}) \/ {O} by A20, A38, A40
.= B \/ {O} by XBOOLE_1:39
.= B by A42, ZFMISC_1:40 ;
hence  contradiction by A35, A37; ::_thesis: verum
end;
A43: B c= O
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in O )
assume A44: x in B ; ::_thesis: x in O
 ( x in O or x in {O} ) by A15, A37, A44, XBOOLE_0:def_3;
hence  x in O by A41, A44, TARSKI:def_1; ::_thesis: verum
end;
 B \ {O} = B by A41, ZFMISC_1:57;
then  B in X2 by A14, A37, A43;
hence  B = A by A20, A39; ::_thesis: verum
end;
hence  ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A36; ::_thesis: verum
end;
hence  ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A25; ::_thesis: verum
end;
end;
A45: for O being Ordinal st O <> {} & O is limit_ordinal & ( for B being Ordinal st B in O holds
S2[B] ) holds
S2[O]
proof
let O be Ordinal; ::_thesis: ( O <> {} & O is limit_ordinal & ( for B being Ordinal st B in O holds
S2[B] ) implies S2[O] )
assume that
A46: O <> {} and
A47: O is limit_ordinal and
 for B being Ordinal st B in O holds
S2[B] and
A48: O in omega ; ::_thesis: for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
 {} in O by A46, ORDINAL1:14;
then  omega c= O by A47, ORDINAL1:def_11;
then  O in O by A48;
hence  for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ; ::_thesis: verum
end;
 for O being Ordinal holds S2[O] from ORDINAL2:sch_1(A8, A10, A45);
then consider g being set  such that
A49: g in GX and
A50: for B being set st B in GX & g c= B holds
B = g by A4, A7;
take  p .: g ; ::_thesis: ( p .: g in X & ( for B being set st B in X & p .: g c= B holds
B = p .: g ) )
 for B being set st B in X & p .: g c= B holds
B = p .: g
proof
let B be set ; ::_thesis: ( B in X & p .: g c= B implies B = p .: g )
assume A51: B in X ; ::_thesis: ( not p .: g c= B or B = p .: g )
assume  p .: g c= B ; ::_thesis: B = p .: g
then A52: p " (p .: g) c= p " B by RELAT_1:143;
A53: g c= p " (p .: g) by A49, FUNCT_1:76;
A54: p .: (p " B) = B by A3, A51, FUNCT_1:77;
 p " B c= dom p by RELAT_1:132;
then  p " B in GX by A5, A51, A54;
hence  B = p .: g by A50, A52, A53, A54, XBOOLE_1:1; ::_thesis: verum
end;
hence  ( p .: g in X & ( for B being set st B in X & p .: g c= B holds
B = p .: g ) ) by A5, A49; ::_thesis: verum
end;

scheme :: FINSET_1:sch 2
Finite{ F1() ->  set , P1[ set ] } :
 P1[F1()]
provided
A1: F1() is finite and
A2: P1[ {} ] and
A3: for x, B being set st x in F1() & B c= F1() & P1[B] holds
P1[B \/ {x}]
proof
now__::_thesis:_(_F1()_<>_{}_implies_P1[F1()]_)
assume  F1() <> {} ; ::_thesis: P1[F1()]
defpred S1[ set ] means  ex B being set st
( B = $1 & P1[B] );
consider G being set  such that
A4: for x being set holds
( x in G iff ( x in bool F1() & S1[x] ) ) from XBOOLE_0:sch_1();
 G c= bool F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in bool F1() )
assume  x in G ; ::_thesis: x in bool F1()
hence  x in bool F1() by A4; ::_thesis: verum
end;
then reconsider GA = G as Subset-Family of F1() ;
 {} c= F1() by XBOOLE_1:2;
then  GA <> {} by A2, A4;
then consider B being set  such that
A5: B in GA and
A6: for X being set st X in GA & B c= X holds
B = X by A1, Th6;
A7: ex A being set st
( A = B & P1[A] ) by A4, A5;
now__::_thesis:_not_B_<>_F1()
set x = the Element of F1() \ B;
assume  B <> F1() ; ::_thesis: contradiction
then  not F1() c= B by A5, XBOOLE_0:def_10;
then A8: F1() \ B <> {} by XBOOLE_1:37;
then A9: the Element of F1() \ B in F1() by XBOOLE_0:def_5;
then A10: P1[B \/ { the Element of F1() \ B}] by A3, A5, A7;
 { the Element of F1() \ B} c= F1() by A9, ZFMISC_1:31;
then  B \/ { the Element of F1() \ B} c= F1() by A5, XBOOLE_1:8;
then A11: B \/ { the Element of F1() \ B} in GA by A4, A10;
 not the Element of F1() \ B in B by A8, XBOOLE_0:def_5;
then  not { the Element of F1() \ B} c= B by ZFMISC_1:31;
then  B \/ { the Element of F1() \ B} <> B by XBOOLE_1:7;
hence  contradiction by A6, A11, XBOOLE_1:7; ::_thesis: verum
end;
hence  P1[F1()] by A7; ::_thesis: verum
end;
hence  P1[F1()] by A2; ::_thesis: verum
end;

Lm3:  for A being set st A is finite & ( for X being set st X in A holds
X is finite ) holds
union A is finite
proof
let A be set ; ::_thesis: ( A is finite & ( for X being set st X in A holds
X is finite ) implies union A is finite )
assume that
A1: A is finite and
A2: for X being set st X in A holds
X is finite ; ::_thesis: union A is finite
defpred S1[ set ] means  ex B being set st
( B = $1 & union B is finite );
consider G being set  such that
A3: for x being set holds
( x in G iff ( x in bool A & S1[x] ) ) from XBOOLE_0:sch_1();
defpred S2[ set ] means $1 in G;
 {} c= A by XBOOLE_1:2;
then A4: S2[ {} ] by A3, ZFMISC_1:2;
A5: for x, B being set st x in A & B c= A & S2[B] holds
S2[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in A & B c= A & S2[B] implies S2[B \/ {x}] )
assume that
A6: x in A and
 B c= A and
A7: B in G ; ::_thesis: S2[B \/ {x}]
A8: ex X being set st
( X = B & union X is finite ) by A3, A7;
A9: x is finite by A2, A6;
A10: union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ x by ZFMISC_1:25 ;
A11: {x} c= A by A6, ZFMISC_1:31;
 B in bool A by A3, A7;
then  B \/ {x} c= A by A11, XBOOLE_1:8;
hence  S2[B \/ {x}] by A3, A8, A9, A10; ::_thesis: verum
end;
 S2[A] from FINSET_1:sch_2(A1, A4, A5);
then  ex X being set st
( X = A & union X is finite ) by A3;
hence  union A is finite ; ::_thesis: verum
end;

registration
let A, B be finite set ;
cluster[:A,B:] ->  finite ;
coherence
 [:A,B:] is finite
proof
A1: for y being set holds [:A,{y}:] is finite
proof
let y be set ; ::_thesis: [:A,{y}:] is finite
deffunc H1( set ) ->  set = [A,y];
consider f being Function such that
A2: ( dom f = A & ( for x being set st x in A holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
 for x being set holds
( x in rng f iff x in [:A,{y}:] )
proof
let x be set ; ::_thesis: ( x in rng f iff x in [:A,{y}:] )
thus  ( x in rng f implies x in [:A,{y}:] ) ::_thesis: ( x in [:A,{y}:] implies x in rng f )
proof
assume  x in rng f ; ::_thesis: x in [:A,{y}:]
then consider z being set  such that
A3: z in dom f and
A4: f . z = x by FUNCT_1:def_3;
 x = [z,y] by A2, A3, A4;
hence  x in [:A,{y}:] by A2, A3, ZFMISC_1:106; ::_thesis: verum
end;
thus  ( x in [:A,{y}:] implies x in rng f ) ::_thesis: verum
proof
assume  x in [:A,{y}:] ; ::_thesis: x in rng f
then consider x1, x2 being set  such that
A5: x1 in A and
A6: x2 in {y} and
A7: x = [x1,x2] by ZFMISC_1:def_2;
 x2 = y by A6, TARSKI:def_1;
then  x = f . x1 by A2, A5, A7;
hence  x in rng f by A2, A5, FUNCT_1:def_3; ::_thesis: verum
end;
end;
then  rng f = [:A,{y}:] by TARSKI:1;
then  f .: A = [:A,{y}:] by A2, RELAT_1:113;
hence  [:A,{y}:] is finite ; ::_thesis: verum
end;
defpred S1[ set ] means  ex y being set st
( y in B & A = [:A,{y}:] );
consider G being set  such that
A8: for x being set holds
( x in G iff ( x in bool [:A,B:] & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set holds
( x in union G iff x in [:A,B:] )
proof
let x be set ; ::_thesis: ( x in union G iff x in [:A,B:] )
thus  ( x in union G implies x in [:A,B:] ) ::_thesis: ( x in [:A,B:] implies x in union G )
proof
assume  x in union G ; ::_thesis: x in [:A,B:]
then consider X being set  such that
A9: x in X and
A10: X in G by TARSKI:def_4;
 X in bool [:A,B:] by A8, A10;
hence  x in [:A,B:] by A9; ::_thesis: verum
end;
assume  x in [:A,B:] ; ::_thesis: x in union G
then consider y, z being set  such that
A11: y in A and
A12: z in B and
A13: x = [y,z] by ZFMISC_1:def_2;
A14: [y,z] in [:A,{z}:] by A11, ZFMISC_1:106;
 {z} c= B by A12, ZFMISC_1:31;
then  [:A,{z}:] c= [:A,B:] by ZFMISC_1:95;
then  [:A,{z}:] in G by A8, A12;
hence  x in union G by A13, A14, TARSKI:def_4; ::_thesis: verum
end;
then A15: union G = [:A,B:] by TARSKI:1;
deffunc H1( set ) ->  set = [:A,{A}:];
consider g being Function such that
A16: ( dom g = B & ( for x being set st x in B holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
 for x being set holds
( x in rng g iff x in G )
proof
let x be set ; ::_thesis: ( x in rng g iff x in G )
thus  ( x in rng g implies x in G ) ::_thesis: ( x in G implies x in rng g )
proof
assume  x in rng g ; ::_thesis: x in G
then consider y being set  such that
A17: y in dom g and
A18: g . y = x by FUNCT_1:def_3;
A19: x = [:A,{y}:] by A16, A17, A18;
 {y} c= B by A16, A17, ZFMISC_1:31;
then  x c= [:A,B:] by A19, ZFMISC_1:95;
hence  x in G by A8, A16, A17, A19; ::_thesis: verum
end;
assume  x in G ; ::_thesis: x in rng g
then consider y being set  such that
A20: y in B and
A21: x = [:A,{y}:] by A8;
 x = g . y by A16, A20, A21;
hence  x in rng g by A16, A20, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng g = G by TARSKI:1;
then A22: g .: B = G by A16, RELAT_1:113;
 for X being set st X in G holds
X is finite
proof
let X be set ; ::_thesis: ( X in G implies X is finite )
assume  X in G ; ::_thesis: X is finite
then  ex y being set st
( y in B & X = [:A,{y}:] ) by A8;
hence  X is finite by A1; ::_thesis: verum
end;
hence  [:A,B:] is finite by A15, A22, Lm3; ::_thesis: verum
end;
end;

registration
let A, B, C be finite set ;
cluster[:A,B,C:] ->  finite ;
coherence
 [:A,B,C:] is finite
proof
 [:[:A,B:],C:] is finite ;
hence  [:A,B,C:] is finite by ZFMISC_1:def_3; ::_thesis: verum
end;
end;

registration
let A, B, C, D be finite set ;
cluster[:A,B,C,D:] ->  finite ;
coherence
 [:A,B,C,D:] is finite
proof
 [:[:A,B,C:],D:] is finite ;
hence  [:A,B,C,D:] is finite by ZFMISC_1:def_4; ::_thesis: verum
end;
end;

registration
let A be finite set ;
cluster bool A ->  finite ;
coherence
 bool A is finite
proof
A1: A is finite ;
defpred S1[ set ] means  bool A is finite ;
consider G being set  such that
A2: for x being set holds
( x in G iff ( x in bool A & S1[x] ) ) from XBOOLE_0:sch_1();
defpred S2[ set ] means A in G;
A3: bool {} is finite by ZFMISC_1:1;
 {} c= A by XBOOLE_1:2;
then A4: S2[ {} ] by A3, A2;
A5: for x, B being set st x in A & B c= A & S2[B] holds
S2[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in A & B c= A & S2[B] implies S2[B \/ {x}] )
assume that
A6: x in A and
 B c= A and
A7: B in G ; ::_thesis: S2[B \/ {x}]
A8: now__::_thesis:_(_x_in_B_implies_S2[B_\/_{x}]_)
assume  x in B ; ::_thesis: S2[B \/ {x}]
then  {x} c= B by ZFMISC_1:31;
hence  S2[B \/ {x}] by A7, XBOOLE_1:12; ::_thesis: verum
end;
now__::_thesis:_(_not_x_in_B_implies_S2[B_\/_{x}]_)
assume A9: not x in B ; ::_thesis: S2[B \/ {x}]
defpred S3[ set , set ] means  ex Y being set st
( Y = A & c2 = Y \/ {x} );
A10: for y, y1, y2 being set st y in bool B & S3[y,y1] & S3[y,y2] holds
y1 = y2 ;
A11: for y being set st y in bool B holds
ex z being set st S3[y,z]
proof
let y be set ; ::_thesis: ( y in bool B implies ex z being set st S3[y,z] )
assume  y in bool B ; ::_thesis: ex z being set st S3[y,z]
 ex Y being set st
( Y = y & y \/ {x} = Y \/ {x} ) ;
hence  ex z being set st S3[y,z] ; ::_thesis: verum
end;
consider f being Function such that
A12: dom f = bool B and
A13: for y being set st y in bool B holds
S3[y,f . y] from FUNCT_1:sch_2(A10, A11);
A14: bool B is finite by A2, A7;
 for y being set holds
( y in rng f iff y in (bool (B \/ {x})) \ (bool B) )
proof
let y be set ; ::_thesis: ( y in rng f iff y in (bool (B \/ {x})) \ (bool B) )
thus  ( y in rng f implies y in (bool (B \/ {x})) \ (bool B) ) ::_thesis: ( y in (bool (B \/ {x})) \ (bool B) implies y in rng f )
proof
assume  y in rng f ; ::_thesis: y in (bool (B \/ {x})) \ (bool B)
then consider x1 being set  such that
A15: x1 in dom f and
A16: f . x1 = y by FUNCT_1:def_3;
consider X1 being set  such that
A17: X1 = x1 and
A18: f . x1 = X1 \/ {x} by A12, A13, A15;
A19: X1 \/ {x} c= B \/ {x} by A12, A15, A17, XBOOLE_1:13;
 x in {x} by TARSKI:def_1;
then  x in y by A16, A18, XBOOLE_0:def_3;
then  not y in bool B by A9;
hence  y in (bool (B \/ {x})) \ (bool B) by A16, A18, A19, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A20: y in (bool (B \/ {x})) \ (bool B) ; ::_thesis: y in rng f
set Z = y \ {x};
A21: now__::_thesis:_x_in_y
assume A22: not x in y ; ::_thesis: contradiction
 y c= B
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in y or z in B )
assume A23: z in y ; ::_thesis: z in B
then  not z in {x} by A22, TARSKI:def_1;
hence  z in B by A20, A23, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  contradiction by A20, XBOOLE_0:def_5; ::_thesis: verum
end;
A24: y \ {x} c= B by A20, XBOOLE_1:43;
then consider X being set  such that
A25: X = y \ {x} and
A26: f . (y \ {x}) = X \/ {x} by A13;
X \/ {x} = y \/ {x} by A25, XBOOLE_1:39
.= y by A21, ZFMISC_1:40 ;
hence  y in rng f by A12, A24, A26, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng f = (bool (B \/ {x})) \ (bool B) by TARSKI:1;
then A27: f .: (bool B) = (bool (B \/ {x})) \ (bool B) by A12, RELAT_1:113;
A28: bool B c= bool (B \/ {x}) by XBOOLE_1:7, ZFMISC_1:67;
A29: ((bool (B \/ {x})) \ (bool B)) \/ (bool B) = (bool (B \/ {x})) \/ (bool B) by XBOOLE_1:39
.= bool (B \/ {x}) by A28, XBOOLE_1:12 ;
A30: {x} c= A by A6, ZFMISC_1:31;
 B in bool A by A2, A7;
then  B \/ {x} c= A by A30, XBOOLE_1:8;
hence  S2[B \/ {x}] by A2, A14, A27, A29; ::_thesis: verum
end;
hence  S2[B \/ {x}] by A8; ::_thesis: verum
end;
 S2[A] from FINSET_1:sch_2(A1, A4, A5);
hence  bool A is finite by A2; ::_thesis: verum
end;
end;

theorem Th7: :: FINSET_1:7
for A being set holds
( ( A is finite & ( for X being set st X in A holds
X is finite ) ) iff union A is finite )
proof
let A be set ; ::_thesis: ( ( A is finite & ( for X being set st X in A holds
X is finite ) ) iff union A is finite )
thus  ( A is finite & ( for X being set st X in A holds
X is finite ) implies union A is finite ) by Lm3; ::_thesis: ( union A is finite implies ( A is finite & ( for X being set st X in A holds
X is finite ) ) )
thus  ( union A is finite implies ( A is finite & ( for X being set st X in A holds
X is finite ) ) ) ::_thesis: verum
proof
assume A1: union A is finite ; ::_thesis: ( A is finite & ( for X being set st X in A holds
X is finite ) )
 A c= bool (union A) by ZFMISC_1:82;
hence  A is finite by A1; ::_thesis: for X being set st X in A holds
X is finite
let X be set ; ::_thesis: ( X in A implies X is finite )
assume  X in A ; ::_thesis: X is finite
then  X c= union A by ZFMISC_1:74;
hence  X is finite by A1; ::_thesis: verum
end;
end;

theorem Th8: :: FINSET_1:8
for f being Function st dom f is finite holds
rng f is finite
proof
let f be Function; ::_thesis: ( dom f is finite implies rng f is finite )
assume  dom f is finite ; ::_thesis: rng f is finite
then  f .: (dom f) is finite ;
hence  rng f is finite by RELAT_1:113; ::_thesis: verum
end;

theorem :: FINSET_1:9
for Y being set
for f being Function st Y c= rng f & f " Y is finite holds
Y is finite
proof
let Y be set ; ::_thesis: for f being Function st Y c= rng f & f " Y is finite holds
Y is finite
let f be Function; ::_thesis: ( Y c= rng f & f " Y is finite implies Y is finite )
assume  Y c= rng f ; ::_thesis: ( not f " Y is finite or Y is finite )
then  f .: (f " Y) = Y by FUNCT_1:77;
hence  ( not f " Y is finite or Y is finite ) ; ::_thesis: verum
end;

registration
let X, Y be finite set ;
clusterX \+\ Y ->  finite ;
coherence
 X \+\ Y is finite ;
end;

registration
let X be non empty set ;
cluster non empty finite for Element of bool X;
existence
 ex b1 being Subset of X st
( b1 is finite & not b1 is empty )
proof
take  { the Element of X} ; ::_thesis: ( { the Element of X} is finite & not { the Element of X} is empty )
thus  ( { the Element of X} is finite & not { the Element of X} is empty ) ; ::_thesis: verum
end;
end;

begin

theorem Th10: :: FINSET_1:10
for f being Function holds
( dom f is finite iff f is finite )
proof
let f be Function; ::_thesis: ( dom f is finite iff f is finite )
thus  ( dom f is finite implies f is finite ) ::_thesis: ( f is finite implies dom f is finite )
proof
assume A1: dom f is finite ; ::_thesis: f is finite
then A2: rng f is finite by Th8;
 f c= [:(dom f),(rng f):] by RELAT_1:7;
hence  f is finite by A1, A2; ::_thesis: verum
end;
 (pr1 ((dom f),(rng f))) .: f = dom f by FUNCT_3:79;
hence  ( f is finite implies dom f is finite ) ; ::_thesis: verum
end;

theorem :: FINSET_1:11
for F being set st F is finite & F <> {} & F is c=-linear holds
ex m being set st
( m in F & ( for C being set st C in F holds
m c= C ) )
proof
defpred S1[ set ] means ( $1 <> {} implies ex m being set st
( m in $1 & ( for C being set st C in $1 holds
m c= C ) ) );
let F be set ; ::_thesis: ( F is finite & F <> {} & F is c=-linear implies ex m being set st
( m in F & ( for C being set st C in F holds
m c= C ) ) )
assume that
A1: F is finite and
A2: F <> {} and
A3: F is c=-linear ; ::_thesis: ex m being set st
( m in F & ( for C being set st C in F holds
m c= C ) )
A4: S1[ {} ] ;
A5: now__::_thesis:_for_x,_B_being_set_st_x_in_F_&_B_c=_F_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in F & B c= F & S1[B] implies S1[B \/ {x}] )
assume that
A6: x in F and
A7: B c= F and
A8: S1[B] ; ::_thesis: S1[B \/ {x}]
now__::_thesis:_(_B_\/_{x}_<>_{}_implies_ex_m_being_set_st_
(_m_in_B_\/_{x}_&_(_for_C_being_set_st_C_in_B_\/_{x}_holds_
m_c=_C_)_)_)
percases ( for y being set holds
( not y in B or not y c= x ) or ex y being set st
( y in B & y c= x ) ) ;
supposeA9: for y being set holds
( not y in B or not y c= x ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) ) )
assume  B \/ {x} <> {} ; ::_thesis: ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
take m = x; ::_thesis: ( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
 x in {x} by TARSKI:def_1;
hence  m in B \/ {x} by XBOOLE_0:def_3; ::_thesis: for C being set st C in B \/ {x} holds
m c= C
let C be set ; ::_thesis: ( C in B \/ {x} implies m c= C )
assume  C in B \/ {x} ; ::_thesis: m c= C
then A10: ( C in B or C in {x} ) by XBOOLE_0:def_3;
then  C,x are_c=-comparable by A3, A6, A7, ORDINAL1:def_8, TARSKI:def_1;
then  ( C c= x or x c= C ) by XBOOLE_0:def_9;
hence  m c= C by A9, A10, TARSKI:def_1; ::_thesis: verum
end;
suppose ex y being set st
( y in B & y c= x ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) ) )
then consider y being set  such that
A11: y in B and
A12: y c= x ;
assume  B \/ {x} <> {} ; ::_thesis: ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
consider m being set  such that
A13: m in B and
A14: for C being set st C in B holds
m c= C by A8, A11;
 m c= y by A11, A14;
then A15: m c= x by A12, XBOOLE_1:1;
take m = m; ::_thesis: ( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
m c= C ) )
thus  m in B \/ {x} by A13, XBOOLE_0:def_3; ::_thesis: for C being set st C in B \/ {x} holds
m c= C
let C be set ; ::_thesis: ( C in B \/ {x} implies m c= C )
assume  C in B \/ {x} ; ::_thesis: m c= C
then  ( C in B or C in {x} ) by XBOOLE_0:def_3;
hence  m c= C by A14, A15, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  S1[B \/ {x}] ; ::_thesis: verum
end;
 S1[F] from FINSET_1:sch_2(A1, A4, A5);
hence  ex m being set st
( m in F & ( for C being set st C in F holds
m c= C ) ) by A2; ::_thesis: verum
end;

theorem :: FINSET_1:12
for F being set st F is finite & F <> {} & F is c=-linear holds
ex m being set st
( m in F & ( for C being set st C in F holds
C c= m ) )
proof
defpred S1[ set ] means ( $1 <> {} implies ex m being set st
( m in $1 & ( for C being set st C in $1 holds
C c= m ) ) );
let F be set ; ::_thesis: ( F is finite & F <> {} & F is c=-linear implies ex m being set st
( m in F & ( for C being set st C in F holds
C c= m ) ) )
assume that
A1: F is finite and
A2: F <> {} and
A3: F is c=-linear ; ::_thesis: ex m being set st
( m in F & ( for C being set st C in F holds
C c= m ) )
A4: S1[ {} ] ;
A5: now__::_thesis:_for_x,_B_being_set_st_x_in_F_&_B_c=_F_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in F & B c= F & S1[B] implies S1[B \/ {x}] )
assume that
A6: x in F and
A7: B c= F and
A8: S1[B] ; ::_thesis: S1[B \/ {x}]
now__::_thesis:_(_B_\/_{x}_<>_{}_implies_ex_m_being_set_st_
(_m_in_B_\/_{x}_&_(_for_C_being_set_st_C_in_B_\/_{x}_holds_
C_c=_m_)_)_)
percases ( for y being set holds
( not y in B or not x c= y ) or ex y being set st
( y in B & x c= y ) ) ;
supposeA9: for y being set holds
( not y in B or not x c= y ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) ) )
assume  B \/ {x} <> {} ; ::_thesis: ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) )
take m = x; ::_thesis: ( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) )
 x in {x} by TARSKI:def_1;
hence  m in B \/ {x} by XBOOLE_0:def_3; ::_thesis: for C being set st C in B \/ {x} holds
C c= m
let C be set ; ::_thesis: ( C in B \/ {x} implies C c= m )
assume  C in B \/ {x} ; ::_thesis: C c= m
then A10: ( C in B or C in {x} ) by XBOOLE_0:def_3;
then  C,x are_c=-comparable by A3, A6, A7, ORDINAL1:def_8, TARSKI:def_1;
then  ( C c= x or x c= C ) by XBOOLE_0:def_9;
hence  C c= m by A9, A10, TARSKI:def_1; ::_thesis: verum
end;
suppose ex y being set st
( y in B & x c= y ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) ) )
then consider y being set  such that
A11: y in B and
A12: x c= y ;
assume  B \/ {x} <> {} ; ::_thesis: ex m being set st
( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) )
consider m being set  such that
A13: m in B and
A14: for C being set st C in B holds
C c= m by A8, A11;
 y c= m by A11, A14;
then A15: x c= m by A12, XBOOLE_1:1;
take m = m; ::_thesis: ( m in B \/ {x} & ( for C being set st C in B \/ {x} holds
C c= m ) )
thus  m in B \/ {x} by A13, XBOOLE_0:def_3; ::_thesis: for C being set st C in B \/ {x} holds
C c= m
let C be set ; ::_thesis: ( C in B \/ {x} implies C c= m )
assume  C in B \/ {x} ; ::_thesis: C c= m
then  ( C in B or C in {x} ) by XBOOLE_0:def_3;
hence  C c= m by A14, A15, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  S1[B \/ {x}] ; ::_thesis: verum
end;
 S1[F] from FINSET_1:sch_2(A1, A4, A5);
hence  ex m being set st
( m in F & ( for C being set st C in F holds
C c= m ) ) by A2; ::_thesis: verum
end;

definition
let R be Relation;
attrR is finite-yielding  means :Def2: :: FINSET_1:def 2
 for x being set st x in rng R holds
x is finite ;
end;

:: deftheorem Def2 defines finite-yielding FINSET_1:def_2_:_
 for R being Relation holds
( R is finite-yielding iff for x being set st x in rng R holds
x is finite );

 deffunc H1( set ) ->  set = $1 `1 ;

theorem :: FINSET_1:13
for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds
ex A, B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
proof
let X, Y, Z be set ; ::_thesis: ( X is finite & X c= [:Y,Z:] implies ex A, B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] ) )
deffunc H2( set ) ->  set = $1 `2 ;
assume that
A1: X is finite and
A2: X c= [:Y,Z:] ; ::_thesis: ex A, B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
consider f being Function such that
A3: dom f = X and
A4: for a being set st a in X holds
f . a = H1(a) from FUNCT_1:sch_3();
consider g being Function such that
A5: dom g = X and
A6: for a being set st a in X holds
g . a = H2(a) from FUNCT_1:sch_3();
take A = rng f; ::_thesis: ex B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
take B = rng g; ::_thesis: ( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
thus  A is finite by A1, A3, Th8; ::_thesis: ( A c= Y & B is finite & B c= Z & X c= [:A,B:] )
thus  A c= Y ::_thesis: ( B is finite & B c= Z & X c= [:A,B:] )
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in Y )
assume  a in A ; ::_thesis: a in Y
then consider x being set  such that
A7: x in dom f and
A8: f . x = a by FUNCT_1:def_3;
consider y, z being set  such that
A9: y in Y and
 z in Z and
A10: x = [y,z] by A2, A3, A7, ZFMISC_1:def_2;
f . x = x `1 by A3, A4, A7
.= y by A10, MCART_1:7 ;
hence  a in Y by A8, A9; ::_thesis: verum
end;
thus  B is finite by A1, A5, Th8; ::_thesis: ( B c= Z & X c= [:A,B:] )
thus  B c= Z ::_thesis: X c= [:A,B:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in Z )
assume  a in B ; ::_thesis: a in Z
then consider x being set  such that
A11: x in dom g and
A12: g . x = a by FUNCT_1:def_3;
consider y, z being set  such that
 y in Y and
A13: z in Z and
A14: x = [y,z] by A2, A5, A11, ZFMISC_1:def_2;
g . x = x `2 by A5, A6, A11
.= z by A14, MCART_1:7 ;
hence  a in Z by A12, A13; ::_thesis: verum
end;
thus  X c= [:A,B:] ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in [:A,B:] )
assume A15: a in X ; ::_thesis: a in [:A,B:]
then consider x, y being set  such that
 x in Y and
 y in Z and
A16: a = [x,y] by A2, ZFMISC_1:def_2;
A17: g . a = a `2 by A6, A15
.= y by A16, MCART_1:7 ;
f . a = a `1 by A4, A15
.= x by A16, MCART_1:7 ;
then A18: x in A by A3, A15, FUNCT_1:def_3;
 y in B by A5, A15, A17, FUNCT_1:def_3;
hence  a in [:A,B:] by A16, A18, ZFMISC_1:87; ::_thesis: verum
end;
end;

theorem :: FINSET_1:14
for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds
ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] )
proof
let X, Y, Z be set ; ::_thesis: ( X is finite & X c= [:Y,Z:] implies ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] ) )
assume that
A1: X is finite and
A2: X c= [:Y,Z:] ; ::_thesis: ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] )
consider f being Function such that
A3: dom f = X and
A4: for a being set st a in X holds
f . a = H1(a) from FUNCT_1:sch_3();
take A = rng f; ::_thesis: ( A is finite & A c= Y & X c= [:A,Z:] )
thus  A is finite by A1, A3, Th8; ::_thesis: ( A c= Y & X c= [:A,Z:] )
thus  A c= Y ::_thesis: X c= [:A,Z:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in Y )
assume  a in A ; ::_thesis: a in Y
then consider x being set  such that
A5: x in dom f and
A6: f . x = a by FUNCT_1:def_3;
consider y, z being set  such that
A7: y in Y and
 z in Z and
A8: x = [y,z] by A2, A3, A5, ZFMISC_1:def_2;
f . x = x `1 by A3, A4, A5
.= y by A8, MCART_1:7 ;
hence  a in Y by A6, A7; ::_thesis: verum
end;
thus  X c= [:A,Z:] ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in [:A,Z:] )
assume A9: a in X ; ::_thesis: a in [:A,Z:]
then consider x, y being set  such that
 x in Y and
A10: y in Z and
A11: a = [x,y] by A2, ZFMISC_1:def_2;
f . a = a `1 by A4, A9
.= x by A11, MCART_1:7 ;
then  x in A by A3, A9, FUNCT_1:def_3;
hence  a in [:A,Z:] by A10, A11, ZFMISC_1:87; ::_thesis: verum
end;
end;

registration
cluster non empty Relation-like Function-like finite for set ;
existence
 ex b1 being Function st
( b1 is finite & not b1 is empty )
proof
 {[{},{}]} is Function ;
hence  ex b1 being Function st
( b1 is finite & not b1 is empty ) ; ::_thesis: verum
end;
end;

registration
let R be finite Relation;
cluster proj1 R ->  finite ;
coherence
 dom R is finite
proof
consider f being Function such that
A1: dom f = R and
A2: for x being set st x in R holds
f . x = x `1 from FUNCT_1:sch_3();
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_rng_f_implies_ex_y_being_set_st_[x,y]_in_R_)_&_(_ex_y_being_set_st_[x,y]_in_R_implies_x_in_rng_f_)_)
let x be set ; ::_thesis: ( ( x in rng f implies ex y being set st [x,y] in R ) & ( ex y being set st [x,y] in R implies x in rng f ) )
thus  ( x in rng f implies ex y being set st [x,y] in R ) ::_thesis: ( ex y being set st [x,y] in R implies x in rng f )
proof
assume  x in rng f ; ::_thesis: ex y being set st [x,y] in R
then consider a being set  such that
A3: a in dom f and
A4: f . a = x by FUNCT_1:def_3;
take  a `2 ; ::_thesis: [x,(a `2)] in R
A5: ex x, y being set st a = [x,y] by A1, A3, RELAT_1:def_1;
 x = a `1 by A1, A2, A3, A4;
hence  [x,(a `2)] in R by A1, A3, A5, MCART_1:8; ::_thesis: verum
end;
given y being set  such that A6: [x,y] in R ; ::_thesis: x in rng f
f . [x,y] = [x,y] `1 by A2, A6
.= x ;
hence  x in rng f by A1, A6, FUNCT_1:3; ::_thesis: verum
end;
then  rng f = dom R by XTUPLE_0:def_12;
hence  dom R is finite by A1, Th8; ::_thesis: verum
end;
end;

registration
let f be Function;
let g be finite Function;
clusterg * f ->  finite ;
coherence
 f * g is finite
proof
 dom (f * g) c= dom g by RELAT_1:25;
hence  f * g is finite by Th10; ::_thesis: verum
end;
end;

registration
let A be finite set ;
let B be set ;
cluster Function-like V18(A,B)  ->  finite for Element of bool [:A,B:];
coherence
 for b1 being Function of A,B holds b1 is finite
proof
let f be Function of A,B; ::_thesis: f is finite
 dom f is finite ;
hence  f is finite by Th10; ::_thesis: verum
end;
end;

registration
let x, y be set ;
clusterx .--> y ->  finite ;
coherence
 x .--> y is finite ;
end;

registration
let R be finite Relation;
cluster proj2 R ->  finite ;
coherence
 rng R is finite
proof
consider f being Function such that
A1: dom f = R and
A2: for x being set st x in R holds
f . x = x `2 from FUNCT_1:sch_3();
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_f_implies_ex_x_being_set_st_[x,y]_in_R_)_&_(_ex_x_being_set_st_[x,y]_in_R_implies_y_in_rng_f_)_)
let y be set ; ::_thesis: ( ( y in rng f implies ex x being set st [x,y] in R ) & ( ex x being set st [x,y] in R implies y in rng f ) )
thus  ( y in rng f implies ex x being set st [x,y] in R ) ::_thesis: ( ex x being set st [x,y] in R implies y in rng f )
proof
assume  y in rng f ; ::_thesis: ex x being set st [x,y] in R
then consider a being set  such that
A3: a in dom f and
A4: f . a = y by FUNCT_1:def_3;
take  a `1 ; ::_thesis: [(a `1),y] in R
A5: ex x, y being set st a = [x,y] by A1, A3, RELAT_1:def_1;
 y = a `2 by A1, A2, A3, A4;
hence  [(a `1),y] in R by A1, A3, A5, MCART_1:8; ::_thesis: verum
end;
given x being set  such that A6: [x,y] in R ; ::_thesis: y in rng f
f . [x,y] = [x,y] `2 by A2, A6
.= y ;
hence  y in rng f by A1, A6, FUNCT_1:3; ::_thesis: verum
end;
then  rng f = rng R by XTUPLE_0:def_13;
hence  rng R is finite by A1, Th8; ::_thesis: verum
end;
end;

registration
let f be finite Function;
let x be set ;
clusterf " x ->  finite ;
coherence
 f " x is finite
proof
 f " x c= dom f by RELAT_1:132;
hence  f " x is finite ; ::_thesis: verum
end;
end;

registration
let f, g be finite Function;
clusterf +* g ->  finite ;
coherence
 f +* g is finite
proof
 dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
hence  f +* g is finite by Th10; ::_thesis: verum
end;
end;

definition
let F be set ;
attrF is centered  means :: FINSET_1:def 3
( F <> {} & ( for G being set st G <> {} & G c= F & G is finite holds
meet G <> {} ) );
end;

:: deftheorem  defines centered FINSET_1:def_3_:_
 for F being set holds
( F is centered iff ( F <> {} & ( for G being set st G <> {} & G c= F & G is finite holds
meet G <> {} ) ) );

definition
let f be Function;
redefine attr f is finite-yielding  means :Def4: :: FINSET_1:def 4
 for i being set st i in dom f holds
f . i is finite ;
compatibility
 ( f is finite-yielding iff for i being set st i in dom f holds
f . i is finite )
proof
hereby  ::_thesis: ( ( for i being set st i in dom f holds
f . i is finite ) implies f is finite-yielding )
assume A1: f is finite-yielding ; ::_thesis: for i being set st i in dom f holds
f . b2 is finite
let i be set ; ::_thesis: ( i in dom f implies f . b1 is finite )
assume  i in dom f ; ::_thesis: f . b1 is finite
percases ( i in dom f or not i in dom f ) ;
suppose i in dom f ; ::_thesis: f . b1 is finite
then  f . i in rng f by FUNCT_1:3;
hence  f . i is finite by A1, Def2; ::_thesis: verum
end;
suppose not i in dom f ; ::_thesis: f . b1 is finite
hence  f . i is finite by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for i being set st i in dom f holds
f . i is finite ; ::_thesis: f is finite-yielding
let i be set ; :: according to FINSET_1:def_2 ::_thesis: ( i in rng f implies i is finite )
assume  i in rng f ; ::_thesis: i is finite
then  ex x being set st
( x in dom f & i = f . x ) by FUNCT_1:def_3;
hence  i is finite by A2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines finite-yielding FINSET_1:def_4_:_
 for f being Function holds
( f is finite-yielding iff for i being set st i in dom f holds
f . i is finite );

definition
let I be set ;
let IT be I -defined Function;
:: original: finite-yielding
redefine attrIT is finite-yielding  means :: FINSET_1:def 5
 for i being set st i in I holds
IT . i is finite ;
compatibility
 ( IT is finite-yielding iff for i being set st i in I holds
IT . i is finite )
proof
hereby  ::_thesis: ( ( for i being set st i in I holds
IT . i is finite ) implies IT is finite-yielding )
assume A1: IT is finite-yielding ; ::_thesis: for i being set st i in I holds
IT . b2 is finite
let i be set ; ::_thesis: ( i in I implies IT . b1 is finite )
assume  i in I ; ::_thesis: IT . b1 is finite
percases ( i in dom IT or not i in dom IT ) ;
suppose i in dom IT ; ::_thesis: IT . b1 is finite
hence  IT . i is finite by A1, Def4; ::_thesis: verum
end;
suppose not i in dom IT ; ::_thesis: IT . b1 is finite
hence  IT . i is finite by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for i being set st i in I holds
IT . i is finite ; ::_thesis: IT is finite-yielding
let i be set ; :: according to FINSET_1:def_4 ::_thesis: ( i in dom IT implies IT . i is finite )
 dom IT c= I ;
hence  ( i in dom IT implies IT . i is finite ) by A2; ::_thesis: verum
end;
end;

:: deftheorem  defines finite-yielding FINSET_1:def_5_:_
 for I being set
for IT being b1 -defined Function holds
( IT is finite-yielding iff for i being set st i in I holds
IT . i is finite );

theorem :: FINSET_1:15
for B, A being set st B is infinite holds
not B in [:A,B:]
proof
let B, A be set ; ::_thesis: ( B is infinite implies not B in [:A,B:] )
assume that
A1: B is infinite and
A2: B in [:A,B:] ; ::_thesis: contradiction
 ex x being set st
( x in A & B = [x,{x}] ) by A2, ZFMISC_1:129;
hence  contradiction by A1; ::_thesis: verum
end;

registration
let I be set ;
let f be I -defined Function;
cluster Relation-like I -defined Function-like f -compatible finite for set ;
existence
 ex b1 being Function st
( b1 is finite & b1 is I -defined & b1 is f -compatible )
proof
take  {} ; ::_thesis: ( {} is finite & {} is I -defined & {} is f -compatible )
thus  ( {} is finite & {} is I -defined & {} is f -compatible ) by FUNCT_1:104, RELAT_1:171; ::_thesis: verum
end;
end;

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like finite for set ;
existence
 ex b1 being Function st
( b1 is finite & b1 is X -defined & b1 is Y -valued )
proof
take  {} ; ::_thesis: ( {} is finite & {} is X -defined & {} is Y -valued )
thus  ( {} is finite & {} is X -defined & {} is Y -valued ) by RELAT_1:171; ::_thesis: verum
end;
end;

registration
let X, Y be non empty set ;
cluster non empty Relation-like X -defined Y -valued Function-like finite for set ;
existence
 ex b1 being Function st
( b1 is X -defined & b1 is Y -valued & not b1 is empty & b1 is finite )
proof
set x = the Element of X;
set y = the Element of Y;
take F = the Element of X .--> the Element of Y; ::_thesis: ( F is X -defined & F is Y -valued & not F is empty & F is finite )
thus  F is X -defined ; ::_thesis: ( F is Y -valued & not F is empty & F is finite )
thus  F is Y -valued ; ::_thesis: ( not F is empty & F is finite )
thus  ( not F is empty & F is finite ) ; ::_thesis: verum
end;
end;

registration
let A be set ;
let F be finite Relation;
clusterA |` F ->  finite ;
coherence
 A |` F is finite
proof
 A |` F c= F by RELAT_1:86;
hence  A |` F is finite ; ::_thesis: verum
end;
end;

registration
let A be set ;
let F be finite Relation;
clusterF | A ->  finite ;
coherence
 F | A is finite
proof
 F | A c= F by RELAT_1:59;
hence  F | A is finite ; ::_thesis: verum
end;
end;

registration
let A be finite set ;
let F be Function;
clusterF | A ->  finite ;
coherence
 F | A is finite
proof
 dom (F | A) c= A by RELAT_1:58;
hence  F | A is finite by Th10; ::_thesis: verum
end;
end;

registration
let R be finite Relation;
cluster field R ->  finite ;
coherence
 field R is finite ;
end;

registration
cluster trivial  ->  finite for set ;
coherence
 for b1 being set st b1 is trivial holds
b1 is finite
proof
let S be set ; ::_thesis: ( S is trivial implies S is finite )
assume A1: S is trivial ; ::_thesis: S is finite
percases ( S is empty or ex x being set st S = {x} ) by A1, ZFMISC_1:131;
suppose S is empty ; ::_thesis: S is finite
hence  S is finite ; ::_thesis: verum
end;
suppose ex x being set st S = {x} ; ::_thesis: S is finite
hence  S is finite ; ::_thesis: verum
end;
end;
end;
end;

registration
cluster infinite  ->  non trivial for set ;
coherence
 for b1 being set st b1 is infinite holds
not b1 is trivial ;
end;

registration
let X be non trivial set ;
cluster non trivial finite for Element of bool X;
existence
 ex b1 being Subset of X st
( b1 is finite & not b1 is trivial )
proof
consider a1, a2 being set  such that
A1: ( a1 in X & a2 in X & a1 <> a2 ) by ZFMISC_1:def_10;
reconsider A = {a1,a2} as Subset of X by A1, ZFMISC_1:32;
take  A ; ::_thesis: ( A is finite & not A is trivial )
thus  A is finite ; ::_thesis: not A is trivial
 ( a1 in A & a2 in A ) by TARSKI:def_2;
hence  not A is trivial by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
end;

registration
let x, y, a, b be set ;
cluster(x,y) --> (a,b) ->  finite ;
coherence
 (x,y) --> (a,b) is finite ;
end;

definition
let A be set ;
attrA is finite-membered  means :Def6: :: FINSET_1:def 6
 for B being set st B in A holds
B is finite ;
end;

:: deftheorem Def6 defines finite-membered FINSET_1:def_6_:_
 for A being set holds
( A is finite-membered iff for B being set st B in A holds
B is finite );

registration
cluster empty  ->  finite-membered for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is finite-membered
proof
let A be set ; ::_thesis: ( A is empty implies A is finite-membered )
assume A1: A is empty ; ::_thesis: A is finite-membered
let B be set ; :: according to FINSET_1:def_6 ::_thesis: ( B in A implies B is finite )
thus  ( B in A implies B is finite ) by A1; ::_thesis: verum
end;
end;

registration
let A be finite-membered set ;
cluster  ->  finite for Element of A;
coherence
 for b1 being Element of A holds b1 is finite
proof
let B be Element of A; ::_thesis: B is finite
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: B is finite
hence  B is finite by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: B is finite
hence  B is finite by Def6; ::_thesis: verum
end;
end;
end;
end;

registration
cluster non empty finite finite-membered for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is finite & b1 is finite-membered )
proof
take x = {{{}}}; ::_thesis: ( not x is empty & x is finite & x is finite-membered )
thus  ( not x is empty & x is finite ) ; ::_thesis: x is finite-membered
let y be set ; :: according to FINSET_1:def_6 ::_thesis: ( y in x implies y is finite )
thus  ( y in x implies y is finite ) by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let X be finite set ;
cluster{X} ->  finite-membered ;
coherence
 {X} is finite-membered
proof
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( x in {X} implies x is finite )
thus  ( x in {X} implies x is finite ) by TARSKI:def_1; ::_thesis: verum
end;
cluster bool X ->  finite-membered ;
coherence
 bool X is finite-membered
proof
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( x in bool X implies x is finite )
thus  ( x in bool X implies x is finite ) ; ::_thesis: verum
end;
let Y be finite set ;
cluster{X,Y} ->  finite-membered ;
coherence
 {X,Y} is finite-membered
proof
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( x in {X,Y} implies x is finite )
thus  ( x in {X,Y} implies x is finite ) by TARSKI:def_2; ::_thesis: verum
end;
end;

registration
let X be finite-membered set ;
cluster  ->  finite-membered for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is finite-membered
proof
let S be Subset of X; ::_thesis: S is finite-membered
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( x in S implies x is finite )
thus  ( x in S implies x is finite ) ; ::_thesis: verum
end;
let Y be finite-membered set ;
clusterX \/ Y ->  finite-membered ;
coherence
 X \/ Y is finite-membered
proof
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( x in X \/ Y implies x is finite )
assume  x in X \/ Y ; ::_thesis: x is finite
then  ( x in X or x in Y ) by XBOOLE_0:def_3;
hence  x is finite ; ::_thesis: verum
end;
end;

registration
let X be finite finite-membered set ;
cluster union X ->  finite ;
coherence
 union X is finite
proof
 for x being set st x in X holds
x is finite ;
hence  union X is finite by Th7; ::_thesis: verum
end;
end;

registration
cluster non empty Relation-like Function-like finite-yielding for set ;
existence
 ex b1 being Function st
( not b1 is empty & b1 is finite-yielding )
proof
take F = {{}} .--> {{}}; ::_thesis: ( not F is empty & F is finite-yielding )
thus  not F is empty ; ::_thesis: F is finite-yielding
let x be set ; :: according to FINSET_1:def_5 ::_thesis: ( x in {{{}}} implies F . x is finite )
assume  x in {{{}}} ; ::_thesis: F . x is finite
then  x = {{}} by TARSKI:def_1;
hence  F . x is finite by FUNCOP_1:72; ::_thesis: verum
end;
cluster empty Relation-like  ->  finite-yielding for set ;
coherence
 for b1 being Relation st b1 is empty holds
b1 is finite-yielding
proof
let F be Relation; ::_thesis: ( F is empty implies F is finite-yielding )
assume A1: F is empty ; ::_thesis: F is finite-yielding
let x be set ; :: according to FINSET_1:def_2 ::_thesis: ( x in rng F implies x is finite )
thus  ( x in rng F implies x is finite ) by A1; ::_thesis: verum
end;
end;

registration
let F be finite-yielding Function;
let x be set ;
clusterF . x ->  finite ;
coherence
 F . x is finite
proof
percases ( x in dom F or not x in dom F ) ;
suppose x in dom F ; ::_thesis: F . x is finite
hence  F . x is finite by Def4; ::_thesis: verum
end;
suppose not x in dom F ; ::_thesis: F . x is finite
hence  F . x is finite by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
end;

registration
let F be finite-yielding Relation;
cluster proj2 F ->  finite-membered ;
coherence
 rng F is finite-membered
proof
let e be set ; :: according to FINSET_1:def_6 ::_thesis: ( e in rng F implies e is finite )
thus  ( e in rng F implies e is finite ) by Def2; ::_thesis: verum
end;
end;