let X be non-empty 1 -element FinSequence; :: thesis: for S being SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }
let S be SemiringFamily of X; :: thesis: { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }
( S is SemiringFamily of X & 1 in Seg 1 ) by FINSEQ_1:3;
then A1: S . 1 is semiring_of_sets of (X . 1) by Def2;
set S1 = { (product <*s*>) where s is Element of S . 1 : verum } ;
set X1 = { <*x*> where x is Element of X . 1 : verum } ;

now :: thesis: { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }

{ (product <*s*>) where s is Element of S . 1 : verum } c= bool { <*x*> where x is Element of X . 1 : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (product <*s*>) where s is Element of S . 1 : verum } or x in bool { <*x*> where x is Element of X . 1 : verum } )
assume A2: x in { (product <*s*>) where s is Element of S . 1 : verum } ; :: thesis: x in bool { <*x*> where x is Element of X . 1 : verum }
then consider s0 being Element of S . 1 such that
A3: x = product <*s0*> ;

per cases ( not s0 is empty or s0 is empty ) ;

suppose A4: not s0 is empty ; :: thesis: x in bool { <*x*> where x is Element of X . 1 : verum }

reconsider x1 = x as set by A2;
x1 c= { <*x*> where x is Element of X . 1 : verum }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x1 or y in { <*x*> where x is Element of X . 1 : verum } )
assume y in x1 ; :: thesis: y in { <*x*> where x is Element of X . 1 : verum }
then y in { <*a*> where a is Element of s0 : verum } by A3, A4, Thm23;
then consider a being Element of s0 such that
A6: y = <*a*> ;
A7: a in union (S . 1) by A4, A1, TARSKI:def 4;
union (S . 1) c= union (bool (X . 1)) by A1, ZFMISC_1:77;
then union (S . 1) c= X . 1 by ZFMISC_1:81;
hence y in { <*x*> where x is Element of X . 1 : verum } by A6, A7; :: thesis: verum

end;

hence x in bool { <*x*> where x is Element of X . 1 : verum } ; :: thesis: verum

end;

suppose A8: s0 is empty ; :: thesis: x in bool { <*x*> where x is Element of X . 1 : verum }

product <*{}*> c= { <*x*> where x is Element of X . 1 : verum } ;
hence x in bool { <*x*> where x is Element of X . 1 : verum } by A8, A3; :: thesis: verum

end;

end;

end;

then reconsider S2 = { (product <*s*>) where s is Element of S . 1 : verum } as Subset-Family of { <*x*> where x is Element of X . 1 : verum } ;

now :: thesis: ( S2 is with_empty_element & S2 is cap-finite-partition-closed & S2 is diff-c=-finite-partition-closed )

Z: {} is Element of S . 1 by A1, SETFAM_1:def 8;
then A9: {} in { (product <*s*>) where s is Element of S . 1 : verum } by Thm22;
thus S2 is with_empty_element by Z, Thm22; :: thesis: ( S2 is cap-finite-partition-closed & S2 is diff-c=-finite-partition-closed )

now :: thesis: for s1, s2 being Element of S2 st not s1 /\ s2 is empty holds
ex x being finite Subset of S2 st x is a_partition of s1 /\ s2

let s1, s2 be Element of S2; :: thesis: ( not s1 /\ s2 is empty implies ex x being finite Subset of S2 st x is a_partition of s1 /\ s2 )
assume A10: not s1 /\ s2 is empty ; :: thesis: ex x being finite Subset of S2 st x is a_partition of s1 /\ s2
A11: ( s1 in { (product <*s*>) where s is Element of S . 1 : verum } & s2 in S2 ) by A9;
then consider sa1 being Element of S . 1 such that
A12: s1 = product <*sa1*> ;
consider sa2 being Element of S . 1 such that
A13: s2 = product <*sa2*> by A11;
A14: not sa1 /\ sa2 is empty by A12, A13, A10, Thm25, Thm22;
then consider ax being finite Subset of (S . 1) such that
A15: ax is a_partition of sa1 /\ sa2 by A1, SRINGS_1:def 1;
A16: not ax is empty by A14, A15;
set x = { (product <*t*>) where t is Element of ax : verum } ;

now :: thesis: ( { (product <*t*>) where t is Element of ax : verum } is finite & { (product <*t*>) where t is Element of ax : verum } is Subset of S2 & { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 /\ s2 )

deffunc H₁( object ) -> set = product <*$1*>;
consider f being Function such that
A17: dom f = ax and
A18: for x being object st x in ax holds
f . x = H₁(x) from FUNCT_1:sch 3();
rng f = { (product <*t*>) where t is Element of ax : verum }

proof

now :: thesis: ( ( for t being object st t in rng f holds
t in { (product <*t*>) where t is Element of ax : verum } ) & ( for t being object st t in { (product <*t*>) where t is Element of ax : verum } holds
t in rng f ) )

hereby :: thesis: for t being object st t in { (product <*t*>) where t is Element of ax : verum } holds
t in rng f

let t be object ; :: thesis: ( t in rng f implies t in { (product <*t*>) where t is Element of ax : verum } )
assume t in rng f ; :: thesis: t in { (product <*t*>) where t is Element of ax : verum }
then consider q being object such that
A19: q in dom f and
A20: t = f . q by FUNCT_1:def 3;
t = H₁(q) by A17, A19, A20, A18;
hence t in { (product <*t*>) where t is Element of ax : verum } by A17, A19; :: thesis: verum

end;

let t be object ; :: thesis: ( t in { (product <*t*>) where t is Element of ax : verum } implies t in rng f )
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: t in rng f
then consider u being Element of ax such that
A21: t = product <*u*> ;
f . u = H₁(u) by A18, A14, A15;
hence t in rng f by A21, A17, A14, A15, FUNCT_1:def 3; :: thesis: verum

end;

then ( { (product <*t*>) where t is Element of ax : verum } c= rng f & rng f c= { (product <*t*>) where t is Element of ax : verum } ) ;
hence rng f = { (product <*t*>) where t is Element of ax : verum } ; :: thesis: verum

end;

hence { (product <*t*>) where t is Element of ax : verum } is finite by A17, FINSET_1:8; :: thesis: ( { (product <*t*>) where t is Element of ax : verum } is Subset of S2 & { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 /\ s2 )
{ (product <*t*>) where t is Element of ax : verum } c= S2

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (product <*t*>) where t is Element of ax : verum } or t in S2 )
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: t in S2
then consider u being Element of ax such that
A22: t = product <*u*> ;
( u in ax & ax c= S . 1 ) by A16;
hence t in S2 by A22; :: thesis: verum

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset of S2 ; :: thesis: { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 /\ s2

now :: thesis: ( { (product <*t*>) where t is Element of ax : verum } is Subset-Family of (s1 /\ s2) & union { (product <*t*>) where t is Element of ax : verum } = s1 /\ s2 & ( for A being Subset of (s1 /\ s2) st A in { (product <*t*>) where t is Element of ax : verum } holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) ) ) )

A23: { (product <*t*>) where t is Element of ax : verum } c= bool (s1 /\ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (product <*t*>) where t is Element of ax : verum } or t in bool (s1 /\ s2) )
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: t in bool (s1 /\ s2)
then consider u0 being Element of ax such that
A24: t = product <*u0*> ;
reconsider t1 = t as set by A24;

per cases ( t1 is empty or not t1 is empty ) ;

suppose A25: t1 is empty ; :: thesis: t in bool (s1 /\ s2)

{} c= s1 /\ s2 ;
hence t in bool (s1 /\ s2) by A25; :: thesis: verum

end;

suppose A26: not t1 is empty ; :: thesis: t in bool (s1 /\ s2)

then A28: t = { <*y*> where y is Element of u0 : verum } by A24, Thm22, Thm23;
t1 c= s1 /\ s2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in t1 or y in s1 /\ s2 )
assume y in t1 ; :: thesis: y in s1 /\ s2
then consider z being Element of u0 such that
A29: y = <*z*> by A28;
A30: product <*(sa1 /\ sa2)*> = { <*a*> where a is Element of sa1 /\ sa2 : verum } by A14, Thm23;
( u0 in ax & union ax = sa1 /\ sa2 ) by A16, A15, EQREL_1:def 4;
then z in sa1 /\ sa2 by A24, A26, Thm22, TARSKI:def 4;
then y in product <*(sa1 /\ sa2)*> by A29, A30;
hence y in s1 /\ s2 by A12, A13, Thm25; :: thesis: verum

end;

hence t in bool (s1 /\ s2) ; :: thesis: verum

end;

end;

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset-Family of (s1 /\ s2) ; :: thesis: ( union { (product <*t*>) where t is Element of ax : verum } = s1 /\ s2 & ( for A being Subset of (s1 /\ s2) st A in { (product <*t*>) where t is Element of ax : verum } holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) ) ) )

now :: thesis: ( ( for a being object st a in union { (product <*t*>) where t is Element of ax : verum } holds
a in s1 /\ s2 ) & ( for a being object st a in s1 /\ s2 holds
a in union { (product <*t*>) where t is Element of ax : verum } ) )

hereby :: thesis: for a being object st a in s1 /\ s2 holds
a in union { (product <*t*>) where t is Element of ax : verum }

let a be object ; :: thesis: ( a in union { (product <*t*>) where t is Element of ax : verum } implies a in s1 /\ s2 )
assume a in union { (product <*t*>) where t is Element of ax : verum } ; :: thesis: a in s1 /\ s2
then consider b being set such that
A31: a in b and
A32: b in { (product <*t*>) where t is Element of ax : verum } by TARSKI:def 4;
thus a in s1 /\ s2 by A31, A32, A23; :: thesis: verum

end;

let a be object ; :: thesis: ( a in s1 /\ s2 implies a in union { (product <*t*>) where t is Element of ax : verum } )
assume a in s1 /\ s2 ; :: thesis: a in union { (product <*t*>) where t is Element of ax : verum }
then A33: a in product <*(sa1 /\ sa2)*> by A12, A13, Thm25;
product <*(sa1 /\ sa2)*> = { <*u*> where u is Element of sa1 /\ sa2 : verum } by A14, Thm23;
then consider b being Element of sa1 /\ sa2 such that
A34: a = <*b*> by A33;
( b in sa1 /\ sa2 & union ax = sa1 /\ sa2 ) by A14, A15, EQREL_1:def 4;
then consider d being set such that
A35: ( b in d & d in ax ) by TARSKI:def 4;
A36: product <*d*> = { <*u*> where u is Element of d : verum } by A35, Thm23;
( <*b*> in product <*d*> & product <*d*> in { (product <*t*>) where t is Element of ax : verum } ) by A35, A36;
hence a in union { (product <*t*>) where t is Element of ax : verum } by A34, TARSKI:def 4; :: thesis: verum

end;

then ( union { (product <*t*>) where t is Element of ax : verum } c= s1 /\ s2 & s1 /\ s2 c= union { (product <*t*>) where t is Element of ax : verum } ) ;
hence union { (product <*t*>) where t is Element of ax : verum } = s1 /\ s2 ; :: thesis: for A being Subset of (s1 /\ s2) st A in { (product <*t*>) where t is Element of ax : verum } holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) )

hereby :: thesis: verum

let A be Subset of (s1 /\ s2); :: thesis: ( A in { (product <*t*>) where t is Element of ax : verum } implies ( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) ) )
assume A in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: ( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) )
then consider a being Element of ax such that
A37: A = product <*a*> ;
A38: a in ax by A16;
A39: A = { <*u*> where u is Element of a : verum } by A14, A15, A37, Thm23;
consider b being object such that
A40: b in a by A14, A15, XBOOLE_0:def 1;
<*b*> in A by A39, A40;
hence A <> {} ; :: thesis: for B being Subset of (s1 /\ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B )
let B be Subset of (s1 /\ s2); :: thesis: ( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B )
assume B in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: ( A = B or A misses B )
then consider b being Element of ax such that
A41: B = product <*b*> ;
A42: b in ax by A16;
( a misses b implies A misses B ) by A37, A41, Thm25, Thm22;
hence ( A = B or A misses B ) by A42, A38, A15, EQREL_1:def 4, A37, A41; :: thesis: verum

end;

end;

hence { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 /\ s2 by EQREL_1:def 4; :: thesis: verum

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 /\ s2 ; :: thesis: verum

end;

hence S2 is cap-finite-partition-closed ; :: thesis: S2 is diff-c=-finite-partition-closed

now :: thesis: for s1, s2 being Element of S2 st s2 c= s1 holds
ex x being finite Subset of S2 st x is a_partition of s1 \ s2

let s1, s2 be Element of S2; :: thesis: ( s2 c= s1 implies ex x being finite Subset of S2 st b₃ is a_partition of x \ b₂ )
assume A44: s2 c= s1 ; :: thesis: ex x being finite Subset of S2 st b₃ is a_partition of x \ b₂

per cases ( s1 \ s2 is empty or ( not s1 \ s2 is empty & s2 is empty ) or ( not s1 \ s2 is empty & not s2 is empty ) ) ;

suppose A45: s1 \ s2 is empty ; :: thesis: ex x being finite Subset of S2 st b₃ is a_partition of x \ b₂

now :: thesis: ( {} is finite Subset of S2 & {} is a_partition of {} )

{} c= S2 ;
hence {} is finite Subset of S2 ; :: thesis: {} is a_partition of {}
thus {} is a_partition of {} by EQREL_1:45; :: thesis: verum

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 \ s2 by A45; :: thesis: verum

end;

suppose A46: ( not s1 \ s2 is empty & s2 is empty ) ; :: thesis: ex x being finite Subset of S2 st b₃ is a_partition of x \ b₂

now :: thesis: ( {s1} is finite Subset of S2 & {s1} is a_partition of s1 )

{s1} c= S2

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {s1} or t in S2 )
assume t in {s1} ; :: thesis: t in S2
then t = s1 by TARSKI:def 1;
hence t in S2 by A9; :: thesis: verum

end;

hence {s1} is finite Subset of S2 ; :: thesis: {s1} is a_partition of s1
thus {s1} is a_partition of s1 by A46, EQREL_1:39; :: thesis: verum

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 \ s2 by A46; :: thesis: verum

end;

suppose A47: ( not s1 \ s2 is empty & not s2 is empty ) ; :: thesis: ex x being finite Subset of S2 st b₃ is a_partition of x \ b₂

A48: ( s1 in { (product <*s*>) where s is Element of S . 1 : verum } & s2 in S2 ) by A9;
then consider sa1 being Element of S . 1 such that
A49: s1 = product <*sa1*> ;
consider sa2 being Element of S . 1 such that
A50: s2 = product <*sa2*> by A48;
A51: not sa1 is empty by A47, A49;
A52: product <*sa1*> = { <*u*> where u is Element of sa1 : verum } by A47, A49, Thm22, Thm23;
A53: product <*sa2*> = { <*u*> where u is Element of sa2 : verum } by A47, A50, Thm22, Thm23;
sa2 c= sa1

proof

assume not sa2 c= sa1 ; :: thesis: contradiction
then consider a being object such that
A54: a in sa2 and
A55: not a in sa1 ;
<*a*> in s2 by A50, A54, A53;
then <*a*> in product <*sa1*> by A44, A49;
then consider a0 being Element of sa1 such that
A56: <*a*> = <*a0*> by A52;
a = a0 by A56, FINSEQ_1:76;
hence contradiction by A51, A55; :: thesis: verum

end;

then consider ax being finite Subset of (S . 1) such that
A57: ax is a_partition of sa1 \ sa2 by A1, SRINGS_1:def 3;
A58: not ax is empty

proof

assume ax is empty ; :: thesis: contradiction
then sa1 \ sa2 = {} by A57;
hence contradiction by A47, A49, A50, Thm26, Thm22; :: thesis: verum

end;

A59: sa1 \ sa2 <> {} by A49, A50, A47, Thm26, Thm22;
set x = { (product <*t*>) where t is Element of ax : verum } ;

now :: thesis: ( { (product <*t*>) where t is Element of ax : verum } is finite & { (product <*t*>) where t is Element of ax : verum } is Subset of S2 & { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 \ s2 )

deffunc H₁( object ) -> set = product <*$1*>;
consider f being Function such that
A60: dom f = ax and
A61: for x being object st x in ax holds
f . x = H₁(x) from FUNCT_1:sch 3();
rng f = { (product <*t*>) where t is Element of ax : verum }

proof

now :: thesis: ( ( for t being object st t in rng f holds
t in { (product <*t*>) where t is Element of ax : verum } ) & ( for t being object st t in { (product <*t*>) where t is Element of ax : verum } holds
t in rng f ) )

hereby :: thesis: for t being object st t in { (product <*t*>) where t is Element of ax : verum } holds
t in rng f

let t be object ; :: thesis: ( t in rng f implies t in { (product <*t*>) where t is Element of ax : verum } )
assume t in rng f ; :: thesis: t in { (product <*t*>) where t is Element of ax : verum }
then consider q being object such that
A62: q in dom f and
A63: t = f . q by FUNCT_1:def 3;
( t = product <*q*> & q in ax ) by A60, A61, A62, A63;
hence t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: verum

end;

let t be object ; :: thesis: ( t in { (product <*t*>) where t is Element of ax : verum } implies t in rng f )
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: t in rng f
then consider u being Element of ax such that
A64: t = product <*u*> ;
f . u = H₁(u) by A61, A58;
hence t in rng f by A64, A60, A58, FUNCT_1:def 3; :: thesis: verum

end;

then ( { (product <*t*>) where t is Element of ax : verum } c= rng f & rng f c= { (product <*t*>) where t is Element of ax : verum } ) ;
hence rng f = { (product <*t*>) where t is Element of ax : verum } ; :: thesis: verum

end;

hence { (product <*t*>) where t is Element of ax : verum } is finite by A60, FINSET_1:8; :: thesis: ( { (product <*t*>) where t is Element of ax : verum } is Subset of S2 & { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 \ s2 )
{ (product <*t*>) where t is Element of ax : verum } c= S2

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (product <*t*>) where t is Element of ax : verum } or t in S2 )
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: t in S2
then consider u being Element of ax such that
A65: t = product <*u*> ;
( u in ax & ax c= S . 1 ) by A58;
hence t in S2 by A65; :: thesis: verum

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset of S2 ; :: thesis: { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 \ s2

now :: thesis: ( { (product <*t*>) where t is Element of ax : verum } is Subset-Family of (s1 \ s2) & union { (product <*t*>) where t is Element of ax : verum } = s1 \ s2 & ( for A being Subset of (s1 \ s2) st A in { (product <*t*>) where t is Element of ax : verum } holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) ) ) )

A66: { (product <*t*>) where t is Element of ax : verum } c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (product <*t*>) where t is Element of ax : verum } or t in bool (s1 \ s2) )
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: t in bool (s1 \ s2)
then consider u0 being Element of ax such that
A67: t = product <*u0*> ;
reconsider t1 = t as set by A67;

per cases ( t1 is empty or not t1 is empty ) ;

suppose A68: t1 is empty ; :: thesis: t in bool (s1 \ s2)

{} c= s1 \ s2 ;
hence t in bool (s1 \ s2) by A68; :: thesis: verum

end;

suppose A69: not t1 is empty ; :: thesis: t in bool (s1 \ s2)

then A71: t = { <*y*> where y is Element of u0 : verum } by A67, Thm22, Thm23;
t1 c= s1 \ s2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in t1 or y in s1 \ s2 )
assume y in t1 ; :: thesis: y in s1 \ s2
then consider z being Element of u0 such that
A72: y = <*z*> by A71;
A73: product <*(sa1 \ sa2)*> = { <*a*> where a is Element of sa1 \ sa2 : verum } by A59, Thm23;
( u0 in ax & union ax = sa1 \ sa2 ) by A57, A58, EQREL_1:def 4;
then z in sa1 \ sa2 by A67, A69, Thm22, TARSKI:def 4;
then y in product <*(sa1 \ sa2)*> by A72, A73;
hence y in s1 \ s2 by A49, A50, Thm26; :: thesis: verum

end;

hence t in bool (s1 \ s2) ; :: thesis: verum

end;

end;

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset-Family of (s1 \ s2) ; :: thesis: ( union { (product <*t*>) where t is Element of ax : verum } = s1 \ s2 & ( for A being Subset of (s1 \ s2) st A in { (product <*t*>) where t is Element of ax : verum } holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) ) ) )

now :: thesis: ( ( for a being object st a in union { (product <*t*>) where t is Element of ax : verum } holds
a in s1 \ s2 ) & ( for a being object st a in s1 \ s2 holds
a in union { (product <*t*>) where t is Element of ax : verum } ) )

hereby :: thesis: for a being object st a in s1 \ s2 holds
a in union { (product <*t*>) where t is Element of ax : verum }

let a be object ; :: thesis: ( a in union { (product <*t*>) where t is Element of ax : verum } implies a in s1 \ s2 )
assume a in union { (product <*t*>) where t is Element of ax : verum } ; :: thesis: a in s1 \ s2
then consider b being set such that
A74: a in b and
A75: b in { (product <*t*>) where t is Element of ax : verum } by TARSKI:def 4;
thus a in s1 \ s2 by A66, A74, A75; :: thesis: verum

end;

let a be object ; :: thesis: ( a in s1 \ s2 implies a in union { (product <*t*>) where t is Element of ax : verum } )
assume A76: a in s1 \ s2 ; :: thesis: a in union { (product <*t*>) where t is Element of ax : verum }
A77: a in product <*(sa1 \ sa2)*> by Thm26, A76, A49, A50;
product <*(sa1 \ sa2)*> = { <*u*> where u is Element of sa1 \ sa2 : verum } by A59, Thm23;
then consider b being Element of sa1 \ sa2 such that
A78: a = <*b*> by A77;
( b in sa1 \ sa2 & union ax = sa1 \ sa2 ) by A59, A57, EQREL_1:def 4;
then consider d being set such that
A79: ( b in d & d in ax ) by TARSKI:def 4;
A80: product <*d*> = { <*u*> where u is Element of d : verum } by Thm23, A79;
( <*b*> in product <*d*> & product <*d*> in { (product <*t*>) where t is Element of ax : verum } ) by A79, A80;
hence a in union { (product <*t*>) where t is Element of ax : verum } by A78, TARSKI:def 4; :: thesis: verum

end;

then ( union { (product <*t*>) where t is Element of ax : verum } c= s1 \ s2 & s1 \ s2 c= union { (product <*t*>) where t is Element of ax : verum } ) ;
hence union { (product <*t*>) where t is Element of ax : verum } = s1 \ s2 ; :: thesis: for A being Subset of (s1 \ s2) st A in { (product <*t*>) where t is Element of ax : verum } holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) )

hereby :: thesis: verum

let A be Subset of (s1 \ s2); :: thesis: ( A in { (product <*t*>) where t is Element of ax : verum } implies ( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) ) )
assume A in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: ( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B ) ) )
then consider a being Element of ax such that
A81: A = product <*a*> ;
A82: a in ax by A58;
A83: A = { <*u*> where u is Element of a : verum } by A57, A58, A81, Thm23;
consider b being object such that
A84: b in a by A57, A58, XBOOLE_0:def 1;
<*b*> in A by A83, A84;
hence A <> {} ; :: thesis: for B being Subset of (s1 \ s2) holds
( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B )
let B be Subset of (s1 \ s2); :: thesis: ( not B in { (product <*t*>) where t is Element of ax : verum } or A = B or A misses B )
assume B in { (product <*t*>) where t is Element of ax : verum } ; :: thesis: ( A = B or A misses B )
then consider b being Element of ax such that
A85: B = product <*b*> ;
A86: b in ax by A58;
( a misses b implies A misses B ) by A81, A85, Thm25, Thm22;
hence ( A = B or A misses B ) by A86, A81, A85, A82, A57, EQREL_1:def 4; :: thesis: verum

end;

end;

hence { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 \ s2 by EQREL_1:def 4; :: thesis: verum

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 \ s2 ; :: thesis: verum

end;

end;

end;

hence S2 is diff-c=-finite-partition-closed ; :: thesis: verum

end;

hence { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum } ; :: thesis: verum

end;

hence { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum } ; :: thesis: verum