let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for A being Element of S holds {{}} \/ (union ((PARTITIONS A) /\ (Fin S))) is semiring_of_sets of A
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for A being Element of S holds {{}} \/ (union ((PARTITIONS A) /\ (Fin S))) is semiring_of_sets of A
let A be Element of S; :: thesis: {{}} \/ (union ((PARTITIONS A) /\ (Fin S))) is semiring_of_sets of A
set A1 = union ((PARTITIONS A) /\ (Fin S));
set B = (union ((PARTITIONS A) /\ (Fin S))) \/ {{}};
A1: union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A by Thm99;
A2: ( {{}} c= (union ((PARTITIONS A) /\ (Fin S))) \/ {{}} & {} in {{}} ) by XBOOLE_1:7, TARSKI:def 1;
(union ((PARTITIONS A) /\ (Fin S))) \/ {{}} c= bool A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union ((PARTITIONS A) /\ (Fin S))) \/ {{}} or x in bool A )
assume x in (union ((PARTITIONS A) /\ (Fin S))) \/ {{}} ; :: thesis: x in bool A
then ( x in union ((PARTITIONS A) /\ (Fin S)) or x in {{}} ) by XBOOLE_0:def 3;
then A3: ( x in union ((PARTITIONS A) /\ (Fin S)) or x = {} ) by TARSKI:def 1;
{} c= A by XBOOLE_1:2;
hence x in bool A by A1, A3; :: thesis: verum
end;
then reconsider B = (union ((PARTITIONS A) /\ (Fin S))) \/ {{}} as Subset-Family of A ;
A4: B is cap-finite-partition-closed
proof
let S1, S2 be Element of B; :: according to SRINGS_1:def 1 :: thesis: ( not S1 /\ S2 is empty implies ex x being finite Subset of B st x is a_partition of S1 /\ S2 )
assume F1: not S1 /\ S2 is empty ; :: thesis: ex x being finite Subset of B st x is a_partition of S1 /\ S2
reconsider A1 = union ((PARTITIONS A) /\ (Fin S)) as Subset-Family of A by Thm99;
( ( S1 in A1 or S1 in {{}} ) & ( S2 in A1 or S2 in {{}} ) ) by XBOOLE_0:def 3;
then ( ( S1 in A1 or S1 = {} ) & ( S2 in A1 or S2 = {} ) ) by TARSKI:def 1;
then ( S1 is Element of A1 & S2 is Element of A1 & not S1 /\ S2 is empty & A1 is cap-finite-partition-closed ) by F1, Thm99;
then consider P being finite Subset of A1 such that
SOL: P is a_partition of S1 /\ S2 ;
reconsider P = P as finite Subset of B by XBOOLE_1:10;
( P is finite Subset of B & P is a_partition of S1 /\ S2 ) by SOL;
hence ex x being finite Subset of B st x is a_partition of S1 /\ S2 ; :: thesis: verum
end;
B is diff-finite-partition-closed
proof
let S1, S2 be Element of B; :: according to SRINGS_1:def 2 :: thesis: ( not S1 \ S2 is empty implies ex x being finite Subset of B st x is a_partition of S1 \ S2 )
assume F1: not S1 \ S2 is empty ; :: thesis: ex x being finite Subset of B st x is a_partition of S1 \ S2
reconsider A1 = union ((PARTITIONS A) /\ (Fin S)) as Subset-Family of A by Thm99;
F2aa: ( ( S1 in A1 or S1 in {{}} ) & ( S2 in A1 or S2 in {{}} ) ) by XBOOLE_0:def 3;
V1: ( S2 = {} implies ex P being finite Subset of B st P is a_partition of S1 \ S2 )
proof
assume D0: S2 = {} ; :: thesis: ex P being finite Subset of B st P is a_partition of S1 \ S2
D3: {S1} c= B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {S1} or x in B )
assume x in {S1} ; :: thesis: x in B
then x = S1 by TARSKI:def 1;
hence x in B ; :: thesis: verum
end;
{S1} is a_partition of S1 by F1, EQREL_1:39;
hence ex P being finite Subset of B st P is a_partition of S1 \ S2 by D0, D3; :: thesis: verum
end;
( S2 in A1 implies ex P being finite Subset of B st P is a_partition of S1 \ S2 )
proof
assume S2 in A1 ; :: thesis: ex P being finite Subset of B st P is a_partition of S1 \ S2
then ( S1 is Element of A1 & S2 is Element of A1 & not S1 \ S2 is empty & A1 is diff-finite-partition-closed ) by Thm99, F1, F2aa, TARSKI:def 1;
then consider P being finite Subset of A1 such that
SOL: P is a_partition of S1 \ S2 ;
reconsider P = P as finite Subset of B by XBOOLE_1:10;
( P is finite Subset of B & P is a_partition of S1 \ S2 ) by SOL;
hence ex P being finite Subset of B st P is a_partition of S1 \ S2 ; :: thesis: verum
end;
hence ex x being finite Subset of B st x is a_partition of S1 \ S2 by V1, F2aa, TARSKI:def 1; :: thesis: verum
end;
hence {{}} \/ (union ((PARTITIONS A) /\ (Fin S))) is semiring_of_sets of A by A2, A4; :: thesis: verum