let X1, X2 be non empty set ; :: thesis:
let S1 be with_countable_Cover Subset-Family of X1; :: thesis:
let S2 be with_countable_Cover Subset-Family of X2; :: thesis:
let S be Subset-Family of [:X1,X2:]; :: thesis:
assume A1: S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ; :: thesis:
ex U being countable Subset of S st
( union U = [:X1,X2:] & U is Subset of S )

consider U1 being countable Subset of S1 such that
A2: U1 is Cover of X1 by SRINGS_1:def 4;
A3: union U1 = X1 by A2, Lem6a;
consider U2 being countable Subset of S2 such that
A4: U2 is Cover of X2 by SRINGS_1:def 4;
A5: union U2 = X2 by A4, Lem6a;
set U = { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } ;
A6: not U1 is empty by A2, ZFMISC_1:2, Lem6a;
A7: not U1 \ {{}} is empty

assume U1 \ {{}} is empty ; :: thesis:
then union U1 c= union {{}} by ZFMISC_1:77, XBOOLE_1:37;
hence contradiction by A2, Lem6a; :: thesis:

end;

A8: not U2 is empty by A4, Lem6a, ZFMISC_1:2;
A9: not U2 \ {{}} is empty

proof

assume U2 \ {{}} is empty ; :: thesis:
then union U2 c= union {{}} by ZFMISC_1:77, XBOOLE_1:37;
hence contradiction by A4, Lem6a; :: thesis:

end;

set V = { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ;
A10: { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } = { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) }

proof

( U1 is Subset-Family of X1 & U2 is Subset-Family of X2 ) by Lem9;
hence { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } = { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } by A6, A8, Lemme9; :: thesis:

end;

{ u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } is Subset of S

proof

for x being object st x in { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } holds
x in S

proof

let x be object ; :: thesis:
assume x in { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } ; :: thesis:
then consider u0 being Subset of [:X1,X2:] such that
A11: ( x = u0 & ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u0 = [:u1,u2:] ) ) ;
reconsider x = x as Subset of [:X1,X2:] by A11;
thus x in S by A1, A11; :: thesis:

end;

hence { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } is Subset of S by TARSKI:def 3; :: thesis:

end;

then reconsider U = { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } as Subset of S ;
A12: U is countable

proof

( U1 \ {{}} is countable & U2 \ {{}} is countable ) by CARD_3:95;
then A13: [:(U1 \ {{}}),(U2 \ {{}}):] is countable by CARD_4:7;
set W = [:(U1 \ {{}}),(U2 \ {{}}):];
{ [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ,[:(U1 \ {{}}),(U2 \ {{}}):] are_equipotent

proof

set Z = { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ;
A14: ( ( for v being object st v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for w being object st w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for v1, v2, w1, w2 being object st [v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } & [v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
( v1 = v2 iff w1 = w2 ) ) )

proof

A15: for v being object st v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )

proof

let v be object ; :: thesis:
assume v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ; :: thesis:
then consider u1 being Element of U1 such that
A16: ex u2 being Element of U2 st
( v = [:u1,u2:] & u1 in U1 \ {{}} & u2 in U2 \ {{}} ) ;
consider u2 being Element of U2 such that
A17: ( v = [:u1,u2:] & u1 in U1 \ {{}} & u2 in U2 \ {{}} ) by A16;
set w = [u1,u2];
take [u1,u2] ; :: thesis:
thus ( [u1,u2] in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,[u1,u2]] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) by A17, ZFMISC_1:def 2; :: thesis:

end;

A18: for w being object st w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )

proof

let w be object ; :: thesis:
assume w in [:(U1 \ {{}}),(U2 \ {{}}):] ; :: thesis:
then ex u1, u2 being object st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & w = [u1,u2] ) by ZFMISC_1:def 2;
then consider u1, u2 being set such that
A19: ( w = [u1,u2] & u1 in U1 \ {{}} & u2 in U2 \ {{}} ) ;
set v = [:u1,u2:];
take [:u1,u2:] ; :: thesis:
( u1 is Element of U1 & u2 is Element of U2 ) by A19, XBOOLE_1:36, TARSKI:def 3;
hence ( [:u1,u2:] in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [[:u1,u2:],w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) by A19; :: thesis:

end;

for v1, v2, w1, w2 being object st [v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } & [v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
( v1 = v2 iff w1 = w2 )

proof

let v1, v2, w1, w2 be object ; :: thesis:
assume [v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ; :: thesis:
then consider a1 being Element of U1, a2 being Element of U2 such that
A21: ( [v1,w1] = [[:a1,a2:],[a1,a2]] & a1 in U1 \ {{}} & a2 in U2 \ {{}} ) ;
A22: ( v1 = [:a1,a2:] & w1 = [a1,a2] ) by A21, XTUPLE_0:1;
assume [v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ; :: thesis:
then consider b1 being Element of U1, b2 being Element of U2 such that
A23: ( [v2,w2] = [[:b1,b2:],[b1,b2]] & b1 in U1 \ {{}} & b2 in U2 \ {{}} ) ;
A24: ( v2 = [:b1,b2:] & w2 = [b1,b2] ) by A23, XTUPLE_0:1;
thus ( v1 = v2 implies w1 = w2 ) :: thesis:

proof

assume A25: v1 = v2 ; :: thesis:
( not a1 in {{}} & not a2 in {{}} ) by A21, XBOOLE_0:def 5;
then ( a1 <> {} & a2 <> {} ) by TARSKI:def 1;
then ( a1 = b1 & a2 = b2 ) by A22, A24, A25, ZFMISC_1:110;
hence w1 = w2 by A21, A23, XTUPLE_0:1; :: thesis:

end;

assume A26: w1 = w2 ; :: thesis:
( w1 = [a1,a2] & w2 = [b1,b2] ) by A21, A23, XTUPLE_0:1;
then ( a1 = b1 & a2 = b2 ) by A26, XTUPLE_0:1;
hence v1 = v2 by A21, A23, XTUPLE_0:1; :: thesis:

end;

hence ( ( for v being object st v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for w being object st w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for v1, v2, w1, w2 being object st [v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } & [v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
( v1 = v2 iff w1 = w2 ) ) ) by A15, A18; :: thesis:

end;

ex Z being set st
( ( for v being object st v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in Z ) ) & ( for w being object st w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) )

proof

take { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ; :: thesis:
thus ( ( for v being object st v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for w being object st w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for x, y, z, u being object st [x,y] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } & [z,u] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
( x = z iff y = u ) ) ) by A14; :: thesis:

end;

hence { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ,[:(U1 \ {{}}),(U2 \ {{}}):] are_equipotent ; :: thesis:

end;

hence U is countable by A10, A13, YELLOW_8:4; :: thesis:

end;

union U = [:X1,X2:]

proof

set V2 = { [:a,b:] where a is Element of U1 \ {{}}, b is Element of U2 \ {{}} : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ;
A26: U = { [:a,b:] where a is Element of U1 \ {{}}, b is Element of U2 \ {{}} : ( a in U1 \ {{}} & b in U2 \ {{}} ) }

proof

( U1 is Subset-Family of X1 & U2 is Subset-Family of X2 ) by Lem9;
hence U = { [:a,b:] where a is Element of U1 \ {{}}, b is Element of U2 \ {{}} : ( a in U1 \ {{}} & b in U2 \ {{}} ) } by A6, A8, A10, Lem8; :: thesis:

end;

( union (U1 \ {{}}) = union U1 & union (U2 \ {{}}) = union U2 ) by PARTIT1:2;
hence union U = [:X1,X2:] by A3, A5, A7, A9, A26, LATTICE5:2; :: thesis:

end;

hence ex U being countable Subset of S st
( union U = [:X1,X2:] & U is Subset of S ) by A12; :: thesis:

end;

hence S is with_countable_Cover by Lem6a, SRINGS_1:def 4; :: thesis: