let SD be Subset-Family of D; :: thesis: ( SD = Fin D implies SD is with_countable_Cover )
assume SD = Fin D ; :: thesis: SD is with_countable_Cover
then A1: SD = { y where y is Subset of D : y is finite } by FinConv;
defpred S₁[ object ] means ( D in SD & ex x being set st
( x in D & D = {x} ) );
consider XX being set such that
A2: for y being object holds
( y in XX iff ( y in bool D & S₁[y] ) ) from XBOOLE_0:sch 1();
for x being object st x in XX holds
x in SD by A2;
then A3: XX is Subset of SD by TARSKI:def 3;
A4: for x being object holds
( x in union XX iff x in D )

proof

let x be object ; :: thesis: ( x in union XX iff x in D )
thus ( x in union XX implies x in D ) :: thesis: ( x in D implies x in union XX )

proof

assume A5: x in union XX ; :: thesis: x in D
consider U being set such that
A6: ( x in U & U in XX ) by A5, TARSKI:def 4;
consider y0 being set such that
A7: ( y0 in D & U = {y0} ) by A2, A6;
thus x in D by A6, A7, TARSKI:def 1; :: thesis: verum

end;

thus ( x in D implies x in union XX ) :: thesis: verum

proof

assume A8: x in D ; :: thesis: x in union XX
then A9: {x} is Subset of D by SUBSET_1:41;
A10: {x} in SD by A1, A9;
set y = {x};
( x in {x} & {x} in XX ) by A2, A8, A10, TARSKI:def 1;
hence x in union XX by TARSKI:def 4; :: thesis: verum

end;

end;

A11: union XX = D by A4, TARSKI:2;
XX is countable

proof

D,XX are_equipotent

proof

defpred S₂[ object ] means ex x being set st
( x in D & D = [x,{x}] );
consider Z being set such that
A12: for z being object holds
( z in Z iff ( z in [:D,(bool D):] & S₂[z] ) ) from XBOOLE_0:sch 1();
( ( for c being object st c in D holds
ex xx being object st
( xx in XX & [c,xx] in Z ) ) & ( for xx being object st xx in XX holds
ex c being object st
( c in D & [c,xx] in Z ) ) & ( for w1, w2, w3, w4 being object st [w1,w2] in Z & [w3,w4] in Z holds
( w1 = w3 iff w2 = w4 ) ) )

proof

A13: for c being object st c in D holds
ex xx being object st
( xx in XX & [c,xx] in Z )

proof

let c be object ; :: thesis: ( c in D implies ex xx being object st
( xx in XX & [c,xx] in Z ) )
assume A14: c in D ; :: thesis: ex xx being object st
( xx in XX & [c,xx] in Z )
set xx0 = {c};
take {c} ; :: thesis: ( {c} in XX & [c,{c}] in Z )
( [c,{c}] in [:D,(bool D):] & {c} in XX & [c,{c}] in Z )

proof

A15: {c} is Subset of D by A14, SUBSET_1:33;
A16: {c} in SD by A1, A15;
A17: {c} c= D by A14, ZFMISC_1:31;
[c,{c}] in [:D,(bool D):] by A14, A17, ZFMISC_1:def 2;
hence ( [c,{c}] in [:D,(bool D):] & {c} in XX & [c,{c}] in Z ) by A2, A12, A14, A16; :: thesis: verum

end;

hence ( {c} in XX & [c,{c}] in Z ) ; :: thesis: verum

end;

A19: for xx being object st xx in XX holds
ex c being object st
( c in D & [c,xx] in Z )

proof

let xx be object ; :: thesis: ( xx in XX implies ex c being object st
( c in D & [c,xx] in Z ) )
assume A20: xx in XX ; :: thesis: ex c being object st
( c in D & [c,xx] in Z )
consider c0 being set such that
A21: ( c0 in D & xx = {c0} ) by A2, A20;
take c0 ; :: thesis: ( c0 in D & [c0,xx] in Z )
( [c0,xx] in [:D,(bool D):] & [c0,xx] in Z )

proof

[c0,{c0}] in [:D,(bool D):]

proof

{c0} is Subset of D by A21, SUBSET_1:41;
hence [c0,{c0}] in [:D,(bool D):] by A21, ZFMISC_1:def 2; :: thesis: verum

end;

hence ( [c0,xx] in [:D,(bool D):] & [c0,xx] in Z ) by A12, A21; :: thesis: verum

end;

hence ( c0 in D & [c0,xx] in Z ) by A21; :: thesis: verum

end;

for w1, w2, w3, w4 being object st [w1,w2] in Z & [w3,w4] in Z holds
( w1 = w3 iff w2 = w4 )

proof

let w1, w2, w3, w4 be object ; :: thesis: ( [w1,w2] in Z & [w3,w4] in Z implies ( w1 = w3 iff w2 = w4 ) )
assume A23: [w1,w2] in Z ; :: thesis: ( not [w3,w4] in Z or ( w1 = w3 iff w2 = w4 ) )
assume A24: [w3,w4] in Z ; :: thesis: ( w1 = w3 iff w2 = w4 )
thus ( w1 = w3 implies w2 = w4 ) :: thesis: ( w2 = w4 implies w1 = w3 )

proof

assume A25: w1 = w3 ; :: thesis: w2 = w4
A26: ( [w1,w2] in [:D,(bool D):] & ex x0 being set st
( x0 in D & [w1,w2] = [x0,{x0}] ) ) by A12, A23;
consider x0 being set such that
A27: ( x0 in D & [w1,w2] = [x0,{x0}] ) by A12, A23;
A28: ( w1 = x0 & w2 = {x0} ) by A26, A27, Lemme4;
A29: ( [w1,w4] in [:D,(bool D):] & ex y0 being set st
( y0 in D & [w1,w4] = [y0,{y0}] ) ) by A12, A24, A25;
consider y0 being set such that
A30: ( y0 in D & [w1,w4] = [y0,{y0}] ) by A12, A24, A25;
A31: ( w1 = y0 & w4 = {y0} ) by A29, A30, Lemme4;
thus w2 = w4 by A28, A31; :: thesis: verum

end;

thus ( w2 = w4 implies w1 = w3 ) :: thesis: verum

proof

assume A32: w2 = w4 ; :: thesis: w1 = w3
A33: ( [w1,w2] in [:D,(bool D):] & ex x0 being set st
( x0 in D & [w1,w2] = [x0,{x0}] ) ) by A12, A23;
consider x0 being set such that
A34: ( x0 in D & [w1,w2] = [x0,{x0}] ) by A12, A23;
A35: ( w1 = x0 & w2 = {x0} ) by A33, A34, Lemme4;
A36: ( [w3,w2] in [:D,(bool D):] & ex y0 being set st
( y0 in D & [w3,w2] = [y0,{y0}] ) ) by A12, A24, A32;
consider y0 being set such that
A37: ( y0 in D & [w3,w2] = [y0,{y0}] ) by A12, A24, A32;
( w3 = y0 & w2 = {y0} ) by A36, A37, Lemme4;
hence w1 = w3 by A35, ZFMISC_1:3; :: thesis: verum

end;

end;

hence ( ( for c being object st c in D holds
ex xx being object st
( xx in XX & [c,xx] in Z ) ) & ( for xx being object st xx in XX holds
ex c being object st
( c in D & [c,xx] in Z ) ) & ( for w1, w2, w3, w4 being object st [w1,w2] in Z & [w3,w4] in Z holds
( w1 = w3 iff w2 = w4 ) ) ) by A13, A19; :: thesis: verum

end;

hence D,XX are_equipotent ; :: thesis: verum

end;

hence XX is countable by YELLOW_8:4; :: thesis: verum

end;

hence SD is with_countable_Cover by A3, A11, Lem6a, SRINGS_1:def 4; :: thesis: verum