let X1, X2 be set ; :: thesis: for S1 being semiring_of_sets of X1
for S2 being semiring_of_sets of X2 holds { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is semiring_of_sets of [:X1,X2:]
let S1 be semiring_of_sets of X1; :: thesis: for S2 being semiring_of_sets of X2 holds { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is semiring_of_sets of [:X1,X2:]
let S2 be semiring_of_sets of X2; :: thesis: { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is semiring_of_sets of [:X1,X2:]
defpred S1[ object , object ] means ex A, B being set st
( A = $2 `1 & B = $2 `2 & $1 = [:A,B:] );
set Y = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ;
A1: { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is with_empty_element
proof
A2: ( {} in S1 & {} in S2 ) by SETFAM_1:def 8;
[:{},{}:] c= [:X1,X2:] ;
then {} in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } by A2;
hence { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is with_empty_element ; :: thesis: verum
end;
then A3: not { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is empty ;
reconsider Y = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } as Subset-Family of [:X1,X2:] by Lem3;
A4: Y is cap-finite-partition-closed
proof
let D1, D2 be Element of Y; :: according to SRINGS_1:def 1 :: thesis: ( D1 /\ D2 is empty or ex b1 being Element of bool Y st b1 is a_partition of D1 /\ D2 )
D1 in Y by A3;
then consider s1 being Subset of [:X1,X2:] such that
A5: ( D1 = s1 & ex x11, x12 being set st
( x11 in S1 & x12 in S2 & s1 = [:x11,x12:] ) ) ;
consider x11, x12 being set such that
A6: ( x11 in S1 & x12 in S2 & D1 = [:x11,x12:] ) by A5;
D2 in Y by A3;
then consider s2 being Subset of [:X1,X2:] such that
A9: ( D2 = s2 & ex x21, x22 being set st
( x21 in S1 & x22 in S2 & s2 = [:x21,x22:] ) ) ;
consider x21, x22 being set such that
A10: ( x21 in S1 & x22 in S2 & D2 = [:x21,x22:] ) by A9;
assume not D1 /\ D2 is empty ; :: thesis: ex b1 being Element of bool Y st b1 is a_partition of D1 /\ D2
then [:(x11 /\ x21),(x12 /\ x22):] <> {} by ZFMISC_1:100, A6, A10;
then A13: ( not x11 /\ x21 is empty & not x12 /\ x22 is empty ) ;
then consider y1 being finite Subset of S1 such that
A14: y1 is a_partition of x11 /\ x21 by A6, A10, SRINGS_1:def 1;
consider y2 being finite Subset of S2 such that
A15: y2 is a_partition of x12 /\ x22 by A6, A10, A13, SRINGS_1:def 1;
set YY = { [:a,b:] where a is Element of y1, b is Element of y2 : verum } ;
A16: not y1 is empty by A13, A14;
A17: not y2 is empty by A13, A15;
A18: { [:a,b:] where a is Element of y1, b is Element of y2 : verum } c= Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:a,b:] where a is Element of y1, b is Element of y2 : verum } or x in Y )
assume x in { [:a,b:] where a is Element of y1, b is Element of y2 : verum } ; :: thesis: x in Y
then consider a0 being Element of y1, b0 being Element of y2 such that
A19: x = [:a0,b0:] ;
reconsider x = x as set by TARSKI:1;
A20: a0 in S1
proof
a0 in y1 by A16;
hence a0 in S1 ; :: thesis: verum
end;
A21: b0 in S2
proof
b0 in y2 by A17;
hence b0 in S2 ; :: thesis: verum
end;
x is Subset of [:X1,X2:]
proof
x c= [:X1,X2:]
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x or y in [:X1,X2:] )
assume y in x ; :: thesis: y in [:X1,X2:]
then consider ya0, yb0 being object such that
A22: ( ya0 in a0 & yb0 in b0 & y = [ya0,yb0] ) by A19, ZFMISC_1:def 2;
thus y in [:X1,X2:] by A20, A21, A22, ZFMISC_1:def 2; :: thesis: verum
end;
hence x is Subset of [:X1,X2:] ; :: thesis: verum
end;
hence x in Y by A19, A20, A21; :: thesis: verum
end;
set YY = { [:a,b:] where a is Element of y1, b is Element of y2 : verum } ;
{ [:a,b:] where a is Element of y1, b is Element of y2 : verum } is a_partition of [:(x11 /\ x21),(x12 /\ x22):] by A13, A14, A15, PUA2MSS1:8;
then A24: { [:a,b:] where a is Element of y1, b is Element of y2 : verum } is a_partition of D1 /\ D2 by A6, A10, ZFMISC_1:100;
{ [:a,b:] where a is Element of y1, b is Element of y2 : verum } is finite
proof
A25: for x being object st x in { [:a,b:] where a is Element of y1, b is Element of y2 : verum } holds
ex y being object st
( y in [:y1,y2:] & S1[x,y] )
proof
let x be object ; :: thesis: ( x in { [:a,b:] where a is Element of y1, b is Element of y2 : verum } implies ex y being object st
( y in [:y1,y2:] & S1[x,y] ) )
assume x in { [:a,b:] where a is Element of y1, b is Element of y2 : verum } ; :: thesis: ex y being object st
( y in [:y1,y2:] & S1[x,y] )
then consider x1 being Element of y1, x2 being Element of y2 such that
A26: x = [:x1,x2:] ;
set y = [x1,x2];
reconsider Y1 = [x1,x2] `1 , Y2 = [x1,x2] `2 as set ;
A27: x = [:Y1,Y2:] by A26;
[x1,x2] in [:y1,y2:] by ZFMISC_1:def 2, A13, A14, A15;
hence ex y being object st
( y in [:y1,y2:] & S1[x,y] ) by A27; :: thesis: verum
end;
consider f being Function such that
A28: ( dom f = { [:a,b:] where a is Element of y1, b is Element of y2 : verum } & rng f c= [:y1,y2:] ) and
A29: for x being object st x in { [:a,b:] where a is Element of y1, b is Element of y2 : verum } holds
S1[x,f . x] from FUNCT_1:sch 6(A25);
 f is one-to-one
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A30: a in dom f and
A31: b in dom f and
A32: f . a = f . b ; :: thesis: a = b
( S1[a,f . a] & S1[b,f . a] ) by A29, A32, A28, A30, A31;
hence a = b ; :: thesis: verum
end;
then card { [:a,b:] where a is Element of y1, b is Element of y2 : verum } c= card [:y1,y2:] by A28, CARD_1:10;
hence { [:a,b:] where a is Element of y1, b is Element of y2 : verum } is finite ; :: thesis: verum
end;
hence ex b1 being Element of bool Y st b1 is a_partition of D1 /\ D2 by A18, A24; :: thesis: verum
end;
Y is diff-finite-partition-closed
proof
let D3, D4 be Element of Y; :: according to SRINGS_1:def 2 :: thesis: ( D3 \ D4 is empty or ex b1 being Element of bool Y st b1 is a_partition of D3 \ D4 )
D3 in Y by A3;
then consider s1 being Subset of [:X1,X2:] such that
A34: ( D3 = s1 & ex x11, x12 being set st
( x11 in S1 & x12 in S2 & s1 = [:x11,x12:] ) ) ;
consider x11, x12 being set such that
A35: x11 in S1 and
A36: x12 in S2 and
A37: D3 = [:x11,x12:] by A34;
D4 in Y by A3;
then consider s2 being Subset of [:X1,X2:] such that
A40: ( D4 = s2 & ex x21, x22 being set st
( x21 in S1 & x22 in S2 & s2 = [:x21,x22:] ) ) ;
consider x21, x22 being set such that
A41: x21 in S1 and
A42: x22 in S2 and
A43: D4 = [:x21,x22:] by A40;
assume not D3 \ D4 is empty ; :: thesis: ex b1 being Element of bool Y st b1 is a_partition of D3 \ D4
A46: ( not x11 \ x21 is empty & x12 <> {} implies ex Z1 being finite Subset of Y st Z1 is a_partition of [:(x11 \ x21),x12:] )
proof
assume A47: ( not x11 \ x21 is empty & x12 <> {} ) ; :: thesis: ex Z1 being finite Subset of Y st Z1 is a_partition of [:(x11 \ x21),x12:]
then consider z1 being finite Subset of S1 such that
A48: z1 is a_partition of x11 \ x21 by A35, A41, SRINGS_1:def 2;
A49: not z1 is empty by A48, A47;
set Z1 = { [:u1,x12:] where u1 is Element of z1 : verum } ;
A50: { [:u1,x12:] where u1 is Element of z1 : verum } is Subset of Y
proof
for x being object st x in { [:u1,x12:] where u1 is Element of z1 : verum } holds
x in Y
proof
let x be object ; :: thesis: ( x in { [:u1,x12:] where u1 is Element of z1 : verum } implies x in Y )
assume x in { [:u1,x12:] where u1 is Element of z1 : verum } ; :: thesis: x in Y
then consider a0 being Element of z1 such that
A51: x = [:a0,x12:] ;
A52: a0 in S1
proof
a0 in z1 by SUBSET_1:def 1, A47, A48;
hence a0 in S1 ; :: thesis: verum
end;
reconsider x = x as set by TARSKI:1;
x is Subset of [:X1,X2:]
proof
for y being object st y in x holds
y in [:X1,X2:]
proof
let y be object ; :: thesis: ( y in x implies y in [:X1,X2:] )
assume y in x ; :: thesis: y in [:X1,X2:]
then consider ya0, yx12 being object such that
A53: ( ya0 in a0 & yx12 in x12 & y = [ya0,yx12] ) by A51, ZFMISC_1:def 2;
thus y in [:X1,X2:] by A36, A52, A53, ZFMISC_1:def 2; :: thesis: verum
end;
hence x is Subset of [:X1,X2:] by TARSKI:def 3; :: thesis: verum
end;
hence x in Y by A51, A52, A36; :: thesis: verum
end;
hence { [:u1,x12:] where u1 is Element of z1 : verum } is Subset of Y by TARSKI:def 3; :: thesis: verum
end;
A56: { [:u1,x12:] where u1 is Element of z1 : verum } is finite
proof
defpred S2[ object , object ] means ex A being set st
( A = $2 & $1 = [:A,x12:] );
A57: for x being object st x in { [:u1,x12:] where u1 is Element of z1 : verum } holds
ex y being object st
( y in z1 & S2[x,y] )
proof
let x be object ; :: thesis: ( x in { [:u1,x12:] where u1 is Element of z1 : verum } implies ex y being object st
( y in z1 & S2[x,y] ) )
assume x in { [:u1,x12:] where u1 is Element of z1 : verum } ; :: thesis: ex y being object st
( y in z1 & S2[x,y] )
then consider x1 being Element of z1 such that
A58: x = [:x1,x12:] ;
take x1 ; :: thesis: ( x1 in z1 & S2[x,x1] )
thus ( x1 in z1 & S2[x,x1] ) by A49, A58; :: thesis: verum
end;
consider f being Function such that
A59: ( dom f = { [:u1,x12:] where u1 is Element of z1 : verum } & rng f c= z1 ) and
A60: for x being object st x in { [:u1,x12:] where u1 is Element of z1 : verum } holds
S2[x,f . x] from FUNCT_1:sch 6(A57);
 f is one-to-one
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A61: a in dom f and
A62: b in dom f and
A63: f . a = f . b ; :: thesis: a = b
( S2[a,f . a] & S2[b,f . b] ) by A59, A60, A61, A62;
hence a = b by A63; :: thesis: verum
end;
then card { [:u1,x12:] where u1 is Element of z1 : verum } c= card z1 by A59, CARD_1:10;
hence { [:u1,x12:] where u1 is Element of z1 : verum } is finite ; :: thesis: verum
end;
{ [:u1,x12:] where u1 is Element of z1 : verum } is a_partition of [:(x11 \ x21),x12:]
proof
set Z2 = { [:p,q:] where p is Element of z1, q is Element of {x12} : verum } ;
A65: { [:u1,x12:] where u1 is Element of z1 : verum } = { [:p,q:] where p is Element of z1, q is Element of {x12} : verum }
proof
A66: { [:u1,x12:] where u1 is Element of z1 : verum } c= { [:p,q:] where p is Element of z1, q is Element of {x12} : verum }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:u1,x12:] where u1 is Element of z1 : verum } or x in { [:p,q:] where p is Element of z1, q is Element of {x12} : verum } )
assume x in { [:u1,x12:] where u1 is Element of z1 : verum } ; :: thesis: x in { [:p,q:] where p is Element of z1, q is Element of {x12} : verum }
then consider x00 being Element of z1 such that
A67: x = [:x00,x12:] ;
x12 is Element of {x12} by TARSKI:def 1;
hence x in { [:p,q:] where p is Element of z1, q is Element of {x12} : verum } by A67; :: thesis: verum
end;
{ [:p,q:] where p is Element of z1, q is Element of {x12} : verum } c= { [:u1,x12:] where u1 is Element of z1 : verum }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:p,q:] where p is Element of z1, q is Element of {x12} : verum } or x in { [:u1,x12:] where u1 is Element of z1 : verum } )
assume x in { [:p,q:] where p is Element of z1, q is Element of {x12} : verum } ; :: thesis: x in { [:u1,x12:] where u1 is Element of z1 : verum }
then consider x01 being Element of z1, x02 being Element of {x12} such that
A68: x = [:x01,x02:] ;
x = [:x01,x12:] by A68, TARSKI:def 1;
hence x in { [:u1,x12:] where u1 is Element of z1 : verum } ; :: thesis: verum
end;
hence { [:u1,x12:] where u1 is Element of z1 : verum } = { [:p,q:] where p is Element of z1, q is Element of {x12} : verum } by A66; :: thesis: verum
end;
{x12} is a_partition of x12 by A47, EQREL_1:39;
hence { [:u1,x12:] where u1 is Element of z1 : verum } is a_partition of [:(x11 \ x21),x12:] by A65, PUA2MSS1:8, A47, A48; :: thesis: verum
end;
hence ex Z1 being finite Subset of Y st Z1 is a_partition of [:(x11 \ x21),x12:] by A50, A56; :: thesis: verum
end;
A71: ( x11 /\ x21 <> {} & x12 \ x22 <> {} implies ex Z2 being finite Subset of Y st Z2 is a_partition of [:(x11 /\ x21),(x12 \ x22):] )
proof
assume A72: ( x11 /\ x21 <> {} & x12 \ x22 <> {} ) ; :: thesis: ex Z2 being finite Subset of Y st Z2 is a_partition of [:(x11 /\ x21),(x12 \ x22):]
then consider z1 being finite Subset of S1 such that
A73: z1 is a_partition of x11 /\ x21 by A35, A41, SRINGS_1:def 1;
consider z2 being finite Subset of S2 such that
A74: z2 is a_partition of x12 \ x22 by A72, A36, A42, SRINGS_1:def 2;
A75: not z2 is empty by A72, A74;
set Z2 = { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } ;
A76: { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } is Subset of Y
proof
for x being object st x in { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } holds
x in Y
proof
let x be object ; :: thesis: ( x in { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } implies x in Y )
assume x in { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } ; :: thesis: x in Y
then consider a0 being Element of z1, b0 being Element of z2 such that
A77: x = [:a0,b0:] ;
reconsider x = x as set by TARSKI:1;
A78: a0 in S1
proof
a0 in z1 by SUBSET_1:def 1, A72, A73;
hence a0 in S1 ; :: thesis: verum
end;
A79: b0 in S2
proof
b0 in z2 by A75;
hence b0 in S2 ; :: thesis: verum
end;
x is Subset of [:X1,X2:]
proof
for y being object st y in x holds
y in [:X1,X2:]
proof
let y be object ; :: thesis: ( y in x implies y in [:X1,X2:] )
assume y in x ; :: thesis: y in [:X1,X2:]
then consider ya0, yb0 being object such that
A80: ( ya0 in a0 & yb0 in b0 & y = [ya0,yb0] ) by A77, ZFMISC_1:def 2;
thus y in [:X1,X2:] by A78, A79, A80, ZFMISC_1:def 2; :: thesis: verum
end;
hence x is Subset of [:X1,X2:] by TARSKI:def 3; :: thesis: verum
end;
hence x in Y by A77, A78, A79; :: thesis: verum
end;
hence { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } is Subset of Y by TARSKI:def 3; :: thesis: verum
end;
A83: { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } is finite
proof
A84: for x being object st x in { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } holds
ex y being object st
( y in [:z1,z2:] & S1[x,y] )
proof
let x be object ; :: thesis: ( x in { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } implies ex y being object st
( y in [:z1,z2:] & S1[x,y] ) )
assume x in { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } ; :: thesis: ex y being object st
( y in [:z1,z2:] & S1[x,y] )
then consider x1 being Element of z1, x2 being Element of z2 such that
A85: x = [:x1,x2:] ;
set y = [x1,x2];
reconsider Y1 = [x1,x2] `1 , Y2 = [x1,x2] `2 as set ;
A86: x = [:Y1,Y2:] by A85;
[x1,x2] in [:z1,z2:] by A74, A73, A72, ZFMISC_1:def 2;
hence ex y being object st
( y in [:z1,z2:] & S1[x,y] ) by A86; :: thesis: verum
end;
consider f being Function such that
A87: ( dom f = { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } & rng f c= [:z1,z2:] ) and
A88: for x being object st x in { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } holds
S1[x,f . x] from FUNCT_1:sch 6(A84);
 f is one-to-one
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A89: a in dom f and
A90: b in dom f and
A91: f . a = f . b ; :: thesis: a = b
reconsider Y1 = (f . a) `1 , Y2 = (f . a) `2 as set by TARSKI:1;
( S1[a,f . a] & S1[b,f . b] ) by A87, A88, A89, A90;
hence a = b by A91; :: thesis: verum
end;
then card { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } c= card [:z1,z2:] by A87, CARD_1:10;
hence { [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } is finite ; :: thesis: verum
end;
{ [:u1,u2:] where u1 is Element of z1, u2 is Element of z2 : verum } is a_partition of [:(x11 /\ x21),(x12 \ x22):] by PUA2MSS1:8, A73, A74, A72;
hence ex Z2 being finite Subset of Y st Z2 is a_partition of [:(x11 /\ x21),(x12 \ x22):] by A76, A83; :: thesis: verum
end;
A94: ( [:(x11 \ x21),x12:] <> {} & [:(x11 /\ x21),(x12 \ x22):] = {} implies ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y ) )
proof
assume A95: ( [:(x11 \ x21),x12:] <> {} & [:(x11 /\ x21),(x12 \ x22):] = {} ) ; :: thesis: ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y )
then consider ZZ being finite Subset of Y such that
A96: ZZ is a_partition of [:(x11 \ x21),x12:] by A46;
[:x11,x12:] \ [:x21,x22:] = [:(x11 \ x21),x12:] \/ [:(x11 /\ x21),(x12 \ x22):] by Lem4;
hence ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y ) by A95, A96; :: thesis: verum
end;
A97: ( [:(x11 \ x21),x12:] = {} & [:(x11 /\ x21),(x12 \ x22):] <> {} implies ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y ) )
proof
assume A98: ( [:(x11 \ x21),x12:] = {} & [:(x11 /\ x21),(x12 \ x22):] <> {} ) ; :: thesis: ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y )
then consider ZZ being finite Subset of Y such that
A99: ZZ is a_partition of [:(x11 /\ x21),(x12 \ x22):] by A71;
[:x11,x12:] \ [:x21,x22:] = [:(x11 \ x21),x12:] \/ [:(x11 /\ x21),(x12 \ x22):] by Lem4;
hence ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y ) by A98, A99; :: thesis: verum
end;
A100: ( [:(x11 \ x21),x12:] = {} & [:(x11 /\ x21),(x12 \ x22):] = {} implies ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y ) )
proof
assume A101: ( [:(x11 \ x21),x12:] = {} & [:(x11 /\ x21),(x12 \ x22):] = {} ) ; :: thesis: ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y )
take {} ; :: thesis: ( {} is a_partition of [:x11,x12:] \ [:x21,x22:] & {} is finite Subset of Y )
[:x11,x12:] \ [:x21,x22:] = [:(x11 \ x21),x12:] \/ [:(x11 /\ x21),(x12 \ x22):] by Lem4;
hence ( {} is a_partition of [:x11,x12:] \ [:x21,x22:] & {} is finite Subset of Y ) by A101, EQREL_1:45, SUBSET_1:1; :: thesis: verum
end;
( [:(x11 \ x21),x12:] <> {} & [:(x11 /\ x21),(x12 \ x22):] <> {} implies ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y ) )
proof
assume A104: ( [:(x11 \ x21),x12:] <> {} & [:(x11 /\ x21),(x12 \ x22):] <> {} ) ; :: thesis: ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y )
then consider p1 being finite Subset of Y such that
A105: p1 is a_partition of [:(x11 \ x21),x12:] by A46;
consider p2 being finite Subset of Y such that
A106: p2 is a_partition of [:(x11 /\ x21),(x12 \ x22):] by A71, A104;
( [:x11,x12:] \ [:x21,x22:] = [:(x11 \ x21),x12:] \/ [:(x11 /\ x21),(x12 \ x22):] & [:(x11 \ x21),x12:] misses [:(x11 /\ x21),(x12 \ x22):] ) by Lem4;
then A107: p1 \/ p2 is a_partition of [:x11,x12:] \ [:x21,x22:] by A105, A106, DILWORTH:3;
thus ex ZZ being set st
( ZZ is a_partition of [:x11,x12:] \ [:x21,x22:] & ZZ is finite Subset of Y ) by A107; :: thesis: verum
end;
hence ex b1 being Element of bool Y st b1 is a_partition of D3 \ D4 by A37, A43, A94, A97, A100; :: thesis: verum
end;
hence { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is semiring_of_sets of [:X1,X2:] by A1, A4; :: thesis: verum